Up to index of Isabelle/HOL/CoreSafe
theory SafeDAss_P7
(* Title: Safe DAss P7
Author: Javier de Dios and Ricardo Peņa
Copyright: March 2008, Universidad Complutense de Madrid
*)
header {* Derived Assertions. P7. S L, $\Gamma$,E,h $\cap$ R L, $\Gamma$,E,h = {} *}
theory SafeDAss_P7 imports SafeDAssBasic
BasicFacts
begin
text{*
Lemmas for LET1 Rule
*}
(***************************************** LET1 ************************************************)
lemma P7_e1_dem1:
"[|S1 = S1s ∪ S1r ∪ S1d; S1s ⊆ S; R1 ⊆ R; (S1r ∪ S1d) ∩ R1 = {}; S ∩ R = {}|]
==> S1 ∩ R1 = {}"
apply blast
done
(* S = S1s ∪ S1d ∪ S1r *)
lemma P7_e1_dem2:
"SSet L1 Γ1 E h = SSet1 L1 Γ1 (pp Γ1 Γ2 L2) s'' E h ∪
SSet1 L1 Γ1 (pp Γ1 Γ2 L2) d'' E h ∪
SSet1 L1 Γ1 (pp Γ1 Γ2 L2) r'' E h"
apply (rule equalityI)
(* S ⊆ S1s ∪ S1d ∪ S1r *)
apply (simp add: SSet_def add: Let_def add: SSet1_def,clarsimp)
apply (simp add: pp_def, simp add: dom_def add: safe_def)
apply (rule_tac x="xa" in exI,clarsimp)
apply (erule_tac x="xa" in allE,clarsimp)+
apply (case_tac "y",simp_all)
(* S = S1s ∪ S1d ∪ S1r *)
apply (simp add: SSet_def, simp add: Let_def, simp add: SSet1_def)
by blast
(* S1s ⊆ S *)
lemma P7_e1_dem3 :
"SSet1 L1 Γ1 (pp Γ1 Γ2 L2) s'' E h ⊆ SSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) E h"
apply (simp add: SSet_def, simp add: Let_def, simp add: SSet1_def)
by blast
lemma P7_e1_dem5 :
"[|dom Γ1 ⊆ dom E1|] ==>
((SSet1 L1 Γ1 (pp Γ1 Γ2 L2) d'' (E1,E2) (h,k)) ∪
(SSet1 L1 Γ1 (pp Γ1 Γ2 L2) r'' (E1,E2) (h,k))) ∩ RSet L1 Γ1 (E1,E2) (h,k) ≠ {}
--> (∃x z. x ∈ dom E1 ∧ z ∈ L1 ∧ Γ1 z = Some d'' ∧ Γ1 x = Some s'' ∧
closure (E1,E2) x (h,k) ∩ recReach (E1,E2) z (h,k) ≠ {})"
apply (simp add: SSet1_def add: RSet_def, auto)
apply (erule_tac x="xa" in allE)
apply (erule impE, assumption+)
apply (subgoal_tac "[|dom Γ1 ⊆ dom E1; Γ1 xa = Some s''|] ==> xa ∈ dom E1",clarsimp)
apply (erule_tac x="z" in allE)
apply (erule impE,assumption)+
apply (frule closure_transit,assumption,blast)
apply blast
apply (erule_tac x="xa" in allE)
apply (erule impE, assumption+)
apply (subgoal_tac "[|dom Γ1 ⊆ dom E1; Γ1 xa = Some s''|] ==> xa ∈ dom E1",clarsimp)
apply (erule_tac x="z" in allE)
apply (erule impE,assumption+,simp)
apply (frule closure_transit,assumption,blast)
by blast
lemma P7_e1_dem6 :
"[|shareRec L1 Γ1 (E1,E2) (h,k) (h',k');
dom Γ1 ⊆ dom E1;
((SSet1 L1 Γ1 (pp Γ1 Γ2 L2) d'' (E1,E2) (h,k)) ∪
(SSet1 L1 Γ1 (pp Γ1 Γ2 L2) r'' (E1,E2) (h,k))) ∩ RSet L1 Γ1 (E1,E2) (h,k) ≠ {}
--> (∃x z. x ∈ dom E1 ∧ z ∈ L1 ∧ Γ1 z = Some d'' ∧ Γ1 x = Some s'' ∧
closure (E1,E2) x (h,k) ∩ recReach (E1,E2) z (h,k) ≠ {})|]
==> (SSet1 L1 Γ1 (pp Γ1 Γ2 L2) d'' (E1,E2) (h,k) ∪
SSet1 L1 Γ1 (pp Γ1 Γ2 L2) r'' (E1,E2) (h,k)) ∩ RSet L1 Γ1 (E1,E2) (h,k) = {}"
apply (simp add: shareRec_def add: SSet1_def add: RSet_def)
by blast
lemma P7_e1_dem4_1:
"[|Γ1 x = Some d''|] ==> (pp Γ1 Γ2 L2) x = Some d''"
by (simp add: pp_def add: safe_def add: dom_def)
lemma P7_e1_dem4_2:
"[|xa ∈ live E L1 h|] ==> xa ∈ live E (L1 ∪ (L2 - {x1})) h"
by (simp add: live_def add: closureLS_def)
(* R1 ⊆ R *)
lemma P7_e1_dem4 :
" SSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1, E2) (h, k) ∩
RSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1,E2) (h, k) = {} ==>
RSet L1 Γ1 (E1, E2) (h, k) ⊆ RSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1, E2) (h, k) "
apply (simp add: RSet_def,safe)
apply (erule P7_e1_dem4_2)
apply (rule_tac x="z" in bexI)
apply (rule conjI)
apply (erule P7_e1_dem4_1)
apply blast
by blast
(* S ∩ R ==> S1 ∩ R1 *)
lemma P7_LET_e1:
"[| shareRec L1 Γ1 (E1,E2) (h,k) (h',k');
dom Γ1 ⊆ dom E1;
SSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1,E2) (h,k) ∩
RSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1,E2) (h,k) = {}|]
==> SSet L1 Γ1 (E1,E2) (h,k) ∩ RSet L1 Γ1 (E1,E2) (h,k) = {}"
apply (rule P7_e1_dem1)
apply (rule P7_e1_dem2)
apply (rule P7_e1_dem3)
apply (rule P7_e1_dem4, assumption+)
apply (erule P7_e1_dem6, assumption)
by (erule P7_e1_dem5, assumption)
(* DEMOSTRACION DE P7 PARA e2 de LET1 *)
lemma P7_e2_dem1 :
"[|(x1 ∉ L2 --> S2 ⊆ S);
(x1 ∈ L2 --> S2 = S2' ∪ S2'x1 ∧ S2' ⊆ S ∧ S2'x1 ∩ R2 = {});
R2 ⊆ R;
S ∩ R = {}|]
==> S2 ∩ R2 = {}"
by blast
(* x1 ∉ L2 --> S2 ⊆ S *)
lemma demS2_2_x1_not_L2:
"[|dom Γ1 ⊆ dom E1;
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''));
dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) ⊆ dom (E1(x1 \<mapsto> v1));
def_pp Γ1 Γ2 L2;
x1 ∉ L1;
shareRec L1 Γ1 (E1, E2) (h, k) (h',k')|]
==> x1∉L2 --> SSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) (E1(x1 \<mapsto> r),E2) (h', k') ⊆
SSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1, E2) (h, k)"
apply (rule impI)
apply (simp add: SSet_def, clarsimp)
apply (simp add: Let_def)
apply (erule exE, rename_tac y)
apply (rule_tac x="y" in exI,elim conjE)
apply (case_tac "y ≠ x1",clarsimp)
apply (subgoal_tac "(Γ2 + [x1 \<mapsto> s'']) y = Some s'' ==> Γ2 y = Some s''",clarsimp)
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="y" in ballE)+
prefer 2 apply blast
prefer 2 apply blast
apply (frule safe_Gamma2_triangle,assumption+)
apply (case_tac "¬ identityClosure (E1, E2) y (h, k) (h', k')",simp)
apply simp
apply (simp add: identityClosure_def) apply (elim conjE)
apply (rule conjI)
apply (erule safe_triangle,assumption+)
apply (subgoal_tac " y≠x1 ==> closure (E1, E2) y (h', k') = closure (E1(x1 \<mapsto> r), E2) y (h', k')",simp)
apply (simp add: closure_def)
apply (simp add: disjointUnionEnv_def add: unionEnv_def)
apply (split split_if_asm, simp)
apply simp
apply simp
done
(* x1 ∈ L2 --> S2 = S2' ∪ S2'x1 *)
lemma P7_e2_dem2_1:
"[| def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''));
x1∈L2 |]
==> SSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) (E1(x1 \<mapsto> r),E2) (h', k') =
SSet (L2-{x1}) Γ2 (E1(x1 \<mapsto> r),E2) (h', k') ∪
SSet {x1} (empty(x1 \<mapsto> s'')) (E1(x1 \<mapsto> r),E2) (h', k')"
apply (rule equalityI)
apply (rule subsetI)
apply (simp add: SSet_def add: Let_def)
apply (erule exE)
apply (case_tac "xa=x1",simp)
apply (rule disjI1, erule conjE)
apply (subgoal_tac "(Γ2 + [x1 \<mapsto> s'']) xa = Some s'' ==> Γ2 xa = Some s''",simp)
apply (rule_tac x="xa" in exI,simp)
apply (simp add: disjointUnionEnv_def add: unionEnv_def)
apply (split split_if_asm, simp)
apply simp
apply (rule subsetI)
apply (erule UnE)
apply (simp add: SSet_def add: Let_def)
apply (erule exE)
apply (subgoal_tac "Γ2 xa = Some s'' ==> (Γ2 + [x1 \<mapsto> s'']) xa = Some s''",simp)
apply (rule_tac x="xa" in exI,simp)
apply (simp add: disjointUnionEnv_def add: unionEnv_def add: dom_def)
apply (simp add: SSet_def add: Let_def)
apply (rule_tac x="x1" in exI)
apply (rule conjI,simp)
apply (rule conjI)
apply (simp add: def_disjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def)
by simp
(* x1 ∈ L2 --> S2' ⊆ S *)
lemma demS2_1_1b:
"[|dom Γ1 ⊆ dom E1;
L2 ⊆ dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s'')));
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''));
dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) ⊆ dom (E1(x1 \<mapsto> v1));
def_pp Γ1 Γ2 L2;
x1 ∉ L1; x1∈ L2;
shareRec L1 Γ1 (E1, E2) (h, k) (h',k')|]
==> SSet (L2-{x1}) Γ2 (E1(x1 \<mapsto> r),E2) (h', k') ⊆
SSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1, E2) (h, k)"
apply (simp add: SSet_def, clarsimp)
apply (simp add: Let_def)
apply (erule_tac exE, rename_tac y)
apply (rule_tac x="y" in exI)
apply (case_tac "y ≠ x1",simp)
apply (elim conjE)
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="y" in ballE)+
prefer 2 apply blast
prefer 2 apply blast
apply (frule safe_Gamma2_triangle,assumption+)
apply (case_tac "¬ identityClosure (E1, E2) y (h, k) (h', k')",simp)
apply simp
apply (simp add: identityClosure_def) apply (elim conjE)
apply (rule conjI)
apply (erule safe_triangle,assumption+)
apply (subgoal_tac " y≠x1 ==> closure (E1, E2) y (h', k') = closure (E1(x1 \<mapsto> r), E2) y (h', k')",simp)
apply (simp add: closure_def)
by blast
(* (x1 ∈ L2 --> S2'x1 ∩ R2 = {} *)
lemma demS2_S2x1_subset_R2_aux:
"[| closureL x (h', k') ∩ recReach (E1(x1 \<mapsto> r), E2) z (h', k') ≠ {};
x ∈ closure (E1(x1 \<mapsto> r), E2) x1 (h', k')|] ==>
closure (E1(x1 \<mapsto> r), E2) x1 (h', k') ∩ recReach (E1(x1 \<mapsto> r), E2) z (h', k') ≠ {}"
apply (simp add: closure_def)
apply (case_tac "r",auto)
apply (frule closureL_transit, assumption+)
by blast
lemma demS2_S2x1_subset_R2:
"[|dom Γ1 ⊆ dom E1;
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''));
dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) ⊆ dom (E1(x1 \<mapsto> v1));
def_pp Γ1 Γ2 L2;
x1 ∉ L1; x1 ∈ L2;
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) (E1(x1 \<mapsto> r), E2) (h', k') (hh,kk) |]
==> SSet {x1} (empty(x1 \<mapsto> s'')) (E1(x1 \<mapsto> r),E2) (h', k') ∩
RSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) (E1(x1 \<mapsto> r),E2) (h', k') = {}"
apply (simp add: SSet_def, auto)
apply (simp add: RSet_def)
apply (erule conjE, erule bexE, erule conjE)
apply (unfold shareRec_def)
apply (elim conjE)
apply (erule_tac x="x1" in ballE) prefer 2 apply simp
apply (erule_tac x="x1" in ballE) prefer 2 apply simp
apply (erule_tac x="z" in ballE)
apply (drule_tac P="(Γ2 + [x1 \<mapsto> s'']) z = Some d'' ∧
closure (E1(x1 \<mapsto> r), E2) x1 (h', k') ∩ recReach (E1(x1 \<mapsto> r), E2) z (h', k') ≠ {}" in mp)
apply (rule conjI,simp)
apply (frule demS2_S2x1_subset_R2_aux,assumption+)
apply (erule conjE)
apply (simp add: def_disjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def)
apply simp
done
lemma demS2_2_x1_in_L2:
" [|dom Γ1 ⊆ dom E1;
x1 ∉ L1;
L2 ⊆ dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s'')));
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''));
dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) ⊆ dom (E1(x1 \<mapsto> v1));
def_pp Γ1 Γ2 L2;
shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) (E1(x1 \<mapsto> r), E2) (h', k') (hh,kk);
SSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1, E2) (h, k) ∩
RSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1, E2) (h, k) = {}|]
==> x1 ∈ L2 --> SSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) (E1(x1 \<mapsto> r), E2) (h', k') = ?S2' ∪ ?S2'x1.0 ∧
?S2' ⊆ SSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1, E2) (h, k) ∧
?S2'x1.0 ∩ RSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) (E1(x1 \<mapsto> r), E2) (h', k') = {}"
apply (rule impI, rule conjI)
apply (rule P7_e2_dem2_1,assumption+)
apply (rule conjI)
apply (rule demS2_1_1b,assumption+)
by (rule demS2_S2x1_subset_R2,assumption+)
lemma demR2_subseteq_R :
"[| def_pp Γ1 Γ2 L2; L1 ⊆ dom Γ1;
L2 ⊆ dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s'')));
dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) ⊆ dom (E1(x1 \<mapsto> v1));
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''));
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) (E1(x1 \<mapsto> r), E2) (h', k') (hh,kk);
shareRec L1 Γ1 (E1, E2) (h, k) (h',k')|]
==> RSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) (E1(x1 \<mapsto> r),E2) (h', k') ⊆
RSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1,E2) (h, k)"
apply (rule subsetI, rename_tac p)
apply (simp add: RSet_def)
apply (erule conjE, erule bexE, rename_tac x)
apply (case_tac "x=x1")
apply simp
apply (elim conjE)
apply (simp add: disjointUnionEnv_def add: unionEnv_def add: def_disjointUnionEnv_def)
apply (erule conjE)
apply (subgoal_tac "p ∈ live (E1(x1 \<mapsto> r), E2) L2 (h', k')
==> ∃y∈L2. p ∈ closure (E1(x1 \<mapsto> r), E2) y (h', k')",simp)
prefer 2 apply (simp add: live_def add: closureLS_def)
apply (erule bexE)
apply (unfold shareRec_def)
apply (elim conjE)
apply (erule_tac x="y" and A ="dom (fst (E1(x1 \<mapsto> r), E2))" in ballE)+
prefer 2 apply simp apply (elim conjE) apply blast
apply (erule_tac x="x" and A="L2" in ballE) prefer 2 apply simp
prefer 2 apply simp apply (elim conjE) apply blast
apply (drule_tac P="(Γ2 + [x1 \<mapsto> s'']) x = Some d'' ∧ closure (E1(x1 \<mapsto> r), E2) y (h', k') ∩ recReach (E1(x1 \<mapsto> r), E2) x (h', k') ≠ {}"
in mp)
apply (rule conjI)
apply simp
apply (rule closure_recReach_monotone, assumption+)
apply simp
apply (elim conjE)
apply (rule conjI)
apply (case_tac "y = x1")
apply (simp add: def_disjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def)
apply (subgoal_tac "[| (Γ2 + [x1 \<mapsto> s'']) y ≠ Some s''; y ≠ x1 |] ==> Γ2 y ≠ Some s''",simp)
prefer 2 apply (rule unsafe_Gamma2_triangle, assumption+)
apply (frule_tac y="y" in unsafe_Gamma2_identityClosure) apply assumption+
apply (simp add: identityClosure_def) apply (elim conjE)
apply (subgoal_tac "[|y ≠ x1; y ∈ L2|] ==> closure (E1,E2) y (h, k) ⊆ live (E1, E2) (L1 ∪ (L2 - {x1})) (h, k)",simp)
prefer 2 apply (rule closure_subset_live, assumption+)
apply (subgoal_tac " y≠x1 ==> closure (E1, E2) y (h', k') = closure (E1(x1 \<mapsto> r), E2) y (h', k')",simp)
prefer 2 apply (simp add: closure_def)
apply (rule closure_live_monotone, assumption+)
(* Otra condicion *)
apply (case_tac "y=x1")
apply (simp add: def_disjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def)
apply (rule_tac x="x" in bexI)
apply (rule conjI)
apply (subgoal_tac "[| def_pp Γ1 Γ2 L2; (Γ2 + [x1 \<mapsto> s'']) x = Some d''|] ==> (pp Γ1 Γ2 L2) x = Some d''")
prefer 2 apply (rule condemned_Gamma2_triangle,assumption+)
prefer 2 apply simp
apply (subgoal_tac "[| (Γ2 + [x1 \<mapsto> s'']) y ≠ Some s''; y ≠ x1 |] ==> Γ2 y ≠ Some s''",simp)
prefer 2 apply (rule unsafe_Gamma2_triangle, assumption+)
apply (subgoal_tac "(Γ2 + [x1 \<mapsto> s'']) x ≠ Some s''") prefer 2 apply simp
apply (frule_tac y="y" in unsafe_Gamma2_triangle, assumption+)
apply (frule_tac y="y" in unsafe_Gamma2_identityClosure) apply assumption+
apply (subgoal_tac "[| def_pp Γ1 Γ2 L2; (Γ2 + [x1 \<mapsto> s'']) x = Some d''|] ==> (pp Γ1 Γ2 L2) x = Some d''")
prefer 2 apply (rule condemned_Gamma2_triangle,assumption+)
apply simp
apply (subgoal_tac "(pp Γ1 Γ2 L2) x = Some d'' ==> Γ2 x ≠ Some s''",simp)
apply (frule_tac y="x" in unsafe_Gamma2_identityClosure) apply assumption+
apply (frule_tac x="x" in identityClosure_equals_recReach)
apply (subgoal_tac " y ≠ x1 ==> closure (E1(x1 \<mapsto> r), E2) y (h', k') = closure (E1, E2) y (h', k')",simp)
prefer 2 apply (simp add: closure_def)
apply (subgoal_tac "p ∈ closure (E1, E2) y (h', k') ==> p ∈ closure (E1, E2) y (h, k)",simp)
apply (frule_tac x="y" in identityClosure_closureL_monotone,simp)
apply (simp add: identityClosure_def add: identityClosureL_def, elim conjE)
apply (subgoal_tac " x ≠ x1 ==> recReach (E1(x1 \<mapsto> r), E2) x (h', k') = recReach (E1, E2) x (h', k')",simp)
apply (simp add: recReach_def)
apply (simp add: identityClosure_def)
apply (rule unsafe_triangle_unsafe_2) apply assumption+
done
lemma P7_LET1_e2:
"[| def_pp Γ1 Γ2 L2; L1 ⊆ dom Γ1;
dom Γ1 ⊆ dom E1;
L2 ⊆ dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s'')));
x1 ∉ L1;
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''));
dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) ⊆ dom (E1(x1 \<mapsto> v1)) ;
shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) (E1(x1 \<mapsto> v1), E2) (h', k') (hh,kk);
SSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1, E2) (h, k) ∩
RSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1,E2) (h, k) = {}|]
==> SSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) (E1(x1 \<mapsto> v1),E2) (h', k') ∩
RSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> s''))) (E1(x1 \<mapsto> v1),E2) (h', k') = {}"
apply (rule P7_e2_dem1)
apply (rule demS2_2_x1_not_L2,assumption+)
apply (rule demS2_2_x1_in_L2,assumption+)
by (rule demR2_subseteq_R,assumption+)
text{*
Lemmas for LET2 Rule
*}
(***************************************** LET2 ************************************************)
lemma P7_e2_let2_dem1 :
"[|(x1∈L2 --> R2 = R2'x1 ∪ R2d ∧ R2'x1 ∩ S2 = {} ∧ R2d ∩ S2 = {});
(x1∉L2 --> R2 ⊆ R);
S2 ⊆ S;
S ∩ R = {}|]
==> S2 ∩ R2 = {}"
by blast
(* R2 = R2d ∪ R2'x1 *)
lemma P7_e2_let2_dem2:
"[| def_disjointUnionEnv Γ2 [x1 \<mapsto> d'']; x1 ∈ L2|]
==>
RSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) (E1(x1 \<mapsto> v1),E2) (h', k') =
{p ∈ live (E1(x1 \<mapsto> v1),E2) L2 (h', k'). closureL p (h', k') ∩ recReach (E1(x1 \<mapsto> v1),E2) x1 (h', k') ≠ {}} ∪
{p ∈ live (E1(x1 \<mapsto> v1),E2) L2 (h', k'). ∃z∈ (L2-{x1}). Γ2 z = Some d'' ∧
closureL p (h', k') ∩ recReach (E1(x1 \<mapsto> v1),E2) z (h', k') ≠ {}}"
apply (rule equalityI)
(* R2 ⊆ R2x1 ∪ R2d ∪ R2'x1b *)
apply (rule subsetI)
apply simp
apply (simp only: RSet_def)
apply simp
apply (rule impI)
apply (elim conjE)
apply clarsimp
apply (rule_tac x="z" in bexI)
apply (rule conjI)
apply (case_tac "z=x1")
apply simp
apply (frule disjointUnionEnv_d_Gamma2_d) apply assumption+
apply (case_tac "z=x1")
apply simp
apply simp
(* R2x1 ∪ R2d ∪ R2'x1b ⊆ R2 *)
apply (rule subsetI)
apply (simp only: RSet_def)
apply (elim UnE)
apply simp
apply (rule_tac x="x1" in bexI)
apply simp
apply (rule def_disjointUnionEnv_monotone) apply assumption+
apply simp
apply (erule conjE)
apply (erule bexE)
apply (rule_tac x="z" in bexI) prefer 2 apply simp
apply (elim conjE)
apply (rule conjI) apply (rule Gamma2_d_disjointUnionEnv_d, assumption+)
done
(* R2x1 ∩ S2 = {} *)
lemma P7_e2_let2_dem4:
"[| dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) ⊆ dom (E1(x1 \<mapsto> v1));
def_disjointUnionEnv Γ2 [x1 \<mapsto> d''];
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) (E1(x1 \<mapsto> v1), E2) (h', k') (hh,kk);
x1∈L2 |]
==> {p ∈ live (E1(x1 \<mapsto> v1),E2) L2 (h', k'). closureL p (h', k') ∩ recReach (E1(x1 \<mapsto> v1),E2) x1 (h', k') ≠ {}} ∩
SSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) (E1(x1 \<mapsto> v1),E2) (h', k') = {}"
apply auto
apply (simp add: live_def add: closureLS_def) apply (rename_tac p)
apply (erule bexE, rename_tac z)
apply (simp add: SSet_def)
apply (simp add: Let_def)
apply (erule exE)
apply (elim conjE)
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="xa" in ballE)
apply (drule_tac Q=" xa ∈ dom (Γ2 + [x1 \<mapsto> d'']) ∧ (Γ2 + [x1 \<mapsto> d'']) xa ≠ Some s''" in mp)
apply (rule_tac x="x1" in bexI)
apply (rule conjI)
apply (rule def_disjointUnionEnv_monotone) apply assumption+
apply (subgoal_tac " closureL x (h', k') ∩ recReach (E1(x1 \<mapsto> v1), E2) x1 (h', k') ≠ {}") prefer 2 apply blast
apply (rule closure_recReach_monotone) apply assumption+
apply (elim conjE) apply simp
apply (subgoal_tac "[| dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) ⊆ dom (E1(x1 \<mapsto> v1));
(Γ2 + [x1 \<mapsto> d'']) xa = Some s''|] ==> xa ∈ dom E1")
apply simp
apply (rule dom_disjointUnionEnv_subset_dom_extend) apply assumption+
done
(* x1∈ L2 --> R2d ∩ S2 = {} *)
lemma P7_e2_let2_dem10:
" [| dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) ⊆ dom (E1(x1 \<mapsto> v1));
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) (E1(x1 \<mapsto> v1), E2) (h', k') (hh,kk);
def_disjointUnionEnv Γ2 [x1 \<mapsto> d'']; x1∈L2 |]
==> {p ∈ live (E1(x1 \<mapsto> v1),E2) L2 (h', k'). ∃z∈ (L2-{x1}). Γ2 z = Some d'' ∧
closureL p (h', k') ∩ recReach (E1(x1 \<mapsto> v1),E2) z (h', k') ≠ {}} ∩
SSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) (E1(x1 \<mapsto> v1),E2) (h', k') = {}"
apply auto
apply (rename_tac y)
apply (simp add: SSet_def)
apply (simp add: Let_def)
apply (erule exE)
apply (elim conjE)
apply (simp add: live_def add: closureLS_def)
apply (erule bexE)
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="xa" in ballE)
apply (drule_tac Q=" xa ∈ dom (Γ2 + [x1 \<mapsto> d'']) ∧ (Γ2 + [x1 \<mapsto> d'']) xa ≠ Some s''" in mp)
apply (rule_tac x="z" in bexI)
apply (rule conjI)
apply (rule Gamma2_d_disjointUnionEnv_d) apply assumption+
apply (rule closure_recReach_monotone) apply assumption+
apply blast
apply simp
apply (elim conjE) apply simp
apply (subgoal_tac "[| dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) ⊆ dom (E1(x1 \<mapsto> v1));
(Γ2 + [x1 \<mapsto> d'']) xa = Some s''|] ==> xa ∈ dom E1")
apply simp
apply (rule dom_disjointUnionEnv_subset_dom_extend) apply assumption+
done
(* S2 ⊆ S *)
lemma P7_e2_let2_dem7:
"[|def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''));
dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) ⊆ dom (E1(x1 \<mapsto> v1)) ;
shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
def_pp Γ1 Γ2 L2|] ==>
SSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) (E1(x1 \<mapsto> v1),E2) (h', k') ⊆
SSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1, E2) (h, k)"
apply (simp add: SSet_def, clarsimp)
apply (simp add: Let_def)
apply (erule exE, rename_tac y)
apply (rule_tac x="y" in exI,elim conjE)
apply (case_tac "y ≠ x1",clarsimp)
apply (subgoal_tac "(Γ2 + [x1 \<mapsto> d'']) y = Some s'' ==> Γ2 y = Some s''",clarsimp)
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="y" in ballE)+
prefer 2 apply blast
prefer 2 apply blast
apply (frule safe_Gamma2_triangle,assumption+)
apply (case_tac "¬ identityClosure (E1, E2) y (h, k) (h', k')",simp)
apply simp
apply (simp add: identityClosure_def) apply (elim conjE)
apply (rule conjI)
apply (erule safe_triangle,assumption+)
apply (subgoal_tac " y≠x1 ==> closure (E1, E2) y (h', k') = closure (E1(x1 \<mapsto> r), E2) y (h', k')",simp)
apply (simp add: closure_def)
apply (simp add: disjointUnionEnv_def add: unionEnv_def)
apply (split split_if_asm, simp)
apply (simp add: closure_def)
apply (simp add: closure_def)
apply (simp add: disjointUnionEnv_def add: unionEnv_def)
apply (split split_if_asm, simp,simp,simp)
by (simp add: disjointUnionEnv_def add: unionEnv_def add: def_disjointUnionEnv_def)
lemma P7_e2_let2_dem8:
"[| def_pp Γ1 Γ2 L2; L1 ⊆ dom Γ1;
L2 ⊆ dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d'')));
dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) ⊆ dom (E1(x1 \<mapsto> v1));
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''));
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) (E1(x1 \<mapsto> r), E2) (h', k') (hh,kk);
shareRec L1 Γ1 (E1, E2) (h, k) (h',k'); x1∉ L2|]
==> RSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) (E1(x1 \<mapsto> r),E2) (h', k') ⊆
RSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1,E2) (h, k)"
apply (rule subsetI, rename_tac p)
apply (simp add: RSet_def)
apply (erule conjE, erule bexE, rename_tac x)
apply (subgoal_tac "p ∈ live (E1(x1 \<mapsto> r), E2) L2 (h', k')
==> ∃y∈L2. p ∈ closure (E1(x1 \<mapsto> r), E2) y (h', k')",simp)
prefer 2 apply (simp add: live_def add: closureLS_def)
apply (erule bexE)
apply (unfold shareRec_def)
apply (elim conjE)
apply (erule_tac x="y" and A ="dom (fst (E1(x1 \<mapsto> r), E2))" in ballE)+
prefer 2 apply simp apply (elim conjE) apply blast
apply (erule_tac x="x" and A="L2" in ballE) prefer 2 apply simp
prefer 2 apply simp apply (elim conjE) apply blast
apply (drule_tac P="(Γ2 + [x1 \<mapsto> d'']) x = Some d'' ∧ closure (E1(x1 \<mapsto> r), E2) y (h', k') ∩ recReach (E1(x1 \<mapsto> r), E2) x (h', k') ≠ {}"
in mp)
apply (rule conjI)
apply simp
apply (rule closure_recReach_monotone, assumption+)
apply simp
apply (elim conjE)
apply (rule conjI)
apply (case_tac "y≠x1")
apply (subgoal_tac "[| (Γ2 + [x1 \<mapsto> d'']) y ≠ Some s'' |] ==> Γ2 y ≠ Some s''")
prefer 2 apply (rule unsafe_Gamma2_triangle, assumption+)
apply (frule_tac y="y" in unsafe_Gamma2_identityClosure) apply assumption+
apply (simp add: identityClosure_def) apply (elim conjE)
apply (subgoal_tac "[|y ≠ x1; y ∈ L2|] ==> closure (E1,E2) y (h, k) ⊆ live (E1, E2) (L1 ∪ (L2 - {x1})) (h, k)",simp)
prefer 2 apply (rule closure_subset_live, assumption+)
apply (subgoal_tac " y≠x1 ==> closure (E1, E2) y (h', k') = closure (E1(x1 \<mapsto> r), E2) y (h', k')",simp)
prefer 2 apply (simp add: closure_def)
apply blast
apply simp
(* Otra condicion *)
apply (case_tac "y=x1")
apply (simp add: def_disjointUnionEnv_def add: disjointUnionEnv_def add: unionEnv_def)
apply (rule_tac x="x" in bexI) prefer 2 apply simp
apply (rule conjI)
apply (case_tac "x=x1") apply simp
apply (subgoal_tac "[|x≠x1; def_pp Γ1 Γ2 L2; (Γ2 + [x1 \<mapsto> d'']) x = Some d''|] ==> (pp Γ1 Γ2 L2) x = Some d''")
prefer 2 apply (rule disjounitUnionEnv_d_triangle_d, assumption+)
apply (subgoal_tac "[| (Γ2 + [x1 \<mapsto> d'']) y ≠ Some s''; y ≠ x1 |] ==> Γ2 y ≠ Some s''",simp)
prefer 2 apply (rule unsafe_Gamma2_triangle, assumption+)
apply (subgoal_tac "(Γ2 + [x1 \<mapsto> d'']) x ≠ Some s''") prefer 2 apply simp
apply (frule_tac y="y" in unsafe_Gamma2_triangle, assumption+)
apply (frule_tac y="y" in unsafe_Gamma2_identityClosure) apply assumption+
apply (subgoal_tac "[| x≠x1; def_pp Γ1 Γ2 L2; (Γ2 + [x1 \<mapsto> d'']) x = Some d''|] ==> (pp Γ1 Γ2 L2) x = Some d''")
prefer 2 apply (rule disjounitUnionEnv_d_triangle_d,assumption+)
apply (case_tac "x=x1") apply simp
apply simp
apply (subgoal_tac "(pp Γ1 Γ2 L2) x = Some d'' ==> Γ2 x ≠ Some s''")
apply (frule_tac y="x" in unsafe_Gamma2_identityClosure) apply assumption+
apply (frule_tac x="x" in identityClosure_equals_recReach)
apply (subgoal_tac " y ≠ x1 ==> closure (E1(x1 \<mapsto> r), E2) y (h', k') = closure (E1, E2) y (h', k')",simp)
prefer 2 apply (simp add: closure_def)
apply (subgoal_tac "p ∈ closure (E1, E2) y (h', k') ==> p ∈ closure (E1, E2) y (h, k)",simp)
apply (frule_tac x="y" in identityClosure_closureL_monotone,simp)
apply (simp add: identityClosure_def add: identityClosureL_def, elim conjE)
apply (subgoal_tac " x ≠ x1 ==> recReach (E1(x1 \<mapsto> r), E2) x (h', k') = recReach (E1, E2) x (h', k')",simp)
apply (simp add: recReach_def)
apply (simp add: identityClosure_def)
apply (rule unsafe_triangle_unsafe_2) apply assumption+
done
lemma P7_LET2_e2:
"[| def_pp Γ1 Γ2 L2; L1 ⊆ dom Γ1;
dom Γ1 ⊆ dom E1;
L2 ⊆ dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d'')));
x1 ∉ L1;
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''));
dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) ⊆ dom (E1(x1 \<mapsto> v1)) ;
shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) (E1(x1 \<mapsto> v1), E2) (h', k') (hh,kk);
SSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1, E2) (h, k) ∩
RSet (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1,E2) (h, k) = {}|]
==> SSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) (E1(x1 \<mapsto> v1),E2) (h', k') ∩
RSet L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> d''))) (E1(x1 \<mapsto> v1),E2) (h', k') = {}"
apply (rule P7_e2_let2_dem1)
apply (rule impI) apply (rule conjI)
apply (rule P7_e2_let2_dem2, assumption+)
apply (rule conjI) apply (rule P7_e2_let2_dem4) apply assumption+
apply (rule P7_e2_let2_dem10) apply assumption+
apply (rule impI)
apply (rule P7_e2_let2_dem8) apply assumption+
apply (rule P7_e2_let2_dem7) apply assumption+
done
text{*
Lemmas for CASE Rule
*}
(***************************************** CASE ************************************************)
lemma dom_foldl_monotone_list:
" dom (foldl op ⊗ (empty ⊗ x) xs) =
dom x ∪ dom (foldl op ⊗ empty xs)"
apply (subgoal_tac "empty ⊗ x = x ⊗ empty",simp)
apply (subgoal_tac "foldl op ⊗ (x ⊗ empty) xs =
x ⊗ foldl op ⊗ empty xs",simp)
apply (rule union_dom_nonDisjointUnionEnv)
apply (rule foldl_prop1)
apply (subgoal_tac "def_nonDisjointUnionEnv empty x")
apply (erule nonDisjointUnionEnv_conmutative)
by (simp add: def_nonDisjointUnionEnv_def)
lemma dom_restrict_neg_map:
"dom (restrict_neg_map m A) = dom m - (dom m ∩ A)"
apply (simp add: restrict_neg_map_def)
apply auto
by (split split_if_asm,simp_all)
lemma x_notin_Γ_cased:
"x ∉ dom (foldl op ⊗ empty
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert))))"
apply (induct_tac assert alts rule: list_induct2',simp_all)
apply (subgoal_tac
" dom (foldl op ⊗ (empty ⊗ restrict_neg_map (snd xa) (insert x (set (snd (extractP (fst y))))))
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li))) (zip (map (λa. snd (extractP (fst a))) ys) (map snd xs)))) =
dom (restrict_neg_map (snd xa) (insert x (set (snd (extractP (fst y)))))) ∪
dom (foldl op ⊗ empty (map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (λa. snd (extractP (fst a))) ys) (map snd xs))))",simp)
apply (subst dom_restrict_neg_map,blast)
by (rule dom_foldl_monotone_list)
lemma Γ_case_x_is_d:
"[| Γ = foldl op ⊗ empty
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li))) (zip (map (snd o extractP o fst) alts) (map snd assert))) +
[x \<mapsto> d''] |]
==> Γ x = Some d''"
apply (simp add: disjointUnionEnv_def)
apply (simp add: unionEnv_def)
apply (rule impI)
apply (insert x_notin_Γ_cased)
by force
lemma restrict_neg_map_m:
"[| G y = Some m; x≠ y ; y ∉ L|]
==> restrict_neg_map G (insert x L) y = Some m"
by (simp add: restrict_neg_map_def)
lemma disjointUnionEnv_G_G'_G_x:
"[| x ∉ dom G'; def_disjointUnionEnv G G' |]
==> (G + G') x = G x"
apply (simp add: disjointUnionEnv_def)
apply (simp add: unionEnv_def)
apply (simp add: def_disjointUnionEnv_def)
by force
lemma dom_Γi_in_Γcased_2 [rule_format]:
"length assert > 0
--> x ≠ y
--> length assert = length alts
--> (∀ i < length alts. y ∈ dom (snd (assert ! i))
--> y ∉ set (snd (extractP (fst (alts ! i))))
--> y ∈ dom (foldl op ⊗ empty
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert)))))"
apply (induct assert alts rule:list_induct2',simp_all)
apply (rule impI)+
apply (case_tac "xs = []",simp)
apply (rule impI)+
apply (subst empty_nonDisjointUnionEnv)
apply (subst dom_restrict_neg_map)
apply force
apply simp
apply (rule allI, rule impI)
apply (case_tac i,simp_all)
apply (rule impI)+
apply (subst dom_foldl_monotone_list)
apply (subst dom_restrict_neg_map)
apply force
apply (rule impI)
apply (erule_tac x="nat" in allE,simp)
apply (rule impI)+
apply (subst dom_foldl_monotone_list)
by blast
declare def_nonDisjointUnionEnvList.simps [simp del]
lemma Otimes_prop4 [rule_format]:
"length assert > 0
--> y ≠ x
--> length assert = length alts
--> def_nonDisjointUnionEnvList (map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert)))
--> def_disjointUnionEnv
(foldl op ⊗ empty
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
[x \<mapsto> d'']
--> (∀ i < length alts. y ∈ dom (snd (assert ! i))
--> snd (assert ! i) y = Some m
--> y ∉ set (snd (extractP (fst (alts ! i))))
--> (foldl op ⊗ empty
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert))) +
[x \<mapsto> d'']) y = Some m)"
apply (induct assert alts rule:list_induct2',simp_all)
apply (rule impI)+
apply (case_tac "xs = []",simp)
apply (rule impI)
apply (subst empty_nonDisjointUnionEnv)
apply (simp add: disjointUnionEnv_def)
apply (simp add: unionEnv_def)
apply (rule conjI)
apply (rule impI)+
apply (simp add: restrict_neg_map_def)
apply (rule impI)+
apply (simp add: restrict_neg_map_def)
apply force
apply simp
apply (drule mp)
apply (simp add: def_nonDisjointUnionEnvList.simps)
apply (simp add: Let_def)
apply (drule mp)
apply (simp add: def_disjointUnionEnv_def)
apply (subst (asm) dom_foldl_monotone_list)
apply blast
apply (rule allI, rule impI)
apply (subgoal_tac "x≠y")
prefer 2 apply simp
apply (erule thin_rl)
apply (case_tac i,simp_all)
apply (rule impI)+
apply (subst disjointUnionEnv_G_G'_G_x,force,force)
apply (subst nonDisjointUnionEnv_conmutative)
apply (simp add: def_nonDisjointUnionEnv_def)
apply (subst foldl_prop1)
apply (subst nonDisjointUnionEnv_prop6_1)
apply (subst dom_restrict_neg_map,force)
apply (rule restrict_neg_map_m,assumption+,simp)
apply (rule impI)+
apply (rotate_tac 5)
apply (erule_tac x="nat" in allE,simp)
apply (subst disjointUnionEnv_G_G'_G_x,force,simp)
apply (subst nonDisjointUnionEnv_conmutative)
apply (simp add: def_nonDisjointUnionEnv_def)
apply (subst foldl_prop1)
apply (subst (asm) disjointUnionEnv_G_G'_G_x,force)
apply (simp add: def_disjointUnionEnv_def)
apply (subst (asm) dom_foldl_monotone_list)
apply blast
apply (subst nonDisjointUnionEnv_prop6_2)
apply (simp add: def_nonDisjointUnionEnvList.simps)
apply (simp add: Let_def)
apply (subgoal_tac
"y ∈ dom (foldl op ⊗ empty
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) ys) (map snd xs))))",simp)
apply (rule dom_Γi_in_Γcased_2)
by (force,assumption+,simp)
(* Lemas auxiliares closures *)
lemma closureL_p_None_p:
"closureL p (h(p := None), k) = {p}"
apply (rule equalityI)
apply (rule subsetI)
apply (erule closureL.induct,simp)
apply (simp add: descendants_def)
apply (rule subsetI,simp)
by (rule closureL_basic)
lemma recReachL_p_None_p:
"recReachL p (h(p := None), k) = {p}"
apply (rule equalityI)
apply (rule subsetI)
apply (erule recReachL.induct,simp)
apply (simp add: recDescendants_def)
apply (rule subsetI,simp)
by (rule recReachL_basic)
lemma closure_extend_p_None_subseteq_closure:
"[| E1 x = Some (Loc p);
E1 x = (extend E1 (snd (extractP (fst (alts ! i)))) vs) x |]
==> closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h(p := None), k) ⊆
closure (E1, E2) x (h, k)"
apply (simp add: closure_def)
apply (subst closureL_p_None_p,simp)
by (rule closureL_basic)
lemma recReach_extend_p_None_subseteq_recReach:
"[| E1 x = Some (Loc p);
E1 x = (extend E1 (snd (extractP (fst (alts ! i)))) vs) x |]
==> recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h(p := None), k) ⊆
recReach (E1, E2) x (h, k)"
apply (simp add: recReach_def)
apply (subst recReachL_p_None_p,simp)
by (rule recReachL_basic)
lemma descendants_p_None_q:
"[| d ∈ descendants q (h(p:=None),k); q≠p |]
==> d ∈ descendants q (h,k)"
by (simp add: descendants_def)
lemma recDescendants_p_None_q:
"[| d ∈ recDescendants q (h(p:=None),k); q≠p |]
==> d ∈ recDescendants q (h,k)"
by (simp add: recDescendants_def)
lemma closureL_p_None_subseteq_closureL:
"p ≠ q
==> closureL q (h(p := None), k) ⊆ closureL q (h, k)"
apply (rule subsetI)
apply (erule closureL.induct)
apply (rule closureL_basic)
apply clarsimp
apply (subgoal_tac "d ∈ descendants qa (h,k)")
apply (rule closureL_step,simp,simp)
apply (rule descendants_p_None_q,assumption+)
apply (simp add: descendants_def)
by (case_tac "qa = p",simp_all)
lemma recReachL_p_None_subseteq_recReachL:
"p ≠ q
==> recReachL q (h(p := None), k) ⊆ recReachL q (h, k)"
apply (rule subsetI)
apply (erule recReachL.induct)
apply (rule recReachL_basic)
apply clarsimp
apply (subgoal_tac "d ∈ recDescendants qa (h,k)")
apply (rule recReachL_step,simp,simp)
apply (rule recDescendants_p_None_q,assumption+)
apply (simp add: recDescendants_def)
by (case_tac "qa = p",simp_all)
lemma closure_p_None_subseteq_closure:
"[| E1 x = Some (Loc p);
E1 y = Some (Loc q);
p≠q;
E1 y = (extend E1 (snd (extractP (fst (alts ! i)))) vs) y;
w ∈ closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) y (h(p := None), k) |]
==> w ∈ closure (E1, E2) y (h, k)"
apply (simp add: closure_def)
apply (case_tac
"extend E1 (snd (extractP (fst (alts ! i)))) vs y",simp_all)
apply (case_tac a, simp_all)
apply (frule closureL_p_None_subseteq_closureL)
by blast
lemma recReach_p_None_subseteq_recReach:
"[| E1 x = Some (Loc p); E1 y = Some (Loc q); p≠q;
E1 y = (extend E1 (snd (extractP (fst (alts ! i)))) vs) y;
w ∈ recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) y (h(p := None), k) |]
==> w ∈ recReach (E1, E2) y (h, k)"
apply (simp add: recReach_def)
apply (case_tac
"extend E1 (snd (extractP (fst (alts ! i)))) vs y",simp_all)
apply (case_tac a, simp_all)
apply (frule recReachL_p_None_subseteq_recReachL)
by blast
(* Lemas patrones *)
lemma closureV_subseteq_closureL:
"h p = Some (j,C,vs)
==> (\<Union> i < length vs. closureV (vs!i) (h,k)) ⊆ closureL p (h,k)"
apply (frule closureV_equals_closureL)
by blast
lemma vs_defined:
"[| set xs ∩ dom E1 = {};
length xs = length vs;
y ∈ set xs;
extend E1 xs vs y = Some (Loc q) |]
==>∃ j < length vs. vs!j = Loc q"
apply (simp add: extend_def)
apply (induct xs vs rule: list_induct2',simp_all)
by (split split_if_asm,force,force)
lemma closure_Loc_subseteq_closureV_Loc:
"[| vs ! i = Loc q;
i < length vs |]
==> closureL q (h,k) ⊆ (\<Union>i < length vs closureV (vs ! i) (h, k))"
apply (rule subsetI)
apply clarsimp
apply (rule_tac x="i" in bexI)
apply (simp add: closureV_def)
by simp
lemma patrones:
"[| E1 x = Some (Loc p); h p = Some (j,C,vs);
i < length alts; length alts > 0; length assert = length alts;
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
y ∈ set (snd (extractP (fst (alts ! i)))) |]
==> closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) y (h, k) ⊆
closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h, k)"
apply (rule subsetI)
apply (subst (asm) closure_def)
apply (case_tac
"extend E1 (snd (extractP (fst (alts ! i)))) vs y",simp_all)
apply (case_tac a,simp_all)
apply (subgoal_tac "x ∉ set (snd (extractP (fst (alts ! i))))")
prefer 2 apply blast
apply (frule_tac x="x" and E="E1" and vs="vs" in extend_monotone_i)
apply (simp,simp,simp)
apply (rename_tac q)
apply (frule_tac y="y" in vs_defined,force,assumption+)
apply (simp add: closure_def)
apply (frule_tac k="k" in closureV_subseteq_closureL)
apply (elim exE,elim conjE)
apply (frule closure_Loc_subseteq_closureV_Loc,assumption+)
by force
lemma patrones_2:
"[| E1 x = Some (Loc p); h p = Some (j,C,vs);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
i < length alts; length alts > 0; length assert = length alts;
y ∈ set (snd (extractP (fst (alts ! i)))) |]
==> closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) y (h(p:=None), k) ⊆ {p}"
apply (rule subsetI)
apply (subst (asm) closure_def)
apply (case_tac
"extend E1 (snd (extractP (fst (alts ! i)))) vs y",simp_all)
apply (case_tac a,simp_all)
apply (rename_tac q)
apply (frule_tac y="y" in vs_defined,force,assumption+)
apply (elim exE,elim conjE)
apply (frule_tac h="h(p:=None)" and k="k" in closure_Loc_subseteq_closureV_Loc,assumption+)
apply (frule_tac h="h" and k="k" in closureV_subseteq_closureL_None)
apply (subst (asm) closureL_p_None_p)
by blast
(* Lemas auxiliares *)
lemma dom_extend_in_E1_or_xs: (*tont2*)
"[| y ∈ dom (extend E1 xs vs); length xs = length vs |]
==> y ∈ dom E1 ∨ y ∈ set xs"
apply (simp add: extend_def)
apply (erule disjE)
apply (induct xs vs rule: list_induct2')
apply simp_all
by force
lemma extend_monotone_x_in_dom_E1_2:
"[| set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
length assert = length alts; i < length alts;
x ∈ fst (assert ! i);
x ∈ dom E1|]
==> E1 x = extend E1 (snd (extractP (fst (alts ! i)))) vs x"
apply (subgoal_tac "x ∉ set (snd (extractP (fst (alts ! i))))")
apply (rule extend_monotone,assumption)
by blast
lemma closure_extend_None_subset_closure: (*auxiliar_conv*)
"[| alts ≠ []; i < length alts; length assert = length alts;
E1 x = Some (Loc p); h p = Some (j, C, vs);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
y ∈ fst (assert ! i);
y ∉ set (snd (extractP (fst (alts ! i))));
y ∈ dom E1;
q ∈ closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) y (h(p := None), k)|]
==> q ∈ closure (E1, E2) y (h, k)"
apply (case_tac "E1 y = E1 x",simp)
(* E1 y = E1 x *)
apply (frule extend_monotone_x_in_dom_E1_2,assumption+)
apply (subgoal_tac
"closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) y (h(p := None), k) ⊆
closure (E1, E2) y (h, k)")
prefer 2 apply (rule closure_extend_p_None_subseteq_closure,simp,simp)
apply blast
apply simp
apply (subgoal_tac "∃ z. E1 y = Some z")
prefer 2 apply (simp add: dom_def)
apply (elim exE)
apply (frule extend_monotone_x_in_dom_E1_2,assumption+)
apply (case_tac z,simp_all)
(* E1 y = Some (Lop p) *)
apply (frule_tac extend_monotone_x_in_dom_E1_2,assumption+)
apply (rule_tac i="i" and alts="alts" and vs="vs"
in closure_p_None_subseteq_closure,assumption+,simp,simp)
apply simp
(* E1 y = IntT n *)
apply (simp add: closure_def)
(* E1 y = BoolT b *)
apply (simp add: closure_def)
done
lemma recReach_extend_None_subset_recReach: (*auxiliar_2_conv:*)
"[| alts ≠ []; i < length alts; length assert = length alts;
E1 x = Some (Loc p); h p = Some (j, C, vs);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
y ∈ fst (assert ! i);
y ∉ set (snd (extractP (fst (alts ! i))));
y ∈ dom E1;
q ∈ recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) y (h(p := None), k)|]
==> q ∈ recReach (E1, E2) y (h, k)"
apply (case_tac "E1 y = E1 x",simp)
(* E1 y = E1 x *)
apply (frule extend_monotone_x_in_dom_E1_2,assumption+)
apply (subgoal_tac
"recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) y (h(p := None), k) ⊆
recReach (E1, E2) y (h, k)")
prefer 2 apply (rule recReach_extend_p_None_subseteq_recReach,simp,simp)
apply blast
apply simp
apply (subgoal_tac "∃ z. E1 y = Some z")
prefer 2 apply (simp add: dom_def)
apply (elim exE)
apply (frule extend_monotone_x_in_dom_E1_2,assumption+)
apply (case_tac z,simp_all)
(* E1 y = Some (Lop p) *)
apply (frule_tac extend_monotone_x_in_dom_E1_2,assumption+)
apply (rule_tac i="i" and alts="alts" and vs="vs"
in recReach_p_None_subseteq_recReach,assumption+,simp,simp)
apply simp
(* E1 y = IntT n *)
apply (simp add: recReach_def)
(* E1 y = BoolT b *)
apply (simp add: recReach_def)
done
lemma closure_monotone_extend_3:
"[| set (snd (extractP (fst (alts ! i)))) ∩ dom E = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
x∈ dom E;
length alts > 0;
i < length alts |]
==> closure (E, E') x (h, k) = closure (extend E (snd (extractP (fst (alts ! i)))) vs, E') x (h, k)"
apply (subgoal_tac " x ∉ set (snd (extractP (fst (alts ! i))))")
apply (subgoal_tac
"E x = extend E (snd (extractP (fst (alts ! i)))) vs x")
apply (simp add:closure_def)
apply (rule extend_monotone_i)
apply (simp,simp,simp)
by blast
lemma recReach_monotone_extend_3:
"[| set (snd (extractP (fst (alts ! i)))) ∩ dom E = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
x∈ dom E;
length alts > 0;
i < length alts |]
==> recReach (E, E') x (h, k) = recReach (extend E (snd (extractP (fst (alts ! i)))) vs, E') x (h, k)"
apply (subgoal_tac " x ∉ set (snd (extractP (fst (alts ! i))))")
apply (subgoal_tac
"E x = extend E (snd (extractP (fst (alts ! i)))) vs x")
apply (simp add:recReach_def)
apply (rule extend_monotone_i)
apply (simp,simp,simp)
by blast
lemma pp12:
"[| xa ∈ closure (E1, E2) xaa (h, k);
xb ∈ closureL xa (h, k);
xb ∈ recReach (E1, E2) z (h, k)|]
==>
closure (E1, E2) xaa (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {}"
apply (simp add: closure_def)
apply (case_tac "E1 xaa")
apply simp
apply simp
apply (case_tac "a", simp_all,clarsimp)
apply (subgoal_tac " xa ∈ closureL nat (h, k) ==> closureL xa (h, k) ⊆ closureL nat (h, k)")
apply blast
apply (erule closureL_monotone)
done
lemma P7_case_dem1:
"[| Si = S'i ∪ S''i;
Ri = R'i ∪ R''i;
S'i ⊆ S;
R'i ⊆ R;
Γ x = Some s'' --> S''i ⊆ S ∧ R''i = {};
Γ x ≠ Some s'' --> S''i ∩ R'i = {} ∧ R''i = {};
S ∩ R = {}|]
==> Si ∩ Ri = {}"
by blast
(* Si = S'i ∪ S''i *)
lemma P7_case_dem1_1:
"[| length assert = length alts; i < length assert|] ==>
SSet (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) =
SSet ((fst (assert ! i)) ∩ (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))))
(snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) ∪
SSet ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k)"
by (simp add: SSet_def add: Let_def,blast)
(* Ri = R'i ∪ R''i *)
lemma P7_case_dem1_2:
"[| length assert = length alts; i < length assert|] ==>
RSet (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) =
RSet2 ((fst (assert ! i)) ∩ (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))))
(fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) ∪
RSet2 ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k)"
apply (simp add: RSet_def add: RSet2_def add: live_def add: closureLS_def)
by blast
(* S'i ⊆ S *)
lemma P7_case_dem1_3:
" [| ∀ i < length assert. ∀ x ∈ set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
∀ i < length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
∀ i < length alts. x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
dom (snd (assert ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
def_nonDisjointUnionEnvList (map snd assert);
∀ i < length alts. ∀ j < length alts. i ≠ j --> (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j))))) = {};
length assert > 0;
x ∈ dom (nonDisjointUnionEnvList (map snd assert));
E1 x = Some (Loc p);
length assert = length alts;
i < length assert |] ==>
SSet ((fst (assert ! i)) ∩ (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))))
(snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) ⊆
SSet (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1, E2) (h, k)"
apply (clarsimp)
apply (simp add: SSet_def add: Let_def)
apply (erule exE, elim conjE)
apply (erule disjE)
apply simp
apply (rule_tac x="x" in exI)
apply (rule conjI)
apply (rule disjI1) apply simp
apply (rule conjI)
apply (subgoal_tac
" i < length (map snd assert) -->
length (map snd assert) > 0 -->
def_nonDisjointUnionEnvList (map snd assert) -->
snd (assert ! i) x = Some s'' -->
foldl op ⊗ empty (map snd assert) x = Some s''",simp)
apply (rule Otimes_prop3)
apply (subgoal_tac "x ∈ dom E1")
apply (frule_tac E'="E2" and h="h" and k="k" in closure_monotone_extend_3,assumption+,simp,assumption+,simp)
apply (simp add: dom_def)
apply (rule_tac x="xaa" in exI)
apply (erule bexE, simp, elim conjE)
apply (case_tac "xaa ∈ set (snd (extractP (fst (alts ! i))))")
apply (case_tac "i=ia", simp)
apply (rotate_tac 7)
apply (erule_tac x="ia" in allE,simp)
apply (rotate_tac 20)
apply (erule_tac x="i" in allE,simp)
apply blast
apply (rule conjI)
apply (rule disjI2)
apply (rule_tac x="i" in bexI,simp,simp)
apply (subgoal_tac
" i < length (map snd assert) -->
length (map snd assert) > 0 -->
def_nonDisjointUnionEnvList (map snd assert) -->
snd (assert ! i) xaa = Some s'' -->
foldl op ⊗ empty (map snd assert) xaa = Some s''",simp)
prefer 2 apply (rule Otimes_prop3)
apply (subgoal_tac "xaa ∈ dom E1")
apply (frule_tac E'="E2" and h="h" and k="k" in closure_monotone_extend_3,assumption+,simp,assumption+,simp)
apply (erule_tac x="i" in allE,simp)+
apply (subgoal_tac "xaa ∈ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)")
apply (rule extend_prop1,simp,simp,simp)
by blast
(* R'i ⊆ R *)
lemma P7_case_dem1_4:
" [| ∀ i < length assert. ∀ x ∈ set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
∀ i < length alts. x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
∀ i < length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
dom (snd (assert ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
∀ i < length alts. ∀ j < length alts. i ≠ j --> (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j))))) = {};
def_nonDisjointUnionEnvList (map snd assert);
length assert > 0;
x ∈ dom (nonDisjointUnionEnvList (map snd assert));
E1 x = Some (Loc p);
h p = Some (j,C,vs);
length assert = length alts;
i < length assert |]
==> RSet2 ((fst (assert ! i)) ∩ (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))))
(fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) ⊆
RSet (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1, E2) (h, k)"
apply (simp add: RSet_def add: RSet2_def)
apply (unfold live_def)
apply (unfold closureLS_def)
apply simp
apply (rule subsetI)
apply simp
apply (elim conjE)
apply (rename_tac q)
apply (rule conjI)
apply (erule bexE)
apply (rename_tac q y)
apply (case_tac "y ∉ set (snd (extractP (fst (alts ! i))))")
apply (rule disjI2)
apply (rule_tac x="i" in bexI) prefer 2 apply simp
apply (rule_tac x="y" in bexI) prefer 2 apply simp
apply (subgoal_tac "y ∈ dom E1")
apply (frule_tac E'="E2" and h="h" and k="k"
in closure_monotone_extend_3)
apply (simp,simp,simp,simp)
apply (erule_tac x="i" in allE,simp)
apply (erule_tac x="i" in allE,simp)
apply (erule_tac x="i" in allE,simp)
apply (erule_tac x="i" in allE,simp)
apply (elim conjE)
apply (subgoal_tac "y ∈ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)")
apply (rule extend_prop1,assumption+)
apply blast
apply simp
apply (subgoal_tac
"closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) y (h, k) ⊆
closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h, k)")
prefer 2 apply (rule patrones,assumption+) apply simp apply assumption+
apply (rule disjI1)
apply (subgoal_tac "x ∈ dom E1")
apply (frule_tac E'="E2" and h="h" and k="k" in closure_monotone_extend_3,assumption+,simp, assumption+,simp)
apply blast
apply (simp add: dom_def)
apply (erule bexE)
apply (erule bexE)
apply simp
apply (elim conjE)
apply (erule disjE)
apply (rule disjI2)
apply simp
apply (rule_tac x="i" in bexI) prefer 2 apply simp
apply (rule_tac x="x" in bexI) prefer 2 apply simp
apply (rule conjI)
apply (subgoal_tac
" i < length (map snd assert) -->
length (map snd assert) > 0 -->
def_nonDisjointUnionEnvList (map snd assert) -->
snd (assert ! i) x = Some d'' -->
foldl op ⊗ empty (map snd assert) x = Some d''",simp)
apply (rule Otimes_prop3)
apply (subgoal_tac "x ∈ dom E1")
apply (frule_tac E'="E2" and h="h" and k="k" in recReach_monotone_extend_3,assumption+,simp, assumption+,simp)
apply (simp add: dom_def)
apply (rule disjI2)
apply (erule bexE)
apply (elim conjE)
apply (rule_tac x="ia" in bexI) prefer 2 apply simp
apply (rule_tac x="z" in bexI) prefer 2 apply simp
apply (rule conjI)
apply (subgoal_tac
" i < length (map snd assert) -->
length (map snd assert) > 0 -->
def_nonDisjointUnionEnvList (map snd assert) -->
snd (assert ! i) z = Some d'' -->
foldl op ⊗ empty (map snd assert) z = Some d''",simp)
apply (rule Otimes_prop3)
apply (case_tac "z ∈ set (snd (extractP (fst (alts ! i))))")
apply (case_tac "i=ia", simp)
apply (rotate_tac 6)
apply (erule_tac x="ia" in allE)
apply (drule mp,simp)
apply (rotate_tac 6)
apply (erule_tac x="i" in allE,simp)
apply simp
apply (subgoal_tac "z ∈ dom E1")
apply (frule_tac E'="E2" and h="h" and k="k" in recReach_monotone_extend_3,assumption+,simp, assumption+,simp)
apply (erule_tac x="i" in allE,simp)
apply (erule_tac x="i" in allE,simp)
apply (erule_tac x="i" in allE,simp)
apply (elim conjE)
apply (subgoal_tac "z ∈ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)")
apply (rule extend_prop1,assumption+)
by blast
(* Γ x = Some s'' --> S''i ⊆ S *)
lemma P7_case_dem1_5_1:
" [| E1 x = Some (Loc p);
h p = Some (j,C,vs);
∀i<length alts. x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
(foldl op ⊗ empty (map snd assert)) x = Some s'';
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
length assert > 0;
length assert = length alts;
i < length assert |] ==>
SSet ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) ⊆
SSet (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1, E2) (h, k)"
apply (rule subsetI)
apply (simp add: SSet_def, simp add: Let_def)
apply (elim exE, elim conjE)
apply (rule_tac x="x" in exI)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (frule patrones [where ?E2.0="E2" and k="k"],assumption+)
apply (simp,assumption+)
apply (subgoal_tac
"closure (E1, E2) x (h, k) =
closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h, k)",simp)
apply blast
apply (rule closure_monotone_extend_3)
by (simp, simp, simp add:dom_def,simp,simp)
(* Γ x = Some s'' --> R''i = {} *)
lemma P7_case_dem1_5_2:
" [| (foldl op ⊗ empty (map snd assert)) x = Some s'';
∀ i < length assert. ∀ x ∈ set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
length assert = length alts;
i < length assert |] ==>
RSet2 ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) = {}"
apply (erule_tac x="i" in allE) apply simp
by (simp add: RSet2_def)
(* Γ x ≠ Some s'' --> S''i ∩ R'i = {} *)
lemma P7_case_dem1_6_1:
" [| (foldl op ⊗ empty (map snd assert)) x ≠ Some s'';
shareRec (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) (hh, k);
∀ i < length alts. x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
∀ i < length assert. ∀ x ∈ set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
∀ i < length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
def_nonDisjointUnionEnvList (map snd assert);
x ∈ dom (nonDisjointUnionEnvList (map snd assert));
E1 x = Some (Loc p);
length assert > 0;
length assert = length alts;
i < length assert |] ==>
SSet ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) ∩
RSet2 ((fst (assert ! i)) ∩ (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))))
(fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) = {}"
apply (rule equalityI)
prefer 2 apply simp
apply (rule subsetI)
apply (simp add: SSet_def)
apply (simp add: Let_def)
apply (elim conjE)
apply (elim exE)
apply (elim conjE)
apply (rename_tac xij)
apply (case_tac
"(∃z∈fst (assert ! i) - set (snd (extractP (fst (alts ! i)))).
snd (assert ! i) z = Some d'' ∧
closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) xij (h, k) ∩
recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) z (h, k) ≠ {})")
apply (elim bexE)
apply (elim conjE)
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="xij" in ballE)
prefer 2 apply (simp add: extend_def) apply force
apply (rotate_tac 19)
apply (erule thin_rl)
apply (drule mp)
apply (rule_tac x="z" in bexI)
prefer 2 apply simp
apply (rule conjI)
apply simp
apply simp
apply simp
apply simp
apply (simp only: RSet2_def)
apply (simp only: live_def)
apply (simp only: closureLS_def)
apply simp
apply (elim conjE)
apply (elim bexE)
apply (elim conjE)
apply (erule_tac x="z" in ballE)
prefer 2 apply simp
apply simp
apply (elim conjE)
apply (subgoal_tac "∃ w. w ∈ closureL xa (h, k) ∧ w ∈ recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) z (h, k)")
prefer 2 apply blast
apply (elim exE,elim conjE)
apply (frule pp12) apply simp apply simp apply simp
done
(* Γ x ≠ Some s'' --> R''i = {} *)
lemma P7_case_dem1_6_2:
"[| ∀i<length assert. ∀x∈set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
i < length assert; length assert = length alts|]
==> RSet2 ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) = {}"
apply (rule equalityI)
apply (rule subsetI)
apply (simp only: RSet2_def)
apply (simp only: live_def)
apply (simp only: closureLS_def)
apply simp
apply simp
done
lemma P7_CASE:
"[| length assert = length alts;
∀ i < length assert. ∀ x ∈ set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
∀ i < length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
dom (snd (assert ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
∀ i < length alts. ∀ j < length alts. i ≠ j --> (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j))))) = {};
∀ i < length alts. x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
shareRec (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) (hh, k);
def_nonDisjointUnionEnvList (map snd assert);
E1 x = Some (Loc p);
h p = Some (j,C,vs);
x ∈ dom (nonDisjointUnionEnvList (map snd assert));
length assert > 0;
SSet (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert))(E1, E2) (h, k) ∩
RSet (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1, E2) (h, k) = {};
i < length assert |]
==>
SSet (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) ∩
RSet (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) = {}"
apply (rule P7_case_dem1)
apply (rule P7_case_dem1_1,assumption+)
apply (rule P7_case_dem1_2,assumption+)
apply (rule P7_case_dem1_3,assumption+)
apply (rule P7_case_dem1_4,assumption+)
apply (rule impI, rule conjI)
apply (rule P7_case_dem1_5_1,assumption+)
apply (rule P7_case_dem1_5_2,assumption+)
apply (rule impI, rule conjI)
apply (rule P7_case_dem1_6_1,assumption+)
apply (rule P7_case_dem1_6_2,assumption+)
done
text{*
Lemmas for CASEL Rule
*}
lemma P7_casel_dem1:
"[| Si = S'i ∪ S''i;
Ri = R'i ∪ R''i;
S'i ⊆ S;
R'i ⊆ R;
Γ x = Some s'' --> S''i ⊆ S ∧ R''i = {};
Γ x ≠ Some s'' --> S''i ∩ R'i = {} ∧ R''i = {};
S ∩ R = {}|]
==> Si ∩ Ri = {}"
by blast
(* Si = S'i ∪ S''i *)
lemma P7_casel_dem1_1:
"[| length assert = length alts; i < length assert|] ==>
SSet (fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k) =
SSet ((fst (assert ! i)) ∩ (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))))
(snd (assert ! i)) (E1, E2) (h, k) ∪
SSet ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (E1, E2) (h, k)"
by (simp add: SSet_def add: Let_def,blast)
(* Ri = R'i ∪ R''i *)
lemma P7_casel_dem1_2:
"[| length assert = length alts; i < length assert|] ==>
RSet (fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k) =
RSet2 ((fst (assert ! i)) ∩ (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))))
(fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k) ∪
RSet2 ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k)"
apply (simp add: RSet_def add: RSet2_def add: live_def add: closureLS_def)
by blast
(* S'i ⊆ S *)
lemma P7_casel_dem1_3:
"[| def_nonDisjointUnionEnvList (map snd assert);
length assert > 0;
x ∈ dom (nonDisjointUnionEnvList (map snd assert));
length assert = length alts;
i < length assert |] ==>
SSet ((fst (assert ! i)) ∩ (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))))
(snd (assert ! i)) (E1,E2) (h, k) ⊆
SSet (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1, E2) (h, k)"
apply (clarsimp)
apply (simp add: SSet_def add: Let_def)
apply (erule exE, elim conjE)
apply (erule disjE)
apply simp
apply (rule_tac x="x" in exI)
apply (rule conjI)
apply (rule disjI1) apply simp
apply (rule conjI)
apply (subgoal_tac
" i < length (map snd assert) -->
length (map snd assert) > 0 -->
def_nonDisjointUnionEnvList (map snd assert) -->
snd (assert ! i) x = Some s'' -->
foldl op ⊗ empty (map snd assert) x = Some s''",simp)
apply (rule Otimes_prop3)
apply simp
apply (rule_tac x="xaa" in exI)
apply (erule bexE, simp, elim conjE)
apply (rule conjI)
apply (rule disjI2)
apply (rule_tac x="ia" in bexI,simp,simp)
apply (subgoal_tac
" i < length (map snd assert) -->
length (map snd assert) > 0 -->
def_nonDisjointUnionEnvList (map snd assert) -->
snd (assert ! i) xaa = Some s'' -->
foldl op ⊗ empty (map snd assert) xaa = Some s''",simp)
by (rule Otimes_prop3)
(* R'i ⊆ R *)
lemma P7_casel_dem1_4:
" [| ∀ i < length alts. x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
fst (assert ! i) ⊆ dom (snd (assert ! i));
dom (snd (assert ! i)) ⊆ dom E1;
def_nonDisjointUnionEnvList (map snd assert);
length assert > 0;
(E1 x = Some aa ∧ aa = IntT n ∧ fst (alts ! i) = ConstP (LitN n) ∨
E1 x = Some aa ∧ aa = BoolT b ∧ fst (alts ! i) = ConstP (LitB b));
x ∈ dom (nonDisjointUnionEnvList (map snd assert));
length assert = length alts;
i < length assert |]
==> RSet2 ((fst (assert ! i)) ∩ (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))))
(fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k) ⊆
RSet (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1, E2) (h, k)"
apply (simp add: RSet_def add: RSet2_def)
apply (unfold live_def)
apply (unfold closureLS_def)
apply simp
apply (rule subsetI)
apply simp
apply (elim conjE)
apply (rename_tac q)
apply (rule conjI)
apply clarsimp
apply (erule disjE)
apply clarsimp
apply clarsimp
apply (erule bexE)
apply (erule bexE)
apply simp
apply (elim conjE)
apply (erule_tac P="z=x" in disjE)
apply (rule disjI2)
apply (rule_tac x="i" in bexI) prefer 2 apply simp
apply (rule_tac x="x" in bexI) prefer 2 apply simp
apply (rule conjI)
apply (subgoal_tac
" i < length (map snd assert) -->
length (map snd assert) > 0 -->
def_nonDisjointUnionEnvList (map snd assert) -->
snd (assert ! i) x = Some d'' -->
foldl op ⊗ empty (map snd assert) x = Some d''",simp)
apply (rule Otimes_prop3)
apply simp
apply (rule disjI2)
apply (rule_tac x="i" in bexI)
prefer 2 apply simp
apply (rule_tac x="z" in bexI)
prefer 2 apply force
apply (rule conjI)
apply (subgoal_tac
" i < length (map snd assert) -->
length (map snd assert) > 0 -->
def_nonDisjointUnionEnvList (map snd assert) -->
snd (assert ! i) z = Some d'' -->
foldl op ⊗ empty (map snd assert) z = Some d''",simp)
apply (rule Otimes_prop3)
by simp
(* Γ x = Some s'' --> S''i ⊆ S *)
lemma P7_casel_dem1_5_1:
" [| (E1 x = Some aa ∧ aa = IntT n ∧ fst (alts ! i) = ConstP (LitN n)) ∨
(E1 x = Some aa ∧ aa = BoolT b ∧ fst (alts ! i) = ConstP (LitB b)) ;
length assert > 0;
length assert = length alts;
i < length assert |] ==>
SSet ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (E1,E2) (h, k) ⊆
SSet (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1, E2) (h, k)"
apply (rule subsetI)
apply (erule disjE)
by (simp add: SSet_def)+
(* Γ x = Some s'' --> R''i = {} *)
lemma P7_casel_dem1_5_2:
" [| (foldl op ⊗ empty (map snd assert)) x = Some s'';
(E1 x = Some aa ∧ aa = IntT n ∧ fst (alts ! i) = ConstP (LitN n)) ∨
(E1 x = Some aa ∧ aa = BoolT b ∧ fst (alts ! i) = ConstP (LitB b));
length assert = length alts;
i < length assert |] ==>
RSet2 ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i)) (E1,E2) (h, k) = {}"
apply (erule disjE)
by (simp add: RSet2_def)+
(* Γ x ≠ Some s'' --> S''i ∩ R'i = {} *)
lemma P7_casel_dem1_6_1:
" [| (foldl op ⊗ empty (map snd assert)) x ≠ Some s'';
(E1 x = Some aa ∧ aa = IntT n ∧ fst (alts ! i) = ConstP (LitN n)) ∨
(E1 x = Some aa ∧ aa = BoolT b ∧ fst (alts ! i) = ConstP (LitB b));
length assert > 0;
length assert = length alts;
i < length assert |] ==>
SSet ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (E1, E2) (h, k) ∩
RSet2 ((fst (assert ! i)) ∩ (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))))
(fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k) = {}"
apply (rule equalityI)
prefer 2 apply simp
apply (rule subsetI)
apply (erule disjE)
by (simp add: SSet_def)+
(* Γ x ≠ Some s'' --> R''i = {} *)
lemma P7_casel_dem1_6_2:
"[| (E1 x = Some aa ∧ aa = IntT n ∧ fst (alts ! i) = ConstP (LitN n)) ∨
(E1 x = Some aa ∧ aa = BoolT b ∧ fst (alts ! i) = ConstP (LitB b));
length assert > 0; i < length assert; length assert = length alts|]
==> RSet2 ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k) = {}"
apply (rule equalityI)
apply (rule subsetI)
apply (simp only: RSet2_def)
apply (simp only: live_def)
apply (simp only: closureLS_def)
apply (erule disjE)
apply simp
apply simp
by simp
lemma P7_CASEL:
" [| ∀ i < length alts. x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
x ∈ dom (nonDisjointUnionEnvList (map snd assert));
dom (nonDisjointUnionEnvList (map snd assert)) ⊆ dom E1;
(E1 x = Some aa ∧ aa = IntT n ∧ fst (alts ! i) = ConstP (LitN n)) ∨
(E1 x = Some aa ∧ aa = BoolT b ∧ fst (alts ! i) = ConstP (LitB b));
i < length alts;
0 < length assert;
def_nonDisjointUnionEnvList (map snd assert);
0 < length (map snd assert);
length assert = length alts;
fst (assert ! i) ⊆ dom (snd (assert ! i));
SSet ((\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪ {x})
(nonDisjointUnionEnvList (map snd assert)) (E1, E2) (h, k) ∩
RSet ((\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪ {x})
(nonDisjointUnionEnvList (map snd assert)) (E1, E2) (h, k) =
{};
dom (snd (assert ! i)) ⊆ dom E1|]
==> SSet (fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k) ∩ RSet (fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k) = {}"
apply (rule P7_casel_dem1)
apply (rule P7_casel_dem1_1,assumption+,simp)
apply (rule P7_casel_dem1_2,assumption+,simp)
apply (rule P7_casel_dem1_3,assumption+,simp)
apply (rule P7_casel_dem1_4,assumption+,simp)
apply (rule impI, rule conjI)
apply (rule P7_casel_dem1_5_1,assumption+,simp)
apply (rule P7_casel_dem1_5_2,assumption+,simp)
apply (rule impI, rule conjI)
apply (rule P7_casel_dem1_6_1,assumption+,simp)
apply (rule P7_casel_dem1_6_2,assumption+,simp,simp)
by simp
text{*
Lemmas for CASED Rule
*}
lemma P7_cased_dem1:
"[| Si = S'i ∪ S''i;
Ri = R'i ∪ R''i;
S'i ⊆ S;
R'i ⊆ R;
S''i ∩ Ri = {};
S'i ∩ R''i = {};
S ∩ R = {}|]
==> Si ∩ Ri = {}"
by blast
(* Si = S'i ∪ S''i *)
lemma P7_cased_dem1_1:
"[| length assert = length alts; i < length assert|] ==>
SSet (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) =
SSet ((fst (assert ! i)) ∩ (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) ∪
SSet ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k)"
by (simp add: SSet_def add: Let_def,blast)
(* Ri = R'i ∪ R''i *)
lemma P7_cased_dem1_2:
"[| length assert = length alts; i < length assert|] ==>
RSet (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) =
RSet2 ((fst (assert ! i)) ∩ (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))))
(fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) ∪
RSet2 ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k)"
apply (simp add: RSet_def add: RSet2_def add: live_def add: closureLS_def)
by blast
(* S'i ⊆ S *)
lemma P7_cased_dem1_3:
"[| length assert > 0;
E1 x = Some (Loc p); h p = Some (j,C,vs);
∀ z ∈ dom Γ. Γ z ≠ Some s'' --> (∀i<length alts. z ∉ fst (assert ! i));
Γ = disjointUnionEnv
(nonDisjointUnionEnvList ((map (λ(Li,Γi). restrict_neg_map Γi (set Li∪{x})))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
(empty(x\<mapsto>d''));
∀ i < length alts. ∀ j < length alts. i ≠ j --> (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j))))) = {};
def_nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert)));
def_disjointUnionEnv
(nonDisjointUnionEnvList ((map (λ(Li,Γi). restrict_neg_map Γi (set Li∪{x})))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
[x \<mapsto> d''];
shareRec (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (E1, E2) (h, k) (hh, k);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
dom (snd (assert ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs);
length assert = length alts;
i < length assert |]
==> SSet ((fst (assert ! i)) ∩ (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) ⊆
SSet ((\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪ {x})
Γ (E1, E2) (h, k)"
apply (rule subsetI)
apply (simp add: SSet_def add: Let_def)
apply (rename_tac q)
apply (erule exE, elim conjE)
apply (rename_tac y)
apply (erule bexE, simp, elim conjE)
apply (rule_tac x="y" in exI)
apply (rule conjI)
apply (rule disjI2)
apply (rule_tac x="ia" in bexI,simp,simp)
apply (case_tac "y ∈ set (snd (extractP (fst (alts ! i))))")
apply (case_tac "i=ia", simp)
apply (rotate_tac 5)
apply (erule_tac x="ia" in allE,simp)
apply (rotate_tac 21)
apply (erule_tac x="i" in allE,simp)
apply blast
apply (rule conjI)
apply (frule Γ_case_x_is_d)
apply (erule_tac x="x" in ballE)
prefer 2 apply force
apply (drule mp, simp)
apply (case_tac "y = x",blast)
apply (rule Otimes_prop4)
apply (simp,assumption+,force,assumption+)
apply (subgoal_tac
"y ∈ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)")
prefer 2 apply blast
apply (frule dom_extend_in_E1_or_xs,assumption+)
apply simp
apply (rule closure_extend_None_subset_closure)
by assumption+
(* R'i ⊆ R *)
lemma P7_cased_dem1_4:
"[| length assert > 0;
E1 x = Some (Loc p); h p = Some (j,C,vs);
Γ = disjointUnionEnv
(nonDisjointUnionEnvList ((map (λ(Li,Γi). restrict_neg_map Γi (set Li∪{x})))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
(empty(x\<mapsto>d''));
def_nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert)));
def_disjointUnionEnv
(nonDisjointUnionEnvList ((map (λ(Li,Γi). restrict_neg_map Γi (set Li∪{x})))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
[x \<mapsto> d''];
∀ i < length alts. ∀ j < length alts. i ≠ j --> (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j))))) = {};
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
dom (snd (assert ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs);
∀ i < length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
length assert = length alts;
i < length assert |]
==> RSet2 ((fst (assert ! i)) ∩ (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))))
(fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) ⊆
RSet ((\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪ {x})
Γ (E1, E2) (h, k)"
apply (simp add: RSet_def add: RSet2_def)
apply (unfold live_def)
apply (unfold closureLS_def,simp)
apply (rule subsetI,simp)
apply (elim conjE)
apply (rename_tac q)
apply (erule bexE)
apply (rename_tac y)
apply (rule conjI)
apply (case_tac "y ∉ set (snd (extractP (fst (alts ! i))))")
apply (rule disjI2)
apply (rule_tac x="i" in bexI)
prefer 2 apply simp
apply (rule_tac x="y" in bexI)
prefer 2 apply simp
apply (subgoal_tac
"y ∈ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)")
prefer 2 apply (erule_tac x="i" in allE,simp)+ apply blast
apply (subgoal_tac "y ∈ dom E1")
prefer 2 apply (rule extend_prop1,simp,simp,simp)
apply (rule closure_extend_None_subset_closure,assumption+)
apply simp
apply (frule_tac k="k" and ?E2.0="E2" in patrones_2)
apply (assumption+,force,assumption+)
apply (subgoal_tac "q = p")
prefer 2 apply blast
apply (rule disjI1)
apply clarsimp
apply (simp add: closure_def)
apply (rule closureL_basic)
apply (erule bexE,elim conjE)
apply (simp, elim conjE)
apply (erule disjE)
apply (rule disjI2,simp)
apply (rule_tac x="i" in bexI)
prefer 2 apply simp
apply (rule_tac x="x" in bexI)
prefer 2 apply blast
apply (rule conjI)
apply (frule Γ_case_x_is_d,simp)
apply (case_tac "p=q")
apply (simp add: recReach_def)
apply (subgoal_tac "p ∈ closureL p (h,k)")
apply (subgoal_tac "p ∈ recReachL p (h,k)")
apply blast
apply (rule recReachL_basic)
apply (rule closureL_basic)
apply (subgoal_tac "x ∈ dom E1")
prefer 2 apply (simp add: dom_def)
apply (subgoal_tac
"∃ w. w ∈ closureL q (h(p := None), k) ∧
w ∈ recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h(p := None), k)")
prefer 2 apply blast
apply (elim exE, elim conjE)
apply (frule_tac x="x" and E="E1" and vs="vs" in extend_monotone_i,simp,blast)
apply (simp add: recReach_def)
apply (subgoal_tac "w = p",simp)
prefer 2 apply (subst (asm) recReachL_p_None_p,simp)+
apply (frule_tac h="h" and k="k" in closureL_p_None_subseteq_closureL)
apply (subgoal_tac "p ∈ recReachL p (h,k)")
apply (subgoal_tac "p ∈ closureL q (h,k)")
apply blast
apply blast
apply (rule recReachL_basic)
apply (rule disjI2)
apply (erule bexE,elim conjE)
apply simp
apply (case_tac "z ∈ set (snd (extractP (fst (alts ! i))))")
apply (case_tac "i=ia",simp)
apply (rotate_tac 5)
apply (erule_tac x="ia" in allE,simp)
apply (rotate_tac 22)
apply (erule_tac x="i" in allE,simp)
apply blast
apply (rule_tac x="i" in bexI)
prefer 2 apply simp
apply (rule_tac x="z" in bexI)
prefer 2 apply simp
apply (rule conjI)
apply (case_tac "z = x",simp)
apply (frule Γ_case_x_is_d,simp)
apply (rule Otimes_prop4)
apply (simp,assumption+,force,assumption+)
apply (subgoal_tac
"∃ w. w ∈ closureL q (h(p := None), k) ∧
w ∈ recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) z (h(p := None), k)")
prefer 2 apply blast
apply (subgoal_tac "z ∈ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)")
prefer 2 apply (erule_tac x="i" in allE,simp)+ apply blast
apply (subgoal_tac "z ∈ dom E1")
prefer 2 apply (rule extend_prop1,simp,simp,simp)
apply (elim exE,elim conjE)
apply (frule_tac y="z" in recReach_extend_None_subset_recReach,assumption+)
apply (case_tac "p≠q")
apply (frule_tac h="h" and k="k" in closureL_p_None_subseteq_closureL)
apply (subgoal_tac "w ∈ closureL q (h,k)")
apply blast
apply (rotate_tac 26)
apply (erule thin_rl)
apply blast
apply simp
apply (subst (asm) closureL_p_None_p)+
apply simp
apply (subgoal_tac "q ∈ closureL q (h,k)")
apply blast
by (rule closureL_basic)
(* S''i ∩ Ri = {} *)
lemma P7_cased_dem1_5:
"[| length assert > 0;
length assert = length alts;
shareRec (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p:=None), k) (hh, k);
dom (snd (assert ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs);
∀ i < length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
i < length assert |]
==> SSet ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) ∩
RSet (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) = {}"
apply (rule equalityI)
prefer 2 apply simp
apply (rule subsetI)
apply (simp add: SSet_def)
apply (simp add: Let_def)
apply (elim conjE)
apply (elim exE, elim conjE)
apply (simp add: RSet_def)
apply (elim conjE)
apply (elim bexE,elim conjE)
apply (simp add: live_def)
apply (simp add: closureLS_def)
apply (elim bexE)
apply (simp add: shareRec_def)
apply (elim conjE)
apply (rotate_tac 16)
apply (erule thin_rl)
apply (erule_tac x="xa" in ballE)
apply (drule mp)
apply (rule_tac x="z" in bexI,simp)
apply (subgoal_tac
"∃ w. w ∈ closureL x (h(p := None), k) ∧
w ∈ recReach (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) z (h(p := None), k)")
prefer 2 apply blast
apply (elim exE,elim conjE)
apply (subgoal_tac
"w ∈ closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) xa (h(p := None), k)")
apply blast
apply (rule closure_transit,simp,simp)
apply simp
apply simp
apply (erule_tac x="i" in allE,simp)+
by blast
(* S'i ∩ R''i = {} *)
lemma P7_cased_dem1_6:
"[|E1 x = Some (Loc p);
h p = Some (j,C,vs);
Γ = disjointUnionEnv
(nonDisjointUnionEnvList ((map (λ(Li,Γi). restrict_neg_map Γi (set Li∪{x})))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
(empty(x\<mapsto>d''));
i < length alts; length assert = length alts;
shareRec (fst (assert ! i)) (snd (assert ! i))
(extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) (hh, k);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
dom (snd (assert ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs);
∀ i < length assert. fst (assert ! i) ⊆ dom (snd (assert ! i)) |]
==> SSet ((fst (assert ! i)) ∩ (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) ∩
RSet2 ((fst (assert ! i)) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) = {}"
apply (rule equalityI)
prefer 2 apply simp
apply (rule subsetI)
apply (simp add: SSet_def)
apply (simp add: Let_def)
apply (elim conjE)
apply (elim exE, elim conjE)
apply (simp add: RSet2_def)
apply (elim bexE, elim conjE)
apply (elim bexE, elim conjE)
apply (rename_tac q y ia z)
apply (simp add: live_def)
apply (simp add: closureLS_def)
apply (elim bexE,clarsimp)
apply (simp add: shareRec_def)
apply (elim conjE)
apply (rotate_tac 20)
apply (erule_tac x="y" in ballE)
apply (drule mp)
apply (rule_tac x="z" in bexI)
apply (rule conjI)
apply simp
apply (simp add: closure_def)
apply (case_tac "extend E1 (snd (extractP (fst (alts ! i)))) vs y")
apply simp
apply simp
apply (case_tac "a", simp_all,clarsimp)
apply (frule closureL_monotone)
apply blast
by blast
lemma P7_CASED:
"[| Γ = disjointUnionEnv
(nonDisjointUnionEnvList ((map (λ(Li,Γi). restrict_neg_map Γi (set Li∪{x})))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
(empty(x\<mapsto>d''));
set (snd (extractP (fst (alts ! i)))) ∩ dom E1 = {};
def_nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert)));
def_disjointUnionEnv
(nonDisjointUnionEnvList ((map (λ(Li,Γi). restrict_neg_map Γi (set Li∪{x})))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
[x \<mapsto> d''];
length (snd (extractP (fst (alts ! i)))) = length vs;
∀i<length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
dom (snd (assert ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs);
shareRec (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) (hh, k);
∀z∈ dom Γ. Γ z ≠ Some s'' --> (∀i<length alts. z ∉ fst (assert ! i));
∀ i < length alts. ∀ j < length alts. i ≠ j --> (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j))))) = {};
E1 x = Some (Loc p); h p = Some (j, C, vs); i < length alts;
0 < length (map snd assert); length assert = length alts;
∀i<length alts. ∀j. ∀x∈set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x = Some d'' --> j ∈ RecPos Ci;
shareRec (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (E1, E2) (h, k) (hh,k);
SSet ((\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪ {x})
Γ (E1, E2) (h, k) ∩
RSet ((\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪ {x})
Γ (E1, E2) (h, k) =
{}|]
==> SSet (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) ∩
RSet (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p := None), k) =
{}"
apply (rule P7_cased_dem1)
apply (rule P7_cased_dem1_1,assumption+,simp)
apply (rule P7_cased_dem1_2,assumption+,simp)
apply (rule P7_cased_dem1_3,simp,assumption+,simp)
apply (rule P7_cased_dem1_4,simp,assumption+,simp)
apply (rule P7_cased_dem1_5,simp,assumption+,simp)
apply (rule P7_cased_dem1_6,simp,assumption+)
done
(** P7_APP **)
lemma nth_map_of_xs_atom2val:
"[| length xs = length as;
distinct xs |]
==> ∀ i < length xs.
map_of (zip xs (map (atom2val E1) as)) (xs!i) =
Some (atom2val E1 (as!i))"
apply clarsimp
apply (induct xs as rule: list_induct2',simp_all)
by (case_tac i,simp,clarsimp)
lemma closureL_k_equals_closureL_Suc_k:
"closureL p (h, Suc k) = closureL p (h,k)"
apply (rule equalityI)
apply (rule subsetI)
apply (erule_tac closureL.induct)
apply (rule closureL_basic)
apply (rule closureL_step,simp)
apply (simp add: descendants_def)
apply (rule subsetI)
apply (erule_tac closureL.induct)
apply (rule closureL_basic)
apply (rule closureL_step,simp)
by (simp add: descendants_def)
lemma recReachL_k_equals_recReachL_Suc_k:
"recReachL x (h, k) = recReachL x (h, Suc k)"
apply (rule equalityI)
apply (rule subsetI)
apply (erule_tac recReachL.induct)
apply (rule recReachL_basic)
apply (rule recReachL_step,simp)
apply (simp add: recDescendants_def)
apply (rule subsetI)
apply (erule_tac recReachL.induct)
apply (rule recReachL_basic)
apply (rule recReachL_step,simp)
by (simp add: recDescendants_def)
lemma closure_APP_equals_closure_ef:
"[| length xs = length as; distinct xs;
distinct xs;
(∀ i < length as. ∀ x a. as!i = VarE x a --> x ∈ dom E1);
i < length as; as ! i = VarE xa a |]
==> closure (E1, E2) xa (h, k) =
closure (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) (xs ! i) (h, Suc k)"
apply (frule_tac ?E1.0="E1" in nth_map_of_xs_atom2val,assumption+)
apply (erule_tac x="i" in allE,simp)
apply (erule_tac x="i" in allE,simp)
apply (rule equalityI)
(* closure App ⊆ closure ef *)
apply (rule subsetI)
apply (simp add: closure_def)
apply (case_tac "E1 xa",simp_all)
apply (case_tac aa, simp_all)
apply (subst closureL_k_equals_closureL_Suc_k,assumption)
(* closure ef ⊆ closure App *)
apply (rule subsetI)
apply (simp add: closure_def)
apply (case_tac "E1 xa",simp_all)
apply (simp add: dom_def)
apply (case_tac aa, simp_all)
apply (insert closureL_k_equals_closureL_Suc_k)
by simp
lemma recReach_APP_equals_recReach_ef:
"[| i < length as; as ! i = VarE z a;
(∀ i < length as. ∀ x a. as!i = VarE x a --> x ∈ dom E1);
length xs = length as; distinct xs |]
==> recReach (E1, E2) z (h, k) =
recReach (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) (xs ! i) (h, Suc k)"
apply (rule equalityI)
(* recReach App ⊆ recReach ef *)
apply (rule subsetI)
apply (frule_tac ?E1.0="E1" in nth_map_of_xs_atom2val, assumption+)
apply (rotate_tac 6)
apply (erule_tac x="i" in allE,simp)
apply (simp add: recReach_def)
apply (case_tac "E1 z",simp_all)
apply (case_tac aa, simp_all)
apply (subgoal_tac
"recReachL nat (h, k) = recReachL nat (h, Suc k)",simp)
apply (rule recReachL_k_equals_recReachL_Suc_k)
(* recReach ef ⊆ recREach App *)
apply (rule subsetI)
apply (frule_tac ?E1.0="E1" in nth_map_of_xs_atom2val, assumption+)
apply (rotate_tac 6)
apply (erule_tac x="i" in allE,simp)
apply (simp add: recReach_def)
apply (case_tac "E1 z",simp_all)
apply force
apply (case_tac aa, simp_all)
apply (subgoal_tac
"recReachL nat (h, k) = recReachL nat (h, Suc k)",simp)
by (rule recReachL_k_equals_recReachL_Suc_k)
lemma closureL_recReach_APP_equals_closureL_recReach_ef:
"[| z ∈ fvs' as;
i < length as; as ! i = VarE z a;
(∀ i < length as. ∀ x a. as!i = VarE x a --> x ∈ dom E1);
length xs = length as; distinct xs |]
==> closureL x (h, k) ∩ recReach (E1, E2) z (h, k) =
closureL x (h, Suc k) ∩
recReach (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) (xs ! i) (h, Suc k)"
apply (subst closureL_k_equals_closureL_Suc_k)
apply (frule recReach_APP_equals_recReach_ef,assumption+)
by blast
lemma nth_set_distinct:
"[| x ∈ set xs; distinct xs |]
==> ∃ i < length xs. xs!i = x"
by (induct xs,simp,force)
lemma nth_map_add_map_of_y:
"[| i < length xs; ms ! i = y;
length xs = length ms; distinct xs|]
==> (map_of (zip xs ms)) (xs ! i) = Some y"
by (simp, subst set_zip,force)
lemma nth_map_add_map_of:
"[| i < length xs; length xs = length ms; distinct xs |]
==> (map_of (zip xs ms)) (xs!i) = Some (ms!i)"
apply (subgoal_tac
"set (zip xs ms) =
{(xs!i, ms!i) | i. i < min (length xs) (length ms)}")
apply force
by (rule set_zip)
lemma map_add_map_of:
"[| x ∈ set xs; dom E1 ∩ set xs = {}; length xs = length ys|]
==> (E1 ++ map_of (zip xs ys)) x = map_of (zip xs ys) x"
apply (subgoal_tac "E1 x = None")
apply (simp only: map_add_def)
apply (case_tac "map_of (zip xs ys) x",simp_all)
by blast
lemma var_in_fvs:
"[| i < length as; as ! i = VarE x a|]
==> x ∈ fvs' as"
apply (induct as arbitrary: i, simp_all)
apply clarsimp
apply (case_tac i,simp_all)
apply (case_tac aa, simp_all)
by auto
lemma atom_fvs_VarE:
"[| (∀ a ∈ set as. atom a); xa ∈ fvs' as |]
==> (∃ i < length as. ∃ a. as!i = VarE xa a)"
apply (induct as,simp_all)
apply (case_tac a, simp_all)
by force
declare atom.simps [simp del]
lemma live_APP_equals_live_ef:
"[| (∀ a ∈ set as. atom a); length xs = length as;
length xs = length ms;
dom E1 ∩ set xs = {}; distinct xs;
(∀ i < length as. ∀ x a. ∃ y. as!i = VarE x a --> x ∈ dom E1)|]
==> live (E1, E2) (fvs' as) (h, k) =
live (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) (set xs) (h, Suc k)"
apply (rule equalityI)
(* live App ⊆ live ef *)
apply (rule subsetI)
apply (simp add: live_def)
apply (simp add: closureLS_def)
apply (erule bexE)
apply (frule atom_fvs_VarE,assumption+)
apply (elim exE)
apply (elim conjE, elim exE)
apply (rule_tac x="xs!i" in bexI)
prefer 2 apply simp
apply (frule_tac ?E1.0="E1" in closure_APP_equals_closure_ef)
apply (assumption+,force,assumption+)
apply blast
(* live ef ⊆ live App *)
apply (rule subsetI)
apply (simp add: live_def)
apply (simp add: closureLS_def)
apply (elim bexE)
apply (frule nth_set_distinct,assumption+)
apply (elim exE,elim conjE)
apply (frule_tac ?E1.0="E1" in nth_map_of_xs_atom2val, assumption+)
apply (rotate_tac 10)
apply (erule_tac x="i" in allE,simp)
apply (erule_tac x="as!i" in ballE)
prefer 2 apply simp
apply (subgoal_tac
"length xs = length (map (atom2val E1) as)")
apply (frule_tac ?E1.0="E1" in map_add_map_of,assumption+)
prefer 2 apply simp
apply (simp add: atom.simps)
apply (case_tac "(as ! i)",simp_all)
apply (simp add: closure_def)
apply (rule_tac x="list" in bexI)
apply (case_tac "E1 list",simp_all) apply force
apply (case_tac aa, simp_all)
apply (subst (asm) closureL_k_equals_closureL_Suc_k)
apply blast
by (frule var_in_fvs,assumption+)
lemma map_le_nonDisjointUnionSafeEnvList:
"[| nonDisjointUnionSafeEnvList Γs x = Some y;
(nonDisjointUnionSafeEnvList Γs) ⊆m Γ' |]
==> Γ' x = Some y"
apply (simp add: map_le_def)
by force
declare nonDisjointUnionSafeEnvList.simps [simp del]
lemma nonDisjointUnionSafeEnv_assoc:
"nonDisjointUnionSafeEnv (nonDisjointUnionSafeEnv G1 G2) G3 =
nonDisjointUnionSafeEnv G1 (nonDisjointUnionSafeEnv G2 G3)"
apply (simp add: nonDisjointUnionSafeEnv_def add: unionEnv_def)
apply (rule ext, auto)
apply (split split_if_asm, simp, simp)
apply (split split_if_asm, simp,simp)
by (split split_if_asm, simp, simp add: dom_def)
lemma foldl_nonDisjointUnionSafeEnv_prop:
"foldl nonDisjointUnionSafeEnv (G' ⊕ G) Gs = G' ⊕ foldl op ⊕ G Gs"
apply (induct Gs arbitrary: G)
apply simp
by (simp_all add: nonDisjointUnionSafeEnv_assoc)
lemma nonDisjointUnionSafeEnv_empty:
"nonDisjointUnionSafeEnv empty x = x"
apply (simp add: nonDisjointUnionSafeEnv_def)
by (simp add: unionEnv_def)
lemma nonDisjointUnionSafeEnv_conmutative:
"def_nonDisjointUnionSafeEnv G G' ==> (G ⊕ G') = (G' ⊕ G)"
apply (simp add: nonDisjointUnionSafeEnv_def add: unionEnv_def)
apply (rule ext)
apply (simp add: def_nonDisjointUnionSafeEnv_def)
apply (simp add: safe_def)
by clarsimp
declare dom_fun_upd [simp del]
lemma nth_nonDisjointUnionSafeEnvList:
"[| length xs = length ms; def_nonDisjointUnionSafeEnvList (maps_of (zip xs ms)) |]
==> (∀ i < length xs . nonDisjointUnionSafeEnvList (maps_of (zip xs ms)) (xs!i) = Some (ms!i))"
apply (induct xs ms rule: list_induct2',simp_all)
apply clarsimp
apply (case_tac i)
apply simp
apply (simp add: nonDisjointUnionSafeEnvList.simps)
apply (subgoal_tac "empty ⊕ [x \<mapsto> y] = [x \<mapsto> y] ⊕ empty",simp)
apply (subgoal_tac "foldl op ⊕ ([x \<mapsto> y] ⊕ empty) (maps_of (zip xs ys)) =
[x \<mapsto> y] ⊕ foldl op ⊕ empty (maps_of (zip xs ys))",simp)
apply (simp add: nonDisjointUnionSafeEnv_def)
apply (simp add: unionEnv_def)
apply (simp add: dom_def)
apply (rule foldl_nonDisjointUnionSafeEnv_prop)
apply (subst nonDisjointUnionSafeEnv_empty)
apply (subst nonDisjointUnionSafeEnv_conmutative)
apply (simp only: def_nonDisjointUnionSafeEnv_def)
apply (simp only: safe_def)
apply force
apply (subst nonDisjointUnionSafeEnv_empty)
apply simp
apply clarsimp
apply (simp add: nonDisjointUnionSafeEnvList.simps)
apply (subgoal_tac "empty ⊕ [x \<mapsto> y] = [x \<mapsto> y] ⊕ empty",simp)
apply (subgoal_tac "foldl op ⊕ ([x \<mapsto> y] ⊕ empty) (maps_of (zip xs ys)) =
[x \<mapsto> y] ⊕ foldl op ⊕ empty (maps_of (zip xs ys))",simp)
apply (simp add: Let_def)
apply (erule_tac x="nat" in allE,simp)
apply (simp add: nonDisjointUnionSafeEnv_def)
apply (simp add: unionEnv_def)
apply (rule conjI)
apply (rule impI)+
apply (elim conjE)
apply (simp add: def_nonDisjointUnionSafeEnv_def)
apply (erule_tac x="x" in ballE)
apply (simp add: safe_def)
apply (simp add: dom_def)
apply clarsimp
apply (rule foldl_nonDisjointUnionSafeEnv_prop)
apply (rule nonDisjointUnionSafeEnv_conmutative)
by (simp add: def_nonDisjointUnionSafeEnv_def)
lemma union_dom_nonDisjointUnionSafeEnv:
" dom (nonDisjointUnionSafeEnv A B) = dom A ∪ dom B"
apply (simp add: nonDisjointUnionSafeEnv_def add: unionEnv_def,auto)
by (split split_if_asm,simp_all)
lemma dom_foldl_nonDisjointUnionSafeEnv_monotone:
" dom (foldl nonDisjointUnionSafeEnv (empty ⊕ x) xs) =
dom x ∪ dom (foldl op ⊕ empty xs)"
apply (subgoal_tac "empty ⊕ x = x ⊕ empty",simp)
apply (subgoal_tac "foldl op ⊕ (x ⊕ empty) xs =
x ⊕ foldl op ⊕ empty xs",simp)
apply (rule union_dom_nonDisjointUnionSafeEnv)
apply (rule foldl_nonDisjointUnionSafeEnv_prop)
apply (rule nonDisjointUnionSafeEnv_conmutative)
by (simp add: def_nonDisjointUnionSafeEnv_def)
lemma dom_nonDisjointUnionSafeEnvList_fvs:
"[| ∀ a ∈ set xs. atom a; length xs = length ys |]
==> fvs' xs ⊆ dom (nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var xs) ys)))"
apply (induct xs ys rule: list_induct2',simp_all)
apply (simp add: nonDisjointUnionSafeEnvList.simps)
apply (subst dom_foldl_nonDisjointUnionSafeEnv_monotone)
apply (rule conjI)
apply (simp add: atom.simps)
apply (case_tac x, simp_all)
apply (simp add: dom_def)
apply (subst dom_foldl_nonDisjointUnionSafeEnv_monotone)
by blast
lemma nonDisjointUnionSafeEnvList_prop1:
"[| nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ;
xa ∈ fvs' as; Γ xa = Some y;
def_nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
(∀ a ∈ set as. atom a); length as = length ms |]
==> ∃ i < length as. ∃ a. as!i = VarE xa a ∧ ms!i = y"
apply (frule atom_fvs_VarE,assumption+)
apply (elim exE, elim conjE, elim exE)
apply (rule_tac x="i" in exI,simp)
apply (simp add: map_le_def)
apply (erule_tac x="xa" in ballE,simp)
apply (subgoal_tac "length (map atom2var as) = length ms")
prefer 2 apply simp
apply (frule nth_nonDisjointUnionSafeEnvList,assumption+)
apply (erule_tac x="i" in allE,simp)
apply (frule dom_nonDisjointUnionSafeEnvList_fvs,assumption+)
by blast
lemma xs_ms_in_set:
"[| length ms = length as; length xs = length as; distinct xs;
i < length as; as ! i = VarE xa a; ms ! i = m|]
==> (xs ! i, m) ∈ set (zip xs ms)"
apply clarsimp
apply (subgoal_tac
"set (zip xs ms) =
{(xs!i, ms!i) | i. i < min (length xs) (length ms)}")
apply force
by (rule set_zip)
lemma xs_ms_in_set_ms:
"[| length ms = length as; length xs = length as; distinct xs;
i < length xs; (xs!i, m) ∈ set (zip xs ms)|]
==> ms!i = m"
apply (simp add: set_conv_nth cong: rev_conj_cong)
apply (elim exE, elim conjE)
apply (rename_tac j)
apply (frule_tac j=j in nth_eq_iff_index_eq)
by (simp,simp,simp)
lemma SSet_APP_equals_SSet_ef:
"[|def_nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ;
length xs = length as;
length xs = length ms; distinct xs; (∀ a ∈ set as. atom a);
dom E1 ∩ set xs = {}; fvs' as ⊆ dom Γ; dom Γ ⊆ dom E1;
(∀ i < length as. ∀ x a. as!i = VarE x a --> x ∈ dom E1)|]
==> SSet (fvs' as) Γ (E1, E2) (h, k) =
SSet (set xs) (map_of (zip xs ms))
(map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) (h, Suc k)"
apply (rule equalityI)
(* SSet APP ⊆ SSet ef *)
apply (rule subsetI)
apply (simp add: SSet_def)
apply (simp add: Let_def)
apply (elim exE, elim conjE)
apply (frule nonDisjointUnionSafeEnvList_prop1, assumption+,simp)
apply (elim exE,elim conjE)+
apply (rule_tac x="xs!i" in exI)
apply (rule conjI)
apply simp
apply (rule conjI)
(* Γef = Some s'' *)
apply (rule xs_ms_in_set,assumption+)
(* closure ef *)
apply (subgoal_tac
"closure (E1, E2) xa (h, k) =
closure (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) (xs ! i) (h, Suc k)")
apply blast
apply (rule closure_APP_equals_closure_ef)
apply (assumption+,simp,assumption+)
(* SSet ef ⊆ SSet APP *)
apply (rule subsetI)
apply (simp add: SSet_def)
apply (simp add: Let_def)
apply (elim exE, elim conjE)
apply (frule_tac ?E1.0="E1" in nth_map_of_xs_atom2val,assumption+)
apply (frule nth_set_distinct,assumption+)
apply (elim exE)
apply (rotate_tac 13)
apply (erule_tac x="i" in allE,simp)
apply (elim conjE)
apply (erule_tac x="as!i" in ballE)
prefer 2 apply simp
apply (simp add: atom.simps)
apply (case_tac "(as ! i)",simp_all)
(* as!i = VarE *)
apply (rule_tac x="list" in exI)
apply (rule conjI)
apply (rule var_in_fvs,assumption+)
apply (rule conjI)
(* Γ app = Some s'' *)
apply (subgoal_tac "length (map atom2var as) = length ms")
prefer 2 apply simp
apply (frule nth_nonDisjointUnionSafeEnvList,assumption+)
apply (rotate_tac 17)
apply (erule_tac x="i" in allE,simp)
apply (frule map_le_nonDisjointUnionSafeEnvList,assumption+)
apply (subgoal_tac "i < length xs")
prefer 2 apply simp
apply (frule nth_map_of_xs_atom2val,assumption+)
apply (rotate_tac 19)
apply (erule_tac x="i" in allE,simp)
apply (rule xs_ms_in_set_ms,assumption+,simp,simp)
(* closure app *)
apply clarsimp
apply (subgoal_tac
"closure (E1, E2) list (h, k) =
closure (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) (xs ! i) (h, Suc k)")
apply blast
apply (rule closure_APP_equals_closure_ef)
by (assumption+,simp,assumption+)
lemma RSet_APP_equals_RSet_ef:
"[| def_nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ;
(∀ a ∈ set as. atom a); length xs = length as;
(∀ i < length as. ∀ x a. as!i = VarE x a --> x ∈ dom E1);
length xs = length ms;
dom E1 ∩ set xs = {}; distinct xs |]
==> RSet (fvs' as) Γ (E1, E2) (h, k) =
RSet (set xs) (map_of (zip xs ms))
(map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) (h, Suc k)"
apply (rule equalityI)
(* RSet APP ⊆ RSet ef *)
apply (rule subsetI)
apply (simp add: RSet_def)
apply (elim conjE,elim bexE,elim conjE)
apply (rule conjI)
(* live *)
apply (frule live_APP_equals_live_ef)
apply assumption+ apply force apply blast
apply (frule nonDisjointUnionSafeEnvList_prop1)
apply (assumption+,simp)
apply (elim exE, elim conjE)+
apply (rule_tac x="xs!i" in bexI)
prefer 2 apply simp
apply (rule conjI)
(* Γ *)
apply (rule xs_ms_in_set,assumption+)
(* closure ∩ recReach *)
apply (subgoal_tac
" closureL x (h, k) ∩ recReach (E1, E2) z (h, k) =
closureL x (h, Suc k) ∩ recReach (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k))
(xs ! i) (h, Suc k)")
apply blast
apply (rule closureL_recReach_APP_equals_closureL_recReach_ef)
apply (assumption+,force,simp,assumption+)
(* RSet ef ⊆ RSet App *)
apply (rule subsetI)
apply (simp add: RSet_def)
apply (elim conjE,elim bexE,elim conjE)
apply (rule conjI)
(* live *)
apply (frule live_APP_equals_live_ef)
apply (assumption+,force,blast)
(* ∃z∈fvs' as *)
apply (frule_tac ?E1.0="E1" in nth_map_of_xs_atom2val,assumption+)
apply (frule nth_set_distinct,assumption+)
apply (elim exE)
apply (rotate_tac 12)
apply (erule_tac x="i" in allE,simp)
apply (elim conjE)
apply (erule_tac x="as!i" in ballE)
prefer 2 apply simp
apply (simp add: atom.simps)
apply (case_tac "(as ! i)",simp_all)
apply (frule var_in_fvs) apply assumption+
apply (rule_tac x="list" in bexI)
prefer 2 apply simp
apply (rule conjI)
(* Γ *)
apply (subgoal_tac "i<length xs")
prefer 2 apply simp
apply (frule_tac xs=xs and ms=ms in nth_map_add_map_of)
apply (simp,simp)
apply (subgoal_tac "length (map atom2var as) = length ms")
prefer 2 apply simp
apply (frule nth_nonDisjointUnionSafeEnvList,assumption+)
apply (rotate_tac 19)
apply (erule_tac x="i" in allE)
apply clarsimp
apply (rule map_le_nonDisjointUnionSafeEnvList,assumption+)
(* closure ∩ recReach *)
apply (subgoal_tac " closureL x (h, k) ∩ recReach (E1, E2) list (h, k) =
closureL x (h, Suc k) ∩ recReach (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k))
(xs ! i) (h, Suc k)")
apply blast
apply (rule closureL_recReach_APP_equals_closureL_recReach_ef)
by (assumption+,force,simp,assumption+)
lemma fvs_as_in_dom_E1:
"[| fvs' as ⊆ dom Γ; dom Γ ⊆ dom E1 |]
==> (∀ i < length as. ∀ x a. as!i = VarE x a --> x ∈ dom E1)"
apply (case_tac "as = []",simp_all)
apply (induct as,simp_all)
apply (rule allI,rule impI)
apply (case_tac "as = []",simp_all)
apply (case_tac a,simp_all,blast)
apply (case_tac i,simp_all)
apply (erule_tac x=0 in allE,simp)
apply (case_tac a,simp_all)
by blast
lemma P7_APP_ef:
"[| length xs = length as; distinct xs; length xs = length ms;
nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ;
def_nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
∀a∈set as. atom a;
dom E1 ∩ set xs = {}; fvs' as ⊆ dom Γ; dom Γ ⊆ dom E1;
SSet (fvs' as) Γ (E1, E2) (h, k) ∩ RSet (fvs' as) Γ (E1, E2) (h, k) = {} |]
==> SSet (set xs) (map_of (zip xs ms)) (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k))
(h, Suc k) ∩
RSet (set xs) (map_of (zip xs ms)) (map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k))
(h, Suc k) = {}"
apply (frule fvs_as_in_dom_E1,assumption+)
apply (frule SSet_APP_equals_SSet_ef
[where h="h" and k="k"],assumption+)
apply (frule RSet_APP_equals_RSet_ef
[where h="h" and k="k"],assumption+)
by blast
end
lemma P7_e1_dem1:
[| S1.0 = S1s ∪ S1r ∪ S1d; S1s ⊆ S; R1.0 ⊆ R; (S1r ∪ S1d) ∩ R1.0 = {};
S ∩ R = {} |]
==> S1.0 ∩ R1.0 = {}
lemma P7_e1_dem2:
SSet L1.0 Γ1.0 E h =
SSet1 L1.0 Γ1.0 Γ1.0\<triangleright>Γ2.0 L2.0 s'' E h ∪
SSet1 L1.0 Γ1.0 Γ1.0\<triangleright>Γ2.0 L2.0 d'' E h ∪
SSet1 L1.0 Γ1.0 Γ1.0\<triangleright>Γ2.0 L2.0 r'' E h
lemma P7_e1_dem3:
SSet1 L1.0 Γ1.0 Γ1.0\<triangleright>Γ2.0 L2.0 s'' E h
⊆ SSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 E h
lemma P7_e1_dem5:
dom Γ1.0 ⊆ dom E1.0
==> (SSet1 L1.0 Γ1.0 Γ1.0\<triangleright>Γ2.0 L2.0 d'' (E1.0, E2.0) (h, k) ∪
SSet1 L1.0 Γ1.0 Γ1.0\<triangleright>Γ2.0 L2.0 r'' (E1.0, E2.0) (h, k)) ∩
RSet L1.0 Γ1.0 (E1.0, E2.0) (h, k) ≠
{} -->
(∃x z. x ∈ dom E1.0 ∧
z ∈ L1.0 ∧
Γ1.0 z = Some d'' ∧
Γ1.0 x = Some s'' ∧
closure (E1.0, E2.0) x (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠ {})
lemma P7_e1_dem6:
[| shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k'); dom Γ1.0 ⊆ dom E1.0;
(SSet1 L1.0 Γ1.0 Γ1.0\<triangleright>Γ2.0 L2.0 d'' (E1.0, E2.0) (h, k) ∪
SSet1 L1.0 Γ1.0 Γ1.0\<triangleright>Γ2.0 L2.0 r'' (E1.0, E2.0) (h, k)) ∩
RSet L1.0 Γ1.0 (E1.0, E2.0) (h, k) ≠
{} -->
(∃x z. x ∈ dom E1.0 ∧
z ∈ L1.0 ∧
Γ1.0 z = Some d'' ∧
Γ1.0 x = Some s'' ∧
closure (E1.0, E2.0) x (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠
{}) |]
==> (SSet1 L1.0 Γ1.0 Γ1.0\<triangleright>Γ2.0 L2.0 d'' (E1.0, E2.0) (h, k) ∪
SSet1 L1.0 Γ1.0 Γ1.0\<triangleright>Γ2.0 L2.0 r'' (E1.0, E2.0) (h, k)) ∩
RSet L1.0 Γ1.0 (E1.0, E2.0) (h, k) =
{}
lemma P7_e1_dem4_1:
Γ1.0 x = Some d'' ==> Γ1.0\<triangleright>Γ2.0 L2.0 x = Some d''
lemma P7_e1_dem4_2:
xa ∈ live E L1.0 h ==> xa ∈ live E (L1.0 ∪ (L2.0 - {x1.0})) h
lemma P7_e1_dem4:
SSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k) ∩
RSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k) =
{}
==> RSet L1.0 Γ1.0 (E1.0, E2.0) (h, k)
⊆ RSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k)
lemma P7_LET_e1:
[| shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k'); dom Γ1.0 ⊆ dom E1.0;
SSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k) ∩
RSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k) =
{} |]
==> SSet L1.0 Γ1.0 (E1.0, E2.0) (h, k) ∩ RSet L1.0 Γ1.0 (E1.0, E2.0) (h, k) = {}
lemma P7_e2_dem1:
[| x1.0 ∉ L2.0 --> S2.0 ⊆ S;
x1.0 ∈ L2.0 --> S2.0 = S2' ∪ S2'x1.0 ∧ S2' ⊆ S ∧ S2'x1.0 ∩ R2.0 = {};
R2.0 ⊆ R; S ∩ R = {} |]
==> S2.0 ∩ R2.0 = {}
lemma demS2_2_x1_not_L2:
[| dom Γ1.0 ⊆ dom E1.0; def_disjointUnionEnv Γ2.0 [x1.0 |-> s''];
dom (Γ2.0 + [x1.0 |-> s'']) ⊆ dom (E1.0(x1.0 |-> v1.0));
def_pp Γ1.0 Γ2.0 L2.0; x1.0 ∉ L1.0;
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k') |]
==> x1.0 ∉ L2.0 -->
SSet L2.0 (Γ2.0 + [x1.0 |-> s'']) (E1.0(x1.0 |-> r), E2.0) (h', k')
⊆ SSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k)
lemma P7_e2_dem2_1:
[| def_disjointUnionEnv Γ2.0 [x1.0 |-> s'']; x1.0 ∈ L2.0 |]
==> SSet L2.0 (Γ2.0 + [x1.0 |-> s'']) (E1.0(x1.0 |-> r), E2.0) (h', k') =
SSet (L2.0 - {x1.0}) Γ2.0 (E1.0(x1.0 |-> r), E2.0) (h', k') ∪
SSet {x1.0} [x1.0 |-> s''] (E1.0(x1.0 |-> r), E2.0) (h', k')
lemma demS2_1_1b:
[| dom Γ1.0 ⊆ dom E1.0; L2.0 ⊆ dom (Γ2.0 + [x1.0 |-> s'']);
def_disjointUnionEnv Γ2.0 [x1.0 |-> s''];
dom (Γ2.0 + [x1.0 |-> s'']) ⊆ dom (E1.0(x1.0 |-> v1.0));
def_pp Γ1.0 Γ2.0 L2.0; x1.0 ∉ L1.0; x1.0 ∈ L2.0;
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k') |]
==> SSet (L2.0 - {x1.0}) Γ2.0 (E1.0(x1.0 |-> r), E2.0) (h', k')
⊆ SSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k)
lemma demS2_S2x1_subset_R2_aux:
[| closureL x (h', k') ∩ recReach (E1.0(x1.0 |-> r), E2.0) z (h', k') ≠ {};
x ∈ closure (E1.0(x1.0 |-> r), E2.0) x1.0 (h', k') |]
==> closure (E1.0(x1.0 |-> r), E2.0) x1.0 (h', k') ∩
recReach (E1.0(x1.0 |-> r), E2.0) z (h', k') ≠
{}
lemma demS2_S2x1_subset_R2:
[| dom Γ1.0 ⊆ dom E1.0; def_disjointUnionEnv Γ2.0 [x1.0 |-> s''];
dom (Γ2.0 + [x1.0 |-> s'']) ⊆ dom (E1.0(x1.0 |-> v1.0));
def_pp Γ1.0 Γ2.0 L2.0; x1.0 ∉ L1.0; x1.0 ∈ L2.0;
shareRec L2.0 (Γ2.0 + [x1.0 |-> s'']) (E1.0(x1.0 |-> r), E2.0) (h', k')
(hh, kk) |]
==> SSet {x1.0} [x1.0 |-> s''] (E1.0(x1.0 |-> r), E2.0) (h', k') ∩
RSet L2.0 (Γ2.0 + [x1.0 |-> s'']) (E1.0(x1.0 |-> r), E2.0) (h', k') =
{}
lemma demS2_2_x1_in_L2:
[| dom Γ1.0 ⊆ dom E1.0; x1.0 ∉ L1.0; L2.0 ⊆ dom (Γ2.0 + [x1.0 |-> s'']);
def_disjointUnionEnv Γ2.0 [x1.0 |-> s''];
dom (Γ2.0 + [x1.0 |-> s'']) ⊆ dom (E1.0(x1.0 |-> v1.0));
def_pp Γ1.0 Γ2.0 L2.0; shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k');
shareRec L2.0 (Γ2.0 + [x1.0 |-> s'']) (E1.0(x1.0 |-> r), E2.0) (h', k')
(hh, kk);
SSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k) ∩
RSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k) =
{} |]
==> x1.0 ∈ L2.0 -->
SSet L2.0 (Γ2.0 + [x1.0 |-> s'']) (E1.0(x1.0 |-> r), E2.0) (h', k') =
SSet (L2.0 - {x1.0}) Γ2.0 (E1.0(x1.0 |-> r), E2.0) (h', k') ∪
SSet {x1.0} [x1.0 |-> s''] (E1.0(x1.0 |-> r), E2.0) (h', k') ∧
SSet (L2.0 - {x1.0}) Γ2.0 (E1.0(x1.0 |-> r), E2.0) (h', k')
⊆ SSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k) ∧
SSet {x1.0} [x1.0 |-> s''] (E1.0(x1.0 |-> r), E2.0) (h', k') ∩
RSet L2.0 (Γ2.0 + [x1.0 |-> s'']) (E1.0(x1.0 |-> r), E2.0) (h', k') =
{}
lemma demR2_subseteq_R:
[| def_pp Γ1.0 Γ2.0 L2.0; L1.0 ⊆ dom Γ1.0; L2.0 ⊆ dom (Γ2.0 + [x1.0 |-> s'']);
dom (Γ2.0 + [x1.0 |-> s'']) ⊆ dom (E1.0(x1.0 |-> v1.0));
def_disjointUnionEnv Γ2.0 [x1.0 |-> s''];
shareRec L2.0 (Γ2.0 + [x1.0 |-> s'']) (E1.0(x1.0 |-> r), E2.0) (h', k')
(hh, kk);
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k') |]
==> RSet L2.0 (Γ2.0 + [x1.0 |-> s'']) (E1.0(x1.0 |-> r), E2.0) (h', k')
⊆ RSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k)
lemma P7_LET1_e2:
[| def_pp Γ1.0 Γ2.0 L2.0; L1.0 ⊆ dom Γ1.0; dom Γ1.0 ⊆ dom E1.0;
L2.0 ⊆ dom (Γ2.0 + [x1.0 |-> s'']); x1.0 ∉ L1.0;
def_disjointUnionEnv Γ2.0 [x1.0 |-> s''];
dom (Γ2.0 + [x1.0 |-> s'']) ⊆ dom (E1.0(x1.0 |-> v1.0));
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k');
shareRec L2.0 (Γ2.0 + [x1.0 |-> s'']) (E1.0(x1.0 |-> v1.0), E2.0) (h', k')
(hh, kk);
SSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k) ∩
RSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k) =
{} |]
==> SSet L2.0 (Γ2.0 + [x1.0 |-> s'']) (E1.0(x1.0 |-> v1.0), E2.0) (h', k') ∩
RSet L2.0 (Γ2.0 + [x1.0 |-> s'']) (E1.0(x1.0 |-> v1.0), E2.0) (h', k') =
{}
lemma P7_e2_let2_dem1:
[| x1.0 ∈ L2.0 --> R2.0 = R2'x1.0 ∪ R2d ∧ R2'x1.0 ∩ S2.0 = {} ∧ R2d ∩ S2.0 = {};
x1.0 ∉ L2.0 --> R2.0 ⊆ R; S2.0 ⊆ S; S ∩ R = {} |]
==> S2.0 ∩ R2.0 = {}
lemma P7_e2_let2_dem2:
[| def_disjointUnionEnv Γ2.0 [x1.0 |-> d'']; x1.0 ∈ L2.0 |]
==> RSet L2.0 (Γ2.0 + [x1.0 |-> d'']) (E1.0(x1.0 |-> v1.0), E2.0) (h', k') =
{p : live (E1.0(x1.0 |-> v1.0), E2.0) L2.0 (h', k').
closureL p (h', k') ∩ recReach (E1.0(x1.0 |-> v1.0), E2.0) x1.0 (h', k') ≠
{}} ∪
{p : live (E1.0(x1.0 |-> v1.0), E2.0) L2.0 (h', k').
∃z∈L2.0 - {x1.0}.
Γ2.0 z = Some d'' ∧
closureL p (h', k') ∩ recReach (E1.0(x1.0 |-> v1.0), E2.0) z (h', k') ≠
{}}
lemma P7_e2_let2_dem4:
[| dom (Γ2.0 + [x1.0 |-> d'']) ⊆ dom (E1.0(x1.0 |-> v1.0));
def_disjointUnionEnv Γ2.0 [x1.0 |-> d''];
shareRec L2.0 (Γ2.0 + [x1.0 |-> d'']) (E1.0(x1.0 |-> v1.0), E2.0) (h', k')
(hh, kk);
x1.0 ∈ L2.0 |]
==> {p : live (E1.0(x1.0 |-> v1.0), E2.0) L2.0 (h', k').
closureL p (h', k') ∩ recReach (E1.0(x1.0 |-> v1.0), E2.0) x1.0 (h', k') ≠
{}} ∩
SSet L2.0 (Γ2.0 + [x1.0 |-> d'']) (E1.0(x1.0 |-> v1.0), E2.0) (h', k') =
{}
lemma P7_e2_let2_dem10:
[| dom (Γ2.0 + [x1.0 |-> d'']) ⊆ dom (E1.0(x1.0 |-> v1.0));
shareRec L2.0 (Γ2.0 + [x1.0 |-> d'']) (E1.0(x1.0 |-> v1.0), E2.0) (h', k')
(hh, kk);
def_disjointUnionEnv Γ2.0 [x1.0 |-> d'']; x1.0 ∈ L2.0 |]
==> {p : live (E1.0(x1.0 |-> v1.0), E2.0) L2.0 (h', k').
∃z∈L2.0 - {x1.0}.
Γ2.0 z = Some d'' ∧
closureL p (h', k') ∩ recReach (E1.0(x1.0 |-> v1.0), E2.0) z (h', k') ≠
{}} ∩
SSet L2.0 (Γ2.0 + [x1.0 |-> d'']) (E1.0(x1.0 |-> v1.0), E2.0) (h', k') =
{}
lemma P7_e2_let2_dem7:
[| def_disjointUnionEnv Γ2.0 [x1.0 |-> d''];
dom (Γ2.0 + [x1.0 |-> d'']) ⊆ dom (E1.0(x1.0 |-> v1.0));
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k'); def_pp Γ1.0 Γ2.0 L2.0 |]
==> SSet L2.0 (Γ2.0 + [x1.0 |-> d'']) (E1.0(x1.0 |-> v1.0), E2.0) (h', k')
⊆ SSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k)
lemma P7_e2_let2_dem8:
[| def_pp Γ1.0 Γ2.0 L2.0; L1.0 ⊆ dom Γ1.0; L2.0 ⊆ dom (Γ2.0 + [x1.0 |-> d'']);
dom (Γ2.0 + [x1.0 |-> d'']) ⊆ dom (E1.0(x1.0 |-> v1.0));
def_disjointUnionEnv Γ2.0 [x1.0 |-> d''];
shareRec L2.0 (Γ2.0 + [x1.0 |-> d'']) (E1.0(x1.0 |-> r), E2.0) (h', k')
(hh, kk);
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k'); x1.0 ∉ L2.0 |]
==> RSet L2.0 (Γ2.0 + [x1.0 |-> d'']) (E1.0(x1.0 |-> r), E2.0) (h', k')
⊆ RSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k)
lemma P7_LET2_e2:
[| def_pp Γ1.0 Γ2.0 L2.0; L1.0 ⊆ dom Γ1.0; dom Γ1.0 ⊆ dom E1.0;
L2.0 ⊆ dom (Γ2.0 + [x1.0 |-> d'']); x1.0 ∉ L1.0;
def_disjointUnionEnv Γ2.0 [x1.0 |-> d''];
dom (Γ2.0 + [x1.0 |-> d'']) ⊆ dom (E1.0(x1.0 |-> v1.0));
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k');
shareRec L2.0 (Γ2.0 + [x1.0 |-> d'']) (E1.0(x1.0 |-> v1.0), E2.0) (h', k')
(hh, kk);
SSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k) ∩
RSet (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k) =
{} |]
==> SSet L2.0 (Γ2.0 + [x1.0 |-> d'']) (E1.0(x1.0 |-> v1.0), E2.0) (h', k') ∩
RSet L2.0 (Γ2.0 + [x1.0 |-> d'']) (E1.0(x1.0 |-> v1.0), E2.0) (h', k') =
{}
lemma dom_foldl_monotone_list:
dom (foldl op ⊗ (empty ⊗ x) xs) = dom x ∪ dom (foldl op ⊗ empty xs)
lemma dom_restrict_neg_map:
dom (restrict_neg_map m A) = dom m - dom m ∩ A
lemma x_notin_Γ_cased:
x ∉ dom (foldl op ⊗ empty
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
lemma Γ_case_x_is_d:
Γ = foldl op ⊗ empty
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert))) +
[x |-> d'']
==> Γ x = Some d''
lemma restrict_neg_map_m:
[| G y = Some m; x ≠ y; y ∉ L |] ==> restrict_neg_map G (insert x L) y = Some m
lemma disjointUnionEnv_G_G'_G_x:
[| x ∉ dom G'; def_disjointUnionEnv G G' |] ==> (G + G') x = G x
lemma dom_Γi_in_Γcased_2:
[| 0 < length assert; x ≠ y; length assert = length alts; i < length alts;
y ∈ dom (snd (assert ! i)); y ∉ set (snd (extractP (fst (alts ! i)))) |]
==> y ∈ dom (foldl op ⊗ empty
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
lemma Otimes_prop4:
[| 0 < length assert; y ≠ x; length assert = length alts;
def_nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert)));
def_disjointUnionEnv
(foldl op ⊗ empty
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
[x |-> d''];
i < length alts; y ∈ dom (snd (assert ! i)); snd (assert ! i) y = Some m;
y ∉ set (snd (extractP (fst (alts ! i)))) |]
==> (foldl op ⊗ empty
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert))) +
[x |-> d''])
y =
Some m
lemma closureL_p_None_p:
closureL p (h(p := None), k) = {p}
lemma recReachL_p_None_p:
recReachL p (h(p := None), k) = {p}
lemma closure_extend_p_None_subseteq_closure:
[| E1.0 x = Some (Loc p);
E1.0 x = extend E1.0 (snd (extractP (fst (alts ! i)))) vs x |]
==> closure (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) x
(h(p := None), k)
⊆ closure (E1.0, E2.0) x (h, k)
lemma recReach_extend_p_None_subseteq_recReach:
[| E1.0 x = Some (Loc p);
E1.0 x = extend E1.0 (snd (extractP (fst (alts ! i)))) vs x |]
==> recReach (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) x
(h(p := None), k)
⊆ recReach (E1.0, E2.0) x (h, k)
lemma descendants_p_None_q:
[| d ∈ descendants q (h(p := None), k); q ≠ p |] ==> d ∈ descendants q (h, k)
lemma recDescendants_p_None_q:
[| d ∈ recDescendants q (h(p := None), k); q ≠ p |]
==> d ∈ recDescendants q (h, k)
lemma closureL_p_None_subseteq_closureL:
p ≠ q ==> closureL q (h(p := None), k) ⊆ closureL q (h, k)
lemma recReachL_p_None_subseteq_recReachL:
p ≠ q ==> recReachL q (h(p := None), k) ⊆ recReachL q (h, k)
lemma closure_p_None_subseteq_closure:
[| E1.0 x = Some (Loc p); E1.0 y = Some (Loc q); p ≠ q;
E1.0 y = extend E1.0 (snd (extractP (fst (alts ! i)))) vs y;
w ∈ closure (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) y
(h(p := None), k) |]
==> w ∈ closure (E1.0, E2.0) y (h, k)
lemma recReach_p_None_subseteq_recReach:
[| E1.0 x = Some (Loc p); E1.0 y = Some (Loc q); p ≠ q;
E1.0 y = extend E1.0 (snd (extractP (fst (alts ! i)))) vs y;
w ∈ recReach (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) y
(h(p := None), k) |]
==> w ∈ recReach (E1.0, E2.0) y (h, k)
lemma closureV_subseteq_closureL:
h p = Some (j, C, vs)
==> (UN i<length vs. closureV (vs ! i) (h, k)) ⊆ closureL p (h, k)
lemma vs_defined:
[| set xs ∩ dom E1.0 = {}; length xs = length vs; y ∈ set xs;
extend E1.0 xs vs y = Some (Loc q) |]
==> ∃j<length vs. vs ! j = Loc q
lemma closure_Loc_subseteq_closureV_Loc:
[| vs ! i = Loc q; i < length vs |]
==> closureL q (h, k) ⊆ (UN i<length vs. closureV (vs ! i) (h, k))
lemma patrones:
[| E1.0 x = Some (Loc p); h p = Some (j, C, vs); i < length alts;
0 < length alts; length assert = length alts;
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
y ∈ set (snd (extractP (fst (alts ! i)))) |]
==> closure (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) y (h, k)
⊆ closure (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) x (h, k)
lemma patrones_2:
[| E1.0 x = Some (Loc p); h p = Some (j, C, vs);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs; i < length alts;
0 < length alts; length assert = length alts;
y ∈ set (snd (extractP (fst (alts ! i)))) |]
==> closure (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) y
(h(p := None), k)
⊆ {p}
lemma dom_extend_in_E1_or_xs:
[| y ∈ dom (extend E1.0 xs vs); length xs = length vs |]
==> y ∈ dom E1.0 ∨ y ∈ set xs
lemma extend_monotone_x_in_dom_E1_2:
[| set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
length assert = length alts; i < length alts; x ∈ fst (assert ! i);
x ∈ dom E1.0 |]
==> E1.0 x = extend E1.0 (snd (extractP (fst (alts ! i)))) vs x
lemma closure_extend_None_subset_closure:
[| alts ≠ []; i < length alts; length assert = length alts;
E1.0 x = Some (Loc p); h p = Some (j, C, vs);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs; y ∈ fst (assert ! i);
y ∉ set (snd (extractP (fst (alts ! i)))); y ∈ dom E1.0;
q ∈ closure (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) y
(h(p := None), k) |]
==> q ∈ closure (E1.0, E2.0) y (h, k)
lemma recReach_extend_None_subset_recReach:
[| alts ≠ []; i < length alts; length assert = length alts;
E1.0 x = Some (Loc p); h p = Some (j, C, vs);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs; y ∈ fst (assert ! i);
y ∉ set (snd (extractP (fst (alts ! i)))); y ∈ dom E1.0;
q ∈ recReach (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) y
(h(p := None), k) |]
==> q ∈ recReach (E1.0, E2.0) y (h, k)
lemma closure_monotone_extend_3:
[| set (snd (extractP (fst (alts ! i)))) ∩ dom E = {};
length (snd (extractP (fst (alts ! i)))) = length vs; x ∈ dom E;
0 < length alts; i < length alts |]
==> closure (E, E') x (h, k) =
closure (extend E (snd (extractP (fst (alts ! i)))) vs, E') x (h, k)
lemma recReach_monotone_extend_3:
[| set (snd (extractP (fst (alts ! i)))) ∩ dom E = {};
length (snd (extractP (fst (alts ! i)))) = length vs; x ∈ dom E;
0 < length alts; i < length alts |]
==> recReach (E, E') x (h, k) =
recReach (extend E (snd (extractP (fst (alts ! i)))) vs, E') x (h, k)
lemma pp12:
[| xa ∈ closure (E1.0, E2.0) xaa (h, k); xb ∈ closureL xa (h, k);
xb ∈ recReach (E1.0, E2.0) z (h, k) |]
==> closure (E1.0, E2.0) xaa (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠ {}
lemma P7_case_dem1:
[| Si = S'i ∪ S''i; Ri = R'i ∪ R''i; S'i ⊆ S; R'i ⊆ R;
Γ x = Some s'' --> S''i ⊆ S ∧ R''i = {};
Γ x ≠ Some s'' --> S''i ∩ R'i = {} ∧ R''i = {}; S ∩ R = {} |]
==> Si ∩ Ri = {}
lemma P7_case_dem1_1:
[| length assert = length alts; i < length assert |]
==> SSet (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k) =
SSet (fst (assert ! i) ∩
insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(snd (assert ! i)) (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h, k) ∪
SSet (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h, k)
lemma P7_case_dem1_2:
[| length assert = length alts; i < length assert |]
==> RSet (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k) =
RSet2
(fst (assert ! i) ∩
insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k) ∪
RSet2 (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k)
lemma P7_case_dem1_3:
[| ∀i<length assert.
∀x∈set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
∀i<length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
∀i<length alts.
x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
dom (snd (assert ! i))
⊆ dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
def_nonDisjointUnionEnvList (map snd assert);
∀i<length alts.
∀j<length alts.
i ≠ j -->
fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j)))) = {};
0 < length assert; x ∈ dom (nonDisjointUnionEnvList (map snd assert));
E1.0 x = Some (Loc p); length assert = length alts; i < length assert |]
==> SSet (fst (assert ! i) ∩
insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(snd (assert ! i)) (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h, k)
⊆ SSet (insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1.0, E2.0) (h, k)
lemma P7_case_dem1_4:
[| ∀i<length assert.
∀x∈set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
∀i<length alts.
x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
∀i<length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
dom (snd (assert ! i))
⊆ dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
∀i<length alts.
∀j<length alts.
i ≠ j -->
fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j)))) = {};
def_nonDisjointUnionEnvList (map snd assert); 0 < length assert;
x ∈ dom (nonDisjointUnionEnvList (map snd assert)); E1.0 x = Some (Loc p);
h p = Some (j, C, vs); length assert = length alts; i < length assert |]
==> RSet2
(fst (assert ! i) ∩
insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k)
⊆ RSet (insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1.0, E2.0) (h, k)
lemma P7_case_dem1_5_1:
[| E1.0 x = Some (Loc p); h p = Some (j, C, vs);
∀i<length alts.
x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
foldl op ⊗ empty (map snd assert) x = Some s'';
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs; 0 < length assert;
length assert = length alts; i < length assert |]
==> SSet (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h, k)
⊆ SSet (insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1.0, E2.0) (h, k)
lemma P7_case_dem1_5_2:
[| foldl op ⊗ empty (map snd assert) x = Some s'';
∀i<length assert.
∀x∈set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
length assert = length alts; i < length assert |]
==> RSet2 (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k) =
{}
lemma P7_case_dem1_6_1:
[| foldl op ⊗ empty (map snd assert) x ≠ Some s'';
shareRec (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k) (hh, k);
∀i<length alts.
x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
∀i<length assert.
∀x∈set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
∀i<length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
def_nonDisjointUnionEnvList (map snd assert);
x ∈ dom (nonDisjointUnionEnvList (map snd assert)); E1.0 x = Some (Loc p);
0 < length assert; length assert = length alts; i < length assert |]
==> SSet (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h, k) ∩
RSet2
(fst (assert ! i) ∩
insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k) =
{}
lemma P7_case_dem1_6_2:
[| ∀i<length assert.
∀x∈set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
i < length assert; length assert = length alts |]
==> RSet2 (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k) =
{}
lemma P7_CASE:
[| length assert = length alts;
∀i<length assert.
∀x∈set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
∀i<length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
dom (snd (assert ! i))
⊆ dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
∀i<length alts.
∀j<length alts.
i ≠ j -->
fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j)))) = {};
∀i<length alts.
x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
shareRec (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k) (hh, k);
def_nonDisjointUnionEnvList (map snd assert); E1.0 x = Some (Loc p);
h p = Some (j, C, vs); x ∈ dom (nonDisjointUnionEnvList (map snd assert));
0 < length assert;
SSet (insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1.0, E2.0) (h, k) ∩
RSet (insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1.0, E2.0) (h, k) =
{};
i < length assert |]
==> SSet (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k) ∩
RSet (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k) =
{}
lemma P7_casel_dem1:
[| Si = S'i ∪ S''i; Ri = R'i ∪ R''i; S'i ⊆ S; R'i ⊆ R;
Γ x = Some s'' --> S''i ⊆ S ∧ R''i = {};
Γ x ≠ Some s'' --> S''i ∩ R'i = {} ∧ R''i = {}; S ∩ R = {} |]
==> Si ∩ Ri = {}
lemma P7_casel_dem1_1:
[| length assert = length alts; i < length assert |]
==> SSet (fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k) =
SSet (fst (assert ! i) ∩
insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(snd (assert ! i)) (E1.0, E2.0) (h, k) ∪
SSet (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (E1.0, E2.0) (h, k)
lemma P7_casel_dem1_2:
[| length assert = length alts; i < length assert |]
==> RSet (fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k) =
RSet2
(fst (assert ! i) ∩
insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k) ∪
RSet2 (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k)
lemma P7_casel_dem1_3:
[| def_nonDisjointUnionEnvList (map snd assert); 0 < length assert;
x ∈ dom (nonDisjointUnionEnvList (map snd assert));
length assert = length alts; i < length assert |]
==> SSet (fst (assert ! i) ∩
insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(snd (assert ! i)) (E1.0, E2.0) (h, k)
⊆ SSet (insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1.0, E2.0) (h, k)
lemma P7_casel_dem1_4:
[| ∀i<length alts.
x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
fst (assert ! i) ⊆ dom (snd (assert ! i)); dom (snd (assert ! i)) ⊆ dom E1.0;
def_nonDisjointUnionEnvList (map snd assert); 0 < length assert;
E1.0 x = Some aa ∧ aa = IntT n ∧ fst (alts ! i) = ConstP (LitN n) ∨
E1.0 x = Some aa ∧ aa = BoolT b ∧ fst (alts ! i) = ConstP (LitB b);
x ∈ dom (nonDisjointUnionEnvList (map snd assert));
length assert = length alts; i < length assert |]
==> RSet2
(fst (assert ! i) ∩
insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k)
⊆ RSet (insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1.0, E2.0) (h, k)
lemma P7_casel_dem1_5_1:
[| E1.0 x = Some aa ∧ aa = IntT n ∧ fst (alts ! i) = ConstP (LitN n) ∨
E1.0 x = Some aa ∧ aa = BoolT b ∧ fst (alts ! i) = ConstP (LitB b);
0 < length assert; length assert = length alts; i < length assert |]
==> SSet (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (E1.0, E2.0) (h, k)
⊆ SSet (insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (E1.0, E2.0) (h, k)
lemma P7_casel_dem1_5_2:
[| foldl op ⊗ empty (map snd assert) x = Some s'';
E1.0 x = Some aa ∧ aa = IntT n ∧ fst (alts ! i) = ConstP (LitN n) ∨
E1.0 x = Some aa ∧ aa = BoolT b ∧ fst (alts ! i) = ConstP (LitB b);
length assert = length alts; i < length assert |]
==> RSet2 (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k) =
{}
lemma P7_casel_dem1_6_1:
[| foldl op ⊗ empty (map snd assert) x ≠ Some s'';
E1.0 x = Some aa ∧ aa = IntT n ∧ fst (alts ! i) = ConstP (LitN n) ∨
E1.0 x = Some aa ∧ aa = BoolT b ∧ fst (alts ! i) = ConstP (LitB b);
0 < length assert; length assert = length alts; i < length assert |]
==> SSet (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (E1.0, E2.0) (h, k) ∩
RSet2
(fst (assert ! i) ∩
insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k) =
{}
lemma P7_casel_dem1_6_2:
[| E1.0 x = Some aa ∧ aa = IntT n ∧ fst (alts ! i) = ConstP (LitN n) ∨
E1.0 x = Some aa ∧ aa = BoolT b ∧ fst (alts ! i) = ConstP (LitB b);
0 < length assert; i < length assert; length assert = length alts |]
==> RSet2 (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k) =
{}
lemma P7_CASEL:
[| ∀i<length alts.
x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
x ∈ dom (nonDisjointUnionEnvList (map snd assert));
dom (nonDisjointUnionEnvList (map snd assert)) ⊆ dom E1.0;
E1.0 x = Some aa ∧ aa = IntT n ∧ fst (alts ! i) = ConstP (LitN n) ∨
E1.0 x = Some aa ∧ aa = BoolT b ∧ fst (alts ! i) = ConstP (LitB b);
i < length alts; 0 < length assert;
def_nonDisjointUnionEnvList (map snd assert); 0 < length (map snd assert);
length assert = length alts; fst (assert ! i) ⊆ dom (snd (assert ! i));
SSet ((UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪
{x})
(nonDisjointUnionEnvList (map snd assert)) (E1.0, E2.0) (h, k) ∩
RSet ((UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪
{x})
(nonDisjointUnionEnvList (map snd assert)) (E1.0, E2.0) (h, k) =
{};
dom (snd (assert ! i)) ⊆ dom E1.0 |]
==> SSet (fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k) ∩
RSet (fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k) =
{}
lemma P7_cased_dem1:
[| Si = S'i ∪ S''i; Ri = R'i ∪ R''i; S'i ⊆ S; R'i ⊆ R; S''i ∩ Ri = {};
S'i ∩ R''i = {}; S ∩ R = {} |]
==> Si ∩ Ri = {}
lemma P7_cased_dem1_1:
[| length assert = length alts; i < length assert |]
==> SSet (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h(p := None), k) =
SSet (fst (assert ! i) ∩
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(snd (assert ! i)) (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h(p := None), k) ∪
SSet (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h(p := None), k)
lemma P7_cased_dem1_2:
[| length assert = length alts; i < length assert |]
==> RSet (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h(p := None), k) =
RSet2
(fst (assert ! i) ∩
insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h(p := None), k) ∪
RSet2 (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h(p := None), k)
lemma P7_cased_dem1_3:
[| 0 < length assert; E1.0 x = Some (Loc p); h p = Some (j, C, vs);
∀z∈dom Γ. Γ z ≠ Some s'' --> (∀i<length alts. z ∉ fst (assert ! i));
Γ = nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (set Li ∪ {x}))
(zip (map (snd o extractP o fst) alts) (map snd assert))) +
[x |-> d''];
∀i<length alts.
∀j<length alts.
i ≠ j -->
fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j)))) = {};
def_nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert)));
def_disjointUnionEnv
(nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (set Li ∪ {x}))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
[x |-> d''];
shareRec
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (E1.0, E2.0) (h, k) (hh, k);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
dom (snd (assert ! i))
⊆ dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs);
length assert = length alts; i < length assert |]
==> SSet (fst (assert ! i) ∩
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(snd (assert ! i)) (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h(p := None), k)
⊆ SSet ((UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪
{x})
Γ (E1.0, E2.0) (h, k)
lemma P7_cased_dem1_4:
[| 0 < length assert; E1.0 x = Some (Loc p); h p = Some (j, C, vs);
Γ = nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (set Li ∪ {x}))
(zip (map (snd o extractP o fst) alts) (map snd assert))) +
[x |-> d''];
def_nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert)));
def_disjointUnionEnv
(nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (set Li ∪ {x}))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
[x |-> d''];
∀i<length alts.
∀j<length alts.
i ≠ j -->
fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j)))) = {};
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
dom (snd (assert ! i))
⊆ dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs);
∀i<length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
length assert = length alts; i < length assert |]
==> RSet2
(fst (assert ! i) ∩
insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h(p := None), k)
⊆ RSet ((UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪
{x})
Γ (E1.0, E2.0) (h, k)
lemma P7_cased_dem1_5:
[| 0 < length assert; length assert = length alts;
shareRec (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h(p := None), k)
(hh, k);
dom (snd (assert ! i))
⊆ dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs);
∀i<length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
i < length assert |]
==> SSet (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(snd (assert ! i)) (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h(p := None), k) ∩
RSet (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h(p := None), k) =
{}
lemma P7_cased_dem1_6:
[| E1.0 x = Some (Loc p); h p = Some (j, C, vs);
Γ = nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (set Li ∪ {x}))
(zip (map (snd o extractP o fst) alts) (map snd assert))) +
[x |-> d''];
i < length alts; length assert = length alts;
shareRec (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h(p := None), k)
(hh, k);
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
length (snd (extractP (fst (alts ! i)))) = length vs;
dom (snd (assert ! i))
⊆ dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs);
∀i<length assert. fst (assert ! i) ⊆ dom (snd (assert ! i)) |]
==> SSet (fst (assert ! i) ∩
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(snd (assert ! i)) (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h(p := None), k) ∩
RSet2 (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! i)))))
(fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h(p := None), k) =
{}
lemma P7_CASED:
[| Γ = nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (set Li ∪ {x}))
(zip (map (snd o extractP o fst) alts) (map snd assert))) +
[x |-> d''];
set (snd (extractP (fst (alts ! i)))) ∩ dom E1.0 = {};
def_nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert)));
def_disjointUnionEnv
(nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (set Li ∪ {x}))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
[x |-> d''];
length (snd (extractP (fst (alts ! i)))) = length vs;
∀i<length assert. fst (assert ! i) ⊆ dom (snd (assert ! i));
dom (snd (assert ! i))
⊆ dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs);
shareRec (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h(p := None), k)
(hh, k);
∀z∈dom Γ. Γ z ≠ Some s'' --> (∀i<length alts. z ∉ fst (assert ! i));
∀i<length alts.
∀j<length alts.
i ≠ j -->
fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j)))) = {};
E1.0 x = Some (Loc p); h p = Some (j, C, vs); i < length alts;
0 < length (map snd assert); length assert = length alts;
∀i<length alts.
∀j. ∀x∈set (snd (extractP (fst (alts ! i)))).
snd (assert ! i) x = Some d'' --> j ∈ RecPos Ci;
shareRec
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (E1.0, E2.0) (h, k) (hh, k);
SSet ((UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪
{x})
Γ (E1.0, E2.0) (h, k) ∩
RSet ((UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪
{x})
Γ (E1.0, E2.0) (h, k) =
{} |]
==> SSet (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h(p := None), k) ∩
RSet (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
(h(p := None), k) =
{}
lemma nth_map_of_xs_atom2val:
[| length xs = length as; distinct xs |]
==> ∀i<length xs.
map_of (zip xs (map (atom2val E1.0) as)) (xs ! i) =
Some (atom2val E1.0 (as ! i))
lemma closureL_k_equals_closureL_Suc_k:
closureL p (h, Suc k) = closureL p (h, k)
lemma recReachL_k_equals_recReachL_Suc_k:
recReachL x (h, k) = recReachL x (h, Suc k)
lemma closure_APP_equals_closure_ef:
[| length xs = length as; distinct xs; distinct xs;
∀i<length as. ∀x a. as ! i = VarE x a --> x ∈ dom E1.0; i < length as;
as ! i = VarE xa a |]
==> closure (E1.0, E2.0) xa (h, k) =
closure
(map_of (zip xs (map (atom2val E1.0) as)),
map_of (zip rs (map (the o E2.0) rs'))(self |-> Suc k))
(xs ! i) (h, Suc k)
lemma recReach_APP_equals_recReach_ef:
[| i < length as; as ! i = VarE z a;
∀i<length as. ∀x a. as ! i = VarE x a --> x ∈ dom E1.0;
length xs = length as; distinct xs |]
==> recReach (E1.0, E2.0) z (h, k) =
recReach
(map_of (zip xs (map (atom2val E1.0) as)),
map_of (zip rs (map (the o E2.0) rs'))(self |-> Suc k))
(xs ! i) (h, Suc k)
lemma closureL_recReach_APP_equals_closureL_recReach_ef:
[| z ∈ fvs' as; i < length as; as ! i = VarE z a;
∀i<length as. ∀x a. as ! i = VarE x a --> x ∈ dom E1.0;
length xs = length as; distinct xs |]
==> closureL x (h, k) ∩ recReach (E1.0, E2.0) z (h, k) =
closureL x (h, Suc k) ∩
recReach
(map_of (zip xs (map (atom2val E1.0) as)),
map_of (zip rs (map (the o E2.0) rs'))(self |-> Suc k))
(xs ! i) (h, Suc k)
lemma nth_set_distinct:
[| x ∈ set xs; distinct xs |] ==> ∃i<length xs. xs ! i = x
lemma nth_map_add_map_of_y:
[| i < length xs; ms ! i = y; length xs = length ms; distinct xs |]
==> map_of (zip xs ms) (xs ! i) = Some y
lemma nth_map_add_map_of:
[| i < length xs; length xs = length ms; distinct xs |]
==> map_of (zip xs ms) (xs ! i) = Some (ms ! i)
lemma map_add_map_of:
[| x ∈ set xs; dom E1.0 ∩ set xs = {}; length xs = length ys |]
==> (E1.0 ++ map_of (zip xs ys)) x = map_of (zip xs ys) x
lemma var_in_fvs:
[| i < length as; as ! i = VarE x a |] ==> x ∈ fvs' as
lemma atom_fvs_VarE:
[| ∀a∈set as. atom a; xa ∈ fvs' as |] ==> ∃i<length as. ∃a. as ! i = VarE xa a
lemma live_APP_equals_live_ef:
[| ∀a∈set as. atom a; length xs = length as; length xs = length ms;
dom E1.0 ∩ set xs = {}; distinct xs;
∀i<length as. ∀x a. ∃y. as ! i = VarE x a --> x ∈ dom E1.0 |]
==> live (E1.0, E2.0) (fvs' as) (h, k) =
live (map_of (zip xs (map (atom2val E1.0) as)),
map_of (zip rs (map (the o E2.0) rs'))(self |-> Suc k))
(set xs) (h, Suc k)
lemma map_le_nonDisjointUnionSafeEnvList:
[| nonDisjointUnionSafeEnvList Γs x = Some y;
nonDisjointUnionSafeEnvList Γs ⊆m Γ' |]
==> Γ' x = Some y
lemma nonDisjointUnionSafeEnv_assoc:
G1.0 ⊕ G2.0 ⊕ G3.0 = G1.0 ⊕ (G2.0 ⊕ G3.0)
lemma foldl_nonDisjointUnionSafeEnv_prop:
foldl op ⊕ (G' ⊕ G) Gs = G' ⊕ foldl op ⊕ G Gs
lemma nonDisjointUnionSafeEnv_empty:
empty ⊕ x = x
lemma nonDisjointUnionSafeEnv_conmutative:
def_nonDisjointUnionSafeEnv G G' ==> G ⊕ G' = G' ⊕ G
lemma nth_nonDisjointUnionSafeEnvList:
[| length xs = length ms;
def_nonDisjointUnionSafeEnvList (maps_of (zip xs ms)) |]
==> ∀i<length xs.
nonDisjointUnionSafeEnvList (maps_of (zip xs ms)) (xs ! i) =
Some (ms ! i)
lemma union_dom_nonDisjointUnionSafeEnv:
dom (A ⊕ B) = dom A ∪ dom B
lemma dom_foldl_nonDisjointUnionSafeEnv_monotone:
dom (foldl op ⊕ (empty ⊕ x) xs) = dom x ∪ dom (foldl op ⊕ empty xs)
lemma dom_nonDisjointUnionSafeEnvList_fvs:
[| ∀a∈set xs. atom a; length xs = length ys |]
==> fvs' xs
⊆ dom (nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var xs) ys)))
lemma nonDisjointUnionSafeEnvList_prop1:
[| nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ;
xa ∈ fvs' as; Γ xa = Some y;
def_nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
∀a∈set as. atom a; length as = length ms |]
==> ∃i<length as. ∃a. as ! i = VarE xa a ∧ ms ! i = y
lemma xs_ms_in_set:
[| length ms = length as; length xs = length as; distinct xs; i < length as;
as ! i = VarE xa a; ms ! i = m |]
==> (xs ! i, m) ∈ set (zip xs ms)
lemma xs_ms_in_set_ms:
[| length ms = length as; length xs = length as; distinct xs; i < length xs;
(xs ! i, m) ∈ set (zip xs ms) |]
==> ms ! i = m
lemma SSet_APP_equals_SSet_ef:
[| def_nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ;
length xs = length as; length xs = length ms; distinct xs; ∀a∈set as. atom a;
dom E1.0 ∩ set xs = {}; fvs' as ⊆ dom Γ; dom Γ ⊆ dom E1.0;
∀i<length as. ∀x a. as ! i = VarE x a --> x ∈ dom E1.0 |]
==> SSet (fvs' as) Γ (E1.0, E2.0) (h, k) =
SSet (set xs) (map_of (zip xs ms))
(map_of (zip xs (map (atom2val E1.0) as)),
map_of (zip rs (map (the o E2.0) rs'))(self |-> Suc k))
(h, Suc k)
lemma RSet_APP_equals_RSet_ef:
[| def_nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ;
∀a∈set as. atom a; length xs = length as;
∀i<length as. ∀x a. as ! i = VarE x a --> x ∈ dom E1.0;
length xs = length ms; dom E1.0 ∩ set xs = {}; distinct xs |]
==> RSet (fvs' as) Γ (E1.0, E2.0) (h, k) =
RSet (set xs) (map_of (zip xs ms))
(map_of (zip xs (map (atom2val E1.0) as)),
map_of (zip rs (map (the o E2.0) rs'))(self |-> Suc k))
(h, Suc k)
lemma fvs_as_in_dom_E1:
[| fvs' as ⊆ dom Γ; dom Γ ⊆ dom E1.0 |]
==> ∀i<length as. ∀x a. as ! i = VarE x a --> x ∈ dom E1.0
lemma P7_APP_ef:
[| length xs = length as; distinct xs; length xs = length ms;
nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ;
def_nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
∀a∈set as. atom a; dom E1.0 ∩ set xs = {}; fvs' as ⊆ dom Γ; dom Γ ⊆ dom E1.0;
SSet (fvs' as) Γ (E1.0, E2.0) (h, k) ∩ RSet (fvs' as) Γ (E1.0, E2.0) (h, k) =
{} |]
==> SSet (set xs) (map_of (zip xs ms))
(map_of (zip xs (map (atom2val E1.0) as)),
map_of (zip rs (map (the o E2.0) rs'))(self |-> Suc k))
(h, Suc k) ∩
RSet (set xs) (map_of (zip xs ms))
(map_of (zip xs (map (atom2val E1.0) as)),
map_of (zip rs (map (the o E2.0) rs'))(self |-> Suc k))
(h, Suc k) =
{}