(* Title: JinjaThreads/Compiler/JJ1WellForm.thy Author: Andreas Lochbihler Reminiscent of the Jinja theory Compiler/Correctness1 *) section ‹Preservation of well-formedness from source code to intermediate language› theory JJ1WellForm imports "../J/JWellForm" J1WellForm Compiler1 begin text‹The compiler preserves well-formedness. Is less trivial than it may appear. We start with two simple properties: preservation of well-typedness› lemma assumes wf: "wf_prog wfmd P" shows compE1_pres_wt: "⟦ P,[Vs[↦]Ts] ⊢ e :: U; size Ts = size Vs ⟧ ⟹ compP f P,Ts ⊢1 compE1 Vs e :: U" and compEs1_pres_wt: "⟦ P,[Vs[↦]Ts] ⊢ es [::] Us; size Ts = size Vs ⟧ ⟹ compP f P,Ts ⊢1 compEs1 Vs es [::] Us" proof(induct Vs e and Vs es arbitrary: Ts U and Ts Us rule: compE1_compEs1_induct) case Var thus ?case by(fastforce simp:map_upds_apply_eq_Some split:if_split_asm) next case LAss thus ?case by(fastforce simp:map_upds_apply_eq_Some split:if_split_asm) next case Call thus ?case by(fastforce dest: sees_method_compP[where f = f]) next case Block thus ?case by(fastforce simp:nth_append) next case (Synchronized Vs V exp1 exp2 Ts U) note IH1 = ‹⋀Ts U. ⟦P,[Vs [↦] Ts] ⊢ exp1 :: U; length Ts = length Vs⟧ ⟹ compP f P,Ts ⊢1 compE1 Vs exp1 :: U› note IH2 = ‹⋀Ts U. ⟦P,[(Vs @ [fresh_var Vs]) [↦] Ts] ⊢ exp2 :: U; length Ts = length (Vs @ [fresh_var Vs])⟧ ⟹ compP f P,Ts ⊢1 compE1 (Vs @ [fresh_var Vs]) exp2 :: U› note length = ‹length Ts = length Vs› from ‹P,[Vs [↦] Ts] ⊢ sync⇘V⇙ (exp1) exp2 :: U› obtain U1 where wt1: "P,[Vs [↦] Ts] ⊢ exp1 :: U1" and wt2: "P,[Vs [↦] Ts] ⊢ exp2 :: U" and U1: "is_refT U1" "U1 ≠ NT" by(auto) from IH1[of Ts U1] wt1 length have wt1': "compP f P,Ts ⊢1 compE1 Vs exp1 :: U1" by simp from length fresh_var_fresh[of Vs] have "[Vs [↦] Ts] ⊆⇩_{m}[Vs @ [fresh_var Vs] [↦] Ts @ [Class Object]]" by(auto simp add: map_le_def fun_upd_def) with wt2 have "P,[Vs@[fresh_var Vs] [↦] Ts @ [Class Object]] ⊢ exp2 :: U" by(rule wt_env_mono) with length IH2[of "Ts @ [Class Object]" U] have "compP f P,Ts @ [Class Object] ⊢1 compE1 (Vs @ [fresh_var Vs]) exp2 :: U" by simp with wt1' U1 show ?case by(auto) next case (TryCatch Vs exp1 C V exp2) note IH1 = ‹⋀Ts U. ⟦P,[Vs [↦] Ts] ⊢ exp1 :: U; length Ts = length Vs⟧ ⟹ compP f P,Ts ⊢1 compE1 Vs exp1 :: U› note IH2 = ‹⋀Ts U. ⟦P,[(Vs @ [V]) [↦] Ts] ⊢ exp2 :: U; length Ts = length (Vs @ [V])⟧ ⟹ compP f P,Ts ⊢1 compE1 (Vs @ [V]) exp2 :: U› note length = ‹length Ts = length Vs› with ‹P,[Vs [↦] Ts] ⊢ try exp1 catch(C V) exp2 :: U› have wt1: "P,[Vs [↦] Ts] ⊢ exp1 :: U" and wt2: "P,[(Vs@[V]) [↦] (Ts@[Class C])] ⊢ exp2 :: U" and C: "P ⊢ C ≼⇧^{*}Throwable" by(auto simp add: nth_append) from wf C have "is_class P C" by(rule is_class_sub_Throwable) with IH1[OF wt1 length] IH2[OF wt2] length show ?case by(auto) qed(fastforce)+ text‹\noindent and the correct block numbering:› text‹The main complication is preservation of definite assignment @{term"𝒟"}.› lemma fixes e :: "'addr expr" and es :: "'addr expr list" shows A_compE1_None[simp]: "𝒜 e = None ⟹ 𝒜 (compE1 Vs e) = None" and As_compEs1_None: "𝒜s es = None ⟹ 𝒜s (compEs1 Vs es) = None" apply(induct Vs e and Vs es rule: compE1_compEs1_induct) apply(auto simp:hyperset_defs) done lemma fixes e :: "'addr expr" and es :: "'addr expr list" shows A_compE1: "⟦ 𝒜 e = ⌊A⌋; fv e ⊆ set Vs ⟧ ⟹ 𝒜 (compE1 Vs e) = ⌊index Vs ` A⌋" and As_compEs1: "⟦ 𝒜s es = ⌊A⌋; fvs es ⊆ set Vs ⟧ ⟹ 𝒜s (compEs1 Vs es) = ⌊index Vs ` A⌋" proof(induct Vs e and Vs es arbitrary: A and A rule: compE1_compEs1_induct) case (Block Vs V' T vo e) hence "fv e ⊆ set (Vs@[V'])" by fastforce moreover obtain B where "𝒜 e = ⌊B⌋" using Block.prems by(simp add: hyperset_defs) moreover from calculation have "B ⊆ set (Vs@[V'])" by(auto dest!:A_fv) ultimately show ?case using Block by(auto simp add: hyperset_defs image_index) next case (Synchronized Vs V exp1 exp2 A) have IH1: "⋀A. ⟦𝒜 exp1 = ⌊A⌋; fv exp1 ⊆ set Vs⟧ ⟹ 𝒜 (compE1 Vs exp1) = ⌊index Vs ` A⌋" by fact have IH2: "⋀A. ⟦𝒜 exp2 = ⌊A⌋; fv exp2 ⊆ set (Vs @ [fresh_var Vs])⟧ ⟹ 𝒜 (compE1 (Vs @ [fresh_var Vs]) exp2) = ⌊index (Vs @ [fresh_var Vs]) ` A⌋" by fact from ‹fv (sync⇘V⇙ (exp1) exp2) ⊆ set Vs› have fv1: "fv exp1 ⊆ set Vs" and fv2: "fv exp2 ⊆ set Vs" by auto from ‹𝒜 (sync⇘V⇙ (exp1) exp2) = ⌊A⌋› have A: "𝒜 exp1 ⊔ 𝒜 exp2 = ⌊A⌋" by(simp) then obtain A1 A2 where A1: "𝒜 exp1 = ⌊A1⌋" and A2: "𝒜 exp2 = ⌊A2⌋" by(auto simp add: hyperset_defs) from A2 fv2 have "A2 ⊆ set Vs" by(auto dest: A_fv del: subsetI) with fresh_var_fresh[of Vs] have "(fresh_var Vs) ∉ A2" by(auto) from fv2 have "fv exp2 ⊆ set (Vs @ [fresh_var Vs])" by auto with IH2[OF A2] have "𝒜 (compE1 (Vs @ [fresh_var Vs]) exp2) = ⌊index (Vs @ [fresh_var Vs]) ` A2⌋" by(auto) with IH1[OF A1 fv1] A[symmetric] ‹A2 ⊆ set Vs› ‹(fresh_var Vs) ∉ A2› A1 A2 show ?case by(auto simp add: image_index) next case (InSynchronized Vs V a exp A) have IH: "⋀A. ⟦𝒜 exp = ⌊A⌋; fv exp ⊆ set (Vs @ [fresh_var Vs])⟧ ⟹ 𝒜 (compE1 (Vs @ [fresh_var Vs]) exp) = ⌊index (Vs @ [fresh_var Vs]) ` A⌋" by fact from ‹𝒜 (insync⇘V⇙ (a) exp) = ⌊A⌋› have A: "𝒜 exp = ⌊A⌋" by simp from ‹fv (insync⇘V⇙ (a) exp) ⊆ set Vs› have fv: "fv exp ⊆ set Vs" by simp from A fv have "A ⊆ set Vs" by(auto dest: A_fv del: subsetI) with fresh_var_fresh[of Vs] have "(fresh_var Vs) ∉ A" by(auto) from fv IH[OF A] have " 𝒜 (compE1 (Vs @ [fresh_var Vs]) exp) = ⌊index (Vs @ [fresh_var Vs]) ` A⌋" by simp with ‹A ⊆ set Vs› ‹(fresh_var Vs) ∉ A› show ?case by(simp add: image_index) next case (TryCatch Vs e1 C V' e2) hence fve2: "fv e2 ⊆ set (Vs@[V'])" by auto show ?case proof (cases "𝒜 e1") assume A1: "𝒜 e1 = None" then obtain A2 where A2: "𝒜 e2 = ⌊A2⌋" using TryCatch by(simp add:hyperset_defs) hence "A2 ⊆ set (Vs@[V'])" using TryCatch.prems A_fv[OF A2] by simp blast thus ?thesis using TryCatch fve2 A1 A2 by(auto simp add:hyperset_defs image_index) next fix A1 assume A1: "𝒜 e1 = ⌊A1⌋" show ?thesis proof (cases "𝒜 e2") assume A2: "𝒜 e2 = None" then show ?case using TryCatch A1 by(simp add:hyperset_defs) next fix A2 assume A2: "𝒜 e2 = ⌊A2⌋" have "A1 ⊆ set Vs" using TryCatch.prems A_fv[OF A1] by simp blast moreover have "A2 ⊆ set (Vs@[V'])" using TryCatch.prems A_fv[OF A2] by simp blast ultimately show ?thesis using TryCatch A1 A2 by(fastforce simp add: hyperset_defs image_index Diff_subset_conv inj_on_image_Int[OF inj_on_index]) qed qed next case (Cond Vs e e1 e2) { assume "𝒜 e = None ∨ 𝒜 e1 = None ∨ 𝒜 e2 = None" hence ?case using Cond by(auto simp add:hyperset_defs image_Un) } moreover { fix A A1 A2 assume "𝒜 e = ⌊A⌋" and A1: "𝒜 e1 = ⌊A1⌋" and A2: "𝒜 e2 = ⌊A2⌋" moreover have "A1 ⊆ set Vs" using Cond.prems A_fv[OF A1] by simp blast moreover have "A2 ⊆ set Vs" using Cond.prems A_fv[OF A2] by simp blast ultimately have ?case using Cond by(auto simp add:hyperset_defs image_Un inj_on_image_Int[OF inj_on_index]) } ultimately show ?case by fastforce qed (auto simp add:hyperset_defs) lemma fixes e :: "('a, 'b, 'addr) exp" and es :: "('a, 'b, 'addr) exp list" shows D_None [iff]: "𝒟 e None" and Ds_None [iff]: "𝒟s es None" by(induct e and es rule: 𝒟.induct 𝒟s.induct)(simp_all) declare Un_ac [simp] lemma fixes e :: "'addr expr" and es :: "'addr expr list" shows D_index_compE1: "⟦ A ⊆ set Vs; fv e ⊆ set Vs ⟧ ⟹ 𝒟 e ⌊A⌋ ⟹ 𝒟 (compE1 Vs e) ⌊index Vs ` A⌋" and Ds_index_compEs1: "⟦ A ⊆ set Vs; fvs es ⊆ set Vs ⟧ ⟹ 𝒟s es ⌊A⌋ ⟹ 𝒟s (compEs1 Vs es) ⌊index Vs ` A⌋" proof(induct e and es arbitrary: A Vs and A Vs rule: 𝒟.induct 𝒟s.induct) case (BinOp e1 bop e2) hence IH1: "𝒟 (compE1 Vs e1) ⌊index Vs ` A⌋" by simp show ?case proof (cases "𝒜 e1") case None thus ?thesis using BinOp by simp next case (Some A1) have indexA1: "𝒜 (compE1 Vs e1) = ⌊index Vs ` A1⌋" using A_compE1[OF Some] BinOp.prems by auto have "A ∪ A1 ⊆ set Vs" using BinOp.prems A_fv[OF Some] by auto hence "𝒟 (compE1 Vs e2) ⌊index Vs ` (A1 ∪ A)⌋" using BinOp Some by(auto) hence "𝒟 (compE1 Vs e2) ⌊index Vs ` A1 ∪ index Vs ` A⌋" by(simp add: image_Un) thus ?thesis using IH1 indexA1 by auto qed next case (AAcc a i A Vs) have IH1: "⋀A Vs. ⟦A ⊆ set Vs; fv a ⊆ set Vs; 𝒟 a ⌊A⌋⟧ ⟹ 𝒟 (compE1 Vs a) ⌊index Vs ` A⌋" by fact have IH2: "⋀A Vs. ⟦A ⊆ set Vs; fv i ⊆ set Vs; 𝒟 i ⌊A⌋⟧ ⟹ 𝒟 (compE1 Vs i) ⌊index Vs ` A⌋" by fact from ‹𝒟 (a⌊i⌉) ⌊A⌋› have D1: "𝒟 a ⌊A⌋" and D2: "𝒟 i (⌊A⌋ ⊔ 𝒜 a)" by auto from ‹fv (a⌊i⌉) ⊆ set Vs› have fv1: "fv a ⊆ set Vs" and fv2: "fv i ⊆ set Vs" by auto show ?case proof(cases "𝒜 a") case None thus ?thesis using AAcc by simp next case (Some A1) with fv1 have "𝒜 (compE1 Vs a) = ⌊index Vs ` A1⌋" by-(rule A_compE1) moreover from A_fv[OF Some] fv1 ‹A ⊆ set Vs› have "A1 ∪ A ⊆ set Vs" by auto from IH2[OF this fv2] Some D2 have "𝒟 (compE1 Vs i) ⌊index Vs ` A1 ∪ index Vs ` A⌋" by(simp add: image_Un) ultimately show ?thesis using IH1[OF ‹A ⊆ set Vs› fv1 D1] by(simp) qed next case (AAss a i e A Vs) have IH1: "⋀A Vs. ⟦A ⊆ set Vs; fv a ⊆ set Vs; 𝒟 a ⌊A⌋⟧ ⟹ 𝒟 (compE1 Vs a) ⌊index Vs ` A⌋" by fact have IH2: "⋀A Vs. ⟦A ⊆ set Vs; fv i ⊆ set Vs; 𝒟 i ⌊A⌋⟧ ⟹ 𝒟 (compE1 Vs i) ⌊index Vs ` A⌋" by fact have IH3: "⋀A Vs. ⟦A ⊆ set Vs; fv e ⊆ set Vs; 𝒟 e ⌊A⌋⟧ ⟹ 𝒟 (compE1 Vs e) ⌊index Vs ` A⌋" by fact from ‹𝒟 (a⌊i⌉:=e) ⌊A⌋› have D1: "𝒟 a ⌊A⌋" and D2: "𝒟 i (⌊A⌋ ⊔ 𝒜 a)" and D3: "𝒟 e (⌊A⌋ ⊔ 𝒜 a ⊔ 𝒜 i)" by auto from ‹fv (a⌊i⌉ := e) ⊆ set Vs› have fv1: "fv a ⊆ set Vs" and fv2: "fv i ⊆ set Vs" and fv3: "fv e ⊆ set Vs" by auto show ?case proof(cases "𝒜 a") case None thus ?thesis using AAss by simp next case (Some A1) with fv1 have A1: "𝒜 (compE1 Vs a) = ⌊index Vs ` A1⌋" by-(rule A_compE1) from A_fv[OF Some] fv1 ‹A ⊆ set Vs› have "A1 ∪ A ⊆ set Vs" by auto from IH2[OF this fv2] Some D2 have D2': "𝒟 (compE1 Vs i) ⌊index Vs ` A1 ∪ index Vs ` A⌋" by(simp add: image_Un) show ?thesis proof(cases "𝒜 i") case None thus ?thesis using AAss D2' Some A1 by simp next case (Some A2) with fv2 have A2: "𝒜 (compE1 Vs i) = ⌊index Vs ` A2⌋" by-(rule A_compE1) moreover from A_fv[OF Some] fv2 ‹A1 ∪ A ⊆ set Vs› have "A1 ∪ A ∪ A2 ⊆ set Vs" by auto from IH3[OF this fv3] Some ‹𝒜 a = ⌊A1⌋› D3 have "𝒟 (compE1 Vs e) ⌊index Vs ` A1 ∪ index Vs ` A ∪ index Vs ` A2⌋" by(simp add: image_Un Un_commute Un_assoc) ultimately show ?thesis using IH1[OF ‹A ⊆ set Vs› fv1 D1] D2' A1 A2 by(simp) qed qed next case (FAss e1 F D e2) hence IH1: "𝒟 (compE1 Vs e1) ⌊index Vs ` A⌋" by simp show ?case proof (cases "𝒜 e1") case None thus ?thesis using FAss by simp next case (Some A1) have indexA1: "𝒜 (compE1 Vs e1) = ⌊index Vs ` A1⌋" using A_compE1[OF Some] FAss.prems by auto have "A ∪ A1 ⊆ set Vs" using FAss.prems A_fv[OF Some] by auto hence "𝒟 (compE1 Vs e2) ⌊index Vs ` (A ∪ A1)⌋" using FAss Some by auto hence "𝒟 (compE1 Vs e2) ⌊index Vs ` A ∪ index Vs ` A1⌋" by(simp add: image_Un) thus ?thesis using IH1 indexA1 by auto qed next case (CompareAndSwap e1 D F e2 e3 A Vs) have IH1: "⋀A Vs. ⟦A ⊆ set Vs; fv e1 ⊆ set Vs; 𝒟 e1 ⌊A⌋⟧ ⟹ 𝒟 (compE1 Vs e1) ⌊index Vs ` A⌋" by fact have IH2: "⋀A Vs. ⟦A ⊆ set Vs; fv e2 ⊆ set Vs; 𝒟 e2 ⌊A⌋⟧ ⟹ 𝒟 (compE1 Vs e2) ⌊index Vs ` A⌋" by fact have IH3: "⋀A Vs. ⟦A ⊆ set Vs; fv e3 ⊆ set Vs; 𝒟 e3 ⌊A⌋⟧ ⟹ 𝒟 (compE1 Vs e3) ⌊index Vs ` A⌋" by fact from ‹𝒟 (e1∙compareAndSwap(D∙F, e2, e3)) ⌊A⌋› have D1: "𝒟 e1 ⌊A⌋" and D2: "𝒟 e2 (⌊A⌋ ⊔ 𝒜 e1)" and D3: "𝒟 e3 (⌊A⌋ ⊔ 𝒜 e1 ⊔ 𝒜 e2)" by auto from ‹fv (e1∙compareAndSwap(D∙F, e2, e3)) ⊆ set Vs› have fv1: "fv e1 ⊆ set Vs" and fv2: "fv e2 ⊆ set Vs" and fv3: "fv e3 ⊆ set Vs" by auto show ?case proof(cases "𝒜 e1") case None thus ?thesis using CompareAndSwap by simp next case (Some A1) with fv1 have A1: "𝒜 (compE1 Vs e1) = ⌊index Vs ` A1⌋" by-(rule A_compE1) from A_fv[OF Some] fv1 ‹A ⊆ set Vs› have "A1 ∪ A ⊆ set Vs" by auto from IH2[OF this fv2] Some D2 have D2': "𝒟 (compE1 Vs e2) ⌊index Vs ` A1 ∪ index Vs ` A⌋" by(simp add: image_Un) show ?thesis proof(cases "𝒜 e2") case None thus ?thesis using CompareAndSwap D2' Some A1 by simp next case (Some A2) with fv2 have A2: "𝒜 (compE1 Vs e2) = ⌊index Vs ` A2⌋" by-(rule A_compE1) moreover from A_fv[OF Some] fv2 ‹A1 ∪ A ⊆ set Vs› have "A1 ∪ A ∪ A2 ⊆ set Vs" by auto from IH3[OF this fv3] Some ‹𝒜 e1 = ⌊A1⌋› D3 have "𝒟 (compE1 Vs e3) ⌊index Vs ` A1 ∪ index Vs ` A ∪ index Vs ` A2⌋" by(simp add: image_Un Un_commute Un_assoc) ultimately show ?thesis using IH1[OF ‹A ⊆ set Vs› fv1 D1] D2' A1 A2 by(simp) qed qed next case (Call e1 M es) hence IH1: "𝒟 (compE1 Vs e1) ⌊index Vs ` A⌋" by simp show ?case proof (cases "𝒜 e1") case None thus ?thesis using Call by simp next case (Some A1) have indexA1: "𝒜 (compE1 Vs e1) = ⌊index Vs ` A1⌋" using A_compE1[OF Some] Call.prems by auto have "A ∪ A1 ⊆ set Vs" using Call.prems A_fv[OF Some] by auto hence "𝒟s (compEs1 Vs es) ⌊index Vs ` (A ∪ A1)⌋" using Call Some by auto hence "𝒟s (compEs1 Vs es) ⌊index Vs ` A ∪ index Vs ` A1⌋" by(simp add: image_Un) thus ?thesis using IH1 indexA1 by auto qed next case (Synchronized V exp1 exp2 A Vs) have IH1: "⋀A Vs. ⟦A ⊆ set Vs; fv exp1 ⊆ set Vs; 𝒟 exp1 ⌊A⌋⟧ ⟹ 𝒟 (compE1 Vs exp1) ⌊index Vs ` A⌋" by fact have IH2: "⋀A Vs. ⟦A ⊆ set Vs; fv exp2 ⊆ set Vs; 𝒟 exp2 ⌊A⌋⟧ ⟹ 𝒟 (compE1 Vs exp2) ⌊index Vs ` A⌋" by fact from ‹𝒟 (sync⇘V⇙ (exp1) exp2) ⌊A⌋› have D1: "𝒟 exp1 ⌊A⌋" and D2: "𝒟 exp2 (⌊A⌋ ⊔ 𝒜 exp1)" by auto from ‹fv (sync⇘V⇙ (exp1) exp2) ⊆ set Vs› have fv1: "fv exp1 ⊆ set Vs" and fv2: "fv exp2 ⊆ set Vs" by auto show ?case proof(cases "𝒜 exp1") case None thus ?thesis using Synchronized by(simp) next case (Some A1) with fv1 have A1: "𝒜 (compE1 Vs exp1) = ⌊index Vs ` A1⌋" by-(rule A_compE1) from A_fv[OF Some] fv1 ‹A ⊆ set Vs› have "A ∪ A1 ⊆ set Vs" by auto hence "A ∪ A1 ⊆ set (Vs @ [fresh_var Vs])" by simp from IH2[OF this] fv2 Some D2 have D2': "𝒟 (compE1 (Vs @ [fresh_var Vs]) exp2) ⌊index (Vs @ [fresh_var Vs]) ` (A ∪ A1)⌋" by(simp) moreover from fresh_var_fresh[of Vs] ‹A ∪ A1 ⊆ set Vs› have "(fresh_var Vs) ∉ A ∪ A1" by auto with ‹A ∪ A1 ⊆ set Vs› have "index (Vs @ [fresh_var Vs]) ` (A ∪ A1) = index Vs ` A ∪ index Vs ` A1" by(simp add: image_index image_Un) ultimately show ?thesis using IH1[OF ‹A ⊆ set Vs› fv1 D1] D2' A1 by(simp) qed next case (InSynchronized V a e A Vs) have IH: "⋀A Vs. ⟦A ⊆ set Vs; fv e ⊆ set Vs; 𝒟 e ⌊A⌋⟧ ⟹ 𝒟 (compE1 Vs e) ⌊index Vs ` A⌋" by fact from IH[of A "Vs @ [fresh_var Vs]"] ‹A ⊆ set Vs› ‹fv (insync⇘V⇙ (a) e) ⊆ set Vs› ‹𝒟 (insync⇘V⇙ (a) e) ⌊A⌋› have "𝒟 (compE1 (Vs @ [fresh_var Vs]) e) ⌊index (Vs @ [fresh_var Vs]) ` A⌋" by(auto) moreover from fresh_var_fresh[of Vs] ‹A ⊆ set Vs› have "(fresh_var Vs) ∉ A" by auto with ‹A ⊆ set Vs› have "index (Vs @ [fresh_var Vs]) ` A = index Vs ` A" by(simp add: image_index) ultimately show ?case by(simp) next case (TryCatch e1 C V e2) have "⟦ A∪{V} ⊆ set(Vs@[V]); fv e2 ⊆ set(Vs@[V]); 𝒟 e2 ⌊A∪{V}⌋⟧ ⟹ 𝒟 (compE1 (Vs@[V]) e2) ⌊index (Vs@[V]) ` (A∪{V})⌋" by fact hence "𝒟 (compE1 (Vs@[V]) e2) ⌊index (Vs@[V]) ` (A∪{V})⌋" using TryCatch.prems by(simp add:Diff_subset_conv) moreover have "index (Vs@[V]) ` A ⊆ index Vs ` A ∪ {size Vs}" using TryCatch.prems by(auto simp add: image_index split:if_split_asm) ultimately show ?case using TryCatch by(auto simp:hyperset_defs elim!:D_mono') next case (Seq e1 e2) hence IH1: "𝒟 (compE1 Vs e1) ⌊index Vs ` A⌋" by simp show ?case proof (cases "𝒜 e1") case None thus ?thesis using Seq by simp next case (Some A1) have indexA1: "𝒜 (compE1 Vs e1) = ⌊index Vs ` A1⌋" using A_compE1[OF Some] Seq.prems by auto have "A ∪ A1 ⊆ set Vs" using Seq.prems A_fv[OF Some] by auto hence "𝒟 (compE1 Vs e2) ⌊index Vs ` (A ∪ A1)⌋" using Seq Some by auto hence "𝒟 (compE1 Vs e2) ⌊index Vs ` A ∪ index Vs ` A1⌋" by(simp add: image_Un) thus ?thesis using IH1 indexA1 by auto qed next case (Cond e e1 e2) hence IH1: "𝒟 (compE1 Vs e) ⌊index Vs ` A⌋" by simp show ?case proof (cases "𝒜 e") case None thus ?thesis using Cond by simp next case (Some B) have indexB: "𝒜 (compE1 Vs e) = ⌊index Vs ` B⌋" using A_compE1[OF Some] Cond.prems by auto have "A ∪ B ⊆ set Vs" using Cond.prems A_fv[OF Some] by auto hence "𝒟 (compE1 Vs e1) ⌊index Vs ` (A ∪ B)⌋" and "𝒟 (compE1 Vs e2) ⌊index Vs ` (A ∪ B)⌋" using Cond Some by auto hence "𝒟 (compE1 Vs e1) ⌊index Vs ` A ∪ index Vs ` B⌋" and "𝒟 (compE1 Vs e2) ⌊index Vs ` A ∪ index Vs ` B⌋" by(simp add: image_Un)+ thus ?thesis using IH1 indexB by auto qed next case (While e1 e2) hence IH1: "𝒟 (compE1 Vs e1) ⌊index Vs ` A⌋" by simp show ?case proof (cases "𝒜 e1") case None thus ?thesis using While by simp next case (Some A1) have indexA1: "𝒜 (compE1 Vs e1) = ⌊index Vs ` A1⌋" using A_compE1[OF Some] While.prems by auto have "A ∪ A1 ⊆ set Vs" using While.prems A_fv[OF Some] by auto hence "𝒟 (compE1 Vs e2) ⌊index Vs ` (A ∪ A1)⌋" using While Some by auto hence "𝒟 (compE1 Vs e2) ⌊index Vs ` A ∪ index Vs ` A1⌋" by(simp add: image_Un) thus ?thesis using IH1 indexA1 by auto qed next case (Block V T vo e A Vs) have IH: "⋀A Vs. ⟦A ⊆ set Vs; fv e ⊆ set Vs; 𝒟 e ⌊A⌋⟧ ⟹ 𝒟 (compE1 Vs e) ⌊index Vs ` A⌋" by fact from ‹fv {V:T=vo; e} ⊆ set Vs› have fv: "fv e ⊆ set (Vs @ [V])" by auto show ?case proof(cases vo) case None with ‹𝒟 {V:T=vo; e} ⌊A⌋› have D: "𝒟 e ⌊A - {V}⌋" by(auto) from ‹A ⊆ set Vs› have "A - {V} ⊆ set (Vs @ [V])" by auto from IH[OF this fv D] have "𝒟 (compE1 (Vs @ [V]) e) ⌊index (Vs @ [V]) ` (A - {V})⌋" . moreover from ‹A ⊆ set Vs› have size: "size Vs ∉ index Vs ` A" by(auto simp add: image_def) hence "⌊index Vs ` (A - {V})⌋ ⊑ ⌊index Vs ` A⌋" by(auto simp add: hyperset_defs) ultimately have "𝒟 (compE1 (Vs @ [V]) e) ⌊index Vs ` A⌋" using ‹A - {V} ⊆ set (Vs @ [V])› by(simp add: image_index)(erule D_mono', auto) thus ?thesis using None size by(simp) next case (Some v) with ‹𝒟 {V:T=vo; e} ⌊A⌋› have D: "𝒟 e ⌊insert V A⌋" by(auto) from ‹A ⊆ set Vs› have "insert V A ⊆ set (Vs @ [V])" by auto from IH[OF this fv D] have "𝒟 (compE1 (Vs @ [V]) e) ⌊index (Vs @ [V]) ` insert V A⌋" by simp moreover from ‹A ⊆ set Vs› have "index (Vs @ [V]) ` insert V A ⊆ insert (length Vs) (index Vs ` A)" by(auto simp add: image_index) ultimately show ?thesis using Some by(auto elim!: D_mono' simp add: hyperset_defs) qed next case (Cons_exp e1 es) hence IH1: "𝒟 (compE1 Vs e1) ⌊index Vs ` A⌋" by simp show ?case proof (cases "𝒜 e1") case None thus ?thesis using Cons_exp by simp next case (Some A1) have indexA1: "𝒜 (compE1 Vs e1) = ⌊index Vs ` A1⌋" using A_compE1[OF Some] Cons_exp.prems by auto have "A ∪ A1 ⊆ set Vs" using Cons_exp.prems A_fv[OF Some] by auto hence "𝒟s (compEs1 Vs es) ⌊index Vs ` (A ∪ A1)⌋" using Cons_exp Some by auto hence "𝒟s (compEs1 Vs es) ⌊index Vs ` A ∪ index Vs ` A1⌋" by(simp add: image_Un) thus ?thesis using IH1 indexA1 by auto qed qed (simp_all add:hyperset_defs) declare Un_ac [simp del] lemma index_image_set: "distinct xs ⟹ index xs ` set xs = {..<size xs}" by(induct xs rule:rev_induct) (auto simp add: image_index) lemma D_compE1: "⟦ 𝒟 e ⌊set Vs⌋; fv e ⊆ set Vs; distinct Vs ⟧ ⟹ 𝒟 (compE1 Vs e) ⌊{..<length Vs}⌋" by(fastforce dest!: D_index_compE1[OF subset_refl] simp add:index_image_set) lemma D_compE1': assumes "𝒟 e ⌊set(V#Vs)⌋" and "fv e ⊆ set(V#Vs)" and "distinct(V#Vs)" shows "𝒟 (compE1 (V#Vs) e) ⌊{..length Vs}⌋" proof - have "{..size Vs} = {..<size(V#Vs)}" by auto thus ?thesis using assms by (simp only:)(rule D_compE1) qed lemma compP1_pres_wf: "wf_J_prog P ⟹ wf_J1_prog (compP1 P)" apply simp apply(rule wf_prog_compPI) prefer 2 apply assumption apply(case_tac m) apply(simp add:wf_mdecl_def) apply(clarify) apply(frule WT_fv) apply(fastforce intro!: compE1_pres_wt D_compE1' ℬ syncvars_compE1) done end