Up to index of Isabelle/HOL/CoreSafe
theory SafeRegionDepth(* Title: Safe Region Depth
Author: Javier de Dios and Ricardo Peņa
Copyright: February 2009, Universidad Complutense de Madrid
*)
header {* Region deallocation *}
theory SafeRegionDepth imports SafeRegion_definitions
SafeDAssBasic
BasicFacts
SafeDAss_P1
begin
declare consistent.simps [simp del]
declare argP.simps [simp del]
declare wellT.simps [simp del]
declare SafeRegionDAss.simps [simp del]
(* Demostraciones de los ASERTOS *)
(** Lemmas for ϑ **)
lemma map_add_fst_Some:
"[|ϑ r = Some y; dom ϑ ∩ dom ϑ' = {}|]
==> (ϑ ++ ϑ') r = Some y"
by (subst map_add_Some_iff,force)
(** Lemmas for map_of_zip **)
lemma map_of_zip_is_Some:
assumes "length xs = length ys"
shows "x ∈ set xs <-> (∃ y. map_of (zip xs ys) x = Some y)"
using assms by (induct rule: list_induct2) simp_all
lemma map_of_zip_twice_is_Some:
"[| x ∈ set xs; length xs = length vs; distinct xs; length xs = length zs |]
==> ∃ i < length vs. (map_of (zip xs vs)) x = Some (vs!i) ∧ (map_of (zip xs zs)) x = Some (zs!i)"
apply (frule_tac x="x" in map_of_zip_is_Some,simp)
apply (elim exE)
apply (subgoal_tac
"set (zip xs vs) =
{(xs!i, vs!i) | i. i < min (length xs) (length vs)}")
prefer 2 apply (rule set_zip)
apply (subgoal_tac
"set (zip xs zs) =
{(xs!i, zs!i) | i. i < min (length xs) (length zs)}")
prefer 2 apply (rule set_zip)
by auto
(* Lemmas for map_f_comp *)
lemma dom_map_f_comp:
"dom (f of g) = dom g"
apply (simp add: map_f_comp_def,auto)
by (case_tac "g x",simp,simp)
(* Lemmas for map_comp *)
lemma dom_map_comp:
"∀ x ∈ dom g. (∃ y. f (the (g x)) = Some y)
==> dom (f om g) = dom g"
apply (simp add: map_comp_def,auto)
apply (case_tac "g x",simp,simp)
by force
lemma map_comp_map_of_zip:
"[| x ∈ set xs; length xs = length ys; distinct xs; ∀ i < length ys. ∃ z. m (ys!i) = Some z|]
==> (m om map_of (zip xs ys)) x = map_of (zip xs (map (the o m) ys)) x"
apply (frule_tac x="x" in map_of_zip_is_Some,clarsimp)
apply (insert set_zip [where xs="xs" and ys="ys"])
apply (insert set_zip [where xs="xs" and ys="map (the o m) ys"])
apply clarsimp
apply (erule_tac x="i" in allE,simp)
apply (elim exE,simp)
by force
(* Lemmas for map_f_comp *)
lemma map_f_comp_map_of_zip:
"[| x ∈ set xs; length xs = length ys; distinct xs|]
==> (f of map_of (zip xs ys)) x = map_of (zip xs (map f ys)) x"
apply (frule_tac x="x" in map_of_zip_is_Some,clarsimp)
apply (simp add: map_f_comp_def)
apply (insert set_zip [where xs="xs" and ys="ys"])
apply (insert set_zip [where xs="xs" and ys="map f ys"])
by force
(** Lemmas for map_of **)
lemma map_of_zip_is_SomeI:
"[| x ∈ set xs; length xs = length vs; distinct xs |]
==> ∃ i < length vs. xs!i = x ∧ (map_of (zip xs vs)) x = Some (vs!i)"
apply (frule_tac x="x" in map_of_zip_is_Some,simp)
apply (subgoal_tac
"set (zip xs vs) =
{(xs!i, vs!i) | i. i < min (length xs) (length vs)}")
prefer 2 apply (rule set_zip)
by auto
(** Lemmas for map **)
lemma map_mu_self:
"ρself ∉ set ρs
==> map (the o μ2(ρself \<mapsto> ρself)) ρs = map (the o μ2) ρs"
by simp
lemma map_last:
"xs ≠ []
==> last (map f xs) = f (last xs)"
by (induct xs,simp,simp)
(** Lemmas for Environments **)
lemma as_in_E1:
"[| fvs' as ⊆ dom E1; as ! i = VarE x a; i < length as |]
==> x ∈ dom E1"
apply (induct as arbitrary: i,simp,clarsimp)
by (case_tac i,force,force)
lemma rr_in_E2:
"[| set rr ⊆ dom E2 |]
==> ∀ i < length rr. ∃ n. E2 (rr!i) = Some n"
apply (subgoal_tac "set rr = {rr!i | i. i < length rr}",force)
by (rule set_conv_nth)
(** Lemmas for μ_ren and η_ren **)
lemma η_η_ren:
"[| η x = Some r; x ≠ ρself; ρfake ∉ dom η |]
==> η_ren η x = Some r"
apply (simp add: η_ren_def add: dom_def)
by clarsimp
(********** Assert: (ConstE (LitN i) a) ***********)
lemma SafeDARegionDepth_LitInt:
"(ConstE (LitN i) a) :f , n \<lbrace> (ϑ1,ϑ2), (ConstrT intType [] []) \<rbrace>"
apply (unfold SafeRegionDAssDepth.simps)
apply (intro allI, rule impI,elim conjE)
apply (frule impSemBoundRA [where td=td])
apply (elim exE)
apply (erule SafeRASem.cases,simp_all)
by (rule consistent_v.primitiveI)
(********** Assert: (ConstE (LitB b) a) ***********)
lemma SafeDARegionDepth_LitBool:
"ConstE (LitB b) a :f , n \<lbrace> (ϑ1,ϑ2), (ConstrT boolType [] []) \<rbrace>"
apply (unfold SafeRegionDAssDepth.simps)
apply (intro allI, rule impI,elim conjE)
apply (frule impSemBoundRA [where td=td])
apply (elim exE)
apply (erule SafeRASem.cases,simp_all)
by (rule consistent_v.primitiveB)
(********** Assert: (VarE x a) ***********)
lemma SafeDARegionDepth_Var1:
"[| ϑ1 x = Some t |]
==> VarE x a :f , n \<lbrace> (ϑ1,ϑ2), t \<rbrace>"
apply (unfold SafeRegionDAssDepth.simps)
apply (intro allI, rule impI, elim conjE)
apply (frule impSemBoundRA [where td=td])
apply (elim exE)
apply (erule SafeRASem.cases,simp_all,clarsimp)
apply (simp add: consistent.simps)
apply (elim conjE)
apply (erule_tac x="x" in ballE)
apply clarsimp
by (simp add: dom_def)
(********** Assert: (CopyE x r d) ***********)
lemma ρ_notin_regions_mu_ext_copy_monotone:
"(ρ ∉ regions t --> mu_ext (μ1, μ2(ρ \<mapsto> ρ')) t = mu_ext (μ1, μ2) t) ∧
(ρ ∉ regions' tm --> mu_exts (μ1, μ2(ρ \<mapsto> ρ')) tm = mu_exts (μ1, μ2) tm)"
apply (induct_tac t and tm)
by clarsimp+
lemma map_ρs_equals_butlast_copy:
"[| ρs ≠ []; last ρs = ρ; distinct ρs |]
==> map (the o μ2(ρ \<mapsto> ρ')) ρs =
butlast (map (the o μ2) ρs) @ [ρ']"
by (induct ρs,simp,clarsimp)
lemma copy'_Loc_p:
"[| h p = Some (j', C, vn);
copy'_dom (j, h, Loc p, True);
h' = (fst (mapAccumL (copy' j) h (zip vn (recursiveArgs C))));
p' = getFresh h';
ps' = (snd (mapAccumL (copy' j) h (zip vn (recursiveArgs C)))) |]
==> copy' j h (Loc p, True) = (h'(p'\<mapsto>(j,C,ps')),Val.Loc p')"
apply (simp add: copy'.psimps(2))
apply (simp only: Let_def)
apply (case_tac "(mapAccumL (copy' j) h (zip vn (recursiveArgs C)))")
by simp
lemma copy_h'_p':
"[| copy (h, k) p j = ((h', k), p'); copy'_dom (j, h, Loc p, True);
h p = Some (j', C, vn)|]
==> h' p' = Some (j,C,snd (mapAccumL (copy' j) h (zip vn (recursiveArgs C))))"
apply (simp only: copy.simps)
apply (subgoal_tac
"copy' j h (Loc p, True) =
((fst (mapAccumL (copy' j) h (zip vn (recursiveArgs C))))
(getFresh (fst (mapAccumL (copy' j) h (zip vn (recursiveArgs C)))) \<mapsto>
(j,C, snd (mapAccumL (copy' j) h (zip vn (recursiveArgs C))))),
Val.Loc (getFresh (fst (mapAccumL (copy' j) h (zip vn (recursiveArgs C))))))")
apply clarsimp
apply (rule copy'_Loc_p)
by simp_all
lemma snd_mapAccumL_x_xs:
"snd (mapAccumL f s (x#xs)) = (snd (f s x)) # snd (mapAccumL f (fst (f s x)) xs)"
apply simp
apply (case_tac "f s x",simp)
apply (case_tac " (mapAccumL f a xs)")
by simp
lemma length_snd_mapAccumL:
"∀ s. length (snd (mapAccumL f s xs)) = length xs"
apply (induct xs)
apply simp
by (subst snd_mapAccumL_x_xs,simp)
lemma mapAccumL_snd_length:
"length xs = length ys
==> length (snd (mapAccumL f s ys)) = length xs"
by (insert length_snd_mapAccumL,force)
lemma length_tn'_equals_length_recursiveArgs:
"[| length vn = length tn';
coherentC C;
constructorSignature C = Some (tn', ρ', TypeExpression.ConstrT T tm' ρs') |]
==> length tn' = length (zip vn (recursiveArgs C))"
apply (simp add: coherentC_def)
apply (case_tac "the (ConstructorTable C)",simp)
apply (case_tac "b", simp)
by (simp add: recursiveArgs_def)
lemma SafeDARegion_Var2_length_equals:
"[| length vn = length tn';
coherentC C;
constructorSignature C = Some (tn', ρ', TypeExpression.ConstrT T tm' ρs') |]
==> length (snd (mapAccumL (copy' j) h (zip vn (recursiveArgs C)))) = length tn'"
apply (subgoal_tac "length tn' = length (zip vn (recursiveArgs C))")
apply (rule mapAccumL_snd_length,assumption)
by (rule length_tn'_equals_length_recursiveArgs,assumption+)
declare copy.simps [simp del]
lemma SafeDARegionDepth_Var2:
"[| ϑ1 x = Some (ConstrT T ti ρl);
ϑ2 r = Some ρ';
coherent constructorSignature Tc|]
==> CopyE x r a :f , n \<lbrace>(ϑ1,ϑ2), ConstrT T ti ((butlast ρl)@[ρ']) \<rbrace>"
apply (unfold SafeRegionDAssDepth.simps)
apply (intro allI, rule impI, elim conjE)
apply (frule impSemBoundRA [where td=td])
apply (elim exE)
apply (erule SafeRASem.cases,simp_all)
apply (simp add: consistent.simps)
apply (elim conjE)
apply (erule_tac x="x" in ballE)
prefer 2 apply (simp add: dom_def)
apply (elim exE, elim conjE)
apply (elim exE, elim conjE)
apply clarsimp
apply (erule consistent_v.cases,simp_all)
(* case pa ∉ dom h *)
apply (simp add: def_copy)
apply (erule_tac x="pa" in ballE,simp)
apply (subgoal_tac "pa ∈ closureL pa (h,ka)",simp)
apply (rule closureL_basic)
(* case pa ∈ dom h *)
apply (rule consistent_v.algebraic)
(* h p *)
apply (frule dom_copy')
apply (frule copy_h'_p',force,force,force)
(* ρ' = last (butlast pl @ [ρ']) *)
apply simp
(* ρ' ∈ dom η' *)
apply (erule_tac x="r" and A="dom E2a" in ballE)
prefer 2 apply force
apply (elim exE, elim conjE)+
apply (simp add: dom_def)
(* η' ρ' = Some j *)
apply (erule_tac x="r" and A="dom E2a" in ballE)
prefer 2 apply force
apply (elim exE, elim conjE)+
apply simp
(* constructorSignature *)
apply force
(* wellT *)
apply force
(* length vn = length tn *)
apply (simp only: coherent_def)
apply (elim conjE)
apply (rule SafeDARegion_Var2_length_equals,assumption+)
apply (erule_tac x="C" and A="dom constructorSignature" in ballE)
apply (simp,force,force)
(* consistent_v tn *)
apply clarsimp
apply (rule_tac x="μ1" in exI)
apply (rule_tac x="μ2(last ρs' \<mapsto> ρ')" in exI)
apply (drule_tac s="the (μ2 (last ρs'))" in sym)
apply simp
apply (simp add: wellT.simps)
apply (elim conjE)
apply (subgoal_tac "∃ ρ. last ρs' = ρ")
prefer 2 apply simp
apply (erule exE)
apply simp
apply (rule conjI)
apply (subgoal_tac
"(ρ ∉ regions t
--> mu_ext (μ1, μ2(ρ \<mapsto> ρ')) t = mu_ext (μ1, μ2) t) ∧
(ρ ∉ regions' tm'
--> mu_exts (μ1, μ2(ρ \<mapsto> ρ')) tm' = mu_exts (μ1, μ2) tm')")
apply simp
apply (rule ρ_notin_regions_mu_ext_copy_monotone)
apply (rule conjI)
apply (rule map_ρs_equals_butlast_copy,assumption+)
by (rule SafeDARegion_Var2_2, assumption+)
(********** Assert: (ReuseE x a) ***********)
lemma case_Recursive:
"[|h q = Some (j,C, vn); i < length vn; vn ! i = Loc p;
snd (snd (the (ConstructorTable C)))!i = Recursive;
length (snd (snd (the (ConstructorTable C)))) = length vn|]
==> (Recursive, Loc p) ∈
{x ∈ set (zip (getArgType (getConstructorCell (C, vn)))
(getValuesCell (C, vn))). isNonBasicValue (fst x)}"
apply (subst set_zip)
apply (simp add: getConstructorCell_def)
apply (simp add: getArgType_def)
apply (simp add: getValuesCell_def)
apply (simp add: isNonBasicValue_def)
by force
lemma case_NonRecursive:
" [|h q = Some (j,C, vn); i < length vn; vn ! i = Loc p;
snd (snd (the (ConstructorTable C)))!i = NonRecursive;
length (snd (snd (the (ConstructorTable C)))) = length vn|]
==> (NonRecursive, Loc p) ∈
{x ∈ set (zip (getArgType (getConstructorCell (C, vn))) (getValuesCell (C, vn))). isNonBasicValue (fst x)}"
apply (subst set_zip)
apply (simp add: getConstructorCell_def)
apply (simp add: getArgType_def)
apply (simp add: getValuesCell_def)
apply (simp add: isNonBasicValue_def)
by force
lemma p_in_closureL_Recursive:
" [|h q = Some (j, C, vn); i < length vn; vn ! i = Loc p;
length (snd (snd (the (ConstructorTable C)))) = length vn;
snd (snd (the (ConstructorTable C)))!i = Recursive|]
==> p ∈ closureL q (h, k)"
apply (rule_tac q="q" in closureL_step)
apply (rule closureL_basic)
apply (simp add: descendants_def)
apply (simp add: getNonBasicValuesCell_def)
apply (frule case_Recursive, assumption+)
by force
lemma p_in_closureL_NonRecursive:
"[|h q = Some (j, C, vn); i < length vn; vn ! i = Loc p;
length (snd (snd (the (ConstructorTable C)))) = length vn;
snd (snd (the (ConstructorTable C)))!i = NonRecursive|]
==> p ∈ closureL q (h, k)"
apply (rule_tac q="q" in closureL_step)
apply (rule closureL_basic)
apply (simp add: descendants_def)
apply (simp add: getNonBasicValuesCell_def)
apply (frule case_NonRecursive, assumption+)
by force
lemma closureV_vn_closureV_q:
"[| h q = Some (j, C, vn); coherentC C;
constructorSignature C = Some (tn', ρ', TypeExpression.ConstrT T tm' ρs');
length tn' = length vn|]
==> (\<Union> i < length vn. closureV (vn!i) (h,k)) ⊆
closureV (Loc q) (h, k)"
apply (rule subsetI)
apply (simp add: closureV_def)
apply (elim bexE)
apply (case_tac "vn!i",simp_all)
apply (erule closureL.induct)
prefer 2 apply (rule closureL_step,assumption+)
apply (rename_tac p)
apply (simp only: coherentC_def)
apply (case_tac "the (ConstructorTable C)")
apply (case_tac b)
apply (rename_tac nargs b n largs)
apply (case_tac "the (constructorSignature C)")
apply (case_tac ba)
apply (rename_tac ts ba ρl t)
apply (simp add: Let_def)
apply (elim conjE)
apply (erule_tac x="i" in allE,simp)
apply (elim conjE)
apply (case_tac "ts!i")
(* ts!i = VarT *)
apply simp
apply (rule p_in_closureL_NonRecursive)
apply (assumption+,simp,assumption+,simp,simp)
(* ts!i = TypeExpression.ConstrT list1 list2 list3 *)
apply (case_tac "ts!i = TypeExpression.ConstrT intType [] []")
(* ts!i = TypeExpression.ConstrT intType [] [] *)
apply clarsimp
(* ts!i = TypeExpression.ConstrT boolType [] [] *)
apply (case_tac "ts!i = TypeExpression.ConstrT boolType [] []")
apply clarsimp
(* ts!i ≠ t *)
apply (case_tac "ts!i ≠ ConstrT T tm' ρs'")
apply simp
apply (rule p_in_closureL_NonRecursive)
apply (assumption+,simp,assumption+,simp,simp)
(* ts!i = t *)
apply simp
apply (rule p_in_closureL_Recursive)
apply (assumption+,simp,assumption+,simp,simp)
done
lemma p_notin_closureV_q_notin_closureV_vn:
"[| p ∉ closureV (Loc q) (h, k);
h q = Some (j,C,vn);
constructorSignature C = Some (tn', ρ', TypeExpression.ConstrT T tm' ρs');
length tn' = length vn;
coherentC C |]
==> ∀ i < length vn. p ∉ closureV (vn!i) (h,k)"
apply (subgoal_tac
"(\<Union> i < length vn. closureV (vn!i) (h,k)) ⊆
closureV (Loc q) (h, k)")
apply blast
by (rule closureV_vn_closureV_q,force+)
lemma SafeDARegion_Var3_1 [rule_format]:
"consistent_v t η v h
--> fresh q h
--> h p = Some (j,C,vn)
--> v ∈ rangeHeap h
--> p ∉ closureV v (h,k)
--> coherent constructorSignature Tc
--> consistent_v t η v (h(p := None)(q \<mapsto> c))"
apply (rule impI)
apply (erule consistent_v.induct,simp_all)
(* intType *)
apply (clarsimp, rule consistent_v.primitiveI)
(* boolType *)
apply (clarsimp, rule consistent_v.primitiveB)
(* VarT *)
apply (clarsimp, rule consistent_v.variable)
(* ConstrT None *)
apply (clarsimp, rule consistent_v.algebraic_None)
apply (subgoal_tac "pa ≠ p",simp)
prefer 2 apply force
apply (subgoal_tac "pa ≠ q",clarsimp)
apply (simp add: fresh_def, clarsimp)
(* ConstrT *)
apply (elim exE, elim conjE)
apply (rule impI)+
apply (rule consistent_v.algebraic)
(* h p *)
apply (subgoal_tac "pa ≠ q")
prefer 2 apply (simp add: fresh_def,elim conjE, simp add: dom_def, force)
apply (case_tac "pa ≠ p",force)
apply (simp add: closureV_def)
apply (subgoal_tac "p ∈ closureL p (h, k)")
apply simp
apply (rule closureL.closureL_basic)
(* ρl = last ρs *)
apply force
(* ρl ∈ dom η *)
apply force
(* η ρl = Some j *)
apply force
(* constructorSignature *)
apply force
(* wellT *)
apply force
(* length vn = length tn' *)
apply force
(* consistent_v *)
apply (rule_tac x="μ1" in exI)
apply (rule_tac x="μ2" in exI)
apply (rule conjI)
apply force
apply (rule allI,rule impI)
apply (erule_tac x="i" in allE,simp)
apply (elim conjE)
apply (simp add: coherent_def)
apply (elim conjE)
apply (erule_tac x="Ca" in ballE)
apply (frule p_notin_closureV_q_notin_closureV_vn)
apply (assumption+,simp+)
apply (simp add: rangeHeap_def,clarsimp)
apply force
apply force
done
lemma SafeDARegionDepth_Var3:
"[| ϑ1 x = Some t; coherent constructorSignature Tc |]
==> ReuseE x a :f , n \<lbrace> (ϑ1,ϑ2) , t \<rbrace>"
apply (unfold SafeRegionDAssDepth.simps)
apply (intro allI, rule impI, elim conjE)
apply (frule impSemBoundRA [where td=td])
apply (elim exE)
apply (erule SafeRASem.cases,simp_all,clarsimp)
apply (case_tac t,simp_all)
apply (rule consistent_v.variable)
apply (simp add: consistent.simps)
apply (elim conjE)
apply (erule_tac x="x" in ballE)
prefer 2 apply (simp add: dom_def)
apply (elim exE, elim conjE)
apply (elim exE, elim conjE)
apply clarsimp
apply (erule consistent_v.cases,simp_all)
(* ConstrT None *)
apply (simp add: dom_def)
(* ConstrT *)
apply (elim exE, elim conjE)
apply (rule consistent_v.algebraic)
(* h p *)
apply force
(* ρ' = last ps *)
apply simp
(* ρ' ∈ dom η' *)
apply (erule_tac x="r" and A="dom E2a" in ballE)
prefer 2 apply force
apply (elim exE, elim conjE)+
apply (simp add: dom_def)
(* η' ρ' = Some j *)
apply (erule_tac x="r" and A="dom E2a" in ballE)
prefer 2 apply force
apply (elim exE, elim conjE)+
apply simp
(* constructorSignature *)
apply force
(* wellT *)
apply force
(* length vn = length tn' *)
apply force
(* consistent_v tn *)
apply (rule_tac x="μ1" in exI)
apply (rule_tac x="μ2" in exI)
apply (rule conjI)
apply simp
apply (rule allI,rule impI)
apply (erule_tac x="i" in allE, simp)
apply (frule_tac k="k" in no_cycles)
apply (erule_tac x="i" in allE,simp)
apply (frule SafeDARegion_Var3_1)
apply (assumption+,simp add: rangeHeap_def,force,assumption+)
done
(********** Assert: LET1 ***********)
(*** P1' ***)
lemma SafeDARegion_LET1_P1':
"[| (E1, E2) \<turnstile> h , k , td , Let x1 = e1 In e2 a \<Down> h' , k , v , r;
x1 ∉ fv e1;
fv e1 ∪ fv e2 - {x1} ⊆ dom E1 |]
==> fv e1 ⊆ dom E1 ∧ fv e2 ⊆ insert x1 (dom E1)"
apply (rule conjI)
apply blast
by blast
(*** P5 ***)
lemma consistent_v_notin_dom_h' [rule_format]:
"consistent_v t η v h
--> v ∉ domLoc h'
--> (∀p∈dom h. p ∉ dom h' ∨ h p = h' p)
--> consistent_v t η v h'"
apply (rule impI)
apply (erule consistent_v.induct)
(* intType *)
apply (rule impI)+
apply (rule consistent_v.primitiveI)
(* boolType *)
apply (rule impI)+
apply (rule consistent_v.primitiveB)
(* varT *)
apply (rule impI)+
apply (rule consistent_v.variable)
(* p ∉ dom h *)
apply (rule impI)+
apply (rule consistent_v.algebraic_None)
apply (simp add: domLoc_def)
(* p ∈ dom h. Constr T *)
apply (rule impI)+
apply (elim exE)
apply (erule_tac x="p" in ballE)
apply (erule disjE)
(* p ∉ dom h' *)
apply (rule consistent_v.algebraic_None,simp)
(* p ∈ dom h *)
apply (rule consistent_v.algebraic)
apply (force,force,force,force,force,force,force)
apply (rule_tac x="μ1" in exI)
apply (rule_tac x="μ2" in exI)
apply (simp add: domLoc_def)
apply force
apply (simp add: dom_def)
done
lemma consistent_v_Loc_p_in_dom_h [rule_format]:
"consistent_v t η (Loc p) h
--> (E1, E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r
--> (Loc p) ∈ domLoc h
--> (∀p∈dom h. p ∉ dom h' ∨ h p = h' p)
--> consistent_v t η (Loc p) h'"
apply (rule impI)
apply (erule consistent_v.induct)
(* intType *)
apply (simp add: domLoc_def)
(* boolType *)
apply (simp add: domLoc_def)
(* varT *)
apply (clarsimp,rule consistent_v.variable)
(* p ∉ dom h *)
apply (simp add: domLoc_def)
(* p ∈ dom h. Constr T *)
apply (rule impI)+
apply (case_tac "p ∉ dom h'")
apply (rule consistent_v.algebraic_None,simp)
(* p ∈ dom h' *)
apply (elim exE, elim conjE,simp,elim conjE)
apply (rule consistent_v.algebraic)
apply (simp add: domLoc_def)
apply (force,force,force,force,force,force,force)
apply (rule_tac x="μ1" in exI)
apply (rule_tac x="μ2" in exI)
apply (rule conjI, force)
apply clarsimp
apply (erule_tac x="i" in allE,simp)+
apply (simp add: domLoc_def)
apply (case_tac "(∃p. p ∈ dom h ∧ vn ! i = Loc p)",simp)
apply (rule consistent_v_notin_dom_h',simp)
(*(vn ! i) ∉ dom h *)
apply (erule_tac x="p" in ballE)
prefer 2 apply (simp add: dom_def)
apply (drule mp)
apply (simp add: dom_def)
apply (frule_tac v'="vn!i" in semantic_no_capture_h)
apply (simp add: rangeHeap_def add: domLoc_def)
apply force
apply simp
apply simp
done
lemma monotone_consistent_Loc_p:
"[|(E1, E2) \<turnstile> h , k ,td, e \<Down> h' , k ,v,r;
ϑ1 x = Some t; E1 x = Some (Loc p);
consistent_v t η (Loc p) h|]
==> consistent_v t η (Loc p) h'"
apply (case_tac "p ∈ dom h")
apply (frule semantic_extend_pointers)
apply (rule consistent_v_Loc_p_in_dom_h,assumption+)
apply (simp add: domLoc_def, simp)
apply (frule semantic_no_capture_E1,assumption+)
by (rule consistent_v.algebraic_None,simp)
lemma monotone_consistent_v:
"[|(E1, E2) \<turnstile> h , k , td, e \<Down> h' , k , v, r;
ϑ1 x = Some t; E1 x = Some v'; consistent_v t η v' h|]
==> consistent_v t η v' h'"
apply (case_tac v',simp_all)
(* v = Loc p *)
apply (rule monotone_consistent_Loc_p,assumption+)
(* v = IntT n *)
apply (erule consistent_v.cases,simp_all)
apply (rule consistent_v.primitiveI)
apply (rule consistent_v.variable)
(* v = BoolT b *)
apply (erule consistent_v.cases,simp_all)
apply (rule consistent_v.primitiveB)
apply (rule consistent_v.variable)
done
lemma monotone_consistent:
"[| (E1, E2) \<turnstile> h , k , td, e \<Down> h' , k , v, r;
consistent (ϑ1,ϑ2) η (E1, E2) h |]
==> consistent (ϑ1,ϑ2) η (E1, E2) h'"
apply (simp add: consistent.simps)
apply (rule ballI)
apply (elim conjE)
apply (erule_tac x="x" in ballE)
prefer 2 apply simp
apply (elim exE, elim conjE)
apply (elim exE, elim conjE)
apply (rule_tac x="t" in exI)
apply (rule conjI,assumption)
apply (rule_tac x="va" in exI)
apply (rule conjI,assumption)
by (rule monotone_consistent_v,assumption+)
lemma SafeDARegion_LET1_P5:
"[| (E1, E2) \<turnstile> h , k , td, e1 \<Down>h' , k , v1, r; x1 ∉ dom ϑ1;
consistent (ϑ1,ϑ2) η (E1, E2) h; consistent_v t1 η v1 h' |]
==> consistent (ϑ1(x1 \<mapsto> t1),ϑ2) η (E1(x1 \<mapsto> v1), E2) h'"
apply (drule_tac h'="h'" in monotone_consistent, simp)
apply (unfold consistent.simps)
apply (rule conjI)
apply simp
apply (rule conjI)
apply (rule ballI)
apply (elim conjE)
apply (erule_tac x="r" and A="dom E2" in ballE)
prefer 2 apply simp
apply (elim exE,elim conjE)
apply (rule_tac x="r'" in exI)
apply (rule_tac x="r''" in exI)
apply (rule conjI)
apply clarsimp
apply clarsimp
by clarsimp
(***** Main Theorem LET1 *****)
lemma SafeDARegionDepth_LET1:
"[| ∀ C as r a'. e1 ≠ ConstrE C as r a';
x1 ∉ dom ϑ1; x1 ∉ fv e1;
e1 :f , n \<lbrace> (ϑ1,ϑ2), t1 \<rbrace> ;
e2 :f , n \<lbrace> (ϑ1(x1\<mapsto>t1),ϑ2), t2 \<rbrace> |]
==> Let x1 = e1 In e2 a :f , n \<lbrace> (ϑ1,ϑ2), t2 \<rbrace> "
apply (unfold SafeRegionDAssDepth.simps)
apply (intro allI, rule impI)
apply (elim conjE)
apply (frule impSemBoundRA [where e="Let x1 = e1 In e2 a" and td=td])
apply (elim exE)
apply (frule P1_f_n_LET,assumption)
apply (elim exE)
apply (erule_tac x="C" in allE)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="h'a" in allE)
apply (erule_tac x="v1" in allE)
apply (erule_tac x="η" in allE)
apply (erule_tac x="E1(x1 \<mapsto> v1)" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h'a" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="η" in allE)
apply (frule SafeDARegion_LET1_P1',assumption,simp)
apply (elim conjE)
apply (drule mp)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply simp
apply (drule mp)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (rule conjI,simp,blast)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (frule_tac e=e1 and td=td in impSemBoundRA)
apply (elim exE)
by (rule SafeDARegion_LET1_P5,force,assumption+)
(********** Assert: LETC ***********)
(** P5 **)
lemma fvs_prop2:
"[| i < length as; as ! i = VarE x a |]
==> x ∈ fvs as"
by (induct as i rule: list_induct3, simp_all)
lemma mu_last:
"ρs ≠ []
==> (the (μ2 (last ρs))) = last (map (the o μ2) ρs)"
by (induct ρs,simp,clarsimp)
lemma extend_heaps_upd:
"fresh p h
==> extend_heaps (h,k) (h(p \<mapsto> (j, C, map (atom2val E1) as)),k)"
apply (simp add: extend_heaps.simps)
apply (rule ballI)
apply (subgoal_tac "p ∉ dom h")
apply (subgoal_tac "pa ≠ p",simp)
apply (frule fresh_notin_closureL)
apply force
apply (simp add: dom_def,force)
by (simp add: fresh_def)
lemma not_in_set_conv_nth:
"x ∉ set xs
==> ∀ i < length xs. xs!i ≠ x"
apply (case_tac "xs = []",simp_all)
apply (rule allI, rule impI)
apply (induct xs arbitrary: i,simp_all)
apply (case_tac i, simp_all)
apply force
by force
lemma consistent_v_fresh_p_Loc_q [rule_format]:
"consistent_v t η (Loc q) h
--> (Loc q) ≠ (Loc p)
--> fresh p h
--> consistent_v t η (Loc q) (h(p \<mapsto> (j, C, map (atom2val E1) as)))"
apply (rule impI)
apply (erule consistent_v.induct,simp_all)
(* intType *)
apply (clarsimp,rule consistent_v.primitiveI)
(* boolType *)
apply (clarsimp,rule consistent_v.primitiveB)
(* varT *)
apply (clarsimp,rule consistent_v.variable)
(* p ∉ dom h *)
apply (clarsimp,rule consistent_v.algebraic_None)
apply (simp add: fresh_def, simp add: dom_def)
(* p ∈ dom h*)
apply clarsimp
apply (rule consistent_v.algebraic)
apply (subgoal_tac "p ≠ pa",force)
apply (simp add: fresh_def)
apply (force,force,force,force,force,force)
apply (rule_tac x="μ1" in exI)
apply (rule_tac x="μ2" in exI)
apply (rule conjI, force)
apply (simp add: fresh_def)
apply (elim conjE)
apply (simp add: rangeHeap_def)
apply (rotate_tac 9)
apply (erule_tac x="pa" in allE)
apply (rotate_tac 9)
apply (erule_tac x="ja" in allE)
apply (erule_tac x="Ca" in allE)
apply (erule_tac x="vn" in allE)
apply simp
apply (frule not_in_set_conv_nth)
apply simp
done
lemma monotone_consistent_v_fresh:
"[|(E1, E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r ;
ϑ1 x = Some t; E1 x = Some v'; fresh p h;
consistent_v t η v' h |]
==> consistent_v t η v' (h(p \<mapsto> (j, C, map (atom2val E1) as)))"
apply (case_tac v',simp_all)
(* v = Loc p *)
apply (rename_tac q)
apply (frule semantic_no_capture_E1_fresh,simp)
apply (erule_tac x="x" in ballE)
prefer 2 apply (simp add: dom_def)
apply (erule_tac x="q" in allE, simp)
apply (rule consistent_v_fresh_p_Loc_q,assumption+,force,simp)
(* v = IntT n *)
apply (erule consistent_v.cases,simp_all)
apply (rule consistent_v.primitiveI)
apply (rule consistent_v.variable)
(* v = BoolT b *)
apply (erule consistent_v.cases,simp_all)
apply (rule consistent_v.primitiveB)
apply (rule consistent_v.variable)
done
lemma SafeDARegion_LETC_P5:
"[| (E1, E2) \<turnstile> h , k , td , Let x1 = ConstrE C as r () In e2 () \<Down> h' , k , v , ra ;
E2 r = Some j; x1 ∉ fvs as; fvs as ⊆ dom E1; x1 ∉ dom ϑ1;
constructorSignature C = Some (ti, ρ, TypeExpression.ConstrT T tn ρs);
t' = mu_ext (μ1,μ2) (TypeExpression.ConstrT T tn ρs);
argP (map (mu_ext (μ1,μ2)) ti) (the (μ2 ρ)) as r (ϑ1,ϑ2);
consistent (ϑ1,ϑ2) η (E1, E2) h; fresh p h;
wellT ti ρ (TypeExpression.ConstrT T tn ρs) |]
==> consistent (ϑ1(x1 \<mapsto> t'),ϑ2) η (E1(x1 \<mapsto> Loc p), E2) (h(p \<mapsto> (j, C, map (atom2val E1) as)))"
apply (unfold consistent.simps)
apply (elim conjE)
apply (rule conjI)
(* ∀x∈dom (fst (E1(x1 \<mapsto> Loc p), E2)) *)
apply (rule ballI,simp)
apply (rule conjI)
(* x = x1 *)
apply (rule impI,simp)
apply (simp add: wellT.simps)
apply (simp add: argP.simps)
apply (elim conjE)
apply (erule_tac x="r" and A="dom E2" in ballE)
prefer 2 apply (simp add: dom_def)
apply (elim exE, elim conjE)+
apply (subgoal_tac "(the (μ2 (last ρs))) = last (map (the o μ2) ρs)")
prefer 2 apply (rule mu_last,simp)
apply (rule consistent_v.algebraic)
(* h p *)
apply force
(* ρl = last ρs *)
apply force
(* ρl ∈ dom η *)
apply (simp add: dom_def)
(* η ρl = Some j *)
apply force
(* constructorSignature C *)
apply force
(* wellT *)
apply (simp add: wellT.simps)
(* length vn = length tn' *)
apply force
(* consistent_v tn *)
apply (rule_tac x="μ1" in exI)
apply (rule_tac x="μ2" in exI)
apply clarsimp
apply (erule_tac x="i" in allE,simp)+
apply (erule disjE)
(* ConstE LitN *)
apply (erule exE)+
apply simp
apply (rule consistent_v.primitiveI)
apply (erule disjE)
(* ConstE LitB *)
apply (erule exE)+
apply simp
apply (rule consistent_v.primitiveB)
(* VarE *)
apply (erule exE)+
apply simp
apply (erule_tac x="x" in ballE)
prefer 2 apply (frule fvs_prop2,assumption+,force)
apply (elim exE,elim conjE)+
apply simp
apply (rule monotone_consistent_v_fresh, assumption+)
(* x ≠ x1 *)
apply (rule impI)
apply (erule_tac x="x" in ballE)
prefer 2 apply simp
apply simp
apply (elim exE, elim conjE)+
apply (rule_tac x="t" in exI)
apply (rule conjI, assumption)
apply (rule_tac x="va" in exI)
apply (rule conjI, assumption)
apply (rule monotone_consistent_v_fresh, assumption+)
(* ∀r∈dom (snd (E1(x1 \<mapsto> Loc p), E2) *)
apply (rule conjI)
apply (rule ballI)
apply (erule_tac x="rb" and A="dom E2" in ballE)
prefer 2 apply simp
apply (elim exE)
apply (rule_tac x="r'" in exI)
apply (rule_tac x="r''" in exI)
apply (rule conjI)
apply clarsimp
apply clarsimp
by clarsimp
(***** Main Theorem LETC *****)
lemma SafeDARegionDepth_LETC:
"[| x1 ∉ fvs as; x1 ∉ dom ϑ1;
constructorSignature C = Some (ti,ρ,t);
t = ConstrT T tn ρs;
t' = mu_ext (μ1,μ2) t;
argP (map (mu_ext (μ1,μ2)) ti) ((the o μ2) ρ) as r (ϑ1,ϑ2);
wellT ti ρ t;
e2 :f , n \<lbrace> (ϑ1(x1\<mapsto>t'),ϑ2), t'' \<rbrace> |]
==> Let x1 = ConstrE C as r a' In e2 a :f , n \<lbrace> (ϑ1,ϑ2) , t'' \<rbrace>"
apply (unfold SafeRegionDAssDepth.simps)
apply (intro allI, rule impI)
apply (elim conjE)
apply (frule impSemBoundRA [where e="Let x1 = ConstrE C as r a' In e2 a" and td=td])
apply (elim exE)
apply (frule P1_f_n_LETC)
apply (erule exE)+
apply (elim conjE)
apply (erule_tac x="E1(x1 \<mapsto> Loc p)" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h(p \<mapsto> (j, C, map (atom2val E1) as))" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="η" in allE)
apply (simp)
apply (elim conjE)
apply (drule mp)
apply (rule conjI,blast)
apply (rule conjI,blast)
apply (subgoal_tac "fvs as ⊆ dom E1")
prefer 2 apply blast
apply (rule_tac ?μ1.0="μ1" and ?μ2.0="μ2" in SafeDARegion_LETC_P5)
by (assumption+, simp, assumption+)
(********** Assert: CASE ***********)
(*** P1 ***)
lemma P1_f_n_CASE:
"[| E1 x = Some (Val.Loc p);
(E1, E2) \<turnstile> h , k , Case VarE x a Of alts a' \<Down> (f, n) hh , k , v |]
==> ∃ j C vs. h p = Some (j,C,vs) ∧
( ∃ i<length alts.
((extend E1 (snd (extractP (fst (alts ! i)))) vs, E2)
\<turnstile> h , k , snd (alts ! i) \<Down>(f,n) hh , k , v
∧ def_extend E1 (snd (extractP (fst (alts ! i)))) vs) ∧
(∃ pati ei ps ms.
alts ! i = (pati, ei) ∧
pati = ConstrP C ps ms))"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
by force
(*** P1' ***)
lemma fvTup_subseteq_fvAlts:
"∀ i < length alts. fvTup (alts!i) ⊆ fvAlts alts"
apply (rule allI, rule impI)
apply (rule subsetI)
apply (induct alts arbitrary: i)
apply simp
apply (case_tac i)
apply simp
by clarsimp
(** fv_P1' **)
lemma SafeRegion_CASE_fv_P1' [rule_format]:
"length alts > 0
--> fv (Case VarE x a Of alts a') ⊆ dom E1
--> (∀ i < length alts. ∀ vs.
def_extend E1 (snd (extractP (fst (alts ! i)))) vs
--> fv (snd (alts ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs))"
apply (induct alts arbitrary: i ,simp_all)
apply (rule impI)+
apply (elim conjE)
apply (rule allI)
apply (rule impI)+
apply (case_tac "alts = []",simp_all)
apply (rule allI,rule impI)
apply (simp add: def_extend_def)
apply (case_tac a, simp_all)
apply (elim conjE)
apply (simp add: extend_def)
apply blast
apply (rule allI, rule impI)
apply (case_tac i,simp_all)
apply (case_tac a, simp_all)
apply (simp add: def_extend_def)
apply (erule_tac x="0" in allE,simp)
apply (erule_tac x="vs" in allE)
apply (simp add: extend_def)
by blast
(** fv_P1' (LitN) **)
lemma SafeRegion_CASEL_LitN_fv_P1' [rule_format]:
"length alts > 0
--> fv (Case VarE x a Of alts a') ⊆ dom E1
--> (∀ i < length alts.
fst (alts ! i) = ConstP (LitN n)
--> fv (snd (alts ! i)) ⊆ dom E1)"
apply (induct alts arbitrary: i ,simp_all)
apply (rule impI)+
apply (elim conjE)
apply (rule allI)
apply (rule impI)+
apply (case_tac "alts = []",simp_all)
apply (case_tac a, simp_all)
apply (case_tac i,simp_all)
by (case_tac a, simp_all)
(** fv_P1' (LitB) **)
lemma SafeRegion_CASEL_LitB_fv_P1' [rule_format]:
"length alts > 0
--> fv (Case VarE x a Of alts a') ⊆ dom E1
--> (∀ i < length alts.
fst (alts ! i) = ConstP (LitB b)
--> fv (snd (alts ! i)) ⊆ dom E1)"
apply (induct alts arbitrary: i ,simp_all)
apply (rule impI)+
apply (elim conjE)
apply (rule allI)
apply (rule impI)+
apply (case_tac "alts = []",simp_all)
apply (case_tac a, simp_all)
apply (case_tac i,simp_all)
by (case_tac a, simp_all)
(** fvReg_P1' **)
lemma SafeRegion_CASE_fvReg_P1':
"[| fvReg (Case VarE x a Of alts a') ⊆ dom E2; i < length alts |]
==> fvReg (snd (alts ! i)) ⊆ dom E2"
apply (induct alts arbitrary: i,simp_all)
apply (case_tac i,simp)
by (case_tac a, simp_all)
(*** P2 ***)
lemma SafeRegion_CASE_E1_P2:
"[| dom E1 ⊆ dom ϑ1;
i < length alts;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = TypeExpression.ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) = ϑ1 ++ map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti)) ∧
dom ϑ1 ∩ dom (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) = {} ∧
ϑ1 x = Some (mu_ext μ t) ∧ snd (assert ! i) = ϑ2;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
∀i<length alts. x ∉ set (snd (extractP (fst (alts ! i)))) |]
==> dom (extend E1 (snd (extractP (fst (alts ! i)))) vs) ⊆ dom (fst (assert ! i))"
apply (simp only: def_extend_def)
apply (rule subsetI)
apply (erule_tac x="i" in allE)+
apply (simp del: dom_map_add)
apply (elim conjE)
apply (frule_tac E="E1" and vs="vs" in extend_monotone)
apply (simp only: extend_def)
apply (subst dom_map_add,simp)
apply (erule disjE)
apply simp
apply (rule disjI2)
by blast
(*** P2 (CASEL) ***)
lemma SafeRegion_CASEL_E1_P2:
"[| dom E1 ⊆ dom ϑ1;
i < length alts;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = TypeExpression.ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) = ϑ1 ++ map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti)) ∧
dom ϑ1 ∩ dom (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) = {} ∧
ϑ1 x = Some (mu_ext μ t) ∧ snd (assert ! i) = ϑ2;
∀i<length alts. x ∉ set (snd (extractP (fst (alts ! i)))) |]
==> dom E1 ⊆ dom (fst (assert ! i))"
apply (rule subsetI)
apply (erule_tac x="i" in allE)+
apply (simp del: dom_map_add)
apply (elim conjE)
apply (simp only: extend_def)
apply (subst dom_map_add,simp)
apply (rule disjI2)
by blast
(** P4 **)
lemma in_set_conv_nth_2: "(x ∈ set xs) ==> (∃ i < length xs. xs!i = x)"
by(auto simp:set_conv_nth)
lemma x_in_variables_same_μ:
"(x ∈ variables t ∧ mu_ext μ' t = mu_ext μ t --> the (fst μ x) = the (fst μ' x)) ∧
(x ∈ variables' tm ∧ mu_exts μ' tm = mu_exts μ tm --> the (fst μ x) = the (fst μ' x))"
apply (induct_tac t and tm,simp_all)
by clarsimp
lemma x_in_regions_same_μ:
"(x ∈ regions t ∪ set ρs ∧ (∀x∈set ρs. the (snd μ' x) = the (snd μ x))
∧ mu_ext μ' t = mu_ext μ t
--> the (snd μ x) = the (snd μ' x)) ∧
(x ∈ regions' tm ∪ set ρs ∧ (∀x∈set ρs. the (snd μ' x) = the (snd μ x))
∧ mu_exts μ' tm = mu_exts μ tm
--> the (snd μ x) = the (snd μ' x))"
apply (induct_tac t and tm,simp_all)
by clarsimp+
lemma regions_variables_same_μ:
"(regions t ⊆ regions' tm' ∪ set ρs ∧ (∀x∈set ρs. the (snd μ' x) = the (snd μ x)) ∧
variables t ⊆ variables' tm' ∧ mu_exts μ' tm' = mu_exts μ tm'
--> mu_ext μ t = mu_ext μ' t) ∧
(regions' tm ⊆ regions' tm' ∪ set ρs ∧ (∀x∈set ρs. the (snd μ' x) = the (snd μ x)) ∧
variables' tm ⊆ variables' tm' ∧ mu_exts μ' tm' = mu_exts μ tm'
--> mu_exts μ tm = mu_exts μ' tm)"
apply (induct_tac t and tm,simp_all)
apply (rename_tac x)
apply (subgoal_tac
"(x ∈ variables t ∧ mu_ext μ' t = mu_ext μ t --> the (fst μ x) = the (fst μ' x)) ∧
(x ∈ variables' tm' ∧ mu_exts μ' tm' = mu_exts μ tm' --> the (fst μ x) = the (fst μ' x))")
prefer 2 apply (rule x_in_variables_same_μ)
apply simp
apply clarsimp
apply (subgoal_tac
"(x ∈ regions t ∪ set ρs ∧ (∀x∈set ρs. the (snd μ' x) = the (snd μ x))
∧ mu_ext μ' t = mu_ext μ t
--> the (snd μ x) = the (snd μ' x)) ∧
(x ∈ regions' tm' ∪ set ρs ∧ (∀x∈set ρs. the (snd μ' x) = the (snd μ x))
∧ mu_exts μ' tm' = mu_exts μ tm'
--> the (snd μ x) = the (snd μ' x))")
prefer 2 apply (rule x_in_regions_same_μ)
by force
lemma same_μ:
"[| constructorSignature C = Some (tn, ρ, ConstrT T tm ρs);
wellT tn ρ (TypeExpression.ConstrT T tm ρs);
mu_ext μ (ConstrT T tm ρs) = t';
mu_ext μ' (ConstrT T tm ρs) = t' |]
==> map (mu_ext μ) tn = map (mu_ext μ') tn"
apply (simp only: wellT.simps)
apply (elim conjE)
apply (induct_tac tm, simp_all)
apply (rule ballI)
apply (drule in_set_conv_nth_2)
apply (elim exE,elim conjE)
apply (erule_tac x="i" in allE, simp)
apply (elim conjE, clarsimp)
apply (subgoal_tac
"(regions (tn ! i) ⊆ regions' tm ∪ set ρs ∧ (∀x∈set ρs. the (snd μ' x) =
the (snd μ x)) ∧
variables (tn ! i) ⊆ variables' tm ∧ mu_exts μ' tm = mu_exts μ tm
--> mu_ext μ (tn ! i) = mu_ext μ' (tn ! i)) ∧
(regions' tm' ⊆ regions' tm ∪ set ρs ∧ (∀x∈set ρs. the (snd μ' x) =
the (snd μ x)) ∧
variables' tm' ⊆ variables' tm ∧ mu_exts μ' tm = mu_exts μ tm
--> mu_exts μ tm' = mu_exts μ' tm')")
prefer 2 apply (rule regions_variables_same_μ)
by force
lemma SafeRegion_f_n_CASE_P4:
"[|length assert = length alts; length alts > 0;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) = ϑ1 ++ (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) ∧
dom ϑ1 ∩ dom (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) = {} ∧
ϑ1 x = Some (mu_ext μ t) ∧
snd (assert ! i) = ϑ2;
consistent (ϑ1,ϑ2) η (E1, E2) h; E1 x = Some (Loc p); h p = Some(j,C,vs);
i<length alts;
(extend E1 (snd (extractP (fst (alts ! i)))) vs, E2)
\<turnstile> h , k , snd (alts ! i) \<Down>(f,n) h' , k , v;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
alts ! i = (pati, ei);
pati = ConstrP C ps ms |]
==> consistent (fst (assert ! i), snd (assert!i)) η
(extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) h"
apply (erule_tac x="i" in allE,simp)+
apply (elim conjE)
apply clarsimp
apply (simp add: Let_def)
apply (simp add: consistent.simps)
(* x∈dom (extend E1 (snd (extractP (fst (alts ! i)))) vs) *)
apply (rule ballI)
apply (simp add: extend_def)
apply (erule disjE)
(* xa ∈ dom (map_of (zip (snd (extractP (fst (alts ! i)))) vs))*)
apply (elim conjE)
apply (erule_tac x="x" in ballE)
prefer 2 apply (simp add: dom_def)
apply (elim exE, elim conjE)
apply (elim exE, elim conjE)
apply simp
apply (erule consistent_v.cases)
(* case ConstrT intType *)
apply simp
(* case ConstrT boolType *)
apply simp
(* case VarT a *)
apply simp
(* Case ConstrT None *)
apply (simp add: dom_def)
(* Case ConstrT Ta tm' ρs' *)
apply (case_tac μ,simp)
apply (elim exE, elim conjE)
apply (subgoal_tac "ρs' ≠ []")
prefer 2 apply (simp add: wellT.simps)
apply (frule_tac ?μ2.0="μ2" in mu_last,simp)
apply (case_tac "vs=[]",simp)
apply (unfold def_extend_def)
apply (elim conjE)
apply (frule_tac μ="μ" and μ'="(μ1,μ2)" in same_μ,simp,simp,simp)
apply (subgoal_tac "xa ∈ set (map pat2var ps)")
prefer 2 apply clarsimp
apply (frule_tac x="xa" and vs="(map (mu_ext μ) ti)" and zs="vs" in map_of_zip_twice_is_Some)
apply (simp,simp,simp,simp)
apply (elim exE,elim conjE)
apply (erule_tac x="ia" in allE)
apply (drule mp, simp)
apply (rule_tac x="(mu_ext μ (ti ! ia))" in exI,simp)
(* xa ∈ dom E1 *)
apply (elim conjE)
apply (erule_tac x="xa" in ballE)
prefer 2 apply simp
apply (elim exE,elim conjE)
apply (elim exE,elim conjE)
apply (rule_tac x="t" in exI)
apply (rule conjI)
apply (rule map_add_fst_Some,assumption+)
apply (rule_tac x="va" in exI)
apply (rule conjI)
apply (simp add: def_extend_def)
apply (subgoal_tac "E1 xa = (extend E1 (map pat2var ps) vs) xa")
apply (simp add: extend_def)
apply (rule extend_monotone,force)
by assumption+
lemma SafeRegion_CASEL_LitB_P4:
"[|length assert = length alts; length alts > 0;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) = ϑ1 ++ (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) ∧
dom ϑ1 ∩ dom (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) = {} ∧
ϑ1 x = Some (mu_ext μ t) ∧
snd (assert ! i) = ϑ2;
consistent (ϑ1,ϑ2) η (E1, E2) h; E1 x = Some (BoolT b);
i<length alts;
fst (alts ! i) = ConstP (LitB b)|]
==> consistent (fst (assert ! i), snd (assert!i)) η (E1, E2) h"
apply (erule_tac x="i" in allE,simp)+
done
lemma SafeRegion_CASEL_LitN_P4:
"[|length assert = length alts; length alts > 0;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) = ϑ1 ++ (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) ∧
dom ϑ1 ∩ dom (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) = {} ∧
ϑ1 x = Some (mu_ext μ t) ∧
snd (assert ! i) = ϑ2;
consistent (ϑ1,ϑ2) η (E1, E2) h; E1 x = Some (IntT n);
i<length alts;
fst (alts ! i) = ConstP (LitN n)|]
==> consistent (fst (assert ! i), snd (assert!i)) η (E1, E2) h"
apply (erule_tac x="i" in allE,simp)+
done
(***** Main Theorem CASE *****)
lemma SafeDARegionDepth_CASE:
"[| length assert = length alts; length alts > 0;
∀ i < length alts. constructorSignature (fst (extractP (fst (alts ! i))))
= Some (ti,ρ,t) ∧
t = ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) = ϑ1 ++ (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) ∧
dom ϑ1 ∩ dom (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) = {} ∧
ϑ1 x = Some (mu_ext μ t) ∧
snd (assert ! i) = ϑ2;
∀ i < length alts. snd (alts ! i) :f , n \<lbrace> (fst (assert!i),
snd (assert!i)), t' \<rbrace>;
∀ i < length alts. x ∉ set (snd (extractP (fst (alts ! i))))|]
==> Case (VarE x a) Of alts a' :f , n \<lbrace> (ϑ1,ϑ2), t' \<rbrace>"
apply (unfold SafeRegionDAssDepth.simps)
apply (intro allI, rule impI)
apply (elim conjE)
apply (case_tac "E1 x")
(* E1 x = None *)
apply (simp add: dom_def)
(* E1 x = Some x *)
apply (case_tac aa)
apply (rename_tac p)
apply (frule impSemBoundRA [where e="Case VarE x a Of alts a'" and td=td])
apply (elim exE)
apply (subgoal_tac
" ∃ j C vs. h p = Some (j,C,vs) ∧
( ∃ i<length alts.
((extend E1 (snd (extractP (fst (alts ! i)))) vs, E2)
\<turnstile> h , k , snd (alts ! i) \<Down>(f,n) h' , k , v
∧ def_extend E1 (snd (extractP (fst (alts ! i)))) vs) ∧
(∃ pati ei ps ms.
alts ! i = (pati, ei) ∧
pati = ConstrP C ps ms))")
prefer 2 apply (rule P1_f_n_CASE) apply simp apply simp
apply (elim exE,elim conjE)
apply (elim exE, elim conjE)+
apply (rotate_tac 3)
apply (erule_tac x="i" in allE)
apply (drule mp, simp)
apply (erule_tac x="extend E1 (snd (extractP (fst (alts ! i)))) vs" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (rotate_tac 20)
apply (erule_tac x="k" in allE)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="η" in allE)
apply (drule mp)
(** P1 **)
apply (rule conjI,simp)
(** fv_P1' **)
apply (rule conjI)
apply (rule SafeRegion_CASE_fv_P1',assumption+)
(** fReg_P1' **)
apply (rule conjI)
apply (rule SafeRegion_CASE_fvReg_P1',assumption+)
(** E1_P2 **)
apply (rule conjI)
apply (rule SafeRegion_CASE_E1_P2,assumption+)
(** E2_P2 **)
apply (rule conjI)
apply clarsimp
(** P3 **)
apply (rule conjI)
apply assumption
(** P4 **)
apply (rule SafeRegion_f_n_CASE_P4)
apply (assumption+,simp,assumption+)
(************************** E1 x = IntT **********************)
apply (frule impSemBoundRA [where e="Case VarE x a Of alts a'" and td=td])
apply (elim exE)
apply (subgoal_tac
"(∃ i < length alts.
(E1,E2) \<turnstile> h,k, snd (alts ! i) \<Down>(f,n) h',k,v ∧
fst (alts ! i) = ConstP (LitN int))")
prefer 2 apply (rule P1_f_n_CASE_1_1,simp,simp)
apply (elim exE,elim conjE)
apply (rotate_tac 3)
apply (erule_tac x="i" in allE)
apply (drule mp, simp)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (rotate_tac 17)
apply (erule_tac x="k" in allE)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="η" in allE)
apply (drule mp)
(** P1 **)
apply (rule conjI,simp)
(** fv_P1' **)
apply (rule conjI)
apply (rule SafeRegion_CASEL_LitN_fv_P1',assumption+)
(** fReg_P1' **)
apply (rule conjI)
apply (rule SafeRegion_CASE_fvReg_P1',assumption+)
(** E1_P2 **)
apply (rule conjI)
apply (rule SafeRegion_CASEL_E1_P2,assumption+)
(** E2_P2 **)
apply (rule conjI)
apply clarsimp
(** P3 **)
apply (rule conjI)
apply assumption
(** P4 **)
apply simp
(** P5 **)
apply simp
(************************** E1 x = BoolT **********************)
apply (frule impSemBoundRA [where e="Case VarE x a Of alts a'" and td=td])
apply (elim exE)
apply (subgoal_tac
"(∃ i < length alts.
(E1,E2) \<turnstile> h,k, snd (alts ! i) \<Down>(f,n) h',k,v
∧ fst (alts ! i) = ConstP (LitB bool))")
prefer 2 apply (rule P1_f_n_CASE_1_2) apply simp apply force
apply (elim exE,elim conjE)
apply (rotate_tac 3)
apply (erule_tac x="i" in allE)
apply (drule mp, simp)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (rotate_tac 17)
apply (erule_tac x="k" in allE)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="η" in allE)
apply (drule mp)
(** P1 **)
apply (rule conjI,simp)
(** fv_P1' **)
apply (rule conjI)
apply (rule SafeRegion_CASEL_LitB_fv_P1',assumption+)
(** fReg_P1' **)
apply (rule conjI)
apply (rule SafeRegion_CASE_fvReg_P1',assumption+)
(** E1_P2 **)
apply (rule conjI)
apply (rule SafeRegion_CASEL_E1_P2,assumption+)
(** E2_P2 **)
apply (rule conjI)
apply clarsimp
(** P3 **)
apply (rule conjI)
apply assumption
(** P4 **)
apply simp
(** P5 **)
by simp
(********** Assert: CASED ***********)
(*** P1 ***)
lemma SafeRegion_f_n_CASED_P1:
"[|(E1,E2) \<turnstile> h,k,CaseD (VarE x a) Of alts a \<Down>(f,n) h',k,v|]
==> ∃ p j C vs. E1 x = Some (Loc p) ∧ h p = Some (j,C,vs) ∧
(∃ i<length alts.
(extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) \<turnstile> h(p := None) , k , snd (alts ! i) \<Down>(f,n) h' , k , v
∧ def_extend E1 (snd (extractP (fst (alts ! i)))) vs ∧
(∃ pati ei ps ms.
alts ! i = (pati, ei) ∧
pati = ConstrP C ps ms))"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
by force
(*** P1' ***)
lemma fvTup'_subseteq_fvAlts':
"i < length alts
==> fvTup' (alts!i) ⊆ fvAlts' alts"
apply (rule subsetI)
apply (induct alts arbitrary: i)
apply simp
apply (case_tac i)
apply simp
by clarsimp
(** fv_P1' **)
lemma SafeRegion_CASED_fv_P1' [rule_format]:
"length alts > 0
--> fv (CaseD VarE x a Of alts a') ⊆ dom E1
--> (∀ i < length alts. ∀ vs.
def_extend E1 (snd (extractP (fst (alts ! i)))) vs
--> fv (snd (alts ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs))"
apply (induct alts arbitrary: i ,simp_all)
apply (rule impI)+
apply (elim conjE)
apply (rule allI)
apply (rule impI)+
apply (case_tac "alts = []",simp_all)
apply (rule allI,rule impI)
apply (simp add: def_extend_def)
apply (case_tac a, simp_all)
apply (elim conjE)
apply (simp add: extend_def)
apply blast
apply (rule allI, rule impI)
apply (case_tac i,simp_all)
apply (case_tac a, simp_all)
apply (simp add: def_extend_def)
apply (erule_tac x="0" in allE,simp)
apply (erule_tac x="vs" in allE)
apply (simp add: extend_def)
by blast
(** fvReg_P1' **)
lemma SafeRegion_CASED_fvReg_P1':
"[| fvReg (CaseD VarE x a Of alts a') ⊆ dom E2; i < length alts |]
==> fvReg (snd (alts ! i)) ⊆ dom E2"
apply (induct alts arbitrary: i,simp_all)
apply (case_tac i,simp)
by (case_tac a, simp_all)
(** P4 **)
lemma consistent_v_p_none [rule_format]:
"consistent_v t η v h
--> p ∉ closureV v (h,k)
--> coherent constructorSignature Tc
--> consistent_v t η v (h(p := None))"
apply (rule impI)
apply (erule consistent_v.induct,simp_all)
(* intType *)
apply (clarsimp, rule consistent_v.primitiveI)
(* boolType *)
apply (clarsimp, rule consistent_v.primitiveB)
(* VarT *)
apply (clarsimp, rule consistent_v.variable)
(* ConstrT None *)
apply clarsimp
apply (rule consistent_v.algebraic_None)
apply (simp add: dom_def)
(* ConstrT *)
apply (elim exE, elim conjE)
apply (rule impI)+
apply (rule consistent_v.algebraic)
(* h p *)
apply (case_tac "pa ≠ p",force)
apply (simp add: closureV_def)
apply (subgoal_tac "p ∈ closureL p (h, k)")
apply simp
apply (rule closureL.closureL_basic)
(* ρl = last ρs *)
apply force
(* ρl ∈ dom η *)
apply force
(* η ρl = Some j *)
apply force
(* constructorSignature *)
apply force
(* wellT *)
apply force
(* length vn = length tn' *)
apply force
(* consistent_v *)
apply (rule_tac x="μ1" in exI)
apply (rule_tac x="μ2" in exI)
apply (rule conjI)
apply force
apply (rule allI,rule impI)
apply (erule_tac x="i" in allE,simp)
apply (elim conjE)
apply (simp add: coherent_def)
apply (elim conjE)
apply (erule_tac x="C" in ballE)
apply (frule p_notin_closureV_q_notin_closureV_vn)
apply (assumption+,simp+)
apply force
done
lemma consistent_v_p_none_x_in_dom_E1:
"consistent_v t η v h
==> consistent_v t η v (h(p := None))"
apply (case_tac v,simp_all)
(* v = Loc q *)
apply (rename_tac q)
apply (case_tac "q = p")
(* q = p *)
apply (rule consistent_v.algebraic_None)
apply (simp add: dom_def)
(* q ≠ p *)
apply (erule consistent_v.induct)
(* intType *)
apply (clarsimp, rule consistent_v.primitiveI)
(* boolType *)
apply (clarsimp, rule consistent_v.primitiveB)
(* VarT *)
apply (clarsimp, rule consistent_v.variable)
(* ConstrT None *)
apply (case_tac "pa=p")
apply (rule consistent_v.algebraic_None,force)
apply (rule consistent_v.algebraic_None,force)
(* ConstrT *)
apply (elim exE, elim conjE)
apply (case_tac "pa = p")
apply (rule consistent_v.algebraic_None,force)
apply (rule consistent_v.algebraic)
(* h p *)
apply force
(* ρl = last ρs *)
apply force
(* ρl ∈ dom η *)
apply force
(* η ρl = Some j *)
apply force
(* constructorSignature *)
apply force
(* wellT *)
apply force
(* length vn = length tn' *)
apply force
(* consistent_v *)
apply (rule_tac x="μ1" in exI)
apply (rule_tac x="μ2" in exI)
apply (rule conjI)
apply force
apply force
(* v = IntT i *)
apply (erule consistent_v.cases,simp_all)
apply (rule consistent_v.primitiveI)
apply (rule consistent_v.variable)
(* v = BoolT b *)
apply (erule consistent_v.cases,simp_all)
apply (rule consistent_v.primitiveB)
apply (rule consistent_v.variable)
done
lemma SafeRegion_f_n_CASED_P4:
"[|length assert = length alts; length alts > 0;
coherent constructorSignature Tc;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) = ϑ1 ++ (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) ∧
dom ϑ1 ∩ dom (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) = {} ∧
ϑ1 x = Some (mu_ext μ t) ∧
snd (assert ! i) = ϑ2;
consistent (ϑ1,ϑ2) η (E1, E2) h; E1 x = Some (Loc p); h p = Some(j,C,vs);
i<length alts;
(extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) \<turnstile> h
(p := None) , k , snd (alts ! i) \<Down>(f,n) h' , k , v;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
alts ! i = (pati, ei);
pati = ConstrP C ps ms |]
==> consistent (fst (assert ! i), snd (assert!i)) η
(extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p:=None))"
apply (erule_tac x="i" in allE,simp)+
apply (elim conjE)
apply clarsimp
apply (simp add: Let_def)
apply (simp add: consistent.simps)
(* x∈dom (extend E1 (snd (extractP (fst (alts ! i)))) vs) *)
apply (rule ballI)
apply (simp add: extend_def)
apply (erule disjE)
(* xa ∈ dom (map_of (zip (snd (extractP (fst (alts ! i)))) vs))*)
apply (elim conjE)
apply (erule_tac x="x" in ballE)
prefer 2 apply (simp add: dom_def)
apply (elim exE, elim conjE)
apply (elim exE, elim conjE)
apply simp
apply (erule consistent_v.cases)
(* case ConstrT intType *)
apply simp
(* case ConstrT boolType *)
apply simp
(* case VarT a *)
apply simp
(* Case ConstrT None *)
apply (simp add: dom_def)
(* Case ConstrT Ta tm' ρs' *)
apply (case_tac μ,simp)
apply (elim exE, elim conjE)
apply (subgoal_tac "ρs' ≠ []")
prefer 2 apply (simp add: wellT.simps)
apply (frule_tac ?μ2.0="μ2" in mu_last,simp)
apply (case_tac "vs=[]",simp)
apply (unfold def_extend_def)
apply (elim conjE)
apply (frule_tac μ="μ" and μ'="(μ1,μ2)" in same_μ,simp,simp,simp)
apply (subgoal_tac "xa ∈ set (map pat2var ps)")
prefer 2 apply clarsimp
apply (frule_tac x="xa" and vs="(map (mu_ext μ) ti)" and zs="vs" in map_of_zip_twice_is_Some)
apply (simp,simp,simp,simp)
apply (elim exE,elim conjE)
apply (erule_tac x="ia" in allE)
apply (drule mp, simp)
apply (rule_tac x="(mu_ext μ (ti ! ia))" in exI,simp)
apply (frule no_cycles)
apply (rule consistent_v_p_none)
apply (assumption+,force,assumption)
(* xa ∈ dom E1 *)
apply (elim conjE)
apply (erule_tac x="xa" in ballE)
prefer 2 apply simp
apply (elim exE,elim conjE)
apply (elim exE,elim conjE)
apply (rule_tac x="t" in exI)
apply (rule conjI)
apply (rule map_add_fst_Some,assumption+)
apply (rule_tac x="va" in exI)
apply (rule conjI)
apply (simp add: def_extend_def)
apply (subgoal_tac "E1 xa = (extend E1 (map pat2var ps) vs) xa")
apply (simp add: extend_def)
apply (rule extend_monotone,force)
by (rule consistent_v_p_none_x_in_dom_E1,simp)
(***** Main Theorem CASED *****)
lemma SafeDARegionDepth_CASED:
"[| length assert = length alts; length alts > 0;
coherent constructorSignature Tc;
∀ i < length alts. constructorSignature (fst (extractP (fst (alts ! i))))
= Some (ti,ρ,t) ∧
t = ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) = ϑ1 ++ (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) ∧
dom ϑ1 ∩ dom (map_of (zip (snd (extractP (fst (alts ! i))))
(map (mu_ext μ) ti))) = {} ∧
ϑ1 x = Some (mu_ext μ t) ∧
snd (assert ! i) = ϑ2;
∀ i < length alts. snd (alts ! i) :f , n
\<lbrace> (fst (assert!i), snd (assert!i)), t' \<rbrace>;
∀ i < length alts. x ∉ set (snd (extractP (fst (alts ! i))))|]
==> CaseD (VarE x a) Of alts a' :f , n \<lbrace> (ϑ1,ϑ2), t' \<rbrace> "
apply (unfold SafeRegionDAssDepth.simps)
apply (intro allI, rule impI)
apply (elim conjE)
apply (frule impSemBoundRA [where e="CaseD VarE x a Of alts a'" and td=td])
apply (elim exE)
apply (subgoal_tac
"∃ p j C vs. E1 x = Some (Loc p) ∧ h p = Some (j,C,vs) ∧
(∃ i<length alts.
(extend E1 (snd (extractP (fst (alts ! i)))) vs, E2)
\<turnstile> h(p :=None) , k , snd (alts ! i) \<Down>(f,n) h' , k , v
∧ def_extend E1 (snd (extractP (fst (alts ! i)))) vs ∧
(∃ pati ei ps ms.
alts ! i = (pati, ei) ∧
pati = ConstrP C ps ms))")
prefer 2 apply (rule SafeRegion_f_n_CASED_P1,simp)
apply (elim exE,elim conjE)+
apply (rotate_tac 4)
apply (erule_tac x="i" in allE)
apply (drule mp, simp)
apply (erule_tac x="extend E1 (snd (extractP (fst (alts ! i)))) vs" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h(p:=None)" in allE)
apply (rotate_tac 20)
apply (erule_tac x="k" in allE)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="η" in allE)
apply (drule mp)
(** P1 **)
apply (rule conjI,simp)
(** fv_P1' **)
apply (rule conjI)
apply (rule SafeRegion_CASED_fv_P1',assumption+)
(** fReg_P1' **)
apply (rule conjI)
apply (rule SafeRegion_CASED_fvReg_P1',assumption+)
(** E1_P2 **)
apply (rule conjI)
apply (rule SafeRegion_CASE_E1_P2
[where ti=ti and ρ=ρ and t=t and T=T and tn=tn and
ρs=ρs and μ=μ and x=x and ?ϑ2.0=ϑ2])
apply (simp,simp,force,simp,simp)
(** E2_P2 **)
apply (rule conjI, clarsimp)
(** P3 **)
apply (rule conjI)
apply assumption
(** P4 **)
apply (rule SafeRegion_f_n_CASED_P4
[where ti=ti and ρ=ρ and t=t and T=T and tn=tn and
ρs=ρs and μ=μ and x=x and ?ϑ1.0=ϑ1 and ?ϑ2.0=ϑ2])
by assumption+
(********** Assert: APP ***********)
(* E1_P2 *)
lemma SafeDARegion_APP_E1_P2:
"[| length xs = length as; length xs = length ti; distinct xs |]
==> dom (map_of (zip xs (map (atom2val E1) as))) ⊆
dom (mu_ext (fst (μ_ren (μ1, μ2)), snd (μ_ren (μ1, μ2))(ρself \<mapsto> ρself))
of map_of (zip xs ti))"
by (simp, subst dom_map_f_comp, simp)
(* E2_P2 *)
lemma SafeDARegion_APP_E2_P2:
"[| ∀ i < length ρs. ∃ t. μ2 (ρs!i) = Some t; distinct rs;
length rs = length rr; length rs = length ρs; μ_ren_dom (μ1, μ2) |]
==> dom (map_of (zip rs (map (the o E2) rr))(self \<mapsto> Suc k)) ⊆
dom (snd (μ_ren (μ1, μ2))(ρself \<mapsto> ρself)
om map_of (zip rs ρs)(self \<mapsto> ρself))"
apply simp
apply (rule conjI)
apply force
apply (rule subsetI)
apply (subgoal_tac
" dom ((λρ. Some (ρ_ren (the (μ2 ρ))))(ρself \<mapsto> ρself)
om map_of (zip rs ρs)(self \<mapsto> ρself))
= dom (map_of (zip rs ρs)(self \<mapsto> ρself))")
apply simp
by (rule dom_map_comp,simp)
(** P3 **)
lemma SafeDARegion_APP_P3:
"admissible η k
==> admissible (η_ren η ++ [ρself \<mapsto> Suc k]) (Suc k)"
apply (simp add: admissible_def)
apply (simp add: η_ren_def)
apply (rule conjI)
apply (rule impI)
apply (elim conjE)
apply (erule_tac x="ρself" in ballE)
prefer 2 apply simp
apply clarsimp
apply clarsimp
apply (rule conjI)
apply (rule impI)+
apply (split split_if_asm,simp,simp)
apply (erule_tac x="ρself" in ballE)
prefer 2 apply (simp add: dom_def)
apply (simp, split split_if_asm,simp,simp)
apply (rule impI)
apply (erule_tac x="ρ" in ballE)
prefer 2 apply (simp add: dom_def)
by simp
(** P4 **)
lemma μ_ren_extend_ρself:
"(ρself ∉ regions t
--> mu_ext (λx. Some (t_ren (the (μ1 x))),(λρ. Some (ρ_ren (the (μ2 ρ))))
(ρself \<mapsto> ρself)) t =
mu_ext (λx. Some (t_ren (the (μ1 x))), λρ. Some (ρ_ren (the (μ2 ρ)))) t) ∧
(ρself ∉ regions' ts
--> mu_exts (λx. Some (t_ren (the (μ1 x))),(λρ. Some (ρ_ren (the (μ2 ρ))))
(ρself \<mapsto> ρself)) ts =
mu_exts (λx. Some (t_ren (the (μ1 x))), λρ. Some (ρ_ren (the (μ2 ρ)))) ts)"
by (induct_tac t and ts,simp_all)
lemma map_ρ_ren:
"ρself ∉ set xs ==> xs = map ρ_ren xs"
apply (induct xs,simp_all)
apply (simp add: ρ_ren_def)
by force
lemma t_equals_t_ren:
"(ρself ∉ regions t ∧ ρself ∉ variables t --> t = t_ren t) ∧
(ρself ∉ regions' tm ∧ ρself ∉ variables' tm --> tm = t_rens tm)"
apply (induct_tac t and tm,simp_all)
apply (rule impI, elim conjE)
apply clarsimp
by (rule map_ρ_ren, assumption+)
lemma ρ_equals_ρ_ren:
"[| ρself ∉ (the o μ2) ` set ρs; ρ ∈ set ρs |]
==> the (μ2 ρ) = ρ_ren (the (μ2 ρ))"
apply (induct ρs, simp_all)
apply (simp add: ρ_ren_def)
by force
lemma μ_ren_extend_t_ren:
"(ρself ∉ regions (mu_ext (μ1, μ2) t) ∧ ρself ∉ variables (mu_ext (μ1, μ2) t)
--> mu_ext (μ1, μ2) t =
mu_ext (λx. Some (t_ren (the (μ1 x))), λρ. Some (ρ_ren (the (μ2 ρ)))) t) ∧
(ρself ∉ regions' (mu_exts (μ1, μ2) ts) ∧ ρself ∉ variables' (mu_exts (μ1, μ2) ts)
--> mu_exts (μ1, μ2) ts =
mu_exts (λx. Some (t_ren (the (μ1 x))), λρ. Some (ρ_ren (the (μ2 ρ)))) ts)"
apply (induct_tac t and ts,simp_all)
apply (subgoal_tac
"(ρself ∉ regions (the (μ1 list)) ∧ ρself ∉ variables (the (μ1 list))
--> (the (μ1 list)) = t_ren (the (μ1 list))) ∧
(ρself ∉ regions' tm ∧ ρself ∉ variables' tm --> tm = t_rens tm)",simp)
apply (rule t_equals_t_ren)
apply clarsimp
by (rule ρ_equals_ρ_ren,assumption+)
lemma mu_ext_args_xs:
"[| distinct xs; length xs = length ti; length as = length ti;
x ∈ set xs;
dom (map_of (zip xs (map (atom2val E1) as))) = set xs;
mu_ext (μ1,μ2) (ti ! i) = t;
i < length as;
ρself ∉ regions t; ρself ∉ variables t; ρself ∉ regions (ti!i);
xs ! i = x |]
==> (mu_ext (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))(ρself \<mapsto> ρself)) of
map_of (zip xs ti)) x = Some t"
apply (drule_tac t="t" in sym,simp)
apply (subst map_f_comp_map_of_zip, assumption+)
apply (drule_tac t="x" in sym,simp)
apply (insert
set_zip [where xs="xs" and
ys="(map (mu_ext (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))(ρself \<mapsto> ρself))) ti)"])
apply (simp, rule_tac x="i" in exI,simp)
apply (subgoal_tac
"(ρself ∉ regions (ti!i)
--> mu_ext (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))(ρself \<mapsto> ρself)) (ti!i) =
mu_ext (λx. Some (t_ren (the (μ1 x))), λρ. Some (ρ_ren (the (μ2 ρ)))) (ti!i)) ∧
(ρself ∉ regions' ts
--> mu_exts (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))(ρself \<mapsto> ρself)) ts =
mu_exts (λx. Some (t_ren (the (μ1 x))), λρ. Some (ρ_ren (the (μ2 ρ)))) ts)")
prefer 2 apply (rule μ_ren_extend_ρself)
apply simp
apply (subgoal_tac
"(ρself ∉ regions (mu_ext (μ1, μ2) (ti!i)) ∧ ρself ∉ variables (mu_ext (μ1, μ2) (ti!i))
--> mu_ext (μ1, μ2) (ti!i) =
mu_ext (λx. Some (t_ren (the (μ1 x))), λρ. Some (ρ_ren (the (μ2 ρ)))) (ti!i)) ∧
(ρself ∉ regions' (mu_exts (μ1, μ2) ts) ∧ ρself ∉ variables' (mu_exts (μ1, μ2) ts)
--> mu_exts (μ1, μ2) ts =
mu_exts (λx. Some (t_ren (the (μ1 x))), λρ. Some (ρ_ren (the (μ2 ρ)))) ts)")
prefer 2 apply (rule μ_ren_extend_t_ren)
by simp
lemma map_comp_map_of_zip_μ:
"[|distinct rs; length ρs = length rr; length rs = length rr; rs ! i = r;
rs ! i ≠ self;
∀ i < length ρs. ∃ t. (snd (μ_ren (μ1, μ2))) (ρs!i) = Some t;
ρself ∉ set ρs; i < length rr;
(rs ! i, n) ∈ set (zip rs (map (the o E2) rr)) |]
==> (snd (μ_ren (μ1, μ2))(ρself \<mapsto> ρself)
om map_of (zip rs ρs)(self \<mapsto> ρself)) r =
Some (the (snd (μ_ren (μ1, μ2)) (ρs ! i)))"
apply (drule_tac t="r" in sym)
apply (subgoal_tac
"(snd (μ_ren (μ1, μ2))(ρself \<mapsto> ρself) om
map_of (zip rs ρs)(self \<mapsto> ρself)) (rs ! i) =
(snd (μ_ren (μ1, μ2))(ρself \<mapsto> ρself) om
map_of (zip rs ρs)) (rs ! i)",simp)
prefer 2 apply (simp add: map_comp_def)
apply (subst map_comp_map_of_zip,simp,simp,simp,simp)
apply (subst map_mu_self,simp)
apply (insert set_zip [where xs="rs" and ys="(map (the o snd (μ_ren (μ1, μ2))) ρs)"])
apply (simp,rule_tac x="i" in exI)
by simp
lemma consistent_η_ren_ρs:
"[| i < length ρs; η (the (μ2 (ρs ! i))) = Some n;
ρfake ∉ dom η; ρfake ∉ ran μ2; μ_ren_dom (μ1, μ2);
∀ i < length ρs. ∃ t. μ2 (ρs!i) = Some t|]
==> (η_ren η ++ [ρself \<mapsto> Suc k]) (the (snd (μ_ren (μ1, μ2)) (ρs ! i))) = Some n"
apply simp
apply (rule conjI)
apply (simp add: ρ_ren_def)
apply (simp add: ρself_def add: ρfake_def)
apply (rule impI)
apply (simp add: ρ_ren_def)
apply (rule conjI,rule impI)
apply (simp add: η_ren_def)
apply (rule impI,force)
apply (simp add: η_ren_def)
by force
lemma t_ren_mu_ext:
"t_ren (mu_ext (μ1, μ2) t) =
mu_ext (λx. Some (t_ren (the (μ1 x))), λa. Some (ρ_ren (the (μ2 a)))) t ∧
t_rens (mu_exts (μ1, μ2) ts) =
mu_exts (λx. Some (t_ren (the (μ1 x))), λa. Some (ρ_ren (the (μ2 a)))) ts"
apply (induct_tac t and ts,simp_all)
by (induct_tac list3,simp_all)
lemma mu_exts_ren:
"[| mu_exts (μ1, μ2) tm' = tm; map (the o μ2) ρs' = ρs |]
==> mu_exts (λx. Some (t_ren (the (μ1 x))),
λa. Some (ρ_ren (the (μ2 a)))) tm' = t_rens tm
∧ map (the o (λa. Some (ρ_ren (the (μ2 a))))) ρs' = map ρ_ren ρs"
apply clarsimp
apply (rule conjI)
apply (subgoal_tac
"t_ren (mu_ext (μ1, μ2) t) =
mu_ext (λx. Some (t_ren (the (μ1 x))), λa. Some (ρ_ren (the (μ2 a)))) t ∧
t_rens (mu_exts (μ1, μ2) tm') =
mu_exts (λx. Some (t_ren (the (μ1 x))), λa. Some (ρ_ren (the (μ2 a)))) tm'")
prefer 2 apply (rule t_ren_mu_ext)
apply clarsimp
by (induct_tac ρs',simp_all)
lemma η_ren_ρ_ren_ρl_SomeI:
"[| ρl = last ρs; last ρs ∈ dom η; η (last ρs) = Some j;
η' = η_ren η(ρself \<mapsto> Suc k);
ρs ≠ [];
ρfake ∉ dom η|]
==> (η_ren η(ρself \<mapsto> Suc k)) (ρ_ren (last ρs)) = Some j"
apply (simp add: ρ_ren_def)
apply (rule conjI)
apply (rule impI)
apply (simp add: η_ren_def)
apply clarsimp
apply (rule impI)
apply (simp add: η_ren_def)
by clarsimp
lemma last_map_not_ρself:
"[| ρself ∉ (the o μ2) ` set ρs';
ρs' ≠ [] |]
==> last (map (the o μ2) ρs') ≠ ρself"
by (induct ρs',simp_all,force)
lemma length_ρs:
"[| length ρs' > 0;
(the (μ2 ρ'), mu_ext (μ1, μ2) (TypeExpression.ConstrT T tm' ρs')) =
(ρl, TypeExpression.ConstrT T tm ρs) |]
==> ρs ≠ []"
apply (simp,elim conjE)
by (induct ρs',simp,clarsimp)
lemma consistent_t_consistent_t_ren [rule_format]:
"consistent_v t η v h
--> ρfake ∉ dom η
--> η' = (η_ren η(ρself \<mapsto> Suc k))
--> consistent_v (t_ren t) η' v h"
apply (rule impI)
apply (erule consistent_v.induct)
(* ConstrT intType [] [] *)
apply (rule impI)+
apply simp
apply (rule consistent_v.primitiveI)
(* ConstrT boolType [] [] *)
apply (rule impI)+
apply simp
apply (rule consistent_v.primitiveB)
(* VarT *)
apply (rule impI)+
apply simp
apply (rule consistent_v.variable)
(* ConstrT T tm ρs None *)
apply clarsimp
apply (rule consistent_v.algebraic_None)
apply (simp add: dom_def)
(* ConstrT T tm ρs *)
apply (rule impI)+
apply (elim exE, elim conjE)
apply (simp only: t_ren_t_rens.simps(2))
apply (rule consistent_v.algebraic)
(* h p *)
apply force
(* ρl = last ρs *)
apply force
(* ρl ∈ dom η *)
apply (simp only: wellT.simps)
apply (elim conjE)
apply (frule length_ρs,assumption+)
apply (subst map_last,assumption+)
apply (frule η_ren_ρ_ren_ρl_SomeI, assumption+)
apply (simp add: dom_def)
(* η ρl = Some j *)
apply (simp only: wellT.simps)
apply (elim conjE)
apply (frule length_ρs,assumption+)
apply (subst map_last,assumption+)
apply (frule η_ren_ρ_ren_ρl_SomeI)
apply (assumption,assumption,assumption,assumption,assumption,assumption)
(* constructorSignature C *)
apply force
(* wellT *)
apply force
(* length vs = length tn' *)
apply force
(* μ1,μ2 *)
apply (rule_tac x="(λx. Some (t_ren (the (μ1 x))))" in exI)
apply (rule_tac x="(λa. Some (ρ_ren (the (μ2 a))))" in exI)
apply (rule conjI)
apply (simp only: wellT.simps)
apply (elim conjE)
apply (frule length_ρs,assumption+)
apply simp
apply (rule conjI)
apply (subst map_last,assumption+,simp)
apply (elim conjE)
apply (rule mu_exts_ren,assumption+)
(* ∀ i < length vn. consistent_v *)
apply (rule allI, rule impI)
apply (erule_tac x="i" in allE)
apply (drule mp,simp)
apply (elim conjE)
(* elim premises *)
apply (drule mp,simp)
apply (drule mp,simp)
apply simp
apply (subgoal_tac
"(t_ren (mu_ext (μ1, μ2) (tn' ! i))) =
(mu_ext (λx. Some (t_ren (the (μ1 x))),
λa. Some (ρ_ren (the (μ2 a)))) (tn' ! i)) ∧
t_rens (mu_exts (μ1, μ2) ts) =
mu_exts (λx. Some (t_ren (the (μ1 x))), λa. Some (ρ_ren (the (μ2 a)))) ts")
prefer 2 apply (rule t_ren_mu_ext)
apply simp
done
lemma mu_ext_args_xs_ti:
"[| distinct xs; length xs = length ti; length as = length ti;
x ∈ set xs;
dom (map_of (zip xs (map (atom2val E1) as))) = set xs;
mu_ext (μ1,μ2) (ti ! i) = t;
i < length as; ρself ∉ regions (ti ! i);
xs ! i = x |]
==> (mu_ext (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))(ρself \<mapsto> ρself)) of
map_of (zip xs ti)) x = Some (mu_ext (λx. Some (t_ren (the (μ1 x))),
λρ. Some (ρ_ren (the (μ2 ρ)))) (ti ! i))"
apply (drule_tac t="t" in sym,simp)
apply (subst map_f_comp_map_of_zip, assumption+)
apply (drule_tac t="x" in sym,simp)
apply (insert
set_zip [where xs="xs" and
ys="(map (mu_ext (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))(ρself \<mapsto> ρself))) ti)"])
apply (simp, rule_tac x="i" in exI,simp)
apply (subgoal_tac
"(ρself ∉ regions (ti!i)
--> mu_ext (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))(ρself \<mapsto> ρself)) (ti!i) =
mu_ext (λx. Some (t_ren (the (μ1 x))),
λρ. Some (ρ_ren (the (μ2 ρ)))) (ti!i)) ∧ (ρself ∉ regions' ts
--> mu_exts (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))(ρself \<mapsto> ρself)) ts =
mu_exts (λx. Some (t_ren (the (μ1 x))),
λρ. Some (ρ_ren (the (μ2 ρ)))) ts)")
apply simp
by (rule μ_ren_extend_ρself)
lemma SafeDARegion_APP_P4:
"[| distinct xs; length xs = length ti; length xs = length as;
distinct rs; length rs = length rr; length rs = length ρs;
ρself ∉ regions tg ∪ (\<Union> set (map regions ti)) ∪ set ρs;
∀ i < length ρs. ∃ t. μ2 (ρs!i) = Some t; ρfake ∉ ran μ2;
μ_ren_dom (μ1, μ2);
set rr ⊆ dom E2; fvs' as ⊆ dom E1;
consistent (ϑ1,ϑ2) η (E1, E2) h;
argP_app (map (mu_ext (μ1,μ2)) ti) (map (the o μ2) ρs) as rr (ϑ1,ϑ2) |]
==> consistent
(mu_ext (fst (μ_ren (μ1, μ2)), snd (μ_ren (μ1, μ2))(ρself \<mapsto> ρself))
of map_of (zip xs ti),
snd (μ_ren (μ1, μ2))(ρself \<mapsto> ρself)
om map_of (zip rs ρs)(self \<mapsto> ρself))
(η_ren η ++ [ρself \<mapsto> Suc k]) (map_of (zip xs (map (atom2val E1) as)),
map_of (zip rs (map (the o E2) rr))(self \<mapsto> Suc k)) h"
apply (subgoal_tac "ρfake ∉ dom η")
prefer 2 apply (rule ρfake_not_in_dom_η)
apply (unfold consistent.simps)
apply (elim conjE)
apply (rule conjI)
(* ∀x∈ dom (map_of (zip xs (map (atom2val E1) as))) *)
apply simp
apply (rule ballI)
apply (subgoal_tac
"∃ i < length as. xs!i = x ∧
(map_of (zip xs (map (atom2val E1) as))) x = Some (atom2val E1 (as!i))")
prefer 2 apply (frule_tac vs="map (atom2val E1) as"
in map_of_zip_is_SomeI,simp,simp,force)
apply (elim exE, elim conjE)
apply (simp add: argP_app.simps)
apply (elim conjE)
apply (erule_tac x="i" in allE,simp)+
apply (erule disjE)
(* ConstE (LitN c) a *)
apply (elim exE,simp)
apply (rule_tac x="(ConstrT intType [] [])" in exI)
apply (rule conjI)
apply (rule_tac i="i" in mu_ext_args_xs)
apply (assumption+,simp,assumption+,simp,force,simp,simp,assumption+)
apply (rule_tac x="IntT c" in exI,simp)
apply (rule consistent_v.primitiveI)
apply (erule disjE)
(* ConstE (LitB b) a *)
apply (elim exE,simp)
apply (rule_tac x="(ConstrT boolType [] [])" in exI)
apply (rule conjI)
apply (rule_tac i="i" in mu_ext_args_xs)
apply (assumption+,simp,assumption+,simp,force,simp,simp,assumption+)
apply (rule_tac x="BoolT b" in exI,simp)
apply (rule consistent_v.primitiveB)
(* VarE x a *)
apply (elim exE)
apply (simp add: argP_aux.simps)
apply (rule_tac x="mu_ext (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))) (ti ! i)" in exI)
apply (rule conjI)
apply (rule_tac i="i" in mu_ext_args_xs_ti,assumption+,simp,simp,simp,force,simp)
apply (rule_tac x="the (E1 xa)" in exI,simp)
apply (erule_tac x="xa" in ballE)
apply (elim exE, elim conjE)+
apply simp
apply (subgoal_tac
"t_ren (mu_ext (μ1, μ2) (ti ! i)) =
mu_ext (λx. Some (t_ren (the (μ1 x))), λa. Some (ρ_ren (the (μ2 a)))) (ti ! i) ∧
t_rens (mu_exts (μ1, μ2) ts) =
mu_exts (λx. Some (t_ren (the (μ1 x))), λa. Some (ρ_ren (the (μ2 a)))) ts")
prefer 2 apply (rule t_ren_mu_ext)
apply (elim conjE)
apply (drule_tac s="t_ren (mu_ext (μ1, μ2) (ti ! i))" in sym)
apply simp
apply (rule consistent_t_consistent_t_ren, assumption+,simp)
(* xa ∉ dom E1 *)
apply (frule as_in_E1,simp,simp,simp)
(* ∀r∈dom map_of (zip rs (map (the o E2) rr))(self \<mapsto> Suc k) *)
apply (rule conjI)
apply (rule ballI)
apply (case_tac "r = self")
(* r = self *)
apply clarsimp
(* r ∈ dom (map_of (zip rs (map (the o E2) rr)) *)
apply (subgoal_tac "r ∈ set rs")
prefer 2 apply simp
apply (subgoal_tac
"∃ i < length rr. rs!i = r ∧ (map_of (zip rs (map (the o E2) rr))) r =
Some ((the o E2) (rr!i))")
prefer 2 apply (frule_tac vs="map (the o E2) rr"
in map_of_zip_is_SomeI,simp,simp,force)
apply (simp only: argP_app.simps)
apply (elim exE,elim conjE)
apply (subgoal_tac "∀ i < length rr. ∃ n. E2 (rr!i) = Some n")
prefer 2 apply (rule rr_in_E2,assumption)
apply (rotate_tac 28)
apply (erule_tac x="i" in allE) apply (drule mp) apply simp
apply (erule_tac x="rr!i" and A="dom E2" in ballE)
prefer 2 apply (simp add: dom_def)
apply (elim exE, elim conjE)+
apply (rule_tac x="the ((snd (μ_ren (μ1,μ2))) (ρs!i))" in exI)
apply (rule_tac x="n" in exI)
apply (rule conjI)
apply (drule_tac s="length ρs" in sym)
apply (rule_tac ρs="ρs" and rr="rr" in map_comp_map_of_zip_μ)
apply (assumption+,simp,simp,assumption+,simp)
apply (simp,simp,simp,simp)
apply (rule conjI)
apply (rule consistent_η_ren_ρs)
apply (simp,simp,simp,simp,simp)
apply simp
apply simp
apply (rule conjI)
apply simp
by simp
(** P5 **)
(**** Para wellType ***)
lemma regions_induct_t_var:
"(x ∈ regions (the (fst μ ρ)) ∧ ρ ∈ variables t --> x ∈ regions (mu_ext μ t)) ∧
(x ∈ regions (the (fst μ ρ)) ∧ ρ ∈ variables' tm --> x ∈ regions' (mu_exts μ tm))"
apply (induct_tac t and tm)
by clarsimp+
lemma regions_induct_constr_ρ:
"(ρ ∈ regions t --> the (snd μ ρ) ∈ regions (mu_ext μ t)) ∧
(ρ ∈ regions' tm --> the (snd μ ρ) ∈ regions' (mu_exts μ tm))"
apply (induct_tac t and tm)
by clarsimp+
lemma regions_induct_constr_ρs [rule_format]:
"set ρs ⊆ regions t' -->
(the o snd μ) ` set ρs ⊆ regions (mu_ext μ t')"
apply (induct ρs,simp_all)
apply clarsimp
apply (subgoal_tac
"(a ∈ regions t' --> the (snd μ a) ∈ regions (mu_ext μ t')) ∧
(a ∈ regions' tm --> the (snd μ a) ∈ regions' (mu_exts μ tm))")
apply simp
by (rule regions_induct_constr_ρ)
lemma regions_regions_mu_ext:
"(regions t ⊆ regions t' ∧ variables t ⊆ variables t'
--> regions (mu_ext μ t) ⊆ regions (mu_ext μ t')) ∧
(regions' tm ⊆ regions t' ∧ variables' tm ⊆ variables t'
--> regions' (mu_exts μ tm) ⊆ regions (mu_ext μ t'))"
apply (induct_tac t and tm)
(* t = VarT *)
apply clarsimp
apply (rename_tac ρ x)
apply (subgoal_tac
"(x ∈ regions (the (fst μ ρ)) ∧ ρ ∈ variables t' --> x ∈ regions (mu_ext μ t')) ∧
(x ∈ regions (the (fst μ ρ)) ∧ ρ ∈ variables' tm --> x ∈ regions' (mu_exts μ tm))")
apply simp
apply (rule regions_induct_t_var)
(* t = ConstrT *)
apply (rule impI)
apply (elim conjE)
apply simp
apply (rule regions_induct_constr_ρs,simp)
(* tm = [] *)
apply clarsimp
(* tm = t#ts *)
by clarsimp
lemma wellT_regions:
"[| wellT tn' (last ρs') (TypeExpression.ConstrT T tm' ρs');
mu_ext (μ1, μ2) (TypeExpression.ConstrT T tm' ρs') = TypeExpression.ConstrT T tm ρs;
ρself ∉ regions (TypeExpression.ConstrT T tm ρs)|]
==> ∀i<length tn'. ρself ∉ regions (map (mu_ext (μ1, μ2)) tn' ! i)"
apply (unfold wellT.simps)
apply (elim conjE)
apply (rule allI, rule impI)
apply (erule_tac x="i" in allE)
apply (drule mp, simp)
apply (drule sym)
apply (subgoal_tac
"(regions (tn' ! i) ⊆ regions (TypeExpression.ConstrT T tm' ρs') ∧
variables (tn' ! i) ⊆ variables (TypeExpression.ConstrT T tm' ρs')
--> regions (mu_ext (μ1, μ2) (tn' ! i)) ⊆
regions (mu_ext (μ1, μ2) (TypeExpression.ConstrT T tm' ρs'))) ∧
(regions' tm'' ⊆ regions (TypeExpression.ConstrT T tm' ρs') ∧
variables' tm'' ⊆ variables (TypeExpression.ConstrT T tm' ρs')
--> regions' (mu_exts (μ1, μ2) tm'') ⊆
regions (mu_ext (μ1, μ2) (TypeExpression.ConstrT T tm' ρs')))")
apply (simp del: regions_regions'.simps(2) del: mu_ext_mu_exts.simps(2))
apply (elim conjE)
apply blast
by (rule regions_regions_mu_ext)
lemma last_notin_set:
"[| ρs ≠ []; ρ ∉ set ρs|]
==> last ρs ≠ ρ"
by (induct ρs,simp,clarsimp)
lemma η_ρ_ren_inv_ρ_Some_j:
"[| (η_ren η(ρself \<mapsto> Suc k)) ρ = Some j;
ρfake ∉ dom η;
ρ ≠ ρself |]
==> η (ρ_ren_inv ρ) = Some j"
apply (simp add: η_ren_def)
apply (split split_if_asm)
apply (simp add: ρ_ren_inv_def)
apply force
apply (simp add: ρ_ren_inv_def)
by force
lemma t_ren_in_mu_ext_inv:
"t_ren_inv (mu_ext (μ1, μ2) t) =
mu_ext (λx. Some (t_ren_inv (the (μ1 x))), λa. Some (ρ_ren_inv (the (μ2 a)))) t ∧
t_ren_invs (mu_exts (μ1, μ2) ts) =
mu_exts (λx. Some (t_ren_inv (the (μ1 x))), λa. Some (ρ_ren_inv (the (μ2 a)))) ts"
apply (induct_tac t and ts,simp_all)
by (induct_tac list3,simp_all)
lemma mu_exts_ren_inv:
"[| mu_exts (μ1, μ2) tm' = tm; map (the o μ2) ρs' = ρs |]
==> mu_exts (λx. Some (t_ren_inv (the (μ1 x))),
λa. Some (ρ_ren_inv (the (μ2 a)))) tm' = t_ren_invs tm
∧ map (the o (λa. Some (ρ_ren_inv (the (μ2 a))))) ρs' = map ρ_ren_inv ρs"
apply clarsimp
apply (rule conjI)
apply (subgoal_tac
"t_ren_inv (mu_ext (μ1, μ2) t) =
mu_ext (λx. Some (t_ren_inv (the (μ1 x))), λa. Some (ρ_ren_inv (the (μ2 a)))) t ∧
t_ren_invs (mu_exts (μ1, μ2) tm') =
mu_exts (λx. Some (t_ren_inv (the (μ1 x))), λa. Some (ρ_ren_inv (the (μ2 a)))) tm'")
prefer 2 apply (rule t_ren_in_mu_ext_inv)
apply clarsimp
by (induct_tac ρs',simp_all)
lemma consistent_t_consistent_t_ren_inv [rule_format]:
"consistent_v t' η' v h_e
--> ρself ∉ regions t'
--> η' = (η_ren η(ρself \<mapsto> Suc k))
--> consistent_v (t_ren_inv t') η v h_e"
apply (rule impI)
apply (erule consistent_v.induct)
(* ConstrT intType [] [] *)
apply (rule impI)+
apply simp
apply (rule consistent_v.primitiveI)
(* ConstrT boolType [] [] *)
apply (rule impI)+
apply simp
apply (rule consistent_v.primitiveB)
(* VarT *)
apply (rule impI)+
apply simp
apply (rule consistent_v.variable)
(* ConstrT T tm ρs None *)
apply clarsimp
apply (rule consistent_v.algebraic_None)
apply (simp add: dom_def)
(* ConstrT T tm ρs *)
apply (rule impI)+
apply (elim exE, elim conjE)
apply (simp only: t_ren_inv_t_ren_invs.simps(2))
apply (rule consistent_v.algebraic)
(* h p *)
apply force
(* ρl = last ρs *)
apply force
(* ρl ∈ dom η *)
apply (simp only: wellT.simps)
apply (elim conjE)
apply (frule length_ρs,assumption+)
apply (subst map_last,assumption+)
apply (subgoal_tac "last ρs ≠ ρself")
apply (subgoal_tac "ρfake ∉ dom η")
prefer 2 apply (rule ρfake_not_in_dom_η)
apply (frule η_ρ_ren_inv_ρ_Some_j,assumption+)
apply (simp add: dom_def)
apply (simp, elim conjE)
apply (rule last_notin_set, assumption+)
(* η ρl = Some j *)
apply (simp only: wellT.simps)
apply (elim conjE)
apply (frule length_ρs,assumption+)
apply (subst map_last,assumption+)
apply (subgoal_tac "last ρs ≠ ρself")
apply (subgoal_tac "ρfake ∉ dom η")
prefer 2 apply (rule ρfake_not_in_dom_η)
apply (frule η_ρ_ren_inv_ρ_Some_j,assumption+)
apply (simp, elim conjE)
apply (rule last_notin_set, assumption, assumption)
(* constructorSignature C *)
apply force
(* wellT *)
apply force
(* length vs = length tn' *)
apply force
(* μ1,μ2 *)
apply (rule_tac x="(λx. Some (t_ren_inv (the (μ1 x))))" in exI)
apply (rule_tac x="(λa. Some (ρ_ren_inv (the (μ2 a))))" in exI)
apply (rule conjI)
apply (simp only: wellT.simps)
apply (elim conjE)
apply (frule length_ρs,assumption+)
apply simp
apply (rule conjI)
apply (subst map_last,assumption+,simp)
apply (elim conjE)
apply (rule mu_exts_ren_inv,assumption+)
(* ∀ i < length vn. consistent_v *)
apply (rule allI, rule impI)
apply (erule_tac x="i" in allE)
apply (drule mp,simp)
apply (elim conjE)
(* elim premises *)
apply (frule wellT_regions,force,simp)
apply (drule mp,simp)
apply (drule mp,simp)
apply simp
apply (subgoal_tac
"(t_ren_inv (mu_ext (μ1, μ2) (tn' ! i))) =
(mu_ext (λx. Some (t_ren_inv (the (μ1 x))),
λa. Some (ρ_ren_inv (the (μ2 a)))) (tn' ! i)) ∧
t_ren_invs (mu_exts (μ1, μ2) ts) =
mu_exts (λx. Some (t_ren_inv (the (μ1 x))),
λa. Some (ρ_ren_inv (the (μ2 a)))) ts")
prefer 2 apply (rule t_ren_in_mu_ext_inv)
apply simp
done
lemma mu_ext_ρself_mu_ext [rule_format]:
"(ρself ∉ regions t
--> (mu_ext (μ1,μ2(ρself \<mapsto> ρself)) t) = (mu_ext (μ1,μ2) t)) ∧
(ρself ∉ regions' tm
--> (mu_exts (μ1,μ2(ρself \<mapsto> ρself)) tm) = (mu_exts (μ1,μ2) tm))"
by (induct_tac t and tm,simp_all)
lemma ρself_notin_regions_t_ren [rule_format]:
"ρself ∉ regions (t_ren t) ∧
ρself ∉ regions' (t_rens tm)"
apply (induct_tac t and tm, simp_all)
apply (induct_tac list3,simp_all)
apply (simp add: ρ_ren_def)
by (simp add: ρself_def add: ρfake_def)
lemma ρself_notin_regions_mu_ren:
"(ρself ∉ regions (mu_ext (λx. Some (t_ren (the (μ1 x))),
λa. Some (ρ_ren (the (μ2 a)))) t)) ∧
(ρself ∉ regions' (mu_exts (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))) tm))"
apply (induct_tac t and tm,simp_all)
apply (subst ρself_notin_regions_t_ren,simp)
apply (induct_tac list3,simp_all)
apply (simp add: ρ_ren_def)
by (simp add: ρself_def add: ρfake_def)
lemma t_ren_inv_t_ren:
"(notFake t --> t_ren_inv (t_ren t) = t) ∧
(notFakes tm --> t_ren_invs (t_rens tm) = tm)"
apply (induct_tac t and tm,simp_all)
apply (induct_tac list3,simp_all)
apply clarsimp
by (simp add: ρ_ren_def add: ρ_ren_inv_def)
lemma mu_ext_def_ConstrT:
"mu_ext_def (μ1, μ2) (ConstrT T tm ρs)
==> mu_exts_def (μ1, μ2) tm"
apply (simp add: mu_ext_def_def)
apply (induct tm,simp_all)
apply (case_tac a,simp_all)
apply (simp add: mu_ext_def_def)
by (simp add: mu_ext_def_def)
lemma mu_ext_def_ρs [rule_format]:
"mu_ext_def (μ1, μ2) (ConstrT T tm ρs) -->
map ρ_ren_inv (map (the o (λρ. Some (ρ_ren (the (μ2 ρ))))) ρs)
= map (the o μ2) ρs"
apply (induct_tac ρs, simp_all)
apply (rule impI)+
apply (rule conjI)
apply (simp add: mu_ext_def_def)
apply (simp add: ρ_ren_def add: ρ_ren_inv_def)
by (simp add: mu_ext_def_def)
lemma t_ren_inv_t_ren_t:
"(mu_ext_def (μ1,μ2) t
--> (t_ren_inv (mu_ext (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))) t)) =
(mu_ext (μ1, μ2) t)) ∧
(mu_exts_def (μ1,μ2) tm
--> (t_ren_invs (mu_exts (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))) tm)) =
(mu_exts (μ1, μ2) tm))"
apply (induct_tac t and tm,simp_all)
apply (rule impI)
apply (subst t_ren_inv_t_ren)
apply (simp add: mu_ext_def_def)
apply simp
apply clarsimp
apply (frule mu_ext_def_ConstrT,simp)
by (rule mu_ext_def_ρs,simp)
lemma consistent_t_ren_inv_consistent_t:
"[| ρself ∉ regions tg; mu_ext_def (μ1, μ2) tg;
consistent_v (t_ren_inv (mu_ext (λx. Some (t_ren (the (μ1 x))),
(λρ. Some (ρ_ren (the (μ2 ρ))))(ρself \<mapsto> ρself)) tg)) η v h_e|]
==> consistent_v (mu_ext (μ1, μ2) tg) η v h_e"
apply (insert mu_ext_ρself_mu_ext)
by (insert t_ren_inv_t_ren_t,simp_all)
(* Lemmas for last step *)
lemma restricted_h_equals_h:
"[| h p = Some (j,C,vn);
j < Suc k |]
==> (h |` {p ∈ dom h. fst (the (h p)) ≤ k}) p = h p"
apply (subgoal_tac "p ∈ dom h",simp)
by (simp add: dom_def)
lemma j_le_Suc_k:
"[| η ρl = Some j; admissible η k |]
==> j < Suc k"
apply (simp add: admissible_def)
apply (elim conjE)
apply (erule_tac x="ρl" in ballE)
apply force
by (simp add: dom_def)
lemma SafeDARegion_APP_P5 [rule_format]:
"consistent_v t η v h_e
--> admissible η k
--> consistent_v t η v (h_e |` {p ∈ dom h_e. fst (the (h_e p)) ≤ k})"
apply (rule impI)
apply (erule consistent_v.induct)
(* ConstrT intType [] [] *)
apply (rule impI)+
apply (rule consistent_v.primitiveI)
(* ConstrT boolType [] [] *)
apply (rule impI)+
apply (rule consistent_v.primitiveB)
(* VarT a *)
apply (rule impI)+
apply (rule consistent_v.variable)
(* ConstrT T tm ρs None *)
apply clarsimp
apply (rule consistent_v.algebraic_None)
apply (simp add: dom_def)
(* ConstrT T tm ρs *)
apply (rule impI)+
apply (elim exE, elim conjE)
apply (rule consistent_v.algebraic)
(* h p *)
apply (frule j_le_Suc_k,assumption)
apply (frule_tac h="h" in restricted_h_equals_h,assumption)
apply force
(* ρl = last ρs *)
apply force
(* ρl ∈ dom η *)
apply force
(* η ρl = Some j *)
apply force
(* constructorSignature C *)
apply force
(* wellT *)
apply force
(* length vn = length tn' *)
apply force
(* μ1, μ2 *)
apply (rule_tac x="μ1" in exI)
apply (rule_tac x="μ2" in exI)
apply simp
done
(**** Main Theorem APP ****)
declare dom_fun_upd [simp del]
declare fun_upd_apply [simp del]
declare restrict_map_def [simp del]
declare map_upds_def [simp del]
lemma lemma_19_aux [rule_format]:
"\<Turnstile> Σt
--> Σt g = Some (ti,ρs,tg)
--> Σf g = Some (xs,rs,eg)
--> (bodyAPP Σf g): \<lbrace> (map_of (zip (varsAPP Σf g) (typesArgAPP Σt g)), map_of (zip (regionsAPP Σf g) (regionsArgAPP Σt g)) ++ [self \<mapsto> ρself]),
(typeResAPP Σt g)\<rbrace>"
apply (rule impI)
apply (erule ValidGlobalRegionEnv.induct)
apply simp
apply (rule impI)+
apply (case_tac "g=f")
(* g = f *)
apply (simp add: typeResAPP_def regionsArgAPP_def typesArgAPP_def)
apply (subst (asm) fun_upd_apply, simp)
(* g ≠ f *)
apply (simp add: typeResAPP_def regionsArgAPP_def typesArgAPP_def)
by (subst (asm) fun_upd_apply, simp)
lemma equiv_SafeRegionDAss_all_n_SafeRegionDAssDepth:
"e : \<lbrace> ϑ , t \<rbrace> ==> ∀n. SafeRegionDAssDepth e f n ϑ t"
apply (case_tac ϑ)
apply (simp only: SafeRegionDAss.simps)
apply (simp only: SafeRegionDAssDepth.simps)
apply clarsimp
apply (simp only: SafeBoundSem_def)
apply (simp add: Let_def)
apply (elim exE)
apply (elim conjE)
apply (frule_tac td=td in eqSemDepthRA)
apply (elim exE)
apply (case_tac x,case_tac ba)
apply (erule_tac x=E1 in allE)
apply (erule_tac x=E2 in allE)
apply (erule_tac x=h in allE)
apply (erule_tac x=k in allE)
apply (erule_tac x=td in allE)
apply (erule_tac x=h' in allE)
apply (erule_tac x=v in allE)
apply (erule_tac x=aa in allE)
apply (erule_tac x=ab in allE)
apply (erule_tac x=bb in allE)
apply (erule_tac x=η in allE)
apply (drule mp,force)
by simp
declare SafeRegionDAssDepth.simps [simp del]
lemma lemma_19 [rule_format]:
"ValidGlobalRegionEnvDepth f n Σt
--> Σf g = Some (xs,rs,eg)
--> Σt g = Some (ti,ρs,tg)
--> g ≠ f
--> ϑ1 = map_of (zip xs ti)
--> ϑ2 = map_of (zip rs ρs) ++ [self \<mapsto> ρself]
--> SafeRegionDAssDepth eg f n (ϑ1,ϑ2) tg"
apply (rule impI)
apply (erule ValidGlobalRegionEnvDepth.induct)
(* [| \<Turnstile> Σt; f ∉ dom Σt|] ==> \<Turnstile>f,n Σt *)
apply (rule impI)+
apply (frule lemma_19_aux,force,force)
apply (frule equiv_SafeRegionDAss_all_n_SafeRegionDAssDepth)
apply (simp add: typeResAPP_def regionsArgAPP_def typesArgAPP_def)
apply (simp add: bodyAPP_def varsAPP_def regionsAPP_def)
apply force
(* [| \<Turnstile> Σt; f ∉ dom Σt|] ==> \<Turnstile>f,0 Σt(f\<mapsto>(ti,ρs,tg)) *)
apply (rule impI)+
apply (frule lemma_19_aux, simp add: fun_upd_apply, force)
apply (frule equiv_SafeRegionDAss_all_n_SafeRegionDAssDepth)
apply (subst (asm) fun_upd_apply, simp)
apply (simp add: typeResAPP_def regionsArgAPP_def typesArgAPP_def)
apply (simp add: bodyAPP_def varsAPP_def regionsAPP_def)
apply force
(* \<Turnstile>f,Suc n Σt(f\<mapsto>(ti,ρs,tg)) *)
apply (rule impI)+
apply (frule lemma_19_aux, simp add: fun_upd_apply, force)
apply (frule equiv_SafeRegionDAss_all_n_SafeRegionDAssDepth)
apply (subst (asm) fun_upd_apply, simp)
apply (simp add: typeResAPP_def regionsArgAPP_def typesArgAPP_def)
apply (simp add: bodyAPP_def varsAPP_def regionsAPP_def)
apply force
(* \<Turnstile>f, n Σt(g\<mapsto>(ti,ρs,tg)) *)
apply (case_tac "ga=g",simp_all)
apply (rule impI)+
apply (subst (asm) fun_upd_apply, simp)
apply (simp add: bodyAPP_def varsAPP_def regionsAPP_def)
apply (frule equiv_SafeRegionDAss_all_n_SafeRegionDAssDepth)
apply force
apply (rule impI)+
apply (drule mp,force)
apply (drule mp)
apply (subst (asm) fun_upd_apply, simp)
apply (drule mp, simp)
apply simp
done
lemma lemma_20 [rule_format]:
"ValidGlobalRegionEnvDepth f n Σt
--> Σf f = Some (xs,rs,ef)
--> Σt f = Some (ti,ρs,tf)
--> ϑ1 = map_of (zip xs ti)
--> ϑ2 = map_of (zip rs ρs) ++ [self \<mapsto> ρself]
--> n = Suc n'
--> SafeRegionDAssDepth ef f n' (ϑ1,ϑ2) tf"
apply (rule impI)
apply (erule ValidGlobalRegionEnvDepth.induct)
(* [| \<Turnstile> Σt; f ∉ dom Σt|] ==> \<Turnstile>f,n Σt *)
apply (rule impI)+
apply (frule lemma_19_aux, simp add: fun_upd_apply, force)
apply (frule equiv_SafeRegionDAss_all_n_SafeRegionDAssDepth)
apply (subst (asm) fun_upd_apply, simp)
apply (simp add: typeResAPP_def regionsArgAPP_def typesArgAPP_def)
apply (simp add: bodyAPP_def varsAPP_def regionsAPP_def)
apply force
(* [| \<Turnstile> Σt; f ∉ dom Σt|] ==> \<Turnstile>f,0 Σt(f\<mapsto>(ti,ρs,tg)) *)
apply simp
(* \<Turnstile>f,Suc n Σt(f\<mapsto>(ti,ρs,tg)) *)
apply (rule impI)+
apply simp
apply (subst (asm) fun_upd_apply, simp)
apply (simp add: bodyAPP_def varsAPP_def regionsAPP_def)
(* \<Turnstile>f, n Σt(g\<mapsto>(ti,ρs,tg)) *)
apply (rule impI)+
apply simp
apply (subst (asm) fun_upd_apply, simp)
done
lemma SafeDARegionDepth_APP:
"[| Σt g = Some (ti,ρs,tg); primops g = None;
ρself ∉ regions tg ∪ (\<Union> set (map regions ti)) ∪ set ρs;
length as = length ti; length ρs = length rr;
∀i<length ρs. ∃t. μ2 (ρs ! i) = Some t;
ρfake ∉ ran μ2; μ_ren_dom (μ1, μ2);
t = mu_ext (μ1,μ2) tg; mu_ext_def (μ1,μ2) tg;
Σf g = Some (xs,rs,e); fv e ⊆ set xs; fvReg e ⊆ set rs ∪ {self};
argP_app (map (mu_ext (μ1,μ2)) ti) (map (the o μ2) ρs) as rr (ϑ1,ϑ2);
\<Turnstile>f , n Σt |]
==> AppE g as rr a :f , n \<lbrace> (ϑ1,ϑ2), t \<rbrace>"
apply (case_tac "g≠f")
(* g ≠ f *)
apply (unfold SafeRegionDAssDepth.simps)
apply (intro allI, rule impI)
apply (elim conjE)
apply (frule lemma_19)
apply (force,force,assumption+,simp,simp)
apply (frule_tac ?μ1.0="fst(μ_ren (μ1,μ2))" and
?μ2.0="snd (μ_ren (μ1,μ2))(ρself \<mapsto> ρself)" in Regions_Lemma_5_Depth)
apply (frule P1_f_n_APP_2,simp,force,simp,force)
apply (elim exE,elim conjE)
apply (unfold SafeRegionDAssDepth.simps)
apply (rotate_tac 24)
apply (erule_tac x="(map_of (zip xs (map (atom2val E1) as)))" in allE)
apply (fold SafeRegionDAssDepth.simps)
apply (erule_tac x="(map_of (zip rs (map (the o E2) rr))(self \<mapsto> Suc k))" in allE)
apply (erule_tac x="h" in allE)
apply (rotate_tac 24)
apply (erule_tac x="Suc k" in allE)
apply (rotate_tac 24)
apply (erule_tac x="h'a" in allE)
apply (erule_tac x="v" in allE)
apply (rotate_tac 24)
apply (erule_tac x="(η_ren η) ++ [ρself \<mapsto> Suc k]" in allE)
apply (drule mp)
(* eg *)
apply (rule conjI,simp)
(* fv_P1' *)
apply (rule conjI,simp)
(* fvReg_P1 *)
apply (rule conjI)
apply (simp add: dom_fun_upd)
(* E1_P1 *)
apply (rule conjI)
apply (frule SafeDARegion_APP_E1_P2,simp,simp,simp)
(* E2_P2 *)
apply (rule conjI)
apply (frule SafeDARegion_APP_E2_P2,simp,assumption+,simp,assumption,simp)
(* P3 *)
apply (rule conjI)
apply (rule SafeDARegion_APP_P3, assumption)
(* P4 *)
apply (frule_tac xs=xs and ti=ti and as=as and rs=rs and ρs=ρs in SafeDARegion_APP_P4)
apply (simp,assumption+,simp,force,assumption+,simp,simp,simp,assumption+)
apply simp
(* P5 *)
apply (drule consistent_t_consistent_t_ren_inv)
apply (subst mu_ext_ρself_mu_ext,simp)
apply (subst ρself_notin_regions_mu_ren,simp)
apply simp
apply (elim conjE)
apply (frule consistent_t_ren_inv_consistent_t,assumption+)
apply (rule SafeDARegion_APP_P5,assumption+)
(* g = f *)
apply simp
apply (case_tac n)
(* n = 0 *)
apply (simp only: SafeRegionDAssDepth.simps)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (frule P1_f_n_APP,assumption+,simp)
(* case n > 0 *)
apply (unfold SafeRegionDAssDepth.simps)
apply (intro allI, rule impI)
apply (elim conjE)
apply (frule lemma_20)
apply (force,force,simp,simp,simp)
apply (frule_tac ?μ1.0="fst(μ_ren (μ1,μ2))" and
?μ2.0="snd (μ_ren (μ1,μ2))(ρself \<mapsto> ρself)" in Regions_Lemma_5_Depth)
apply (subgoal_tac " (E1, E2) \<turnstile> h , k , AppE f as rr () \<Down> (f, Suc nat) h' , k , v ")
prefer 2 apply simp
apply (frule P1_f_n_ge_0_APP,simp,force)
apply (elim exE,elim conjE)
apply (unfold SafeRegionDAssDepth.simps)
apply (rotate_tac 27)
apply (erule_tac x="(map_of (zip xs (map (atom2val E1) as)))" in allE)
apply (fold SafeRegionDAssDepth.simps)
apply (erule_tac x="(map_of (zip rs (map (the o E2) rr))(self \<mapsto> Suc k))" in allE)
apply (erule_tac x="h" in allE)
apply (rotate_tac 27)
apply (erule_tac x="Suc k" in allE)
apply (rotate_tac 27)
apply (erule_tac x="h'a" in allE)
apply (erule_tac x="v" in allE)
apply (rotate_tac 27)
apply (erule_tac x="(η_ren η) ++ [ρself \<mapsto> Suc k]" in allE)
apply (drule mp)
(* eg *)
apply (rule conjI,simp)
(* fv_P1' *)
apply (rule conjI,simp)
(* fvReg_P1 *)
apply (rule conjI)
apply (simp add: dom_fun_upd)
(* E1_P1 *)
apply (rule conjI)
apply (frule SafeDARegion_APP_E1_P2,simp,simp,simp)
(* E2_P2 *)
apply (rule conjI)
apply (rule SafeDARegion_APP_E2_P2)
apply (simp,assumption+,simp,assumption+)
(* P3 *)
apply (rule conjI)
apply (rule SafeDARegion_APP_P3, assumption)
(* P4 *)
apply (rule_tac xs=xs and ti=ti and as=as and rs=rs and ρs=ρs in SafeDARegion_APP_P4)
apply (simp,simp,assumption+,simp,simp,simp,assumption+,simp,simp,assumption+)
(* P5 *)
apply simp
apply (drule consistent_t_consistent_t_ren_inv)
apply (subst mu_ext_ρself_mu_ext,simp)
apply (subst ρself_notin_regions_mu_ren,simp)
apply simp
apply (frule consistent_t_ren_inv_consistent_t,assumption+)
by (rule SafeDARegion_APP_P5,assumption+)
end
lemma map_add_fst_Some:
[| ϑ r = Some y; dom ϑ ∩ dom ϑ' = {} |] ==> (ϑ ++ ϑ') r = Some y
lemma map_of_zip_is_Some:
length xs = length ys ==> (x ∈ set xs) = (∃y. map_of (zip xs ys) x = Some y)
lemma map_of_zip_twice_is_Some:
[| x ∈ set xs; length xs = length vs; distinct xs; length xs = length zs |]
==> ∃i<length vs.
map_of (zip xs vs) x = Some (vs ! i) ∧
map_of (zip xs zs) x = Some (zs ! i)
lemma dom_map_f_comp:
dom (map_f_comp f g) = dom g
lemma dom_map_comp:
∀x∈dom g. ∃y. f (the (g x)) = Some y ==> dom (f o_m g) = dom g
lemma map_comp_map_of_zip:
[| x ∈ set xs; length xs = length ys; distinct xs;
∀i<length ys. ∃z. m (ys ! i) = Some z |]
==> (m o_m map_of (zip xs ys)) x = map_of (zip xs (map (the o m) ys)) x
lemma map_f_comp_map_of_zip:
[| x ∈ set xs; length xs = length ys; distinct xs |]
==> map_f_comp f (map_of (zip xs ys)) x = map_of (zip xs (map f ys)) x
lemma map_of_zip_is_SomeI:
[| x ∈ set xs; length xs = length vs; distinct xs |]
==> ∃i<length vs. xs ! i = x ∧ map_of (zip xs vs) x = Some (vs ! i)
lemma map_mu_self:
ρself ∉ set ρs ==> map (the o μ2.0(ρself |-> ρself)) ρs = map (the o μ2.0) ρs
lemma map_last:
xs ≠ [] ==> last (map f xs) = f (last xs)
lemma as_in_E1:
[| fvs' as ⊆ dom E1.0; as ! i = VarE x a; i < length as |] ==> x ∈ dom E1.0
lemma rr_in_E2:
set rr ⊆ dom E2.0 ==> ∀i<length rr. ∃n. E2.0 (rr ! i) = Some n
lemma η_η_ren:
[| η x = Some r; x ≠ ρself; ρfake ∉ dom η |] ==> η_ren η x = Some r
lemma SafeDARegionDepth_LitInt:
ConstE (LitN i)
a :f , n \<lbrace> (ϑ1.0,
ϑ2.0) , TypeExpression.ConstrT intType [] [] \<rbrace>
lemma SafeDARegionDepth_LitBool:
ConstE (LitB b)
a :f , n \<lbrace> (ϑ1.0,
ϑ2.0) , TypeExpression.ConstrT boolType [] [] \<rbrace>
lemma SafeDARegionDepth_Var1:
ϑ1.0 x = Some t ==> VarE x a :f , n \<lbrace> (ϑ1.0, ϑ2.0) , t \<rbrace>
lemma ρ_notin_regions_mu_ext_copy_monotone:
(ρ ∉ regions t --> mu_ext (μ1.0, μ2.0(ρ |-> ρ')) t = mu_ext (μ1.0, μ2.0) t) ∧
(ρ ∉ regions' tm -->
mu_exts (μ1.0, μ2.0(ρ |-> ρ')) tm = mu_exts (μ1.0, μ2.0) tm)
lemma map_ρs_equals_butlast_copy:
[| ρs ≠ []; last ρs = ρ; distinct ρs |]
==> map (the o μ2.0(ρ |-> ρ')) ρs = butlast (map (the o μ2.0) ρs) @ [ρ']
lemma copy'_Loc_p:
[| h p = Some (j', C, vn); copy'_dom (j, h, Loc p, True);
h' = fst (mapAccumL (copy' j) h (zip vn (recursiveArgs C)));
p' = getFresh h';
ps' = snd (mapAccumL (copy' j) h (zip vn (recursiveArgs C))) |]
==> copy' j h (Loc p, True) = (h'(p' |-> (j, C, ps')), Loc p')
lemma copy_h'_p':
[| copy (h, k) p j = ((h', k), p'); copy'_dom (j, h, Loc p, True);
h p = Some (j', C, vn) |]
==> h' p' = Some (j, C, snd (mapAccumL (copy' j) h (zip vn (recursiveArgs C))))
lemma snd_mapAccumL_x_xs:
snd (mapAccumL f s (x # xs)) = snd (f s x) # snd (mapAccumL f (fst (f s x)) xs)
lemma length_snd_mapAccumL:
∀s. length (snd (mapAccumL f s xs)) = length xs
lemma mapAccumL_snd_length:
length xs = length ys ==> length (snd (mapAccumL f s ys)) = length xs
lemma length_tn'_equals_length_recursiveArgs:
[| length vn = length tn'; coherentC C;
constructorSignature C = Some (tn', ρ', TypeExpression.ConstrT T tm' ρs') |]
==> length tn' = length (zip vn (recursiveArgs C))
lemma SafeDARegion_Var2_length_equals:
[| length vn = length tn'; coherentC C;
constructorSignature C = Some (tn', ρ', TypeExpression.ConstrT T tm' ρs') |]
==> length (snd (mapAccumL (copy' j) h (zip vn (recursiveArgs C)))) = length tn'
lemma SafeDARegionDepth_Var2:
[| ϑ1.0 x = Some (TypeExpression.ConstrT T ti ρl); ϑ2.0 r = Some ρ';
coherent constructorSignature Tc |]
==> x @ r a :f , n \<lbrace> (ϑ1.0,
ϑ2.0) , TypeExpression.ConstrT T ti
(butlast ρl @ [ρ']) \<rbrace>
lemma case_Recursive:
[| h q = Some (j, C, vn); i < length vn; vn ! i = Loc p;
snd (snd (the (ConstructorTable C))) ! i = Recursive;
length (snd (snd (the (ConstructorTable C)))) = length vn |]
==> (Recursive, Loc p)
∈ {x : set (zip (getArgType (getConstructorCell (C, vn)))
(getValuesCell (C, vn))).
isNonBasicValue (fst x)}
lemma case_NonRecursive:
[| h q = Some (j, C, vn); i < length vn; vn ! i = Loc p;
snd (snd (the (ConstructorTable C))) ! i = NonRecursive;
length (snd (snd (the (ConstructorTable C)))) = length vn |]
==> (NonRecursive, Loc p)
∈ {x : set (zip (getArgType (getConstructorCell (C, vn)))
(getValuesCell (C, vn))).
isNonBasicValue (fst x)}
lemma p_in_closureL_Recursive:
[| h q = Some (j, C, vn); i < length vn; vn ! i = Loc p;
length (snd (snd (the (ConstructorTable C)))) = length vn;
snd (snd (the (ConstructorTable C))) ! i = Recursive |]
==> p ∈ closureL q (h, k)
lemma p_in_closureL_NonRecursive:
[| h q = Some (j, C, vn); i < length vn; vn ! i = Loc p;
length (snd (snd (the (ConstructorTable C)))) = length vn;
snd (snd (the (ConstructorTable C))) ! i = NonRecursive |]
==> p ∈ closureL q (h, k)
lemma closureV_vn_closureV_q:
[| h q = Some (j, C, vn); coherentC C;
constructorSignature C = Some (tn', ρ', TypeExpression.ConstrT T tm' ρs');
length tn' = length vn |]
==> (UN i<length vn. closureV (vn ! i) (h, k)) ⊆ closureV (Loc q) (h, k)
lemma p_notin_closureV_q_notin_closureV_vn:
[| p ∉ closureV (Loc q) (h, k); h q = Some (j, C, vn);
constructorSignature C = Some (tn', ρ', TypeExpression.ConstrT T tm' ρs');
length tn' = length vn; coherentC C |]
==> ∀i<length vn. p ∉ closureV (vn ! i) (h, k)
lemma SafeDARegion_Var3_1:
[| consistent_v t η v h; fresh q h; h p = Some (j, C, vn); v ∈ rangeHeap h;
p ∉ closureV v (h, k); coherent constructorSignature Tc |]
==> consistent_v t η v (h(p := None)(q |-> c))
lemma SafeDARegionDepth_Var3:
[| ϑ1.0 x = Some t; coherent constructorSignature Tc |]
==> ReuseE x a :f , n \<lbrace> (ϑ1.0, ϑ2.0) , t \<rbrace>
lemma SafeDARegion_LET1_P1':
[| (E1.0,
E2.0) \<turnstile> h , k , td , Let x1.0 = e1.0 In e2.0 a \<Down> h' , k , v , r ;
x1.0 ∉ fv e1.0; fv e1.0 ∪ fv e2.0 - {x1.0} ⊆ dom E1.0 |]
==> fv e1.0 ⊆ dom E1.0 ∧ fv e2.0 ⊆ insert x1.0 (dom E1.0)
lemma consistent_v_notin_dom_h':
[| consistent_v t η v h; v ∉ domLoc h';
!!p. p ∈ dom h ==> p ∉ dom h' ∨ h p = h' p |]
==> consistent_v t η v h'
lemma consistent_v_Loc_p_in_dom_h:
[| consistent_v t η (Loc p) h;
(E1.0, E2.0) \<turnstile> h , k , td , e \<Down> h' , k , v , r ;
Loc p ∈ domLoc h; !!p. p ∈ dom h ==> p ∉ dom h' ∨ h p = h' p |]
==> consistent_v t η (Loc p) h'
lemma monotone_consistent_Loc_p:
[| (E1.0, E2.0) \<turnstile> h , k , td , e \<Down> h' , k , v , r ;
ϑ1.0 x = Some t; E1.0 x = Some (Loc p); consistent_v t η (Loc p) h |]
==> consistent_v t η (Loc p) h'
lemma monotone_consistent_v:
[| (E1.0, E2.0) \<turnstile> h , k , td , e \<Down> h' , k , v , r ;
ϑ1.0 x = Some t; E1.0 x = Some v'; consistent_v t η v' h |]
==> consistent_v t η v' h'
lemma monotone_consistent:
[| (E1.0, E2.0) \<turnstile> h , k , td , e \<Down> h' , k , v , r ;
consistent (ϑ1.0, ϑ2.0) η (E1.0, E2.0) h |]
==> consistent (ϑ1.0, ϑ2.0) η (E1.0, E2.0) h'
lemma SafeDARegion_LET1_P5:
[| (E1.0, E2.0) \<turnstile> h , k , td , e1.0 \<Down> h' , k , v1.0 , r ;
x1.0 ∉ dom ϑ1.0; consistent (ϑ1.0, ϑ2.0) η (E1.0, E2.0) h;
consistent_v t1.0 η v1.0 h' |]
==> consistent (ϑ1.0(x1.0 |-> t1.0), ϑ2.0) η (E1.0(x1.0 |-> v1.0), E2.0) h'
lemma SafeDARegionDepth_LET1:
[| ∀C as r a'. e1.0 ≠ ConstrE C as r a'; x1.0 ∉ dom ϑ1.0; x1.0 ∉ fv e1.0;
e1.0 :f , n \<lbrace> (ϑ1.0, ϑ2.0) , t1.0 \<rbrace>;
e2.0 :f , n \<lbrace> (ϑ1.0(x1.0 |-> t1.0), ϑ2.0) , t2.0 \<rbrace> |]
==> Let x1.0 = e1.0 In e2.0 a :f , n \<lbrace> (ϑ1.0, ϑ2.0) , t2.0 \<rbrace>
lemma fvs_prop2:
[| i < length as; as ! i = VarE x a |] ==> x ∈ fvs as
lemma mu_last:
ρs ≠ [] ==> the (μ2.0 (last ρs)) = last (map (the o μ2.0) ρs)
lemma extend_heaps_upd:
fresh p h ==> (h, k) \<sqsubseteq> (h(p |-> (j, C, map (atom2val E1.0) as)), k)
lemma not_in_set_conv_nth:
x ∉ set xs ==> ∀i<length xs. xs ! i ≠ x
lemma consistent_v_fresh_p_Loc_q:
[| consistent_v t η (Loc q) h; Loc q ≠ Loc p; fresh p h |]
==> consistent_v t η (Loc q) (h(p |-> (j, C, map (atom2val E1.0) as)))
lemma monotone_consistent_v_fresh:
[| (E1.0, E2.0) \<turnstile> h , k , td , e \<Down> h' , k , v , r ;
ϑ1.0 x = Some t; E1.0 x = Some v'; fresh p h; consistent_v t η v' h |]
==> consistent_v t η v' (h(p |-> (j, C, map (atom2val E1.0) as)))
lemma SafeDARegion_LETC_P5:
[| (E1.0,
E2.0) \<turnstile> h , k , td , Let x1.0 = ConstrE C as r
() In e2.0 () \<Down> h' , k , v , ra ;
E2.0 r = Some j; x1.0 ∉ fvs as; fvs as ⊆ dom E1.0; x1.0 ∉ dom ϑ1.0;
constructorSignature C = Some (ti, ρ, TypeExpression.ConstrT T tn ρs);
t' = mu_ext (μ1.0, μ2.0) (TypeExpression.ConstrT T tn ρs);
argP (map (mu_ext (μ1.0, μ2.0)) ti) (the (μ2.0 ρ)) as r (ϑ1.0, ϑ2.0);
consistent (ϑ1.0, ϑ2.0) η (E1.0, E2.0) h; fresh p h;
wellT ti ρ (TypeExpression.ConstrT T tn ρs) |]
==> consistent (ϑ1.0(x1.0 |-> t'), ϑ2.0) η (E1.0(x1.0 |-> Loc p), E2.0)
(h(p |-> (j, C, map (atom2val E1.0) as)))
lemma SafeDARegionDepth_LETC:
[| x1.0 ∉ fvs as; x1.0 ∉ dom ϑ1.0; constructorSignature C = Some (ti, ρ, t);
t = TypeExpression.ConstrT T tn ρs; t' = mu_ext (μ1.0, μ2.0) t;
argP (map (mu_ext (μ1.0, μ2.0)) ti) ((the o μ2.0) ρ) as r (ϑ1.0, ϑ2.0);
wellT ti ρ t;
e2.0 :f , n \<lbrace> (ϑ1.0(x1.0 |-> t'), ϑ2.0) , t'' \<rbrace> |]
==> Let x1.0 = ConstrE C as r
a' In e2.0 a :f , n \<lbrace> (ϑ1.0, ϑ2.0) , t'' \<rbrace>
lemma P1_f_n_CASE:
[| E1.0 x = Some (Loc p);
(E1.0,
E2.0) \<turnstile> h , k , Case VarE x
a Of alts a' \<Down> (f,
n) hh , k , v |]
==> ∃j C vs.
h p = Some (j, C, vs) ∧
(∃i<length alts.
((extend E1.0 (snd (extractP (fst (alts ! i)))) vs,
E2.0) \<turnstile> h , k , snd
(alts ! i) \<Down> (f, n) hh , k , v ∧
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs) ∧
(∃pati ei ps ms. alts ! i = (pati, ei) ∧ pati = ConstrP C ps ms))
lemma fvTup_subseteq_fvAlts:
∀i<length alts. fvTup (alts ! i) ⊆ fvAlts alts
lemma SafeRegion_CASE_fv_P1':
[| 0 < length alts; fv (Case VarE x a Of alts a') ⊆ dom E1.0; i < length alts;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> fv (snd (alts ! i)) ⊆ dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs)
lemma SafeRegion_CASEL_LitN_fv_P1':
[| 0 < length alts; fv (Case VarE x a Of alts a') ⊆ dom E1.0; i < length alts;
fst (alts ! i) = ConstP (LitN n) |]
==> fv (snd (alts ! i)) ⊆ dom E1.0
lemma SafeRegion_CASEL_LitB_fv_P1':
[| 0 < length alts; fv (Case VarE x a Of alts a') ⊆ dom E1.0; i < length alts;
fst (alts ! i) = ConstP (LitB b) |]
==> fv (snd (alts ! i)) ⊆ dom E1.0
lemma SafeRegion_CASE_fvReg_P1':
[| fvReg (Case VarE x a Of alts a') ⊆ dom E2.0; i < length alts |]
==> fvReg (snd (alts ! i)) ⊆ dom E2.0
lemma SafeRegion_CASE_E1_P2:
[| dom E1.0 ⊆ dom ϑ1.0; i < length alts;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = TypeExpression.ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) =
ϑ1.0 ++
map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti)) ∧
dom ϑ1.0 ∩
dom (map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti))) =
{} ∧
ϑ1.0 x = Some (mu_ext μ t) ∧ snd (assert ! i) = ϑ2.0;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs;
∀i<length alts. x ∉ set (snd (extractP (fst (alts ! i)))) |]
==> dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs)
⊆ dom (fst (assert ! i))
lemma SafeRegion_CASEL_E1_P2:
[| dom E1.0 ⊆ dom ϑ1.0; i < length alts;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = TypeExpression.ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) =
ϑ1.0 ++
map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti)) ∧
dom ϑ1.0 ∩
dom (map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti))) =
{} ∧
ϑ1.0 x = Some (mu_ext μ t) ∧ snd (assert ! i) = ϑ2.0;
∀i<length alts. x ∉ set (snd (extractP (fst (alts ! i)))) |]
==> dom E1.0 ⊆ dom (fst (assert ! i))
lemma in_set_conv_nth_2:
x ∈ set xs ==> ∃i<length xs. xs ! i = x
lemma x_in_variables_same_μ:
(x ∈ variables t ∧ mu_ext μ' t = mu_ext μ t -->
the (fst μ x) = the (fst μ' x)) ∧
(x ∈ variables' tm ∧ mu_exts μ' tm = mu_exts μ tm -->
the (fst μ x) = the (fst μ' x))
lemma x_in_regions_same_μ:
(x ∈ regions t ∪ set ρs ∧
(∀x∈set ρs. the (snd μ' x) = the (snd μ x)) ∧ mu_ext μ' t = mu_ext μ t -->
the (snd μ x) = the (snd μ' x)) ∧
(x ∈ regions' tm ∪ set ρs ∧
(∀x∈set ρs. the (snd μ' x) = the (snd μ x)) ∧ mu_exts μ' tm = mu_exts μ tm -->
the (snd μ x) = the (snd μ' x))
lemma regions_variables_same_μ:
(regions t ⊆ regions' tm' ∪ set ρs ∧
(∀x∈set ρs. the (snd μ' x) = the (snd μ x)) ∧
variables t ⊆ variables' tm' ∧ mu_exts μ' tm' = mu_exts μ tm' -->
mu_ext μ t = mu_ext μ' t) ∧
(regions' tm ⊆ regions' tm' ∪ set ρs ∧
(∀x∈set ρs. the (snd μ' x) = the (snd μ x)) ∧
variables' tm ⊆ variables' tm' ∧ mu_exts μ' tm' = mu_exts μ tm' -->
mu_exts μ tm = mu_exts μ' tm)
lemma same_μ:
[| constructorSignature C = Some (tn, ρ, TypeExpression.ConstrT T tm ρs);
wellT tn ρ (TypeExpression.ConstrT T tm ρs);
mu_ext μ (TypeExpression.ConstrT T tm ρs) = t';
mu_ext μ' (TypeExpression.ConstrT T tm ρs) = t' |]
==> map (mu_ext μ) tn = map (mu_ext μ') tn
lemma SafeRegion_f_n_CASE_P4:
[| length assert = length alts; 0 < length alts;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = TypeExpression.ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) =
ϑ1.0 ++
map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti)) ∧
dom ϑ1.0 ∩
dom (map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti))) =
{} ∧
ϑ1.0 x = Some (mu_ext μ t) ∧ snd (assert ! i) = ϑ2.0;
consistent (ϑ1.0, ϑ2.0) η (E1.0, E2.0) h; E1.0 x = Some (Loc p);
h p = Some (j, C, vs); i < length alts;
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs,
E2.0) \<turnstile> h , k , snd (alts ! i) \<Down> (f, n) h' , k , v ;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs; alts ! i = (pati, ei);
pati = ConstrP C ps ms |]
==> consistent (fst (assert ! i), snd (assert ! i)) η
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) h
lemma SafeRegion_CASEL_LitB_P4:
[| length assert = length alts; 0 < length alts;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = TypeExpression.ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) =
ϑ1.0 ++
map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti)) ∧
dom ϑ1.0 ∩
dom (map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti))) =
{} ∧
ϑ1.0 x = Some (mu_ext μ t) ∧ snd (assert ! i) = ϑ2.0;
consistent (ϑ1.0, ϑ2.0) η (E1.0, E2.0) h; E1.0 x = Some (BoolT b);
i < length alts; fst (alts ! i) = ConstP (LitB b) |]
==> consistent (fst (assert ! i), snd (assert ! i)) η (E1.0, E2.0) h
lemma SafeRegion_CASEL_LitN_P4:
[| length assert = length alts; 0 < length alts;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = TypeExpression.ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) =
ϑ1.0 ++
map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti)) ∧
dom ϑ1.0 ∩
dom (map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti))) =
{} ∧
ϑ1.0 x = Some (mu_ext μ t) ∧ snd (assert ! i) = ϑ2.0;
consistent (ϑ1.0, ϑ2.0) η (E1.0, E2.0) h; E1.0 x = Some (IntT n);
i < length alts; fst (alts ! i) = ConstP (LitN n) |]
==> consistent (fst (assert ! i), snd (assert ! i)) η (E1.0, E2.0) h
lemma SafeDARegionDepth_CASE:
[| length assert = length alts; 0 < length alts;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = TypeExpression.ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) =
ϑ1.0 ++
map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti)) ∧
dom ϑ1.0 ∩
dom (map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti))) =
{} ∧
ϑ1.0 x = Some (mu_ext μ t) ∧ snd (assert ! i) = ϑ2.0;
∀i<length alts.
snd (alts !
i) :f , n \<lbrace> (fst (assert ! i),
snd (assert ! i)) , t' \<rbrace>;
∀i<length alts. x ∉ set (snd (extractP (fst (alts ! i)))) |]
==> Case VarE x a Of alts a' :f , n \<lbrace> (ϑ1.0, ϑ2.0) , t' \<rbrace>
lemma SafeRegion_f_n_CASED_P1:
(E1.0,
E2.0) \<turnstile> h , k , CaseD VarE x
a Of alts a \<Down> (f, n) h' , k , v
==> ∃p j C vs.
E1.0 x = Some (Loc p) ∧
h p = Some (j, C, vs) ∧
(∃i<length alts.
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs,
E2.0) \<turnstile> h
(p := None) , k , snd (alts ! i) \<Down> (f, n) h' , k , v ∧
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs ∧
(∃pati ei ps ms. alts ! i = (pati, ei) ∧ pati = ConstrP C ps ms))
lemma fvTup'_subseteq_fvAlts':
i < length alts ==> fvTup' (alts ! i) ⊆ fvAlts' alts
lemma SafeRegion_CASED_fv_P1':
[| 0 < length alts; fv (CaseD VarE x a Of alts a') ⊆ dom E1.0; i < length alts;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> fv (snd (alts ! i)) ⊆ dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs)
lemma SafeRegion_CASED_fvReg_P1':
[| fvReg (CaseD VarE x a Of alts a') ⊆ dom E2.0; i < length alts |]
==> fvReg (snd (alts ! i)) ⊆ dom E2.0
lemma consistent_v_p_none:
[| consistent_v t η v h; p ∉ closureV v (h, k);
coherent constructorSignature Tc |]
==> consistent_v t η v (h(p := None))
lemma consistent_v_p_none_x_in_dom_E1:
consistent_v t η v h ==> consistent_v t η v (h(p := None))
lemma SafeRegion_f_n_CASED_P4:
[| length assert = length alts; 0 < length alts;
coherent constructorSignature Tc;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = TypeExpression.ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) =
ϑ1.0 ++
map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti)) ∧
dom ϑ1.0 ∩
dom (map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti))) =
{} ∧
ϑ1.0 x = Some (mu_ext μ t) ∧ snd (assert ! i) = ϑ2.0;
consistent (ϑ1.0, ϑ2.0) η (E1.0, E2.0) h; E1.0 x = Some (Loc p);
h p = Some (j, C, vs); i < length alts;
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) \<turnstile> h
(p := None) , k , snd (alts ! i) \<Down> (f, n) h' , k , v ;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs; alts ! i = (pati, ei);
pati = ConstrP C ps ms |]
==> consistent (fst (assert ! i), snd (assert ! i)) η
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h(p := None))
lemma SafeDARegionDepth_CASED:
[| length assert = length alts; 0 < length alts;
coherent constructorSignature Tc;
∀i<length alts.
constructorSignature (fst (extractP (fst (alts ! i)))) = Some (ti, ρ, t) ∧
t = TypeExpression.ConstrT T tn ρs ∧
length (snd (extractP (fst (alts ! i)))) = length ti ∧
wellT ti ρ t ∧
fst (assert ! i) =
ϑ1.0 ++
map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti)) ∧
dom ϑ1.0 ∩
dom (map_of (zip (snd (extractP (fst (alts ! i)))) (map (mu_ext μ) ti))) =
{} ∧
ϑ1.0 x = Some (mu_ext μ t) ∧ snd (assert ! i) = ϑ2.0;
∀i<length alts.
snd (alts !
i) :f , n \<lbrace> (fst (assert ! i),
snd (assert ! i)) , t' \<rbrace>;
∀i<length alts. x ∉ set (snd (extractP (fst (alts ! i)))) |]
==> CaseD VarE x a Of alts a' :f , n \<lbrace> (ϑ1.0, ϑ2.0) , t' \<rbrace>
lemma SafeDARegion_APP_E1_P2:
[| length xs = length as; length xs = length ti; distinct xs |]
==> dom (map_of (zip xs (map (atom2val E1.0) as)))
⊆ dom (map_f_comp
(mu_ext
(fst (μ_ren (μ1.0, μ2.0)), snd (μ_ren (μ1.0, μ2.0))(ρself |->
ρself)))
(map_of (zip xs ti)))
lemma SafeDARegion_APP_E2_P2:
[| ∀i<length ρs. ∃t. μ2.0 (ρs ! i) = Some t; distinct rs; length rs = length rr;
length rs = length ρs; μ_ren_dom (μ1.0, μ2.0) |]
==> dom (map_of (zip rs (map (the o E2.0) rr))(self |-> Suc k))
⊆ dom (snd (μ_ren (μ1.0, μ2.0))(ρself |-> ρself) o_m map_of (zip rs ρs)
(self |-> ρself))
lemma SafeDARegion_APP_P3:
admissible η k ==> admissible (η_ren η ++ [ρself |-> Suc k]) (Suc k)
lemma μ_ren_extend_ρself:
(ρself ∉ regions t -->
mu_ext
(λx. Some (t_ren (the (μ1.0 x))), (λρ. Some (ρ_ren (the (μ2.0 ρ))))(ρself |->
ρself))
t =
mu_ext (λx. Some (t_ren (the (μ1.0 x))), λρ. Some (ρ_ren (the (μ2.0 ρ)))) t) ∧
(ρself ∉ regions' ts -->
mu_exts
(λx. Some (t_ren (the (μ1.0 x))), (λρ. Some (ρ_ren (the (μ2.0 ρ))))(ρself |->
ρself))
ts =
mu_exts (λx. Some (t_ren (the (μ1.0 x))), λρ. Some (ρ_ren (the (μ2.0 ρ)))) ts)
lemma map_ρ_ren:
ρself ∉ set xs ==> xs = map ρ_ren xs
lemma t_equals_t_ren:
(ρself ∉ regions t ∧ ρself ∉ variables t --> t = t_ren t) ∧
(ρself ∉ regions' tm ∧ ρself ∉ variables' tm --> tm = t_rens tm)
lemma ρ_equals_ρ_ren:
[| ρself ∉ (the o μ2.0) ` set ρs; ρ ∈ set ρs |]
==> the (μ2.0 ρ) = ρ_ren (the (μ2.0 ρ))
lemma μ_ren_extend_t_ren:
(ρself ∉ regions (mu_ext (μ1.0, μ2.0) t) ∧
ρself ∉ variables (mu_ext (μ1.0, μ2.0) t) -->
mu_ext (μ1.0, μ2.0) t =
mu_ext (λx. Some (t_ren (the (μ1.0 x))), λρ. Some (ρ_ren (the (μ2.0 ρ)))) t) ∧
(ρself ∉ regions' (mu_exts (μ1.0, μ2.0) ts) ∧
ρself ∉ variables' (mu_exts (μ1.0, μ2.0) ts) -->
mu_exts (μ1.0, μ2.0) ts =
mu_exts (λx. Some (t_ren (the (μ1.0 x))), λρ. Some (ρ_ren (the (μ2.0 ρ)))) ts)
lemma mu_ext_args_xs:
[| distinct xs; length xs = length ti; length as = length ti; x ∈ set xs;
dom (map_of (zip xs (map (atom2val E1.0) as))) = set xs;
mu_ext (μ1.0, μ2.0) (ti ! i) = t; i < length as; ρself ∉ regions t;
ρself ∉ variables t; ρself ∉ regions (ti ! i); xs ! i = x |]
==> map_f_comp
(mu_ext
(λx. Some (t_ren (the (μ1.0 x))), (λρ. Some (ρ_ren (the (μ2.0 ρ))))
(ρself |-> ρself)))
(map_of (zip xs ti)) x =
Some t
lemma map_comp_map_of_zip_μ:
[| distinct rs; length ρs = length rr; length rs = length rr; rs ! i = r;
rs ! i ≠ self; ∀i<length ρs. ∃t. snd (μ_ren (μ1.0, μ2.0)) (ρs ! i) = Some t;
ρself ∉ set ρs; i < length rr;
(rs ! i, n) ∈ set (zip rs (map (the o E2.0) rr)) |]
==> (snd (μ_ren (μ1.0, μ2.0))(ρself |-> ρself) o_m map_of (zip rs ρs)(self |->
ρself))
r =
Some (the (snd (μ_ren (μ1.0, μ2.0)) (ρs ! i)))
lemma consistent_η_ren_ρs:
[| i < length ρs; η (the (μ2.0 (ρs ! i))) = Some n; ρfake ∉ dom η;
ρfake ∉ ran μ2.0; μ_ren_dom (μ1.0, μ2.0);
∀i<length ρs. ∃t. μ2.0 (ρs ! i) = Some t |]
==> (η_ren η ++ [ρself |-> Suc k]) (the (snd (μ_ren (μ1.0, μ2.0)) (ρs ! i))) =
Some n
lemma t_ren_mu_ext:
t_ren (mu_ext (μ1.0, μ2.0) t) =
mu_ext (λx. Some (t_ren (the (μ1.0 x))), λa. Some (ρ_ren (the (μ2.0 a)))) t ∧
t_rens (mu_exts (μ1.0, μ2.0) ts) =
mu_exts (λx. Some (t_ren (the (μ1.0 x))), λa. Some (ρ_ren (the (μ2.0 a)))) ts
lemma mu_exts_ren:
[| mu_exts (μ1.0, μ2.0) tm' = tm; map (the o μ2.0) ρs' = ρs |]
==> mu_exts (λx. Some (t_ren (the (μ1.0 x))), λa. Some (ρ_ren (the (μ2.0 a))))
tm' =
t_rens tm ∧
map (the o (λa. Some (ρ_ren (the (μ2.0 a))))) ρs' = map ρ_ren ρs
lemma η_ren_ρ_ren_ρl_SomeI:
[| ρl = last ρs; last ρs ∈ dom η; η (last ρs) = Some j;
η' = η_ren η(ρself |-> Suc k); ρs ≠ []; ρfake ∉ dom η |]
==> (η_ren η(ρself |-> Suc k)) (ρ_ren (last ρs)) = Some j
lemma last_map_not_ρself:
[| ρself ∉ (the o μ2.0) ` set ρs'; ρs' ≠ [] |]
==> last (map (the o μ2.0) ρs') ≠ ρself
lemma length_ρs:
[| 0 < length ρs';
(the (μ2.0 ρ'), mu_ext (μ1.0, μ2.0) (TypeExpression.ConstrT T tm' ρs')) =
(ρl, TypeExpression.ConstrT T tm ρs) |]
==> ρs ≠ []
lemma consistent_t_consistent_t_ren:
[| consistent_v t η v h; ρfake ∉ dom η; η' = η_ren η(ρself |-> Suc k) |]
==> consistent_v (t_ren t) η' v h
lemma mu_ext_args_xs_ti:
[| distinct xs; length xs = length ti; length as = length ti; x ∈ set xs;
dom (map_of (zip xs (map (atom2val E1.0) as))) = set xs;
mu_ext (μ1.0, μ2.0) (ti ! i) = t; i < length as; ρself ∉ regions (ti ! i);
xs ! i = x |]
==> map_f_comp
(mu_ext
(λx. Some (t_ren (the (μ1.0 x))), (λρ. Some (ρ_ren (the (μ2.0 ρ))))
(ρself |-> ρself)))
(map_of (zip xs ti)) x =
Some (mu_ext
(λx. Some (t_ren (the (μ1.0 x))), λρ. Some (ρ_ren (the (μ2.0 ρ))))
(ti ! i))
lemma SafeDARegion_APP_P4:
[| distinct xs; length xs = length ti; length xs = length as; distinct rs;
length rs = length rr; length rs = length ρs;
ρself ∉ regions tg ∪ Union (set (map regions ti)) ∪ set ρs;
∀i<length ρs. ∃t. μ2.0 (ρs ! i) = Some t; ρfake ∉ ran μ2.0;
μ_ren_dom (μ1.0, μ2.0); set rr ⊆ dom E2.0; fvs' as ⊆ dom E1.0;
consistent (ϑ1.0, ϑ2.0) η (E1.0, E2.0) h;
argP_app (map (mu_ext (μ1.0, μ2.0)) ti) (map (the o μ2.0) ρs) as rr
(ϑ1.0, ϑ2.0) |]
==> consistent
(map_f_comp
(mu_ext
(fst (μ_ren (μ1.0, μ2.0)), snd (μ_ren (μ1.0, μ2.0))(ρself |-> ρself)))
(map_of (zip xs ti)),
snd (μ_ren (μ1.0, μ2.0))(ρself |-> ρself) o_m map_of (zip rs ρs)(self |->
ρself))
(η_ren η ++ [ρself |-> Suc k])
(map_of (zip xs (map (atom2val E1.0) as)),
map_of (zip rs (map (the o E2.0) rr))(self |-> Suc k))
h
lemma regions_induct_t_var:
(x ∈ regions (the (fst μ ρ)) ∧ ρ ∈ variables t --> x ∈ regions (mu_ext μ t)) ∧
(x ∈ regions (the (fst μ ρ)) ∧ ρ ∈ variables' tm -->
x ∈ regions' (mu_exts μ tm))
lemma regions_induct_constr_ρ:
(ρ ∈ regions t --> the (snd μ ρ) ∈ regions (mu_ext μ t)) ∧
(ρ ∈ regions' tm --> the (snd μ ρ) ∈ regions' (mu_exts μ tm))
lemma regions_induct_constr_ρs:
set ρs ⊆ regions t' ==> (the o snd μ) ` set ρs ⊆ regions (mu_ext μ t')
lemma regions_regions_mu_ext:
(regions t ⊆ regions t' ∧ variables t ⊆ variables t' -->
regions (mu_ext μ t) ⊆ regions (mu_ext μ t')) ∧
(regions' tm ⊆ regions t' ∧ variables' tm ⊆ variables t' -->
regions' (mu_exts μ tm) ⊆ regions (mu_ext μ t'))
lemma wellT_regions:
[| wellT tn' (last ρs') (TypeExpression.ConstrT T tm' ρs');
mu_ext (μ1.0, μ2.0) (TypeExpression.ConstrT T tm' ρs') =
TypeExpression.ConstrT T tm ρs;
ρself ∉ regions (TypeExpression.ConstrT T tm ρs) |]
==> ∀i<length tn'. ρself ∉ regions (map (mu_ext (μ1.0, μ2.0)) tn' ! i)
lemma last_notin_set:
[| ρs ≠ []; ρ ∉ set ρs |] ==> last ρs ≠ ρ
lemma η_ρ_ren_inv_ρ_Some_j:
[| (η_ren η(ρself |-> Suc k)) ρ = Some j; ρfake ∉ dom η; ρ ≠ ρself |]
==> η (ρ_ren_inv ρ) = Some j
lemma t_ren_in_mu_ext_inv:
t_ren_inv (mu_ext (μ1.0, μ2.0) t) =
mu_ext
(λx. Some (t_ren_inv (the (μ1.0 x))), λa. Some (ρ_ren_inv (the (μ2.0 a)))) t ∧
t_ren_invs (mu_exts (μ1.0, μ2.0) ts) =
mu_exts
(λx. Some (t_ren_inv (the (μ1.0 x))), λa. Some (ρ_ren_inv (the (μ2.0 a)))) ts
lemma mu_exts_ren_inv:
[| mu_exts (μ1.0, μ2.0) tm' = tm; map (the o μ2.0) ρs' = ρs |]
==> mu_exts
(λx. Some (t_ren_inv (the (μ1.0 x))), λa. Some (ρ_ren_inv (the (μ2.0 a))))
tm' =
t_ren_invs tm ∧
map (the o (λa. Some (ρ_ren_inv (the (μ2.0 a))))) ρs' = map ρ_ren_inv ρs
lemma consistent_t_consistent_t_ren_inv:
[| consistent_v t' η' v h_e; ρself ∉ regions t';
η' = η_ren η(ρself |-> Suc k) |]
==> consistent_v (t_ren_inv t') η v h_e
lemma mu_ext_ρself_mu_ext:
(ρself ∉ regions t -->
mu_ext (μ1.0, μ2.0(ρself |-> ρself)) t = mu_ext (μ1.0, μ2.0) t) ∧
(ρself ∉ regions' tm -->
mu_exts (μ1.0, μ2.0(ρself |-> ρself)) tm = mu_exts (μ1.0, μ2.0) tm)
lemma ρself_notin_regions_t_ren:
ρself ∉ regions (t_ren t) ∧ ρself ∉ regions' (t_rens tm)
lemma ρself_notin_regions_mu_ren:
ρself
∉ regions
(mu_ext (λx. Some (t_ren (the (μ1.0 x))), λa. Some (ρ_ren (the (μ2.0 a))))
t) ∧
ρself
∉ regions'
(mu_exts (λx. Some (t_ren (the (μ1.0 x))), λρ. Some (ρ_ren (the (μ2.0 ρ))))
tm)
lemma t_ren_inv_t_ren:
(notFake t --> t_ren_inv (t_ren t) = t) ∧
(notFakes tm --> t_ren_invs (t_rens tm) = tm)
lemma mu_ext_def_ConstrT:
mu_ext_def (μ1.0, μ2.0) (TypeExpression.ConstrT T tm ρs)
==> mu_exts_def (μ1.0, μ2.0) tm
lemma mu_ext_def_ρs:
mu_ext_def (μ1.0, μ2.0) (TypeExpression.ConstrT T tm ρs)
==> map ρ_ren_inv (map (the o (λρ. Some (ρ_ren (the (μ2.0 ρ))))) ρs) =
map (the o μ2.0) ρs
lemma t_ren_inv_t_ren_t:
(mu_ext_def (μ1.0, μ2.0) t -->
t_ren_inv
(mu_ext (λx. Some (t_ren (the (μ1.0 x))), λρ. Some (ρ_ren (the (μ2.0 ρ))))
t) =
mu_ext (μ1.0, μ2.0) t) ∧
(mu_exts_def (μ1.0, μ2.0) tm -->
t_ren_invs
(mu_exts (λx. Some (t_ren (the (μ1.0 x))), λρ. Some (ρ_ren (the (μ2.0 ρ))))
tm) =
mu_exts (μ1.0, μ2.0) tm)
lemma consistent_t_ren_inv_consistent_t:
[| ρself ∉ regions tg; mu_ext_def (μ1.0, μ2.0) tg;
consistent_v
(t_ren_inv
(mu_ext
(λx. Some (t_ren (the (μ1.0 x))), (λρ. Some (ρ_ren (the (μ2.0 ρ))))
(ρself |-> ρself))
tg))
η v h_e |]
==> consistent_v (mu_ext (μ1.0, μ2.0) tg) η v h_e
lemma restricted_h_equals_h:
[| h p = Some (j, C, vn); j < Suc k |]
==> (h |` {p : dom h. fst (the (h p)) ≤ k}) p = h p
lemma j_le_Suc_k:
[| η ρl = Some j; admissible η k |] ==> j < Suc k
lemma SafeDARegion_APP_P5:
[| consistent_v t η v h_e; admissible η k |]
==> consistent_v t η v (h_e |` {p : dom h_e. fst (the (h_e p)) ≤ k})
lemma lemma_19_aux:
[| \<Turnstile> Σt ; Σt g = Some (ti, ρs, tg); Σf g = Some (xs, rs, eg) |]
==> bodyAPP Σf
g : \<lbrace> (map_of (zip (varsAPP Σf g) (typesArgAPP Σt g)),
map_of (zip (regionsAPP Σf g) (regionsArgAPP Σt g)) ++
[self |-> ρself]) , typeResAPP Σt g \<rbrace>
lemma equiv_SafeRegionDAss_all_n_SafeRegionDAssDepth:
e : \<lbrace> ϑ , t \<rbrace> ==> ∀n. e :f , n \<lbrace> ϑ , t \<rbrace>
lemma lemma_19:
[| \<Turnstile>f , n Σt ; Σf g = Some (xs, rs, eg); Σt g = Some (ti, ρs, tg);
g ≠ f; ϑ1.0 = map_of (zip xs ti);
ϑ2.0 = map_of (zip rs ρs) ++ [self |-> ρself] |]
==> eg :f , n \<lbrace> (ϑ1.0, ϑ2.0) , tg \<rbrace>
lemma lemma_20:
[| \<Turnstile>f , n Σt ; Σf f = Some (xs, rs, ef); Σt f = Some (ti, ρs, tf);
ϑ1.0 = map_of (zip xs ti); ϑ2.0 = map_of (zip rs ρs) ++ [self |-> ρself];
n = Suc n' |]
==> ef :f , n' \<lbrace> (ϑ1.0, ϑ2.0) , tf \<rbrace>
lemma SafeDARegionDepth_APP:
[| Σt g = Some (ti, ρs, tg); primops g = None;
ρself ∉ regions tg ∪ Union (set (map regions ti)) ∪ set ρs;
length as = length ti; length ρs = length rr;
∀i<length ρs. ∃t. μ2.0 (ρs ! i) = Some t; ρfake ∉ ran μ2.0;
μ_ren_dom (μ1.0, μ2.0); t = mu_ext (μ1.0, μ2.0) tg;
mu_ext_def (μ1.0, μ2.0) tg; Σf g = Some (xs, rs, e); fv e ⊆ set xs;
fvReg e ⊆ set rs ∪ {self};
argP_app (map (mu_ext (μ1.0, μ2.0)) ti) (map (the o μ2.0) ρs) as rr
(ϑ1.0, ϑ2.0);
\<Turnstile>f , n Σt |]
==> AppE g as rr a :f , n \<lbrace> (ϑ1.0, ϑ2.0) , t \<rbrace>