theory SestoftCorrect imports BalancedTraces "Launchbury" Sestoft begin lemma lemma_2: assumes "Γ : e ⇓⇘L⇙ Δ : z" and "fv (Γ, e, S) ⊆ set L ∪ domA Γ" shows "(Γ, e, S) ⇒⇧* (Δ, z, S)" using assms proof(induction arbitrary: S rule:reds.induct) case (Lambda Γ x e L) show ?case.. next case (Application y Γ e x L Δ Θ z e') from `fv (Γ, App e x, S) ⊆ set L ∪ domA Γ` have prem1: "fv (Γ, e, Arg x # S) ⊆ set L ∪ domA Γ" by simp from prem1 reds_pres_closed[OF `Γ : e ⇓⇘L⇙ Δ : Lam [y]. e'`] reds_doesnt_forget[OF `Γ : e ⇓⇘L⇙ Δ : Lam [y]. e'`] have prem2: "fv (Δ, e'[y::=x], S) ⊆ set L ∪ domA Δ" by (auto simp add: fv_subst_eq) have "(Γ, App e x, S) ⇒ (Γ, e, Arg x # S)".. also have "… ⇒⇧* (Δ, Lam [y]. e', Arg x# S)" by (rule Application.IH(1)[OF prem1]) also have "… ⇒ (Δ, e'[y ::= x], S)".. also have "… ⇒⇧* (Θ, z, S)" by (rule Application.IH(2)[OF prem2]) finally show ?case. next case (Variable Γ x e L Δ z S) from Variable(2) have "isVal z" by (rule result_evaluated) have "x ∉ domA Δ" by (rule reds_avoids_live[OF Variable(2), where x = x]) simp_all from `fv (Γ, Var x, S) ⊆ set L ∪ domA Γ` have prem: "fv (delete x Γ, e, Upd x # S) ⊆ set (x#L) ∪ domA (delete x Γ)" by (auto dest: set_mp[OF fv_delete_subset] set_mp[OF map_of_Some_fv_subset[OF `map_of Γ x = Some e`]]) from `map_of Γ x = Some e` have "(Γ, Var x, S) ⇒ (delete x Γ, e, Upd x # S)".. also have "… ⇒⇧* (Δ, z, Upd x # S)" by (rule Variable.IH[OF prem]) also have "… ⇒ ((x,z)#Δ, z, S)" using `x ∉ domA Δ` `isVal z` by (rule var⇩2) finally show ?case. next case (Bool Γ b L S) show ?case.. next case (IfThenElse Γ scrut L Δ b e⇩1 e⇩2 Θ z S) have "(Γ, scrut ? e⇩1 : e⇩2, S) ⇒ (Γ, scrut, Alts e⇩1 e⇩2 #S)".. also from IfThenElse.prems have prem1: "fv (Γ, scrut, Alts e⇩1 e⇩2 #S) ⊆ set L ∪ domA Γ" by auto hence "(Γ, scrut, Alts e⇩1 e⇩2 #S) ⇒⇧* (Δ, Bool b, Alts e⇩1 e⇩2 #S)" by (rule IfThenElse.IH) also have "(Δ, Bool b, Alts e⇩1 e⇩2 #S) ⇒ (Δ, if b then e⇩1 else e⇩2, S)".. also from prem1 reds_pres_closed[OF IfThenElse(1)] reds_doesnt_forget[OF IfThenElse(1)] have prem2: "fv (Δ, if b then e⇩1 else e⇩2, S) ⊆ set L ∪ domA Δ" by auto hence "(Δ, if b then e⇩1 else e⇩2, S) ⇒⇧* (Θ, z, S)" by (rule IfThenElse.IH(2)) finally show ?case. next case (Let as Γ L body Δ z S) from Let(4) have prem: "fv (as @ Γ, body, S) ⊆ set L ∪ domA (as @ Γ)" by auto from Let(1) have "atom ` domA as ♯* Γ" by (auto simp add: fresh_star_Pair) moreover from Let(1) have "domA as ∩ fv (Γ, L) = {}" by (rule fresh_distinct_fv) hence "domA as ∩ (set L ∪ domA Γ) = {}" by (auto dest: set_mp[OF domA_fv_subset]) with Let(4) have "domA as ∩ fv S = {}" by auto hence "atom ` domA as ♯* S" by (auto simp add: fresh_star_def fv_def fresh_def) ultimately have "(Γ, Terms.Let as body, S) ⇒ (as@Γ, body, S)".. also have "… ⇒⇧* (Δ, z, S)" by (rule Let.IH[OF prem]) finally show ?case. qed type_synonym trace = "conf list" fun stack :: "conf ⇒ stack" where "stack (Γ, e, S) = S" interpretation traces step. abbreviation trace_syn ("_ ⇒⇧*⇘_⇙ _" [50,50,50] 50) where "trace_syn ≡ trace" lemma conf_trace_induct_final[consumes 1, case_names trace_nil trace_cons]: "(Γ, e, S) ⇒⇧*⇘T⇙ final ⟹ (⋀ Γ e S. final = (Γ, e, S) ⟹ P Γ e S [] (Γ, e, S)) ⟹ (⋀Γ e S T Γ' e' S'. (Γ', e', S') ⇒⇧*⇘T⇙ final ⟹ P Γ' e' S' T final ⟹ (Γ, e, S) ⇒ (Γ', e', S') ⟹ P Γ e S ((Γ', e', S') # T) final) ⟹ P Γ e S T final" by (induction "(Γ, e, S)" T final arbitrary: Γ e S rule: trace_induct_final) auto interpretation balance_trace step stack apply standard apply (erule step.cases) apply auto done abbreviation bal_syn ("_ ⇒⇧b⇧*⇘_⇙ _" [50,50,50] 50) where "bal_syn ≡ bal" lemma isVal_stops: assumes "isVal e" assumes "(Γ, e, S) ⇒⇧b⇧*⇘T⇙ (Δ, z, S)" shows "T=[]" using assms apply - apply (erule balE) apply (erule trace.cases) apply simp apply auto apply (auto elim!: step.cases) done lemma Ball_subst[simp]: "(∀p∈set (Γ[y::h=x]). f p) ⟷ (∀p∈set Γ. case p of (z,e) ⇒ f (z, e[y::=x]))" by (induction Γ) auto lemma lemma_3: assumes "(Γ, e, S) ⇒⇧b⇧*⇘T⇙ (Δ, z, S)" assumes "isVal z" shows "Γ : e ⇓⇘upds_list S⇙ Δ : z" using assms proof(induction T arbitrary: Γ e S Δ z rule: measure_induct_rule[where f = length]) case (less T Γ e S Δ z) from `(Γ, e, S) ⇒⇧b⇧*⇘T⇙ (Δ, z, S)` have "(Γ, e, S) ⇒⇧*⇘T⇙ (Δ, z, S)" and "∀ c'∈set T. S ≲ stack c'" unfolding bal.simps by auto from this(1) show ?case proof(cases) case trace_nil from `isVal z` trace_nil show ?thesis by (auto intro: reds_isValI) next case (trace_cons conf' T') from `T = conf' # T'` and `∀ c'∈set T. S ≲ stack c'` have "S ≲ stack conf'" by auto from `(Γ, e, S) ⇒ conf'` show ?thesis proof(cases) case (app⇩1 e x) obtain T⇩1 c⇩3 c⇩4 T⇩2 where "T' = T⇩1 @ c⇩4 # T⇩2" and prem1: "(Γ, e, Arg x # S) ⇒⇧b⇧*⇘T⇩1⇙ c⇩3" and "c⇩3 ⇒ c⇩4" and prem2: " c⇩4 ⇒⇧b⇧*⇘T⇩2⇙ (Δ, z, S)" by (rule bal_consE[OF `bal _ T _`[unfolded app⇩1 trace_cons]]) (simp, rule) from `T = _` `T' = _` have "length T⇩1 < length T" and "length T⇩2 < length T" by auto from prem1 have "stack c⇩3 = Arg x # S" by (auto dest: bal_stackD) moreover from prem2 have "stack c⇩4 = S" by (auto dest: bal_stackD) moreover note `c⇩3 ⇒ c⇩4` ultimately obtain Δ' y e' where "c⇩3 = (Δ', Lam [y]. e', Arg x # S)" and "c⇩4 = (Δ', e'[y ::= x], S)" by (auto elim!: step.cases simp del: exp_assn.eq_iff) from less(1)[OF `length T⇩1 < length T` prem1[unfolded `c⇩3 = _` `c⇩4 = _`]] have "Γ : e ⇓⇘upds_list S⇙ Δ' : Lam [y]. e'" by simp moreover from less(1)[OF `length T⇩2 < length T` prem2[unfolded `c⇩3 = _` `c⇩4 = _`] `isVal z`] have "Δ' : e'[y::=x] ⇓⇘upds_list S⇙ Δ : z" by simp ultimately show ?thesis unfolding app⇩1 by (rule reds_ApplicationI) next case (app⇩2 y e x S') from `conf' =_` `S = _ # S'` `S ≲ stack conf'` have False by (auto simp add: extends_def) thus ?thesis.. next case (var⇩1 x e) obtain T⇩1 c⇩3 c⇩4 T⇩2 where "T' = T⇩1 @ c⇩4 # T⇩2" and prem1: "(delete x Γ, e, Upd x # S) ⇒⇧b⇧*⇘T⇩1⇙ c⇩3" and "c⇩3 ⇒ c⇩4" and prem2: "c⇩4 ⇒⇧b⇧*⇘T⇩2⇙ (Δ, z, S)" by (rule bal_consE[OF `bal _ T _`[unfolded var⇩1 trace_cons]]) (simp, rule) from `T = _` `T' = _` have "length T⇩1 < length T" and "length T⇩2 < length T" by auto from prem1 have "stack c⇩3 = Upd x # S" by (auto dest: bal_stackD) moreover from prem2 have "stack c⇩4 = S" by (auto dest: bal_stackD) moreover note `c⇩3 ⇒ c⇩4` ultimately obtain Δ' z' where "c⇩3 = (Δ', z', Upd x # S)" and "c⇩4 = ((x,z')#Δ', z', S)" and "isVal z'" by (auto elim!: step.cases simp del: exp_assn.eq_iff) from `isVal z'` and prem2[unfolded `c⇩4 = _`] have "T⇩2 = []" by (rule isVal_stops) with prem2 `c⇩4 = _` have "z' = z" and "Δ = (x,z)#Δ'" by auto from less(1)[OF `length T⇩1 < length T` prem1[unfolded `c⇩3 = _` `c⇩4 = _` `z' = _`] `isVal z`] have "delete x Γ : e ⇓⇘x # upds_list S⇙ Δ' : z" by simp with `map_of _ _ = _` show ?thesis unfolding var⇩1(1) `Δ = _` by rule next case (var⇩2 x S') from `conf' = _` `S = _ # S'` `S ≲ stack conf'` have False by (auto simp add: extends_def) thus ?thesis.. next case (if⇩1 scrut e⇩1 e⇩2) obtain T⇩1 c⇩3 c⇩4 T⇩2 where "T' = T⇩1 @ c⇩4 # T⇩2" and prem1: "(Γ, scrut, Alts e⇩1 e⇩2 # S) ⇒⇧b⇧*⇘T⇩1⇙ c⇩3" and "c⇩3 ⇒ c⇩4" and prem2: "c⇩4 ⇒⇧b⇧*⇘T⇩2⇙ (Δ, z, S)" by (rule bal_consE[OF `bal _ T _`[unfolded if⇩1 trace_cons]]) (simp, rule) from `T = _` `T' = _` have "length T⇩1 < length T" and "length T⇩2 < length T" by auto from prem1 have "stack c⇩3 = Alts e⇩1 e⇩2 # S" by (auto dest: bal_stackD) moreover from prem2 have "stack c⇩4 = S" by (auto dest: bal_stackD) moreover note `c⇩3 ⇒ c⇩4` ultimately obtain Δ' b where "c⇩3 = (Δ', Bool b, Alts e⇩1 e⇩2 # S)" and "c⇩4 = (Δ', (if b then e⇩1 else e⇩2), S)" by (auto elim!: step.cases simp del: exp_assn.eq_iff) from less(1)[OF `length T⇩1 < length T` prem1[unfolded `c⇩3 = _` `c⇩4 = _` ] isVal_Bool] have "Γ : scrut ⇓⇘upds_list S⇙ Δ' : Bool b" by simp moreover from less(1)[OF `length T⇩2 < length T` prem2[unfolded `c⇩4 = _`] `isVal z`] have "Δ' : (if b then e⇩1 else e⇩2) ⇓⇘upds_list S⇙ Δ : z". ultimately show ?thesis unfolding if⇩1 by (rule reds.IfThenElse) next case (if⇩2 b e1 e2 S') from `conf' = _` `S = _ # S'` `S ≲ stack conf'` have False by (auto simp add: extends_def) thus ?thesis.. next case (let⇩1 as e) from `T = conf' # T'` have "length T' < length T" by auto moreover have "(as @ Γ, e, S) ⇒⇧b⇧*⇘T'⇙ (Δ, z, S)" using trace_cons `conf' = _` `∀ c'∈set T. S ≲ stack c'` by fastforce moreover note `isVal z` ultimately have "as @ Γ : e ⇓⇘upds_list S⇙ Δ : z" by (rule less) moreover from `atom \` domA as ♯* Γ` `atom \` domA as ♯* S` have "atom ` domA as ♯* (Γ, upds_list S)" by (auto simp add: fresh_star_Pair) ultimately show ?thesis unfolding let⇩1 by (rule reds.Let[rotated]) qed qed qed lemma dummy_stack_extended: "set S ⊆ Dummy ` UNIV ⟹ x ∉ Dummy ` UNIV ⟹ (S ≲ x # S') ⟷ S ≲ S'" apply (auto simp add: extends_def) apply (case_tac S'') apply auto done lemma[simp]: "Arg x ∉ range Dummy" "Upd x ∉ range Dummy" "Alts e⇩1 e⇩2 ∉ range Dummy" by auto lemma dummy_stack_balanced: assumes "set S ⊆ Dummy ` UNIV" assumes "(Γ, e, S) ⇒⇧* (Δ, z, S)" obtains T where "(Γ, e, S) ⇒⇧b⇧*⇘T⇙ (Δ, z, S)" proof- from build_trace[OF assms(2)] obtain T where "(Γ, e, S) ⇒⇧*⇘T⇙ (Δ, z, S)".. moreover hence "∀ c'∈set T. stack (Γ, e, S) ≲ stack c'" by (rule conjunct1[OF traces_list_all]) (auto elim: step.cases simp add: dummy_stack_extended[OF `set S ⊆ Dummy \` UNIV`]) ultimately have "(Γ, e, S) ⇒⇧b⇧*⇘T⇙ (Δ, z, S)" by (rule balI) simp thus ?thesis by (rule that) qed end