Up to index of Isabelle/HOL/CoreSafe
theory SafeDAss_P5_P6(* Title: Safe DAss P5
Author: Javier de Dios and Ricardo Peņa
Copyright: March 2008, Universidad Complutense de Madrid
*)
header {* Derived Assertions. P5. shareRec L $\Gamma$ E h.
P6. $\neg$ identityClosure *}
theory SafeDAss_P5_P6 imports SafeDAssBasic
SafeRegion_definitions
BasicFacts
begin
text{*
Lemma for REUSE
*}
lemma P5_REUSE:
"[| Γ x = Some d'';
wellFormed {x} Γ (ReuseE x ());
(E1, E2) \<turnstile> h , k , td , ReuseE x () \<Down> h(p := None)(q \<mapsto> c) , k , Loc q , r ;
dom Γ ⊆ dom E1; E1 x = Some (Loc p)|]
==> ∀xa∈dom E1.
closure (E1, E2) xa (h, k) ∩ recReach (E1, E2) x (h, k) ≠ {}
--> xa ∈ dom Γ ∧ Γ xa ≠ Some s''"
apply (simp only: wellFormed_def)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="td" in allE)
apply (erule_tac x="h(p := None)(q \<mapsto> c)" in allE)
apply (erule_tac x="Loc q" in allE)
apply (erule_tac x="r" in allE)
apply (rule ballI, rule impI)
apply (rename_tac y)
apply (drule mp,simp, simp add: dom_def)
apply (erule_tac x="y" in ballE)
prefer 2 apply force
apply (erule_tac x="x" in ballE)
prefer 2 apply blast
by simp
lemma reuse_identityClosure_y_in_E1:
"[| (E1, E2) \<turnstile> h , k , td , ReuseE x () \<Down> h(p := None)(q \<mapsto> c) , k , Loc q , r ;
p ∉ closure (E1,E2) y (h,k); h p = Some c; fresh q h |]
==> identityClosure (E1, E2) y (h, k) (h(p := None)(q \<mapsto> c), k)"
(* p ≠ q *)
apply (subgoal_tac "p≠q")
prefer 2 apply (simp add: fresh_def, blast)
(* unfold identityClosure def*)
apply (simp add: identityClosure_def)
apply (simp add: closure_def)
apply (case_tac "E1 y", simp_all)
apply (case_tac a, simp_all)
apply clarsimp
apply (rename_tac w)
apply (case_tac "w = p")
(* w = p *)
apply (subgoal_tac "p ∈ closureL p (h,k)",simp)
apply (rule closureL_basic)
(* w ≠ p *)
apply (frule semantic_no_capture_E1_fresh_2,simp)
(* w ≠ q *)
apply (erule_tac x=y in ballE)
prefer 2 apply force
apply (erule_tac x=w in allE,simp)
apply (rule conjI)
apply (rule equalityI)
(* closureL w (h, k) ⊆ closureL w (h(p := None)(q \<mapsto> c), k) *)
apply (rule subsetI)
apply (erule closureL.induct)
apply (rule closureL_basic)
apply (subgoal_tac "qa ≠ q")
apply (rule closureL_step,simp)
apply (simp add: descendants_def)
apply (case_tac "h qa",simp_all)
apply force
apply force
(* closureL w (h(p := None)(q \<mapsto> c), k) ⊆ closureL w (h, k) *)
apply (rule subsetI)
apply (erule closureL.induct)
apply (rule closureL_basic)
apply (rule closureL_step,simp)
apply (subgoal_tac "qa ≠ q")
apply (subgoal_tac "qa ≠ p")
apply (simp add: descendants_def)
apply force
apply force
by force
lemma P6_REUSE:
"[| Γ x = Some d''; h p = Some c; fresh q h;
wellFormed {x} Γ (ReuseE x ());
(E1, E2) \<turnstile> h , k , td , ReuseE x () \<Down> h(p := None)(q \<mapsto> c) , k , Loc q , r ;
dom Γ ⊆ dom E1; E1 x = Some (Loc p)|]
==> ∀x∈dom E1.
¬ identityClosure (E1, E2) x (h, k) (h(p := None)(q \<mapsto> c), k)
--> x ∈ dom Γ ∧ Γ x ≠ Some s''"
apply (rule ballI, rule impI)
apply (rename_tac y)
apply (frule P5_REUSE,assumption+)
apply (erule_tac x="y" in ballE)
prefer 2 apply simp
apply (case_tac "p ∈ closure (E1, E2) y (h, k)")
apply (subgoal_tac "p ∈ recReach (E1, E2) x (h, k)",force)
apply (simp add: recReach_def)
apply (rule recReachL_basic)
apply (frule_tac q=q and c=c in reuse_identityClosure_y_in_E1)
by (assumption+,simp)
lemma P5_P6_REUSE:
"[| Γ x = Some d''; wellFormed {x} Γ (ReuseE x ());
h p = Some c; fresh q h;
(E1, E2) \<turnstile> h , k , td , ReuseE x () \<Down> h(p := None)(q \<mapsto> c) , k , Loc q , r;
dom Γ ⊆ dom E1;
E1 x = Some (Loc p)|]
==> shareRec {x} Γ (E1, E2) (h, k) (h(p := None)(q \<mapsto> c), k)"
apply (simp add: shareRec_def)
apply (rule conjI)
apply (rule P5_REUSE,assumption+)
by (rule P6_REUSE,assumption+)
text{*
Lemma for COPY
*}
lemma P5_COPY:
"[| wellFormed {x} Γ (x @ r ());
(E1, E2) \<turnstile> h , k , td , x @ r () \<Down> hh , k , v , ra ;
dom Γ ⊆ dom E1; E1 x = Some (Loc p)|]
==> (∀xa∈dom E1. Γ x = Some d'' ∧ closure (E1, E2) xa (h, k) ∩ recReach (E1, E2) x (h, k) ≠ {}
--> xa ∈ dom Γ ∧ Γ xa ≠ Some s'')"
apply (simp only: wellFormed_def)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="td" in allE)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="ra" in allE)
apply (rule ballI, rule impI)
apply (rename_tac y)
apply (drule mp,simp, simp add: dom_def)
apply (erule_tac x="y" in ballE)
prefer 2 apply force
apply (erule_tac x="x" in ballE)
prefer 2 apply blast
by simp
lemma P6_COPY:
"[| wellFormed {x} Γ (x @ r ());
(E1, E2) \<turnstile> h , k , td , x @ r () \<Down> hh , k , v , ra ;
dom Γ ⊆ dom E1; E1 x = Some (Loc p)|]
==> ∀x∈dom E1.
¬ identityClosure (E1, E2) x (h, k) (hh, k)
--> x ∈ dom Γ ∧ Γ x ≠ Some s''"
apply (rule ballI, rule impI)
apply (rename_tac y)
apply (frule P5_COPY,assumption+)
apply (erule_tac x="y" in ballE)
prefer 2 apply simp
apply (frule_tac L="{x}" and Γ="Γ" in z_in_SR)
by (simp add: SR_def)
lemma P5_P6_COPY:
"[| wellFormed {x} Γ (x @ r ());
(E1, E2) \<turnstile> h , k , td , x @ r () \<Down> hh , k , v , ra ;
dom Γ ⊆ dom E1;
E1 x = Some (Loc p)|]
==> shareRec {x} Γ (E1, E2) (h, k) (hh, k)"
apply (simp add: shareRec_def)
apply (rule conjI)
apply (rule P5_COPY,assumption+)
by (rule P6_COPY,assumption+)
text{*
Lemmas for LET1 and LET2
*}
lemma Γ1z_s_Γ2z_d_equals_recReach:
"[| def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> m)); dom Γ1 ⊆ dom E1;
shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
x ∈ dom E1; z≠x1;
Γ1 z = Some s''; z ∈ L1|]
==> recReach (E1, E2) z (h, k) = recReach (E1(x1 \<mapsto> r), E2) z (h', k')"
apply (simp only: shareRec_def)
apply (elim conjE)
apply (erule_tac x="x" in ballE) prefer 2 apply simp
apply (erule_tac x="z"in ballE) prefer 2 apply simp apply blast
apply (case_tac " ¬ identityClosure (E1, E2) z (h, k) (h', k')",simp)
apply simp apply (rule equals_recReach, assumption+)
done
lemma P5_Γ2z_d_Γ1z_s:
"[|def_pp Γ1 Γ2 L2; dom Γ1 ⊆ dom E1;
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> m));
dom (pp Γ1 Γ2 L2) ⊆ dom E1;
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> m))) (E1(x1 \<mapsto> r), E2) (h', k') (hh,kk);
shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
x ∈ dom E1;
Γ1 z = Some s''; z∈L1;
z ∈ L2; x1 ∉ L1; Γ2 z = Some d'';
(pp Γ1 Γ2 L2) z = Some d'';
x1 ∉ dom E1;
z ≠ x1;
closure (E1, E2) x (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {}|]
==> x ∈ dom (pp Γ1 Γ2 L2) ∧ (pp Γ1 Γ2 L2) x ≠ Some s''"
apply (frule_tac r="r" in Γ1z_s_Γ2z_d_equals_recReach, assumption+)
apply (case_tac "identityClosure (E1, E2) x (h, k) (h',k')")
apply (simp add: identityClosure_def)
apply (elim conjE)
apply (subgoal_tac "x≠x1") prefer 2 apply blast
apply (subgoal_tac "x≠x1 ==> closure (E1, E2) x (h', k') = closure (E1(x1 \<mapsto> r), E2) x (h', k')")
prefer 2 apply (simp add: closure_def)
apply simp
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="x" in ballE)+
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
apply (frule Gamma2_d_disjointUnionEnv_m_d,simp)
apply simp
apply (drule_tac Q=" x ∈ dom (Γ2 + [x1 \<mapsto> m]) ∧ (Γ2 + [x1 \<mapsto> m]) x ≠ Some s''" in mp)
apply (rule_tac x="z" in bexI)
prefer 2 apply simp
apply (rule conjI,simp) apply blast
apply (elim conjE)
apply (rule conjI)
apply (rule dom_Gamma2_dom_triangle,assumption+)
apply (rule usafe_Gamma2_unsafe_triangle,assumption+)
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="x" in ballE)+
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
apply (simp add: identityClosure_def)
apply (elim conjE)
by (rule triangle_prop)
lemma P5_Γ1z_d: " [|shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
x ∈ dom E1; (pp Γ1 Γ2 L2) z = Some d'';
closure (E1, E2) x (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {}; z ∈ L1; Γ1 z = Some d''|]
==> x ∈ dom (pp Γ1 Γ2 L2) ∧ (pp Γ1 Γ2 L2) x ≠ Some s''"
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="x" in ballE)+
apply clarsimp
apply (drule mp)
apply (rule_tac x="z" in bexI)
apply (rule conjI, assumption, clarsimp)
apply simp
apply (erule conjE)
apply (rule triangle_prop, assumption+)
apply simp
apply simp
done
lemma P5_LET_L1: "[|def_pp Γ1 Γ2 L2;
L1 ⊆ dom Γ1;
dom (pp Γ1 Γ2 L2) ⊆ dom E1; dom Γ1 ⊆ dom E1;
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> m));
shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> m))) (E1(x1 \<mapsto> r), E2) (h', k') (hh,kk);
x ∈ dom E1; x1 ∉ dom E1; x1 ∉ L1;
(pp Γ1 Γ2 L2) z = Some d'';
closure (E1, E2) x (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {};
z ∈ L1|]
==> x ∈ dom (pp Γ1 Γ2 L2) ∧ (pp Γ1 Γ2 L2) x ≠ Some s''"
apply (subgoal_tac "[|(pp Γ1 Γ2 L2) z = Some d''|] ==> Γ1 z = Some d'' ∨ Γ2 z = Some d''")
prefer 2 apply (erule triangle_d_Gamma1_d_or_Gamma2_d, simp)
apply (erule disjE)
(* Γ1 z = Some d'' *)
apply (rule P5_Γ1z_d, assumption+)
(* Γ2 z = Some d'' *)
apply (frule triangle_d_Gamma2_d_Gamma1_s,assumption+)
(* Caso Γ1 z = Some s''*)
apply (erule conjE)
apply (case_tac "z≠x1")
apply (rule P5_Γ2z_d_Γ1z_s, assumption+)
by simp
lemma P5_z_notin_L1_Γ1z_s_Γ2z_d:
" [|def_pp Γ1 Γ2 L2; def_disjointUnionEnv Γ2 [x1 \<mapsto> m]; dom (pp Γ1 Γ2 L2) ⊆ dom E1;
shareRec L2 (Γ2 + [x1 \<mapsto> m]) (E1(x1 \<mapsto> r), E2) (h', k') (hh,kk); shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
x ∈ dom E1; Γ1 z = Some s'';
z ∈ L2; x1 ∉ L1; Γ2 z = Some d''; (pp Γ1 Γ2 L2) z = Some d''; x1 ∉ dom E1; z ≠ x1;
closure (E1, E2) x (h, k) ∩ recReach (E1(x1 \<mapsto> r), E2) z (h', k') ≠ {};
recReach (E1, E2) z (h, k) = recReach (E1(x1 \<mapsto> r), E2) z (h', k')|]
==> x ∈ dom (pp Γ1 Γ2 L2) ∧ (pp Γ1 Γ2 L2) x ≠ Some s''"
apply (case_tac "identityClosure (E1, E2) x (h, k) (h',k')")
apply (simp add: identityClosure_def)
apply (elim conjE)
apply (subgoal_tac "x≠x1") prefer 2 apply blast
apply (subgoal_tac "x≠x1 ==> closure (E1, E2) x (h', k') = closure (E1(x1 \<mapsto> r), E2) x (h', k')")
prefer 2 apply (simp add: closure_def)
apply simp
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="x" in ballE)+
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
apply (frule Gamma2_d_disjointUnionEnv_m_d, assumption+)
apply (drule_tac Q=" x ∈ dom (Γ2 + [x1 \<mapsto> m]) ∧ (Γ2 + [x1 \<mapsto> m]) x ≠ Some s''" in mp)
apply (rule_tac x="z" in bexI)
prefer 2 apply simp
apply (rule conjI,simp)
apply simp
apply (elim conjE)
apply (rule conjI)
apply (rule dom_Gamma2_dom_triangle,assumption+)
apply (rule usafe_Gamma2_unsafe_triangle,assumption+)
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="x" in ballE)+
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
apply (simp add: identityClosure_def)
apply (elim conjE)
by (rule triangle_prop)
lemma P5_Γ2z_d_Γ1z_s_z_in_L2:
"[|def_pp Γ1 Γ2 L2;
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> m));
dom (pp Γ1 Γ2 L2) ⊆ dom E1;
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> m))) (E1(x1 \<mapsto> r), E2) (h', k') (hh,kk);
shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
x ∈ dom E1;
Γ1 z = Some s'';z ∈ L2; x1 ∉ L1; Γ2 z = Some d'';
(pp Γ1 Γ2 L2) z = Some d'';
x1 ∉ dom E1;
z ≠ x1;
recReach (E1, E2) z (h, k) = recReach (E1(x1 \<mapsto> r), E2) z (h', k');
closure (E1, E2) x (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {}|]
==> x ∈ dom (pp Γ1 Γ2 L2) ∧ (pp Γ1 Γ2 L2) x ≠ Some s''"
apply (case_tac "x≠x1")
apply (subgoal_tac "x≠x1 ==> closure (E1, E2) x (h', k') = closure (E1(x1 \<mapsto> r), E2) x (h', k')")
prefer 2 apply (simp add: closure_def)
apply simp
prefer 2 apply simp
apply (frule P5_z_notin_L1_Γ1z_s_Γ2z_d, assumption+)
done
lemma P5_Γ2z_d_z_notin_Γ1:
"[|def_pp Γ1 Γ2 L2;
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> m));
dom (pp Γ1 Γ2 L2) ⊆ dom E1;
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> m))) (E1(x1 \<mapsto> r), E2) (h', k') (hh,kk);
shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
x ∈ dom E1;
z ∉ dom Γ1; z ∈ L2; x1 ∉ L1; Γ2 z = Some d'';
(pp Γ1 Γ2 L2) z = Some d'';
x1 ∉ dom E1;
z ≠ x1;
recReach (E1, E2) z (h, k) = recReach (E1(x1 \<mapsto> r), E2) z (h', k');
closure (E1, E2) x (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {}|]
==> x ∈ dom (pp Γ1 Γ2 L2) ∧ (pp Γ1 Γ2 L2) x ≠ Some s''"
apply (case_tac "identityClosure (E1, E2) x (h, k) (h',k')")
apply (simp add: identityClosure_def)
apply (elim conjE)
apply (subgoal_tac "x≠x1") prefer 2 apply blast
apply (subgoal_tac "x≠x1 ==> closure (E1, E2) x (h', k') = closure (E1(x1 \<mapsto> r), E2) x (h', k')")
prefer 2 apply (simp add: closure_def)
apply simp
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="x" in ballE)+
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
apply (frule Gamma2_d_disjointUnionEnv_m_d, assumption+)
apply (drule_tac Q=" x ∈ dom (Γ2 + [x1 \<mapsto> m]) ∧ (Γ2 + [x1 \<mapsto> m]) x ≠ Some s''" in mp)
apply (rule_tac x="z" in bexI)
prefer 2 apply simp
apply (rule conjI,simp)
apply simp
apply (elim conjE)
apply (rule conjI)
apply (rule dom_Gamma2_dom_triangle,assumption+)
apply (rule usafe_Gamma2_unsafe_triangle,assumption+)
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="x" in ballE)+
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
apply (simp add: identityClosure_def)
apply (elim conjE)
by (rule triangle_prop)
lemma P5_LET_L2:
"[| L1 ⊆ dom Γ1; dom Γ1 ⊆ dom E1;
L2 ⊆ dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> m)));
def_pp Γ1 Γ2 L2;
dom (pp Γ1 Γ2 L2) ⊆ dom E1;
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> m));
shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> m))) (E1(x1 \<mapsto> r), E2) (h', k') (hh,kk);
x ∈ dom E1; x1 ∉ dom E1; x1 ∉ L1;
(pp Γ1 Γ2 L2) z = Some d'';
closure (E1, E2) x (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {};
z ∈ L2; z ≠ x1|]
==> x ∈ dom (pp Γ1 Γ2 L2) ∧ (pp Γ1 Γ2 L2) x ≠ Some s''"
apply (frule triangle_d_Gamma1_s_or_not_dom_Gamma1, assumption+)
apply (erule disjE)
(* Caso Γ1 z = Some s'' *)
apply (subgoal_tac "[|(pp Γ1 Γ2 L2) z = Some d''; Γ1 z = Some s''|] ==> Γ2 z = Some d''")
prefer 2 apply (rule triangle_d_Gamma1_s_Gamma2_d, assumption+)
apply simp
apply (subgoal_tac "z∈ dom E1")
prefer 2 apply blast
apply (case_tac "identityClosure (E1, E2) z (h, k) (h',k')")
apply (frule identityClosure_equals_recReach)
apply (subgoal_tac "z≠x1 ==> recReach (E1, E2) z (h', k') = recReach (E1(x1 \<mapsto> r), E2) z (h', k')")
prefer 2 apply (simp add: recReach_def)
apply simp
apply (rule P5_z_notin_L1_Γ1z_s_Γ2z_d, assumption+)
apply (simp add: shareRec_def)
(* z ∉ dom Γ1 *)
apply (case_tac "z∈ dom E1") prefer 2 apply blast
apply (case_tac "identityClosure (E1, E2) z (h, k) (h',k')")
apply (frule identityClosure_equals_recReach)
apply (subgoal_tac "z≠x1 ==> recReach (E1, E2) z (h', k') = recReach (E1(x1 \<mapsto> r), E2) z (h', k')")
prefer 2 apply (simp add: recReach_def)
apply simp
apply (subgoal_tac "Γ2 z = Some d''")
apply (rule P5_Γ2z_d_z_notin_Γ1, assumption+) apply simp
apply (simp add: pp_def)
by (simp add: shareRec_def)
lemma P5_Cond2:
"[|L1 ⊆ dom Γ1;
L2 ⊆ dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> m)));
x1 ∉ dom E1; x1 ∉ L1;
dom (pp Γ1 Γ2 L2) ⊆ dom E1;
def_pp Γ1 Γ2 L2;
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> m));
shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> m))) (E1(x1 \<mapsto> r), E2) (h', k') (hh,kk)|]
==> ∀x∈dom E1. ¬ identityClosure (E1, E2) x (h, k) (hh, kk) --> x ∈ dom (pp Γ1 Γ2 L2) ∧ (pp Γ1 Γ2 L2) x ≠ Some s''"
apply (rule ballI, rule impI)
apply (case_tac "¬identityClosure (E1, E2) x (h, k) (h', k')")
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="x" in ballE)+
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
apply simp
apply (elim conjE)
apply (rule triangle_prop,assumption+)
apply (case_tac "¬ identityClosure (E1(x1 \<mapsto> r), E2) x (h', k') (hh, kk)")
apply (simp add: shareRec_def)
apply (elim conjE)
apply (erule_tac x="x" in ballE)+
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
prefer 2 apply simp
apply simp
apply (elim conjE)
apply (subgoal_tac "x ≠ x1") prefer 2 apply blast
apply (rule conjI)
apply (rule dom_Gamma2_dom_triangle,assumption+)
apply (rule usafe_Gamma2_unsafe_triangle,assumption+)
apply simp
apply (subgoal_tac "x ≠ x1") prefer 2 apply blast
apply (frule monotone_identityClosure, assumption+)
by simp
lemma P5_P6_LET:
"[| L1 ⊆ dom Γ1; dom Γ1 ⊆ dom E1;
L2 ⊆ dom (disjointUnionEnv Γ2 (empty(x1 \<mapsto> m)));
x1 ∉ dom E1; x1 ∉ L1;
dom (pp Γ1 Γ2 L2) ⊆ dom E1;
def_pp Γ1 Γ2 L2;
def_disjointUnionEnv Γ2 (empty(x1 \<mapsto> m));
shareRec L1 Γ1 (E1, E2) (h, k) (h',k');
shareRec L2 (disjointUnionEnv Γ2 (empty(x1 \<mapsto> m))) (E1(x1 \<mapsto> r), E2) (h', k') (hh,kk)|]
==> shareRec (L1 ∪ (L2 - {x1})) (pp Γ1 Γ2 L2) (E1, E2) (h, k) (hh,kk)"
apply (simp (no_asm) add: shareRec_def)
apply (rule conjI)
apply (rule ballI, rule impI)
apply (erule bexE)
apply (erule conjE)+
apply simp
apply (erule disjE)
(* Caso z ∈ L1 *)
apply (erule P5_LET_L1, assumption+)
(* Caso z ∈ L2 *)
apply (erule conjE)+
apply (erule P5_LET_L2, assumption+)
(* Caso distintas closure *)
by (erule P5_Cond2,assumption+)
(* P5_P6 for LET1C_e1 *)
lemma Γ1_z_Some_s:
"z ∈ atom2var ` set as
==> (map_of (zip (map atom2var as) (replicate (length as) s''))) z = Some s''"
by (induct as,simp,clarsimp)
lemma P5_LETC_e1:
"∀x∈dom (fst (E1, E2)).
∀z∈set (map atom2var as).
map_of (zip (map atom2var as) (replicate (length as) s'')) z = Some d'' ∧
closure (E1, E2) x (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {} -->
x ∈ dom (map_of (zip (map atom2var as) (replicate (length as) s''))) ∧
map_of (zip (map atom2var as) (replicate (length as) s'')) x ≠ Some s''"
apply (rule ballI)+
apply (rule impI, elim conjE,simp)
by (frule Γ1_z_Some_s,simp)
lemma ext_h_same_descendants:
"[| fresh p h; q ≠ p |]
==> descendants q (h, k) =
descendants q (h(p \<mapsto> c), k)"
apply (rule equalityI)
apply (rule subsetI)
apply (frule_tac k="k" in fresh_notin_closureL)
apply (subgoal_tac "q ∈ dom h")
apply (simp add: descendants_def)
apply (erule_tac x="q" in ballE)
apply (simp add: descendants_def)
apply (case_tac "h q",simp_all)
apply force
apply (simp add: descendants_def)
apply (case_tac "h q",simp_all)
apply force
apply (rule subsetI)
apply (frule_tac k="k" in fresh_notin_closureL)
apply (subgoal_tac "q ∈ dom h")
apply (simp add: descendants_def)
apply (erule_tac x="q" in ballE)
prefer 2 apply simp
apply (simp add: descendants_def)
apply (case_tac "h q",simp_all)
apply force
apply (simp add: descendants_def)
apply (case_tac "h q",simp_all)
by force
lemma ext_h_same_recDescendants:
"[| fresh p h; q ≠ p |]
==> recDescendants q (h, k) =
recDescendants q (h(p \<mapsto> c), k)"
apply (rule equalityI)
apply (rule subsetI)
apply (frule_tac k="k" in fresh_notin_closureL)
apply (subgoal_tac "q ∈ dom h")
apply (simp add: recDescendants_def)
apply (erule_tac x="q" in ballE)
apply (simp add: recDescendants_def)
apply (case_tac "h q",simp_all)
apply force
apply (simp add: recDescendants_def)
apply (case_tac "h q",simp_all)
apply force
apply (rule subsetI)
apply (frule_tac k="k" in fresh_notin_closureL)
apply (subgoal_tac "q ∈ dom h")
apply (simp add: recDescendants_def)
apply (erule_tac x="q" in ballE)
prefer 2 apply simp
apply (simp add: recDescendants_def)
apply (case_tac "h q",simp_all)
apply force
apply (simp add: recDescendants_def)
apply (case_tac "h q",simp_all)
by force
lemma ext_h_same_closure:
"[| (E1, E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r ;
fresh p h |]
==> closure (E1,E2) x (h,k) =
closure (E1,E2) x (h(p \<mapsto> c), k)"
apply (simp add: closure_def)
apply (case_tac "E1 x",simp_all)
apply (case_tac a,simp_all)
apply clarsimp
apply (rename_tac q)
apply (frule_tac k="k" in semantic_no_capture_E1_fresh_2,assumption+)
apply (erule_tac x="x" in ballE)
prefer 2 apply force
apply (erule_tac x="q" in allE,simp)
apply (rule equalityI)
apply (rule subsetI)
apply (erule closureL.induct)
apply (rule closureL_basic)
apply (subgoal_tac "qa ≠ p")
apply (subgoal_tac "d ∈ descendants qa (h(p \<mapsto> c), k)")
apply (rule closureL_step,assumption+)
apply (subst (asm) ext_h_same_descendants,assumption+)
apply (simp add: descendants_def)
apply (case_tac "h qa", simp_all)
apply (simp add: fresh_def, force)
apply (rule subsetI)
apply (erule closureL.induct)
apply (rule closureL_basic)
apply (subgoal_tac "d ∈ descendants qa (h, k)")
apply (rule closureL_step,assumption+)
apply (subst ext_h_same_descendants,assumption+)
apply (case_tac "qa ≠ p",simp,simp)
by simp
lemma ext_h_same_recReach:
"[| (E1, E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r ;
fresh p h |]
==> recReach (E1,E2) x (h,k) =
recReach (E1,E2) x (h(p \<mapsto> c), k)"
apply (simp add: recReach_def)
apply (case_tac "E1 x",simp_all)
apply (case_tac a,simp_all)
apply clarsimp
apply (rename_tac q)
apply (frule_tac k="k" in semantic_no_capture_E1_fresh_2,assumption+)
apply (erule_tac x="x" in ballE)
prefer 2 apply force
apply (erule_tac x="q" in allE,simp)
apply (rule equalityI)
apply (rule subsetI)
apply (erule recReachL.induct)
apply (rule recReachL_basic)
apply (subgoal_tac "qa ≠ p")
apply (subgoal_tac "d ∈ recDescendants qa (h(p \<mapsto> c), k)")
apply (rule recReachL_step,assumption+)
apply (subst (asm) ext_h_same_recDescendants,assumption+)
apply (simp add: recDescendants_def)
apply (case_tac "h qa", simp_all)
apply (simp add: fresh_def, force)
apply (rule subsetI)
apply (erule recReachL.induct)
apply (rule recReachL_basic)
apply (subgoal_tac "d ∈ recDescendants qa (h, k)")
apply (rule recReachL_step,assumption+)
apply (subst ext_h_same_recDescendants,assumption+)
apply (case_tac "qa ≠ p",simp,simp)
apply (subgoal_tac "recReachL q (h, k) ⊆ closureL q (h, k)")
apply blast
apply (rule recReachL_subseteq_closureL)
by simp
lemma closure_upt_monotone:
"[| x ∈ dom E1; x1 ∉ dom E1 |]
==> closure (E1, E2) x (h, k) =
closure (E1(x1 \<mapsto> Loc p),E2) x (h, k)"
apply (simp add: closure_def)
apply (rule impI)
by (simp add: dom_def)
lemma recReach_upt_monotone:
"[| x ∈ dom E1; x1 ∉ dom E1 |]
==> recReach (E1, E2) x (h, k) =
recReach (E1(x1 \<mapsto> Loc p),E2) x (h, k)"
apply (simp add: recReach_def)
apply (rule impI)
by (simp add: dom_def)
lemma cvte_ext_h_inter_closure_recReach:
"[| (E1, E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r;
fresh p h;
x1 ∉ dom E1; x ∈ dom E1; z ∈ dom E1;
closure (E1, E2) x (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {} |]
==> closure (E1(x1 \<mapsto> Loc p), E2) x (h(p \<mapsto> (j, C, map (atom2val E1) as)), k) ∩
recReach (E1(x1 \<mapsto> Loc p), E2) z (h(p \<mapsto> (j, C, map (atom2val E1) as)), k) ≠ {}"
apply (subst (asm) ext_h_same_closure, assumption+)
apply (subst (asm) ext_h_same_recReach, assumption+)
apply (subst (asm) closure_upt_monotone,assumption+)
by (subst (asm) recReach_upt_monotone,assumption+)
lemma ext_h_same_identityClosure_upt:
"[| fresh p h; x ∈ dom E1;
(E1, E2) \<turnstile> h , k , td , e \<Down> h' , k , v , r |]
==> identityClosure (E1,E2) x (h,k) (h(p \<mapsto> c), k)"
apply (case_tac "E1 x")
apply (simp add: dom_def)
apply (case_tac a,simp_all)
(* Loc p *)
apply (simp add: identityClosure_def)
apply (rule conjI)
apply (rule ext_h_same_closure,assumption+)
apply (rule impI)
apply (simp add: closure_def)
apply (frule semantic_no_capture_E1_fresh_2,assumption+)
apply force
(* IntT n *)
apply (simp add: identityClosure_def)
apply (simp add: closure_def)
(* BoolT n *)
apply (simp add: identityClosure_def)
apply (simp add: closure_def)
done
lemma P6_LETC_e1:
"[| (E1, E2) \<turnstile> h , k , td , Let x1 = ConstrE C as r a' In e2 a \<Down> hh , k , v , ra ;
(E1(x1 \<mapsto> Loc p), E2) \<turnstile> h(p \<mapsto> (j, C, map (atom2val E1) as)) , k , (td + 1) , e2 \<Down> hh , k , v , rs' ;
x1 ∉ L1; x1 ∉ dom E1;
def_pp (map_of (zip (map atom2var as) (replicate (length as) s''))) Γ2 L2;
dom (pp (map_of (zip (map atom2var as) (replicate (length as) s''))) Γ2 L2) ⊆ dom E1;
fresh p h;
∀x∈dom (fst (E1(x1 \<mapsto> Loc p), E2)).
¬ identityClosure (E1(x1 \<mapsto> Loc p), E2) x (h(p \<mapsto> (j, C, map (atom2val E1) as)), k) (hh, k) -->
x ∈ dom (Γ2 + [x1 \<mapsto> m'']) ∧ (Γ2 + [x1 \<mapsto> m'']) x ≠ Some s''|]
==> ∀x∈dom (fst (E1, E2)).
¬ identityClosure (E1, E2) x (h, k) (h(p \<mapsto> (j, C, map (atom2val E1) as)), k) -->
x ∈ dom (map_of (zip (map atom2var as) (replicate (length as) s''))) ∧
map_of (zip (map atom2var as) (replicate (length as) s'')) x ≠ Some s''"
apply (rule ballI,rule impI)
apply (subgoal_tac "x≠x1")
prefer 2 apply force
apply (erule_tac x="x" in ballE)
prefer 2 apply simp
apply (frule ext_h_same_identityClosure_upt)
by (assumption+,simp,force)
lemma P5_P6_LETC_e1:
"[|(E1, E2) \<turnstile> h , k , td , Let x1 = ConstrE C as r a' In e2 a \<Down> hh , k , v , ra ;
(E1(x1 \<mapsto> Loc p), E2) \<turnstile> h(p \<mapsto> (j, C, map (atom2val E1) as)) , k , (td + 1) , e2 \<Down> hh , k , v , rs' ;
x1 ∉ L1; x1 ∉ dom E1;
L1 = set (map atom2var as);
Γ1 = map_of (zip (map atom2var as) (replicate (length as) s''));
dom (pp (map_of (zip (map atom2var as) (replicate (length as) s''))) Γ2 L2) ⊆ dom E1;
def_pp (map_of (zip (map atom2var as) (replicate (length as) s''))) Γ2 L2;
shareRec L2 (Γ2 + [x1 \<mapsto> m'']) (E1(x1 \<mapsto> Loc p), E2) (h(p \<mapsto> (j, C, map (atom2val E1) as)), k) (hh, k);
fresh p h |]
==> shareRec L1 Γ1 (E1, E2) (h,k) (h(p \<mapsto> (j, C, map (atom2val E1) as)), k)"
apply (simp only: shareRec_def)
apply (elim conjE)
apply (rule conjI)
apply (rule P5_LETC_e1)
by (rule P6_LETC_e1,assumption+)
lemma ext_h_same_closure_semDepth:
"[| (E1, E2) \<turnstile> h , k , e \<Down>(f,n) h' , k , v;
fresh p h |]
==> closure (E1,E2) x (h,k) =
closure (E1,E2) x (h(p \<mapsto> c), k)"
apply (simp add: closure_def)
apply (case_tac "E1 x",simp_all)
apply (case_tac a,simp_all)
apply clarsimp
apply (rename_tac q)
apply (frule_tac k="k" in semantic_no_capture_E1_fresh_2_semDepth,assumption+)
apply (erule_tac x="x" in ballE)
prefer 2 apply force
apply (erule_tac x="q" in allE,simp)
apply (rule equalityI)
apply (rule subsetI)
apply (erule closureL.induct)
apply (rule closureL_basic)
apply (subgoal_tac "qa ≠ p")
apply (subgoal_tac "d ∈ descendants qa (h(p \<mapsto> c), k)")
apply (rule closureL_step,assumption+)
apply (subst (asm) ext_h_same_descendants,assumption+)
apply (simp add: descendants_def)
apply (case_tac "h qa", simp_all)
apply (simp add: fresh_def, force)
apply (rule subsetI)
apply (erule closureL.induct)
apply (rule closureL_basic)
apply (subgoal_tac "d ∈ descendants qa (h, k)")
apply (rule closureL_step,assumption+)
apply (subst ext_h_same_descendants,assumption+)
apply (case_tac "qa ≠ p",simp,simp)
by simp
lemma ext_h_same_identityClosure_upt_semDepth:
"[| fresh p h; x ∈ dom E1;
(E1, E2) \<turnstile> h , k , e \<Down>(f,n) h' , k , v|]
==> identityClosure (E1,E2) x (h,k) (h(p \<mapsto> c), k)"
apply (case_tac "E1 x")
apply (simp add: dom_def)
apply (case_tac a,simp_all)
(* Loc p *)
apply (simp add: identityClosure_def)
apply (rule conjI)
apply (rule ext_h_same_closure_semDepth,assumption+)
apply (rule impI)
apply (simp add: closure_def)
apply (frule semantic_no_capture_E1_fresh_2_semDepth,assumption+)
apply force
(* IntT n *)
apply (simp add: identityClosure_def)
apply (simp add: closure_def)
(* BoolT n *)
apply (simp add: identityClosure_def)
apply (simp add: closure_def)
done
lemma P6_f_n_LETC_e1:
"[| (E1, E2) \<turnstile> h , k , Let x1 = ConstrE C as r a' In e2 a \<Down>(f,n) hh , k , v;
(E1(x1 \<mapsto> Loc p), E2) \<turnstile> h(p \<mapsto> (j, C, map (atom2val E1) as)) , k , e2 \<Down>(f,n) hh , k , v;
x1 ∉ L1; x1 ∉ dom E1;
def_pp (map_of (zip (map atom2var as) (replicate (length as) s''))) Γ2 L2;
dom (pp (map_of (zip (map atom2var as) (replicate (length as) s''))) Γ2 L2) ⊆ dom E1;
fresh p h;
∀x∈dom (fst (E1(x1 \<mapsto> Loc p), E2)).
¬ identityClosure (E1(x1 \<mapsto> Loc p), E2) x (h(p \<mapsto> (j, C, map (atom2val E1) as)), k) (hh, k) -->
x ∈ dom (Γ2 + [x1 \<mapsto> m'']) ∧ (Γ2 + [x1 \<mapsto> m'']) x ≠ Some s''|]
==> ∀x∈dom (fst (E1, E2)).
¬ identityClosure (E1, E2) x (h, k) (h(p \<mapsto> (j, C, map (atom2val E1) as)), k) -->
x ∈ dom (map_of (zip (map atom2var as) (replicate (length as) s''))) ∧
map_of (zip (map atom2var as) (replicate (length as) s'')) x ≠ Some s''"
apply (rule ballI,rule impI)
apply (subgoal_tac "x≠x1")
prefer 2 apply force
apply (erule_tac x="x" in ballE)
prefer 2 apply simp
apply (frule ext_h_same_identityClosure_upt_semDepth)
by (assumption+,simp,force)
lemma P5_P6_f_n_LETC_e1:
"[|(E1, E2) \<turnstile> h , k , Let x1 = ConstrE C as r a' In e2 a \<Down>(f,n) hh , k , v;
(E1(x1 \<mapsto> Loc p), E2) \<turnstile> h(p \<mapsto> (j, C, map (atom2val E1) as)) , k , e2 \<Down>(f,n) hh , k , v;
x1 ∉ L1; x1 ∉ dom E1;
L1 = set (map atom2var as);
Γ1 = map_of (zip (map atom2var as) (replicate (length as) s''));
dom (pp (map_of (zip (map atom2var as) (replicate (length as) s''))) Γ2 L2) ⊆ dom E1;
def_pp (map_of (zip (map atom2var as) (replicate (length as) s''))) Γ2 L2;
shareRec L2 (Γ2 + [x1 \<mapsto> m'']) (E1(x1 \<mapsto> Loc p), E2) (h(p \<mapsto> (j, C, map (atom2val E1) as)), k) (hh, k);
fresh p h |]
==> shareRec L1 Γ1 (E1, E2) (h,k) (h(p \<mapsto> (j, C, map (atom2val E1) as)), k)"
apply (simp only: shareRec_def)
apply (elim conjE)
apply (rule conjI)
apply (rule P5_LETC_e1)
by (rule P6_f_n_LETC_e1,assumption+)
text{*
Lemmas for CASE
*}
(**************** CASE *********************)
lemma P5_CASE_shareRec:
"[| (E1, E2) \<turnstile> h , k , td , Case VarE x () Of alts () \<Down> hh , k , v , r ;
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1;
insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ()) ⊆ insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
wellFormed (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ()) |]
==> ∀xa∈dom (fst (E1, E2)).
∀z∈insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))).
foldl op ⊗ empty (map snd assert) z = Some d'' ∧ closure (E1, E2) xa (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {} -->
xa ∈ dom (foldl op ⊗ empty (map snd assert)) ∧ foldl op ⊗ empty (map snd assert) xa ≠ Some s''"
apply (simp only: wellFormed_def)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="td" in allE)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="r" in allE)
apply (drule mp,simp)
by simp
lemma closure_monotone_extend:
"[| x ∈ dom E;
def_extend E (snd (extractP (fst (alts ! i)))) vs;
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 (simp add: def_extend_def)
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 (assumption+,simp,simp)
by blast
lemma identityClosure_monotone_extend:
"[| x ∈ dom E1;
length alts > 0; i < length alts;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
¬ identityClosure (E1, E2) x (h, k) (hh, k) |]
==> ¬ identityClosure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h, k) (hh, k)"
apply (simp add: identityClosure_def)
apply (rule impI)
apply (subgoal_tac
"closure (E1, E2) x (h, k) =
closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h, k)",simp)
apply (subgoal_tac
"closure (E1, E2) x (hh, k) =
closure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (hh, k)",simp)
apply (rule closure_monotone_extend,assumption+,simp,assumption+)
by (rule closure_monotone_extend,assumption+,simp,assumption+)
lemma P5_CASE_identityClosure:
"[| length assert = length alts;
length alts > 0; i < length alts;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
def_nonDisjointUnionEnvList (map snd assert);
(∀x∈dom (fst (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2)).
¬ identityClosure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h, k) (hh, k) -->
x ∈ dom (snd (assert ! i)) ∧ snd (assert ! i) x ≠ Some s'') |]
==>∀x∈dom (fst (E1, E2)).
¬ identityClosure (E1, E2) x (h, k) (hh, k) -->
x ∈ dom (foldl op ⊗ empty (map snd assert)) ∧ foldl op ⊗ empty (map snd assert) x ≠ Some s''"
apply (rule ballI)
apply (erule_tac x="x" in ballE)
apply (rule impI)
apply (drule mp)
apply (rule identityClosure_monotone_extend,simp,assumption+)
apply (elim conjE)
apply (rule conjI)
apply (subgoal_tac "length assert > i")
apply (frule dom_monotone)
apply blast
apply simp
apply (rule Otimes_prop2)
apply (simp,simp,assumption+)
apply (subgoal_tac
"E1 x = extend E1 (snd (extractP (fst (alts ! i)))) vs x")
apply (simp add: dom_def)
apply (rule extend_monotone_i,assumption+)
apply (simp add: def_extend_def)
by blast
lemma P5_P6_CASE:
"[| (E1, E2) \<turnstile> h , k , td , Case VarE x () Of alts () \<Down> hh , k , v , r ;
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1;
insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ()) ⊆ insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
def_nonDisjointUnionEnvList (map snd assert); alts ≠ []; length assert = length alts;
wellFormed (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ());
(E1, E2) \<turnstile> h , k , td , Case VarE x () Of alts () \<Down> hh , k , v , r ;
shareRec (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) (hh, k)|]
==> shareRec (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) (hh, k)"
apply (simp (no_asm) only: shareRec_def)
apply (rule conjI)
apply (rule P5_CASE_shareRec,assumption+)
apply (simp only: shareRec_def)
apply (rule P5_CASE_identityClosure,assumption+)
by (simp,simp,assumption+,simp)
lemma P5_f_n_CASE_shareRec:
"[| (E1, E2) \<turnstile> h , k , Case VarE x () Of alts () \<Down>(f,n) hh , k , v ;
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1;
insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ()) ⊆ insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
wellFormedDepth f n (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ()) |]
==> ∀xa∈dom (fst (E1, E2)).
∀z∈insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))).
foldl op ⊗ empty (map snd assert) z = Some d'' ∧ closure (E1, E2) xa (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {} -->
xa ∈ dom (foldl op ⊗ empty (map snd assert)) ∧ foldl op ⊗ empty (map snd assert) xa ≠ Some s''"
apply (simp only: wellFormedDepth_def)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v" in allE)
apply (drule mp,simp)
by simp
lemma P5_P6_f_n_CASE:
"[| (E1, E2) \<turnstile> h , k , Case VarE x () Of alts () \<Down>(f,n) hh , k , v;
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1;
insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ()) ⊆ insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
def_nonDisjointUnionEnvList (map snd assert); alts ≠ []; length assert = length alts;
wellFormedDepth f n (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ());
shareRec (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h, k) (hh, k)|]
==> shareRec (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) (hh, k)"
apply (simp (no_asm) only: shareRec_def)
apply (rule conjI)
apply (rule P5_f_n_CASE_shareRec,assumption+)
apply (simp only: shareRec_def)
apply (rule P5_CASE_identityClosure,assumption+)
by (simp,simp,assumption+,simp)
(********** Demostracion P5_CASE_1_1 ********************)
lemma P5_CASE_1_1_identityClosure:
"[| length assert = length alts;
length alts > 0; i < length alts;
fst (alts ! i) = ConstP (LitN n);
def_nonDisjointUnionEnvList (map snd assert);
(∀x∈dom (fst (E1, E2)). ¬ identityClosure (E1, E2) x (h, k) (hh, k)
--> x ∈ dom (snd (assert ! i)) ∧ snd (assert ! i) x ≠ Some s'') |]
==>∀x∈dom (fst (E1, E2)).
¬ identityClosure (E1, E2) x (h, k) (hh, k) -->
x ∈ dom (foldl op ⊗ empty (map snd assert)) ∧ foldl op ⊗ empty (map snd assert) x ≠ Some s''"
apply (rule ballI)
apply (erule_tac x="x" in ballE)
apply (rule impI)
apply (drule mp,simp)
apply (rule conjI)
apply (subgoal_tac "length assert > i")
apply (frule dom_monotone)
apply blast
apply simp
apply (rule Otimes_prop2)
apply (simp,simp,assumption+,simp,simp)
by (simp add: dom_def)
lemma P5_P6_CASE_1_1:
"[| (E1, E2) \<turnstile> h , k , td , Case VarE x () Of alts () \<Down> hh , k , v , r ;
fst (alts ! i) = ConstP (LitN n);
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1;
insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ()) ⊆ insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts;
def_nonDisjointUnionEnvList (map snd assert); alts ≠ []; length assert = length alts;
wellFormed (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ());
(E1, E2) \<turnstile> h , k , td , Case VarE x () Of alts () \<Down> hh , k , v , r ;
shareRec (fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k) (hh, k)|]
==> shareRec (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) (hh, k)"
apply (simp (no_asm) only: shareRec_def)
apply (rule conjI)
apply (rule P5_CASE_shareRec,assumption+)
apply (simp only: shareRec_def)
apply (rule P5_CASE_1_1_identityClosure,assumption+)
by (simp,force,force,assumption+,simp)
lemma P5_P6_f_n_CASE_1_1:
"[| (E1, E2) \<turnstile> h , k , Case VarE x () Of alts () \<Down>(f,n) hh , k , v;
fst (alts ! i) = ConstP (LitN n');
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1;
insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ()) ⊆ insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts;
def_nonDisjointUnionEnvList (map snd assert); alts ≠ []; length assert = length alts;
wellFormedDepth f n (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ());
shareRec (fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k) (hh, k)|]
==> shareRec (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) (hh, k)"
apply (simp (no_asm) only: shareRec_def)
apply (rule conjI)
apply (rule P5_f_n_CASE_shareRec,assumption+)
apply (simp only: shareRec_def)
apply (rule P5_CASE_1_1_identityClosure,assumption+)
by (simp,force,force,assumption+,simp)
(********** Demostracion P5_CASE_1_2 ********************)
lemma P5_CASE_1_2_identityClosure:
"[| length assert = length alts;
length alts > 0; i < length alts;
fst (alts ! i) = ConstP (LitB b);
def_nonDisjointUnionEnvList (map snd assert);
(∀x∈dom (fst (E1, E2)). ¬ identityClosure (E1, E2) x (h, k) (hh, k)
--> x ∈ dom (snd (assert ! i)) ∧ snd (assert ! i) x ≠ Some s'') |]
==>∀x∈dom (fst (E1, E2)).
¬ identityClosure (E1, E2) x (h, k) (hh, k) -->
x ∈ dom (foldl op ⊗ empty (map snd assert)) ∧ foldl op ⊗ empty (map snd assert) x ≠ Some s''"
apply (rule ballI)
apply (erule_tac x="x" in ballE)
apply (rule impI)
apply (drule mp,simp)
apply (rule conjI)
apply (subgoal_tac "length assert > i")
apply (frule dom_monotone)
apply blast
apply simp
apply (rule Otimes_prop2)
apply (simp,simp,assumption+,simp,simp)
by (simp add: dom_def)
lemma P5_P6_CASE_1_2:
"[| (E1, E2) \<turnstile> h , k , td , Case VarE x () Of alts () \<Down> hh , k , v , r ;
fst (alts ! i) = ConstP (LitB b);
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1;
insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ()) ⊆ insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts;
def_nonDisjointUnionEnvList (map snd assert); alts ≠ []; length assert = length alts;
wellFormed (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ());
(E1, E2) \<turnstile> h , k , td , Case VarE x () Of alts () \<Down> hh , k , v , r ;
shareRec (fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k) (hh, k)|]
==> shareRec (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) (hh, k)"
apply (simp (no_asm) only: shareRec_def)
apply (rule conjI)
apply (rule P5_CASE_shareRec,assumption+)
apply (simp only: shareRec_def)
apply (rule P5_CASE_1_2_identityClosure,assumption+)
by (simp,force,force,assumption+,simp)
lemma P5_P6_f_n_CASE_1_2:
"[| (E1, E2) \<turnstile> h , k , Case VarE x () Of alts () \<Down>(f,n) hh , k , v;
fst (alts ! i) = ConstP (LitB b);
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1;
insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ()) ⊆ insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts;
def_nonDisjointUnionEnvList (map snd assert); alts ≠ []; length assert = length alts;
wellFormedDepth f n (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ());
shareRec (fst (assert ! i)) (snd (assert ! i)) (E1, E2) (h, k) (hh, k)|]
==> shareRec (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) (hh, k)"
apply (simp (no_asm) only: shareRec_def)
apply (rule conjI)
apply (rule P5_f_n_CASE_shareRec,assumption+)
apply (simp only: shareRec_def)
apply (rule P5_CASE_1_2_identityClosure,assumption+)
by (simp,force,force,assumption+,simp)
(********** Demostracion P5_CASED ********************)
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 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 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 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 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 p_in_closure_q_p_none:
"[| p≠q; closureL q (h, k) ≠ closureL q (h(p := None), k) |]
==> p ∈ closureL q (h(p := None),k)"
apply auto
apply (erule closureL.induct)
apply (rule closureL_basic)
apply (subgoal_tac "p≠qa")
prefer 2 apply blast
apply (rule closureL_step,simp)
apply (simp add: descendants_def)
apply (frule closureL_p_None_subseteq_closureL)
by blast
lemma not_identityClosure_h_h_p_none_inter_not_empty_h:
"[| y ∈ dom E1; E1 x = Some (Loc p); h p = Some (j,C,vn);
¬ identityClosure (E1, E2) y (h, k) (h(p := None), k) |]
==> closure (E1,E2) y (h, k) ∩ recReach (E1,E2) x (h, k) ≠ {}"
apply (simp only: identityClosure_def)
apply (simp add: closure_def)
apply (case_tac "E1 y",simp_all)
apply (case_tac a, simp_all)
apply (simp add: recReach_def)
apply (rename_tac q)
apply (case_tac "p=q")
apply simp
apply (subgoal_tac "q ∈ recReachL q (h,k)")
apply (subgoal_tac "recReachL q (h,k) ⊆ closureL q (h,k)")
apply blast
apply (rule recReachL_subseteq_closureL)
apply (rule recReachL_basic)
apply (case_tac
"closureL q (h, k) ≠ closureL q (h(p := None), k)",simp_all)
apply (frule_tac h="h" and k="k" in p_in_closure_q_p_none,simp)
apply (frule_tac h="h" and k="k" in closureL_p_None_subseteq_closureL)
apply (subgoal_tac
"p ∈ recReachL p (h, k)")
apply blast
apply (rule recReachL_basic)
apply (elim bexE)
apply (case_tac "pa = p",simp_all)
apply (subgoal_tac
"p ∈ recReachL p (h, k)")
apply blast
by (rule recReachL_basic)
lemma dom_foldl_monotone_generic:
" 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_Γ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_generic)
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_generic)
by blast
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_generic)
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 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 restrict_neg_map_not_s:
"[| G y ≠ Some s''; x≠ y ; y ∉ L|]
==> restrict_neg_map G (insert x L) y ≠ Some s''"
by (simp add: restrict_neg_map_def)
declare def_nonDisjointUnionEnvList.simps [simp del]
lemma Otimes_prop_cased_not_s [rule_format]:
"length assert > 0
--> 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 s''
--> 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 s'')"
apply (case_tac "x = y",simp)
apply (rule impI)+
apply (rule allI)
apply (rule impI)+
apply (subgoal_tac
"(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''",simp)
apply (rule_tac
Γ="(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''])" in Γ_case_x_is_d,force)
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 impI)+
apply (simp add: restrict_neg_map_def)
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_generic)
apply blast
apply (rule allI, rule impI)
apply (case_tac i,simp_all)
apply (rule impI)+
apply (subst disjointUnionEnv_G_G'_G_x,simp,simp)
apply (subst nonDisjointUnionEnv_conmutative)
apply (simp add: def_nonDisjointUnionEnv_def)
apply (subst foldl_prop1)
apply (subst nonDisjointUnionEnv_prop5)
apply (subst dom_restrict_neg_map,force)
apply (rule restrict_neg_map_not_s,assumption+,simp)
apply (rule impI)+
apply (rotate_tac 5)
apply (erule_tac x="nat" in allE,simp)
apply (subst disjointUnionEnv_G_G'_G_x,simp,simp)
apply (subst nonDisjointUnionEnv_conmutative)
apply (simp add: def_nonDisjointUnionEnv_def)
apply (subst foldl_prop1)
apply (subst (asm) disjointUnionEnv_G_G'_G_x,simp)
apply (simp add: def_disjointUnionEnv_def)
apply (rule x_notin_Γ_cased)
apply (subst nonDisjointUnionEnv_prop6)
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)
(**)
lemma closure_monotone_extend_def_extend:
"[| def_extend E (snd (extractP (fst (alts ! i)))) 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 (simp add: def_extend_def)
apply (elim conjE)
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_def_extend:
"[| def_extend E (snd (extractP (fst (alts ! i)))) 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 (simp add: def_extend_def)
apply (elim conjE)
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 identityClosure_h_p_none_no_identityClosure_hh:
"[| y ∈ dom E1; E1 x = Some (Loc p); h p = Some (j,C,vs);
i < length alts; length assert = lenght alts; length alts > 0;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
identityClosure (E1, E2) y (h, k) (h(p := None), k);
¬ identityClosure (E1, E2) y (h, k) (hh, k) |]
==> ¬ identityClosure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) y (h(p := None), k) (hh, k)"
apply (simp add: identityClosure_def)
apply (rule impI)
apply (elim conjE)
apply (subgoal_tac
"y ∉ set (snd (extractP (fst (alts ! i))))")
prefer 2 apply (simp add: def_extend_def,elim conjE,blast)
apply (frule_tac E="E1" and vs="vs" in extend_monotone_i,simp,assumption+)
apply (subgoal_tac
"closure (E1, E2) y (h(p := None), k) = closure (E1, E2) y (hh, k)",simp)
prefer 2 apply (subst closure_monotone_extend_def_extend,assumption+,simp,assumption+)+
apply (subst (asm) closure_monotone_extend_def_extend [where E="E1"],assumption+,simp,assumption+)+
apply (simp add: closure_def)
apply (case_tac "E1 y",simp_all)
apply (case_tac "extend E1 (snd (extractP (fst (alts ! i)))) vs y", simp_all)
apply (case_tac "aa", simp_all)
apply (rename_tac q)
apply (case_tac "p = q",simp_all)
apply clarsimp
apply (rule_tac x="pa" in bexI)
prefer 2 apply simp
apply (rule conjI)
apply (rule impI)
apply (erule_tac x="p" in ballE)
prefer 2 apply simp
apply clarsimp
apply clarsimp
apply clarsimp
apply (rule_tac x="pa" in bexI)
prefer 2 apply simp
apply (rule conjI)
apply (erule_tac x="pa" in ballE)
prefer 2 apply simp
apply clarsimp
by clarsimp
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 dom_foldl_monotone_generic:
" 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_foldl_disjointUnionEnv_monotone_generic_2:
" dom (foldl op ⊗ (empty ⊗ y) ys + A) =
dom y ∪ dom (foldl op ⊗ empty ys) ∪ dom A"
apply (subgoal_tac "empty ⊗ y = y ⊗ empty",simp)
apply (subgoal_tac "foldl op ⊗ (y ⊗ empty) ys =
y ⊗ foldl op ⊗ empty ys",simp)
apply (subst dom_disjointUnionEnv_monotone)
apply (subst union_dom_nonDisjointUnionEnv)
apply simp
apply (rule foldl_prop1)
apply (subgoal_tac "def_nonDisjointUnionEnv empty y")
apply (erule nonDisjointUnionEnv_conmutative)
by (simp add: def_nonDisjointUnionEnv_def)
lemma dom_Γi_in_Γcased [rule_format]:
"length assert > 0
--> length assert = length alts
--> 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))
--> 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))) +
[x \<mapsto> d'']))"
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 union_dom_disjointUnionEnv)
apply (subst (asm) empty_nonDisjointUnionEnv)
apply simp
apply (subst dom_restrict_neg_map)
apply force
apply simp
apply (drule mp)
apply (simp add: def_disjointUnionEnv_def)
apply (subst (asm) dom_foldl_monotone_generic)
apply blast
apply (rule allI, rule impI)
apply (case_tac i,simp_all)
apply (rule impI)
apply (subst dom_foldl_disjointUnionEnv_monotone_generic_2)
apply (subst dom_restrict_neg_map)
apply force
apply (rule impI)
apply (rotate_tac 3)
apply (erule_tac x="nat" in allE,simp)
apply (subst dom_foldl_disjointUnionEnv_monotone_generic_2)
apply (subst (asm) union_dom_disjointUnionEnv)
apply (simp add: def_disjointUnionEnv_def)
apply (subst (asm) dom_foldl_monotone_generic)
apply blast
by blast
lemma identityClosure_h_h_p_none:
"[| identityClosure (E1, E2) y (h, k) (h(p := None), k);
¬ identityClosure (E1, E2) y (h, k) (hh, k);
i < length alts; length assert = length alts; length alts > 0;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
y ∈ dom E1; E1 x = Some (Loc p); h p = Some (j,C,vs);
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''];
Γ = 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''];
(∀x∈dom (fst (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2)).
¬ identityClosure (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) x (h(p := None), k) (hh, k) -->
x ∈ dom (snd (assert ! i)) ∧ snd (assert ! i) x ≠ Some s'') |]
==> y ∈ dom Γ ∧ Γ y ≠ Some s''"
apply (subgoal_tac "y ∉ set (snd (extractP (fst (alts ! i))))")
prefer 2 apply (simp add: def_extend_def,blast)
apply (frule_tac hh="hh" and x="x" in
identityClosure_h_p_none_no_identityClosure_hh,assumption+)
apply (erule_tac x="y" in ballE,simp)
apply (elim conjE)
apply (rule conjI)
apply (rule_tac i=i in dom_Γi_in_Γcased,simp,assumption+)
apply (rule_tac alts="alts" and x="x" and assert="assert" in Otimes_prop_cased_not_s)
apply force apply assumption+
by (simp add: extend_def)
lemma P6_CASED:
"[| Γ = 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''];
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''];
dom Γ ⊆ dom E1;
E1 x = Some (Loc p); h p = Some (j, C, vs); x ∈ dom Γ;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
i < length alts; 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);
∀y∈dom (fst (E1, E2)).
∀z∈insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))).
Γ z = Some d'' ∧
closure (E1, E2) y (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {} -->
y ∈ dom Γ ∧ Γ y ≠ Some s'';
y ∈ dom (fst (E1, E2));
¬ identityClosure (E1, E2) y (h, k) (hh, k)|]
==> y ∈ dom Γ ∧ Γ y ≠ Some s''"
apply (case_tac "¬ identityClosure (E1,E2) y (h,k) (h(p:=None),k)")
(* ¬ identityClosure (E1,E2) y (h,k) (h(p:=None),k) *)
apply (frule not_identityClosure_h_h_p_none_inter_not_empty_h,simp,assumption+,simp)
apply (erule_tac x="y" in ballE)
prefer 2 apply simp
apply (erule_tac x="x" in ballE)
prefer 2 apply simp
apply (drule mp)
apply (rule conjI)
apply (rule Γ_case_x_is_d,force)
apply simp
apply simp
(* identityClosure (E1,E2) y (h,k) (h(p:=None),k) *)
apply (rule identityClosure_h_h_p_none)
apply (simp,simp,assumption+,simp,assumption+,simp,assumption+)
by (simp add: shareRec_def)
lemma P5_CASED:
"[| (E1, E2) \<turnstile> h , k , td , CaseD VarE x () Of alts () \<Down> hh , k , v , r ;
Γ = 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''));
x ∈ dom Γ;
dom Γ ⊆ dom E1;
(\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ⊆ dom Γ;
fv (CaseD VarE x () Of alts ()) ⊆ insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
wellFormed (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (CaseD VarE x () Of alts ()) |]
==> ∀xa∈dom (fst (E1, E2)).
∀z∈insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))).
Γ z = Some d'' ∧
closure (E1, E2) xa (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {} -->
xa ∈ dom Γ ∧ Γ xa ≠ Some s''"
apply (simp only: wellFormed_def)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="td" in allE)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="r" in allE)
apply (drule mp,simp)
by simp
lemma P5_P6_CASED:
"[| (E1, E2) \<turnstile> h , k , td , CaseD VarE x () Of alts () \<Down> hh , k , v , r ;
Γ = 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
(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''];
dom Γ ⊆ dom E1; E1 x = Some (Loc p); h p = Some (j,C,vs);
x ∈ dom Γ;
(\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ⊆ dom Γ ;
fv (CaseD VarE x () Of alts ()) ⊆ insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
alts ≠ []; length assert = length alts;
wellFormed (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (CaseD VarE x () Of alts ());
(E1, E2) \<turnstile> h , k , td , CaseD VarE x () Of alts () \<Down> hh , k , v , r ;
shareRec (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p:=None), k) (hh, k)|]
==> shareRec (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (E1, E2) (h, k) (hh, k)"
apply (simp (no_asm) only: shareRec_def)
apply (rule conjI)
apply (rule P5_CASED,assumption+)
apply (rule ballI,rule impI)
apply (frule P5_CASED,assumption+)
by (rule P6_CASED [where p="p"],assumption+)
lemma P5_f_n_CASED:
"[| (E1, E2) \<turnstile> h , k , CaseD VarE x () Of alts () \<Down>(f,n) hh , k , v;
Γ = 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''));
x ∈ dom Γ;
dom Γ ⊆ dom E1;
(\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ⊆ dom Γ;
fv (CaseD VarE x () Of alts ()) ⊆ insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
wellFormedDepth f n (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (CaseD VarE x () Of alts ()) |]
==> ∀xa∈dom (fst (E1, E2)).
∀z∈insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))).
Γ z = Some d'' ∧
closure (E1, E2) xa (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {} -->
xa ∈ dom Γ ∧ Γ xa ≠ Some s''"
apply (simp only: wellFormedDepth_def)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v" in allE)
apply (drule mp,simp)
by simp
lemma P5_P6_f_n_CASED:
"[| (E1, E2) \<turnstile> h , k, CaseD VarE x () Of alts () \<Down>(f,n) hh , k , v;
Γ = 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
(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''];
dom Γ ⊆ dom E1; E1 x = Some (Loc p); h p = Some (j,C,vs);
x ∈ dom Γ;
(\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ⊆ dom Γ ;
fv (CaseD VarE x () Of alts ()) ⊆ insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
alts ≠ []; length assert = length alts;
wellFormedDepth f n (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (CaseD VarE x () Of alts ());
shareRec (fst (assert ! i)) (snd (assert ! i)) (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) (h(p:=None), k) (hh, k)|]
==> shareRec (insert x (\<Union>i < length alts fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (E1, E2) (h, k) (hh, k)"
apply (simp (no_asm) only: shareRec_def)
apply (rule conjI)
apply (rule P5_f_n_CASED,assumption+)
apply (rule ballI,rule impI)
apply (frule P5_f_n_CASED,assumption+)
by (rule P6_CASED [where p="p"],assumption+)
(********** Demostracion P5_P6_APP ********************)
axioms SafeRASem_extend_heaps:
"(E1,E2) \<turnstile> h,k,td, e \<Down> hh,k,v,r
==> extend_heaps (h,k) (hh,k)"
axioms Lemma4_consistent:
"extend_heaps (h,k) (h',k')
==> ∀ ϑ1 ϑ2 η E1 E2.
consistent (ϑ1,ϑ2) η (E1,E2) h
--> consistent (ϑ1,ϑ2) η (E1,E2) h'"
axioms consistent_identityClosure:
"consistent (ϑ1,ϑ2) η (E1,E2) h
--> consistent (ϑ1,ϑ2) η (E1,E2) (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k})
==> ∀x∈dom E1. identityClosure (E1, E2) x (h, k) (h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}, k)"
lemma P5_P6_APP:
"[| (E1, E2) \<turnstile> h , k , td , AppE f as rs' () \<Down> hh , k , v , r ;
hh = h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k};
dom Γ ⊆ dom E1; ∀a∈set as. atom a;
length xs = length ms; length xs = length as;
wellFormed (fvs' as) Γ (AppE f as rs' ());
fvs' as ⊆ dom Γ;
nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ|]
==> shareRec (fvs' as) Γ (E1, E2) (h, k) (hh, k)"
apply (simp add: shareRec_def)
apply (rule conjI)
(* P5 by wellFormed *)
apply (simp only: wellFormed_def)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="td" in allE)
apply (erule_tac x=" h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}" in allE)
apply (erule_tac x="v" in allE)
apply (erule_tac x="r" in allE)
apply (drule mp)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (rule conjI)
apply simp
apply simp
apply simp
(* P6 by consistent *)
apply (frule SafeRASem_extend_heaps)
apply (frule Lemma4_consistent)
apply (erule_tac x="ϑ1" in allE)
apply (erule_tac x="ϑ2" in allE)
apply (erule_tac x="η" in allE)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (frule consistent_identityClosure)
by simp
axioms SafeDepthSem_extend_heaps:
"(E1,E2) \<turnstile> h,k,e \<Down>(f,n) hh,k,v
==> extend_heaps (h,k) (hh,k)"
lemma P5_P6_f_n_APP:
"[| (E1, E2) \<turnstile> h , k , AppE f as rs' () \<Down>(f,n) hh , k , v;
hh = h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k};
dom Γ ⊆ dom E1; ∀a∈set as. atom a;
length xs = length ms; length xs = length as;
wellFormedDepth f n (fvs' as) Γ (AppE f as rs' ());
fvs' as ⊆ dom Γ;
nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ|]
==> shareRec (fvs' as) Γ (E1, E2) (h, k) (hh, k)"
apply (simp add: shareRec_def)
apply (rule conjI)
(* P5 by wellFormed *)
apply (simp only: wellFormedDepth_def)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x=" h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}" in allE)
apply (erule_tac x="v" in allE)
apply (drule mp)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (rule conjI)
apply simp
apply simp
apply simp
(* P6 by consistent *)
apply (frule SafeDepthSem_extend_heaps)
apply (frule Lemma4_consistent)
apply (erule_tac x="ϑ1" in allE)
apply (erule_tac x="ϑ2" in allE)
apply (erule_tac x="η" in allE)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (frule consistent_identityClosure)
by simp
lemma P5_P6_f_n_APP_2:
"[| (E1, E2) \<turnstile> h , k , AppE g as rs' () \<Down>(f,n) hh , k , v;
hh = h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k};
dom Γ ⊆ dom E1; ∀a∈set as. atom a;
length xs = length ms; length xs = length as;
wellFormedDepth f n (fvs' as) Γ (AppE g as rs' ());
fvs' as ⊆ dom Γ;
nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ|]
==> shareRec (fvs' as) Γ (E1, E2) (h, k) (hh, k)"
apply (simp add: shareRec_def)
apply (rule conjI)
(* P5 by wellFormed *)
apply (simp only: wellFormedDepth_def)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x=" h' |` {p ∈ dom h'. fst (the (h' p)) ≤ k}" in allE)
apply (erule_tac x="v" in allE)
apply (drule mp)
apply (rule conjI,simp)
apply (rule conjI,simp)
apply (rule conjI)
apply simp
apply simp
apply simp
(* P6 by consistent *)
apply (frule SafeDepthSem_extend_heaps)
apply (frule Lemma4_consistent)
apply (erule_tac x="ϑ1" in allE)
apply (erule_tac x="ϑ2" in allE)
apply (erule_tac x="η" in allE)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (frule consistent_identityClosure)
by simp
(*********** PRIMOP ***********)
lemma P5_APP_PRIMOP:
"[| Γ0 = [atom2var a1 \<mapsto> s'',atom2var a2 \<mapsto> s''];
Γ0 ⊆m Γ |]
==> (∀x∈dom (fst (E1, E2)).
∀z∈{atom2var a1, atom2var a2}.
Γ z = Some d'' ∧
closure (E1, E2) x (h, k) ∩ recReach (E1, E2) z (h, k) ≠ {} -->
x ∈ dom Γ ∧ Γ x ≠ Some s'')"
apply (rule ballI)+
apply (rule impI)
apply (elim conjE,clarsimp)
apply (erule disjE,simp_all)
apply (simp add: map_le_def)
apply (split split_if_asm,simp,simp)
by (simp add: map_le_def)
lemma P6_APP_PRIMOP:
"[| Γ0 = [atom2var a1 \<mapsto> s'',atom2var a2 \<mapsto> s''];
Γ0 ⊆m Γ |]
==> ∀x∈dom (fst (E1, E2)).
¬ identityClosure (E1, E2) x (h, k) (h, k) -->
x ∈ dom Γ ∧ Γ x ≠ Some s''"
apply (rule ballI, rule impI)
by (simp add: identityClosure_def)
lemma P5_P6_APP_PRIMOP:
"[| Γ0 = [atom2var a1 \<mapsto> s'',atom2var a2 \<mapsto> s''];
Γ0 ⊆m Γ |]
==> shareRec {atom2var a1, atom2var a2}
Γ
(E1, E2) (h, k) (h, k)"
apply (simp only: shareRec_def)
apply (rule conjI)
apply (rule P5_APP_PRIMOP,assumption+,simp)
by (rule P6_APP_PRIMOP,assumption+,simp)
end
lemma P5_REUSE:
[| Γ x = Some d''; wellFormed {x} Γ (ReuseE x ());
(E1.0, E2.0) \<turnstile> h , k , td , ReuseE x () \<Down> h(p := None)(q |->
c) , k , Loc q , r ;
dom Γ ⊆ dom E1.0; E1.0 x = Some (Loc p) |]
==> ∀xa∈dom E1.0.
closure (E1.0, E2.0) xa (h, k) ∩ recReach (E1.0, E2.0) x (h, k) ≠ {} -->
xa ∈ dom Γ ∧ Γ xa ≠ Some s''
lemma reuse_identityClosure_y_in_E1:
[| (E1.0, E2.0) \<turnstile> h , k , td , ReuseE x () \<Down> h(p := None)(q |->
c) , k , Loc q , r ;
p ∉ closure (E1.0, E2.0) y (h, k); h p = Some c; fresh q h |]
==> identityClosure (E1.0, E2.0) y (h, k) (h(p := None)(q |-> c), k)
lemma P6_REUSE:
[| Γ x = Some d''; h p = Some c; fresh q h; wellFormed {x} Γ (ReuseE x ());
(E1.0, E2.0) \<turnstile> h , k , td , ReuseE x () \<Down> h(p := None)(q |->
c) , k , Loc q , r ;
dom Γ ⊆ dom E1.0; E1.0 x = Some (Loc p) |]
==> ∀x∈dom E1.0.
¬ identityClosure (E1.0, E2.0) x (h, k) (h(p := None)(q |-> c), k) -->
x ∈ dom Γ ∧ Γ x ≠ Some s''
lemma P5_P6_REUSE:
[| Γ x = Some d''; wellFormed {x} Γ (ReuseE x ()); h p = Some c; fresh q h;
(E1.0, E2.0) \<turnstile> h , k , td , ReuseE x () \<Down> h(p := None)(q |->
c) , k , Loc q , r ;
dom Γ ⊆ dom E1.0; E1.0 x = Some (Loc p) |]
==> shareRec {x} Γ (E1.0, E2.0) (h, k) (h(p := None)(q |-> c), k)
lemma P5_COPY:
[| wellFormed {x} Γ (x @ r ());
(E1.0, E2.0) \<turnstile> h , k , td , x @ r () \<Down> hh , k , v , ra ;
dom Γ ⊆ dom E1.0; E1.0 x = Some (Loc p) |]
==> ∀xa∈dom E1.0.
Γ x = Some d'' ∧
closure (E1.0, E2.0) xa (h, k) ∩ recReach (E1.0, E2.0) x (h, k) ≠ {} -->
xa ∈ dom Γ ∧ Γ xa ≠ Some s''
lemma P6_COPY:
[| wellFormed {x} Γ (x @ r ());
(E1.0, E2.0) \<turnstile> h , k , td , x @ r () \<Down> hh , k , v , ra ;
dom Γ ⊆ dom E1.0; E1.0 x = Some (Loc p) |]
==> ∀x∈dom E1.0.
¬ identityClosure (E1.0, E2.0) x (h, k) (hh, k) -->
x ∈ dom Γ ∧ Γ x ≠ Some s''
lemma P5_P6_COPY:
[| wellFormed {x} Γ (x @ r ());
(E1.0, E2.0) \<turnstile> h , k , td , x @ r () \<Down> hh , k , v , ra ;
dom Γ ⊆ dom E1.0; E1.0 x = Some (Loc p) |]
==> shareRec {x} Γ (E1.0, E2.0) (h, k) (hh, k)
lemma Γ1z_s_Γ2z_d_equals_recReach:
[| def_disjointUnionEnv Γ2.0 [x1.0 |-> m]; dom Γ1.0 ⊆ dom E1.0;
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k'); x ∈ dom E1.0; z ≠ x1.0;
Γ1.0 z = Some s''; z ∈ L1.0 |]
==> recReach (E1.0, E2.0) z (h, k) =
recReach (E1.0(x1.0 |-> r), E2.0) z (h', k')
lemma P5_Γ2z_d_Γ1z_s:
[| def_pp Γ1.0 Γ2.0 L2.0; dom Γ1.0 ⊆ dom E1.0;
def_disjointUnionEnv Γ2.0 [x1.0 |-> m];
dom Γ1.0\<triangleright>Γ2.0 L2.0 ⊆ dom E1.0;
shareRec L2.0 (Γ2.0 + [x1.0 |-> m]) (E1.0(x1.0 |-> r), E2.0) (h', k')
(hh, kk);
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k'); x ∈ dom E1.0;
Γ1.0 z = Some s''; z ∈ L1.0; z ∈ L2.0; x1.0 ∉ L1.0; Γ2.0 z = Some d'';
Γ1.0\<triangleright>Γ2.0 L2.0 z = Some d''; x1.0 ∉ dom E1.0; z ≠ x1.0;
closure (E1.0, E2.0) x (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠ {} |]
==> x ∈ dom Γ1.0\<triangleright>Γ2.0 L2.0 ∧
Γ1.0\<triangleright>Γ2.0 L2.0 x ≠ Some s''
lemma P5_Γ1z_d:
[| shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k'); x ∈ dom E1.0;
Γ1.0\<triangleright>Γ2.0 L2.0 z = Some d'';
closure (E1.0, E2.0) x (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠ {};
z ∈ L1.0; Γ1.0 z = Some d'' |]
==> x ∈ dom Γ1.0\<triangleright>Γ2.0 L2.0 ∧
Γ1.0\<triangleright>Γ2.0 L2.0 x ≠ Some s''
lemma P5_LET_L1:
[| def_pp Γ1.0 Γ2.0 L2.0; L1.0 ⊆ dom Γ1.0;
dom Γ1.0\<triangleright>Γ2.0 L2.0 ⊆ dom E1.0; dom Γ1.0 ⊆ dom E1.0;
def_disjointUnionEnv Γ2.0 [x1.0 |-> m];
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k');
shareRec L2.0 (Γ2.0 + [x1.0 |-> m]) (E1.0(x1.0 |-> r), E2.0) (h', k')
(hh, kk);
x ∈ dom E1.0; x1.0 ∉ dom E1.0; x1.0 ∉ L1.0;
Γ1.0\<triangleright>Γ2.0 L2.0 z = Some d'';
closure (E1.0, E2.0) x (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠ {};
z ∈ L1.0 |]
==> x ∈ dom Γ1.0\<triangleright>Γ2.0 L2.0 ∧
Γ1.0\<triangleright>Γ2.0 L2.0 x ≠ Some s''
lemma P5_z_notin_L1_Γ1z_s_Γ2z_d:
[| def_pp Γ1.0 Γ2.0 L2.0; def_disjointUnionEnv Γ2.0 [x1.0 |-> m];
dom Γ1.0\<triangleright>Γ2.0 L2.0 ⊆ dom E1.0;
shareRec L2.0 (Γ2.0 + [x1.0 |-> m]) (E1.0(x1.0 |-> r), E2.0) (h', k')
(hh, kk);
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k'); x ∈ dom E1.0;
Γ1.0 z = Some s''; z ∈ L2.0; x1.0 ∉ L1.0; Γ2.0 z = Some d'';
Γ1.0\<triangleright>Γ2.0 L2.0 z = Some d''; x1.0 ∉ dom E1.0; z ≠ x1.0;
closure (E1.0, E2.0) x (h, k) ∩
recReach (E1.0(x1.0 |-> r), E2.0) z (h', k') ≠
{};
recReach (E1.0, E2.0) z (h, k) =
recReach (E1.0(x1.0 |-> r), E2.0) z (h', k') |]
==> x ∈ dom Γ1.0\<triangleright>Γ2.0 L2.0 ∧
Γ1.0\<triangleright>Γ2.0 L2.0 x ≠ Some s''
lemma P5_Γ2z_d_Γ1z_s_z_in_L2:
[| def_pp Γ1.0 Γ2.0 L2.0; def_disjointUnionEnv Γ2.0 [x1.0 |-> m];
dom Γ1.0\<triangleright>Γ2.0 L2.0 ⊆ dom E1.0;
shareRec L2.0 (Γ2.0 + [x1.0 |-> m]) (E1.0(x1.0 |-> r), E2.0) (h', k')
(hh, kk);
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k'); x ∈ dom E1.0;
Γ1.0 z = Some s''; z ∈ L2.0; x1.0 ∉ L1.0; Γ2.0 z = Some d'';
Γ1.0\<triangleright>Γ2.0 L2.0 z = Some d''; x1.0 ∉ dom E1.0; z ≠ x1.0;
recReach (E1.0, E2.0) z (h, k) =
recReach (E1.0(x1.0 |-> r), E2.0) z (h', k');
closure (E1.0, E2.0) x (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠ {} |]
==> x ∈ dom Γ1.0\<triangleright>Γ2.0 L2.0 ∧
Γ1.0\<triangleright>Γ2.0 L2.0 x ≠ Some s''
lemma P5_Γ2z_d_z_notin_Γ1:
[| def_pp Γ1.0 Γ2.0 L2.0; def_disjointUnionEnv Γ2.0 [x1.0 |-> m];
dom Γ1.0\<triangleright>Γ2.0 L2.0 ⊆ dom E1.0;
shareRec L2.0 (Γ2.0 + [x1.0 |-> m]) (E1.0(x1.0 |-> r), E2.0) (h', k')
(hh, kk);
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k'); x ∈ dom E1.0; z ∉ dom Γ1.0;
z ∈ L2.0; x1.0 ∉ L1.0; Γ2.0 z = Some d'';
Γ1.0\<triangleright>Γ2.0 L2.0 z = Some d''; x1.0 ∉ dom E1.0; z ≠ x1.0;
recReach (E1.0, E2.0) z (h, k) =
recReach (E1.0(x1.0 |-> r), E2.0) z (h', k');
closure (E1.0, E2.0) x (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠ {} |]
==> x ∈ dom Γ1.0\<triangleright>Γ2.0 L2.0 ∧
Γ1.0\<triangleright>Γ2.0 L2.0 x ≠ Some s''
lemma P5_LET_L2:
[| L1.0 ⊆ dom Γ1.0; dom Γ1.0 ⊆ dom E1.0; L2.0 ⊆ dom (Γ2.0 + [x1.0 |-> m]);
def_pp Γ1.0 Γ2.0 L2.0; dom Γ1.0\<triangleright>Γ2.0 L2.0 ⊆ dom E1.0;
def_disjointUnionEnv Γ2.0 [x1.0 |-> m];
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k');
shareRec L2.0 (Γ2.0 + [x1.0 |-> m]) (E1.0(x1.0 |-> r), E2.0) (h', k')
(hh, kk);
x ∈ dom E1.0; x1.0 ∉ dom E1.0; x1.0 ∉ L1.0;
Γ1.0\<triangleright>Γ2.0 L2.0 z = Some d'';
closure (E1.0, E2.0) x (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠ {};
z ∈ L2.0; z ≠ x1.0 |]
==> x ∈ dom Γ1.0\<triangleright>Γ2.0 L2.0 ∧
Γ1.0\<triangleright>Γ2.0 L2.0 x ≠ Some s''
lemma P5_Cond2:
[| L1.0 ⊆ dom Γ1.0; L2.0 ⊆ dom (Γ2.0 + [x1.0 |-> m]); x1.0 ∉ dom E1.0;
x1.0 ∉ L1.0; dom Γ1.0\<triangleright>Γ2.0 L2.0 ⊆ dom E1.0;
def_pp Γ1.0 Γ2.0 L2.0; def_disjointUnionEnv Γ2.0 [x1.0 |-> m];
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k');
shareRec L2.0 (Γ2.0 + [x1.0 |-> m]) (E1.0(x1.0 |-> r), E2.0) (h', k')
(hh, kk) |]
==> ∀x∈dom E1.0.
¬ identityClosure (E1.0, E2.0) x (h, k) (hh, kk) -->
x ∈ dom Γ1.0\<triangleright>Γ2.0 L2.0 ∧
Γ1.0\<triangleright>Γ2.0 L2.0 x ≠ Some s''
lemma P5_P6_LET:
[| L1.0 ⊆ dom Γ1.0; dom Γ1.0 ⊆ dom E1.0; L2.0 ⊆ dom (Γ2.0 + [x1.0 |-> m]);
x1.0 ∉ dom E1.0; x1.0 ∉ L1.0; dom Γ1.0\<triangleright>Γ2.0 L2.0 ⊆ dom E1.0;
def_pp Γ1.0 Γ2.0 L2.0; def_disjointUnionEnv Γ2.0 [x1.0 |-> m];
shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k) (h', k');
shareRec L2.0 (Γ2.0 + [x1.0 |-> m]) (E1.0(x1.0 |-> r), E2.0) (h', k')
(hh, kk) |]
==> shareRec (L1.0 ∪ (L2.0 - {x1.0})) Γ1.0\<triangleright>Γ2.0 L2.0 (E1.0, E2.0)
(h, k) (hh, kk)
lemma Γ1_z_Some_s:
z ∈ atom2var ` set as
==> map_of (zip (map atom2var as) (replicate (length as) s'')) z = Some s''
lemma P5_LETC_e1:
∀x∈dom (fst (E1.0, E2.0)).
∀z∈set (map atom2var as).
map_of (zip (map atom2var as) (replicate (length as) s'')) z = Some d'' ∧
closure (E1.0, E2.0) x (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠ {} -->
x ∈ dom (map_of (zip (map atom2var as) (replicate (length as) s''))) ∧
map_of (zip (map atom2var as) (replicate (length as) s'')) x ≠ Some s''
lemma ext_h_same_descendants:
[| fresh p h; q ≠ p |] ==> descendants q (h, k) = descendants q (h(p |-> c), k)
lemma ext_h_same_recDescendants:
[| fresh p h; q ≠ p |]
==> recDescendants q (h, k) = recDescendants q (h(p |-> c), k)
lemma ext_h_same_closure:
[| (E1.0, E2.0) \<turnstile> h , k , td , e \<Down> h' , k , v , r ;
fresh p h |]
==> closure (E1.0, E2.0) x (h, k) = closure (E1.0, E2.0) x (h(p |-> c), k)
lemma ext_h_same_recReach:
[| (E1.0, E2.0) \<turnstile> h , k , td , e \<Down> h' , k , v , r ;
fresh p h |]
==> recReach (E1.0, E2.0) x (h, k) = recReach (E1.0, E2.0) x (h(p |-> c), k)
lemma closure_upt_monotone:
[| x ∈ dom E1.0; x1.0 ∉ dom E1.0 |]
==> closure (E1.0, E2.0) x (h, k) =
closure (E1.0(x1.0 |-> Loc p), E2.0) x (h, k)
lemma recReach_upt_monotone:
[| x ∈ dom E1.0; x1.0 ∉ dom E1.0 |]
==> recReach (E1.0, E2.0) x (h, k) =
recReach (E1.0(x1.0 |-> Loc p), E2.0) x (h, k)
lemma cvte_ext_h_inter_closure_recReach:
[| (E1.0, E2.0) \<turnstile> h , k , td , e \<Down> h' , k , v , r ; fresh p h;
x1.0 ∉ dom E1.0; x ∈ dom E1.0; z ∈ dom E1.0;
closure (E1.0, E2.0) x (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠ {} |]
==> closure (E1.0(x1.0 |-> Loc p), E2.0) x
(h(p |-> (j, C, map (atom2val E1.0) as)), k) ∩
recReach (E1.0(x1.0 |-> Loc p), E2.0) z
(h(p |-> (j, C, map (atom2val E1.0) as)), k) ≠
{}
lemma ext_h_same_identityClosure_upt:
[| fresh p h; x ∈ dom E1.0;
(E1.0, E2.0) \<turnstile> h , k , td , e \<Down> h' , k , v , r |]
==> identityClosure (E1.0, E2.0) x (h, k) (h(p |-> c), k)
lemma P6_LETC_e1:
[| (E1.0,
E2.0) \<turnstile> h , k , td , Let x1.0 = ConstrE C as r
a' In e2.0 a \<Down> hh , k , v , ra ;
(E1.0(x1.0 |-> Loc p), E2.0) \<turnstile> h(p |->
(j, C,
map (atom2val E1.0) as)) , k , (td + 1) , e2.0 \<Down> hh , k , v , rs' ;
x1.0 ∉ L1.0; x1.0 ∉ dom E1.0;
def_pp (map_of (zip (map atom2var as) (replicate (length as) s''))) Γ2.0
L2.0;
dom map_of
(zip (map atom2var as)
(replicate (length as) s''))\<triangleright>Γ2.0 L2.0
⊆ dom E1.0;
fresh p h;
∀x∈dom (fst (E1.0(x1.0 |-> Loc p), E2.0)).
¬ identityClosure (E1.0(x1.0 |-> Loc p), E2.0) x
(h(p |-> (j, C, map (atom2val E1.0) as)), k) (hh, k) -->
x ∈ dom (Γ2.0 + [x1.0 |-> m'']) ∧ (Γ2.0 + [x1.0 |-> m'']) x ≠ Some s'' |]
==> ∀x∈dom (fst (E1.0, E2.0)).
¬ identityClosure (E1.0, E2.0) x (h, k)
(h(p |-> (j, C, map (atom2val E1.0) as)), k) -->
x ∈ dom (map_of (zip (map atom2var as) (replicate (length as) s''))) ∧
map_of (zip (map atom2var as) (replicate (length as) s'')) x ≠ Some s''
lemma P5_P6_LETC_e1:
[| (E1.0,
E2.0) \<turnstile> h , k , td , Let x1.0 = ConstrE C as r
a' In e2.0 a \<Down> hh , k , v , ra ;
(E1.0(x1.0 |-> Loc p), E2.0) \<turnstile> h(p |->
(j, C,
map (atom2val E1.0) as)) , k , (td + 1) , e2.0 \<Down> hh , k , v , rs' ;
x1.0 ∉ L1.0; x1.0 ∉ dom E1.0; L1.0 = set (map atom2var as);
Γ1.0 = map_of (zip (map atom2var as) (replicate (length as) s''));
dom map_of
(zip (map atom2var as)
(replicate (length as) s''))\<triangleright>Γ2.0 L2.0
⊆ dom E1.0;
def_pp (map_of (zip (map atom2var as) (replicate (length as) s''))) Γ2.0
L2.0;
shareRec L2.0 (Γ2.0 + [x1.0 |-> m'']) (E1.0(x1.0 |-> Loc p), E2.0)
(h(p |-> (j, C, map (atom2val E1.0) as)), k) (hh, k);
fresh p h |]
==> shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k)
(h(p |-> (j, C, map (atom2val E1.0) as)), k)
lemma ext_h_same_closure_semDepth:
[| (E1.0, E2.0) \<turnstile> h , k , e \<Down> (f, n) h' , k , v ;
fresh p h |]
==> closure (E1.0, E2.0) x (h, k) = closure (E1.0, E2.0) x (h(p |-> c), k)
lemma ext_h_same_identityClosure_upt_semDepth:
[| fresh p h; x ∈ dom E1.0;
(E1.0, E2.0) \<turnstile> h , k , e \<Down> (f, n) h' , k , v |]
==> identityClosure (E1.0, E2.0) x (h, k) (h(p |-> c), k)
lemma P6_f_n_LETC_e1:
[| (E1.0,
E2.0) \<turnstile> h , k , Let x1.0 = ConstrE C as r
a' In e2.0 a \<Down> (f, n) hh , k , v ;
(E1.0(x1.0 |-> Loc p), E2.0) \<turnstile> h(p |->
(j, C, map (atom2val E1.0) as)) , k , e2.0 \<Down> (f, n) hh , k , v ;
x1.0 ∉ L1.0; x1.0 ∉ dom E1.0;
def_pp (map_of (zip (map atom2var as) (replicate (length as) s''))) Γ2.0
L2.0;
dom map_of
(zip (map atom2var as)
(replicate (length as) s''))\<triangleright>Γ2.0 L2.0
⊆ dom E1.0;
fresh p h;
∀x∈dom (fst (E1.0(x1.0 |-> Loc p), E2.0)).
¬ identityClosure (E1.0(x1.0 |-> Loc p), E2.0) x
(h(p |-> (j, C, map (atom2val E1.0) as)), k) (hh, k) -->
x ∈ dom (Γ2.0 + [x1.0 |-> m'']) ∧ (Γ2.0 + [x1.0 |-> m'']) x ≠ Some s'' |]
==> ∀x∈dom (fst (E1.0, E2.0)).
¬ identityClosure (E1.0, E2.0) x (h, k)
(h(p |-> (j, C, map (atom2val E1.0) as)), k) -->
x ∈ dom (map_of (zip (map atom2var as) (replicate (length as) s''))) ∧
map_of (zip (map atom2var as) (replicate (length as) s'')) x ≠ Some s''
lemma P5_P6_f_n_LETC_e1:
[| (E1.0,
E2.0) \<turnstile> h , k , Let x1.0 = ConstrE C as r
a' In e2.0 a \<Down> (f, n) hh , k , v ;
(E1.0(x1.0 |-> Loc p), E2.0) \<turnstile> h(p |->
(j, C, map (atom2val E1.0) as)) , k , e2.0 \<Down> (f, n) hh , k , v ;
x1.0 ∉ L1.0; x1.0 ∉ dom E1.0; L1.0 = set (map atom2var as);
Γ1.0 = map_of (zip (map atom2var as) (replicate (length as) s''));
dom map_of
(zip (map atom2var as)
(replicate (length as) s''))\<triangleright>Γ2.0 L2.0
⊆ dom E1.0;
def_pp (map_of (zip (map atom2var as) (replicate (length as) s''))) Γ2.0
L2.0;
shareRec L2.0 (Γ2.0 + [x1.0 |-> m'']) (E1.0(x1.0 |-> Loc p), E2.0)
(h(p |-> (j, C, map (atom2val E1.0) as)), k) (hh, k);
fresh p h |]
==> shareRec L1.0 Γ1.0 (E1.0, E2.0) (h, k)
(h(p |-> (j, C, map (atom2val E1.0) as)), k)
lemma P5_CASE_shareRec:
[| (E1.0,
E2.0) \<turnstile> h , k , td , Case VarE x
() Of alts () \<Down> hh , k , v , r ;
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1.0;
insert x
(UN i<length alts. fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ())
⊆ insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
wellFormed
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ()) |]
==> ∀xa∈dom (fst (E1.0, E2.0)).
∀z∈insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))).
foldl op ⊗ empty (map snd assert) z = Some d'' ∧
closure (E1.0, E2.0) xa (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠
{} -->
xa ∈ dom (foldl op ⊗ empty (map snd assert)) ∧
foldl op ⊗ empty (map snd assert) xa ≠ Some s''
lemma closure_monotone_extend:
[| x ∈ dom E; def_extend E (snd (extractP (fst (alts ! i)))) vs;
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 identityClosure_monotone_extend:
[| x ∈ dom E1.0; 0 < length alts; i < length alts;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs;
¬ identityClosure (E1.0, E2.0) x (h, k) (hh, k) |]
==> ¬ identityClosure (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) x
(h, k) (hh, k)
lemma P5_CASE_identityClosure:
[| length assert = length alts; 0 < length alts; i < length alts;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs;
def_nonDisjointUnionEnvList (map snd assert);
∀x∈dom (fst (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)).
¬ identityClosure (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
x (h, k) (hh, k) -->
x ∈ dom (snd (assert ! i)) ∧ snd (assert ! i) x ≠ Some s'' |]
==> ∀x∈dom (fst (E1.0, E2.0)).
¬ identityClosure (E1.0, E2.0) x (h, k) (hh, k) -->
x ∈ dom (foldl op ⊗ empty (map snd assert)) ∧
foldl op ⊗ empty (map snd assert) x ≠ Some s''
lemma P5_P6_CASE:
[| (E1.0,
E2.0) \<turnstile> h , k , td , Case VarE x
() Of alts () \<Down> hh , k , v , r ;
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1.0;
insert x
(UN i<length alts. fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ())
⊆ insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts; def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs;
def_nonDisjointUnionEnvList (map snd assert); alts ≠ [];
length assert = length alts;
wellFormed
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ());
(E1.0,
E2.0) \<turnstile> h , k , td , Case VarE x
() Of alts () \<Down> hh , k , v , r ;
shareRec (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k) (hh, k) |]
==> shareRec
(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) (hh, k)
lemma P5_f_n_CASE_shareRec:
[| (E1.0,
E2.0) \<turnstile> h , k , Case VarE x
() Of alts () \<Down> (f, n) hh , k , v ;
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1.0;
insert x
(UN i<length alts. fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ())
⊆ insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
wellFormedDepth f n
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ()) |]
==> ∀xa∈dom (fst (E1.0, E2.0)).
∀z∈insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))).
foldl op ⊗ empty (map snd assert) z = Some d'' ∧
closure (E1.0, E2.0) xa (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠
{} -->
xa ∈ dom (foldl op ⊗ empty (map snd assert)) ∧
foldl op ⊗ empty (map snd assert) xa ≠ Some s''
lemma P5_P6_f_n_CASE:
[| (E1.0,
E2.0) \<turnstile> h , k , Case VarE x
() Of alts () \<Down> (f, n) hh , k , v ;
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1.0;
insert x
(UN i<length alts. fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ())
⊆ insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts; def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs;
def_nonDisjointUnionEnvList (map snd assert); alts ≠ [];
length assert = length alts;
wellFormedDepth f n
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ());
shareRec (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h, k) (hh, k) |]
==> shareRec
(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) (hh, k)
lemma P5_CASE_1_1_identityClosure:
[| length assert = length alts; 0 < length alts; i < length alts;
fst (alts ! i) = ConstP (LitN n);
def_nonDisjointUnionEnvList (map snd assert);
∀x∈dom (fst (E1.0, E2.0)).
¬ identityClosure (E1.0, E2.0) x (h, k) (hh, k) -->
x ∈ dom (snd (assert ! i)) ∧ snd (assert ! i) x ≠ Some s'' |]
==> ∀x∈dom (fst (E1.0, E2.0)).
¬ identityClosure (E1.0, E2.0) x (h, k) (hh, k) -->
x ∈ dom (foldl op ⊗ empty (map snd assert)) ∧
foldl op ⊗ empty (map snd assert) x ≠ Some s''
lemma P5_P6_CASE_1_1:
[| (E1.0,
E2.0) \<turnstile> h , k , td , Case VarE x
() Of alts () \<Down> hh , k , v , r ;
fst (alts ! i) = ConstP (LitN n);
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1.0;
insert x
(UN i<length alts. fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ())
⊆ insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts; def_nonDisjointUnionEnvList (map snd assert); alts ≠ [];
length assert = length alts;
wellFormed
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ());
(E1.0,
E2.0) \<turnstile> h , k , td , Case VarE x
() Of alts () \<Down> hh , k , v , r ;
shareRec (fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k) (hh, k) |]
==> shareRec
(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) (hh, k)
lemma P5_P6_f_n_CASE_1_1:
[| (E1.0,
E2.0) \<turnstile> h , k , Case VarE x
() Of alts () \<Down> (f, n) hh , k , v ;
fst (alts ! i) = ConstP (LitN n');
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1.0;
insert x
(UN i<length alts. fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ())
⊆ insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts; def_nonDisjointUnionEnvList (map snd assert); alts ≠ [];
length assert = length alts;
wellFormedDepth f n
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ());
shareRec (fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k) (hh, k) |]
==> shareRec
(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) (hh, k)
lemma P5_CASE_1_2_identityClosure:
[| length assert = length alts; 0 < length alts; i < length alts;
fst (alts ! i) = ConstP (LitB b);
def_nonDisjointUnionEnvList (map snd assert);
∀x∈dom (fst (E1.0, E2.0)).
¬ identityClosure (E1.0, E2.0) x (h, k) (hh, k) -->
x ∈ dom (snd (assert ! i)) ∧ snd (assert ! i) x ≠ Some s'' |]
==> ∀x∈dom (fst (E1.0, E2.0)).
¬ identityClosure (E1.0, E2.0) x (h, k) (hh, k) -->
x ∈ dom (foldl op ⊗ empty (map snd assert)) ∧
foldl op ⊗ empty (map snd assert) x ≠ Some s''
lemma P5_P6_CASE_1_2:
[| (E1.0,
E2.0) \<turnstile> h , k , td , Case VarE x
() Of alts () \<Down> hh , k , v , r ;
fst (alts ! i) = ConstP (LitB b);
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1.0;
insert x
(UN i<length alts. fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ())
⊆ insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts; def_nonDisjointUnionEnvList (map snd assert); alts ≠ [];
length assert = length alts;
wellFormed
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ());
(E1.0,
E2.0) \<turnstile> h , k , td , Case VarE x
() Of alts () \<Down> hh , k , v , r ;
shareRec (fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k) (hh, k) |]
==> shareRec
(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) (hh, k)
lemma P5_P6_f_n_CASE_1_2:
[| (E1.0,
E2.0) \<turnstile> h , k , Case VarE x
() Of alts () \<Down> (f, n) hh , k , v ;
fst (alts ! i) = ConstP (LitB b);
dom (foldl op ⊗ empty (map snd assert)) ⊆ dom E1.0;
insert x
(UN i<length alts. fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
⊆ dom (foldl op ⊗ empty (map snd assert));
fv (Case VarE x () Of alts ())
⊆ insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts; def_nonDisjointUnionEnvList (map snd assert); alts ≠ [];
length assert = length alts;
wellFormedDepth f n
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
(foldl op ⊗ empty (map snd assert)) (Case VarE x () Of alts ());
shareRec (fst (assert ! i)) (snd (assert ! i)) (E1.0, E2.0) (h, k) (hh, k) |]
==> shareRec
(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) (hh, k)
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 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 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 closureL_p_None_p:
closureL p (h(p := None), k) = {p}
lemma recReachL_p_None_p:
recReachL p (h(p := None), k) = {p}
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 p_in_closure_q_p_none:
[| p ≠ q; closureL q (h, k) ≠ closureL q (h(p := None), k) |]
==> p ∈ closureL q (h(p := None), k)
lemma not_identityClosure_h_h_p_none_inter_not_empty_h:
[| y ∈ dom E1.0; E1.0 x = Some (Loc p); h p = Some (j, C, vn);
¬ identityClosure (E1.0, E2.0) y (h, k) (h(p := None), k) |]
==> closure (E1.0, E2.0) y (h, k) ∩ recReach (E1.0, E2.0) x (h, k) ≠ {}
lemma dom_foldl_monotone_generic:
dom (foldl op ⊗ (empty ⊗ x) xs) = dom x ∪ dom (foldl op ⊗ empty xs)
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 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 disjointUnionEnv_G_G'_G_x:
[| x ∉ dom G'; def_disjointUnionEnv G G' |] ==> (G + G') x = G x
lemma restrict_neg_map_not_s:
[| G y ≠ Some s''; x ≠ y; y ∉ L |]
==> restrict_neg_map G (insert x L) y ≠ Some s''
lemma Otimes_prop_cased_not_s:
[| 0 < length assert; 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 s'';
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 s''
lemma closure_monotone_extend_def_extend:
[| def_extend E (snd (extractP (fst (alts ! i)))) 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_def_extend:
[| def_extend E (snd (extractP (fst (alts ! i)))) 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 identityClosure_h_p_none_no_identityClosure_hh:
[| y ∈ dom E1.0; E1.0 x = Some (Loc p); h p = Some (j, C, vs); i < length alts;
length assert = lenght alts; 0 < length alts;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs;
identityClosure (E1.0, E2.0) y (h, k) (h(p := None), k);
¬ identityClosure (E1.0, E2.0) y (h, k) (hh, k) |]
==> ¬ identityClosure (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) y
(h(p := None), k) (hh, k)
lemma dom_restrict_neg_map:
dom (restrict_neg_map m A) = dom m - dom m ∩ A
lemma dom_foldl_monotone_generic:
dom (foldl op ⊗ (empty ⊗ x) xs) = dom x ∪ dom (foldl op ⊗ empty xs)
lemma dom_foldl_disjointUnionEnv_monotone_generic_2:
dom (foldl op ⊗ (empty ⊗ y) ys + A) = dom y ∪ dom (foldl op ⊗ empty ys) ∪ dom A
lemma dom_Γi_in_Γcased:
[| 0 < length assert; length assert = length alts;
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));
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))) +
[x |-> d''])
lemma identityClosure_h_h_p_none:
[| identityClosure (E1.0, E2.0) y (h, k) (h(p := None), k);
¬ identityClosure (E1.0, E2.0) y (h, k) (hh, k); i < length alts;
length assert = length alts; 0 < length alts;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs; y ∈ dom E1.0;
E1.0 x = Some (Loc p); h p = Some (j, C, vs);
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''];
Γ = nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (set Li ∪ {x}))
(zip (map (snd o extractP o fst) alts) (map snd assert))) +
[x |-> d''];
∀x∈dom (fst (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)).
¬ identityClosure (extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0)
x (h(p := None), k) (hh, k) -->
x ∈ dom (snd (assert ! i)) ∧ snd (assert ! i) x ≠ Some s'' |]
==> y ∈ dom Γ ∧ Γ y ≠ Some s''
lemma P6_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''];
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''];
dom Γ ⊆ dom E1.0; E1.0 x = Some (Loc p); h p = Some (j, C, vs); x ∈ dom Γ;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs; i < length alts;
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);
∀y∈dom (fst (E1.0, E2.0)).
∀z∈insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))).
Γ z = Some d'' ∧
closure (E1.0, E2.0) y (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠ {} -->
y ∈ dom Γ ∧ Γ y ≠ Some s'';
y ∈ dom (fst (E1.0, E2.0));
¬ identityClosure (E1.0, E2.0) y (h, k) (hh, k) |]
==> y ∈ dom Γ ∧ Γ y ≠ Some s''
lemma P5_CASED:
[| (E1.0,
E2.0) \<turnstile> h , k , td , CaseD VarE x
() Of alts () \<Down> hh , k , v , r ;
Γ = nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (set Li ∪ {x}))
(zip (map (snd o extractP o fst) alts) (map snd assert))) +
[x |-> d''];
x ∈ dom Γ; dom Γ ⊆ dom E1.0;
(UN i<length alts. fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
⊆ dom Γ;
fv (CaseD VarE x () Of alts ())
⊆ insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
wellFormed
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (CaseD VarE x () Of alts ()) |]
==> ∀xa∈dom (fst (E1.0, E2.0)).
∀z∈insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))).
Γ z = Some d'' ∧
closure (E1.0, E2.0) xa (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠
{} -->
xa ∈ dom Γ ∧ Γ xa ≠ Some s''
lemma P5_P6_CASED:
[| (E1.0,
E2.0) \<turnstile> h , k , td , CaseD VarE x
() Of alts () \<Down> hh , k , v , r ;
Γ = 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
(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''];
dom Γ ⊆ dom E1.0; E1.0 x = Some (Loc p); h p = Some (j, C, vs); x ∈ dom Γ;
(UN i<length alts. fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
⊆ dom Γ;
fv (CaseD VarE x () Of alts ())
⊆ insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts; def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs;
alts ≠ []; length assert = length alts;
wellFormed
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (CaseD VarE x () Of alts ());
(E1.0,
E2.0) \<turnstile> h , k , td , CaseD VarE x
() Of alts () \<Down> hh , k , v , r ;
shareRec (fst (assert ! i)) (snd (assert ! i))
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs, E2.0) (h(p := None), k)
(hh, k) |]
==> shareRec
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (E1.0, E2.0) (h, k) (hh, k)
lemma P5_f_n_CASED:
[| (E1.0,
E2.0) \<turnstile> h , k , CaseD VarE x
() Of alts () \<Down> (f,
n) hh , k , v ;
Γ = nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (set Li ∪ {x}))
(zip (map (snd o extractP o fst) alts) (map snd assert))) +
[x |-> d''];
x ∈ dom Γ; dom Γ ⊆ dom E1.0;
(UN i<length alts. fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
⊆ dom Γ;
fv (CaseD VarE x () Of alts ())
⊆ insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
wellFormedDepth f n
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (CaseD VarE x () Of alts ()) |]
==> ∀xa∈dom (fst (E1.0, E2.0)).
∀z∈insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))).
Γ z = Some d'' ∧
closure (E1.0, E2.0) xa (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠
{} -->
xa ∈ dom Γ ∧ Γ xa ≠ Some s''
lemma P5_P6_f_n_CASED:
[| (E1.0,
E2.0) \<turnstile> h , k , CaseD VarE x
() Of alts () \<Down> (f,
n) hh , k , v ;
Γ = 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
(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''];
dom Γ ⊆ dom E1.0; E1.0 x = Some (Loc p); h p = Some (j, C, vs); x ∈ dom Γ;
(UN i<length alts. fst (assert ! i) - set (snd (extractP (fst (alts ! i)))))
⊆ dom Γ;
fv (CaseD VarE x () Of alts ())
⊆ insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i)))));
i < length alts; def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs;
alts ≠ []; length assert = length alts;
wellFormedDepth f n
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (CaseD VarE x () Of 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) |]
==> shareRec
(insert x
(UN i<length alts.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))))
Γ (E1.0, E2.0) (h, k) (hh, k)
lemma P5_P6_APP:
[| (E1.0,
E2.0) \<turnstile> h , k , td , AppE f as rs' () \<Down> hh , k , v , r ;
hh = h' |` {p : dom h'. fst (the (h' p)) ≤ k}; dom Γ ⊆ dom E1.0;
∀a∈set as. atom a; length xs = length ms; length xs = length as;
wellFormed (fvs' as) Γ (AppE f as rs' ()); fvs' as ⊆ dom Γ;
nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ |]
==> shareRec (fvs' as) Γ (E1.0, E2.0) (h, k) (hh, k)
lemma P5_P6_f_n_APP:
[| (E1.0,
E2.0) \<turnstile> h , k , AppE f as rs' () \<Down> (f, n) hh , k , v ;
hh = h' |` {p : dom h'. fst (the (h' p)) ≤ k}; dom Γ ⊆ dom E1.0;
∀a∈set as. atom a; length xs = length ms; length xs = length as;
wellFormedDepth f n (fvs' as) Γ (AppE f as rs' ()); fvs' as ⊆ dom Γ;
nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ |]
==> shareRec (fvs' as) Γ (E1.0, E2.0) (h, k) (hh, k)
lemma P5_P6_f_n_APP_2:
[| (E1.0,
E2.0) \<turnstile> h , k , AppE g as rs' () \<Down> (f, n) hh , k , v ;
hh = h' |` {p : dom h'. fst (the (h' p)) ≤ k}; dom Γ ⊆ dom E1.0;
∀a∈set as. atom a; length xs = length ms; length xs = length as;
wellFormedDepth f n (fvs' as) Γ (AppE g as rs' ()); fvs' as ⊆ dom Γ;
nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)) ⊆m Γ |]
==> shareRec (fvs' as) Γ (E1.0, E2.0) (h, k) (hh, k)
lemma P5_APP_PRIMOP:
[| Γ0.0 = [atom2var a1.0 |-> s'', atom2var a2.0 |-> s'']; Γ0.0 ⊆m Γ |]
==> ∀x∈dom (fst (E1.0, E2.0)).
∀z∈{atom2var a1.0, atom2var a2.0}.
Γ z = Some d'' ∧
closure (E1.0, E2.0) x (h, k) ∩ recReach (E1.0, E2.0) z (h, k) ≠
{} -->
x ∈ dom Γ ∧ Γ x ≠ Some s''
lemma P6_APP_PRIMOP:
[| Γ0.0 = [atom2var a1.0 |-> s'', atom2var a2.0 |-> s'']; Γ0.0 ⊆m Γ |]
==> ∀x∈dom (fst (E1.0, E2.0)).
¬ identityClosure (E1.0, E2.0) x (h, k) (h, k) -->
x ∈ dom Γ ∧ Γ x ≠ Some s''
lemma P5_P6_APP_PRIMOP:
[| Γ0.0 = [atom2var a1.0 |-> s'', atom2var a2.0 |-> s'']; Γ0.0 ⊆m Γ |]
==> shareRec {atom2var a1.0, atom2var a2.0} Γ (E1.0, E2.0) (h, k) (h, k)