Theory JJ1WellForm
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