Up to index of Isabelle/HOL/CoreSafe
theory SafeDAssDepth(* Title: Safe DAss
Author: Javier de Dios and Ricardo Peņa
Copyright: March 2008, Universidad Complutense de Madrid
*)
header {* Derived Assertions *}
theory SafeDAssDepth imports SafeDAssBasic SafeDepthSemantics
SafeDAss_P2 SafeDAss_P3 SafeDAss_P1
SafeDAss_P5_P6 SafeDAss_P4 SafeDAss_P7 SafeDAss_P8
SafeDAss_P9
begin
declare dom_fun_upd [simp del]
(********** Assert: (ConstE (LitN i) a) ***********)
lemma SafeDADepth_LitInt: "ConstE (LitN i) a :f , n \<lbrace> {} , empty \<rbrace>"
apply (simp only: SafeDAssDepth_def)
apply (rule conjI,simp)+
apply (intro allI, rule impI)
apply (elim conjE)
apply (frule impSemBoundRA [where td=td])
apply (elim exE)
apply (erule SafeRASem.cases) apply(simp_all)
apply (simp add: closed_f_def)
apply (simp add: shareRec_def)
by (rule ballI, simp add: identityClosure_def)
(********** Assert: (ConstE (LitB b) a) ***********)
lemma SafeDADepth_LitBool: "ConstE (LitB b) a :f , n \<lbrace> {} , empty \<rbrace>"
apply (simp only: SafeDAssDepth_def)
apply (rule conjI,simp)+
apply (intro allI, rule impI)
apply (elim conjE)
apply (frule impSemBoundRA [where td=td])
apply (elim exE)
apply (erule SafeRASem.cases,simp_all)
apply (simp add: closed_f_def)
apply (simp add: shareRec_def)
by (rule ballI, simp add: identityClosure_def)
(********** Assert: (VarE x a) ***********)
lemma SafeDADepth_Var1:
"[|Γ x = Some s''|]
==> VarE x a :f , n \<lbrace> {x} , Γ \<rbrace>"
apply (simp add: SafeDAssDepth_def)
apply (rule conjI, simp add: dom_def)
apply (intro allI, rule impI)
apply (erule conjE)
apply (frule impSemBoundRA [where td=td])
apply (elim exE)
apply (erule SafeRASem.cases,simp_all)
apply (rule conjI, simp add: shareRec_def)
apply (rule ballI) apply (simp add: identityClosure_def)
apply (rule impI)
apply (elim conjE)
apply (simp add: closed_def add: live_def add: closureLS_def add: closure_def)
by (simp add: closed_f_def)
(********** Assert: (CopyE x r d) ***********)
declare copy.simps [simp del]
lemma SafeDADepth_Var2:
"[|x ∈ dom Γ; wellFormed {x} Γ (CopyE x r d)|]
==> CopyE x r d :f , n \<lbrace> {x} , Γ\<rbrace>"
apply (simp only: SafeDAssDepth_def)
apply (rule conjI, simp)
apply (rule conjI, simp add: dom_def)
apply (intro allI, rule impI)
apply (elim conjE)
apply (frule impSemBoundRA [where td=td])
apply (elim exE)
apply (frule P1_COPY)
apply (elim exE, elim conjE)
apply (rule conjI)
apply simp
apply (rule P5_P6_COPY,assumption+)
apply (rule impI, elim conjE)
by (simp,rule P9_COPY,assumption+)
(********** Assert: (ReuseE x a) ***********)
lemma SafeDADepth_Var3:
"[|Γ x = Some d''; wellFormed {x} Γ (ReuseE x a)|]
==> ReuseE x a :f , n \<lbrace> {x} , Γ\<rbrace>"
apply (simp only: SafeDAssDepth_def)
apply (rule conjI, simp)
apply (rule conjI, simp add: dom_def)
apply (intro allI, rule impI)
apply (elim conjE)
apply (frule impSemBoundRA [where td=td])
apply (elim exE)
apply (frule P1_REUSE)
apply (elim exE, elim conjE)
apply (rule conjI)
apply simp
apply (rule P5_P6_REUSE,assumption+)
apply (rule impI, elim conjE)
by (simp, rule P9_REUSE,assumption+)
(********** Assert: APP_PRIMOP ***********)
lemma SafeDADepth_APP_PRIMOP:
"[| atom a1; atom a2; primops g = Some oper;
L = {atom2var a1, atom2var a2};
Γ0 = [atom2var a1 \<mapsto> s'',atom2var a2 \<mapsto> s''];
Γ0 ⊆m Γ |]
==> AppE g [a1,a2] [] a :f , n \<lbrace> L , Γ \<rbrace>"
apply (simp only: SafeDAssDepth_def)
(** Proof fv e ⊆ L : P4_App *)
apply (rule conjI)
apply (rule P4_APP_PRIMOP,assumption+)
(** Proof L ⊆ Γ : P3_App *)
apply (rule conjI)
apply (rule P3_APP_PRIMOP,assumption+)
(** Assuming P1 for app *)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
(** Proof P5 and P6: shareRec *)
apply (rule conjI)
apply (rule P5_P6_APP_PRIMOP,force,assumption)
(** Proof P9 for APP: closed_f *)
apply (rule impI)
by (rule P9_APP_PRIMOP)
(********** Assert: LET1 ***********)
lemma SafeDADepth_LET1:
"[| e1 :f , n \<lbrace> L1 , Γ1 \<rbrace>;
e2 :f , n \<lbrace> L2, Γ2' \<rbrace>;
Γ2' = disjointUnionEnv Γ2 (empty(x1\<mapsto>s''));
def_disjointUnionEnv Γ2 (empty(x1\<mapsto>s''));
def_pp Γ1 Γ2 L2;
x1 ∉ L1;
L = L1 ∪ (L2-{x1});
Γ = pp Γ1 Γ2 L2;
∀ C as r a'. e1 ≠ ConstrE C as r a'|]
==> Let x1 = e1 In e2 a :f , n \<lbrace> L , Γ \<rbrace>"
apply (simp (no_asm) only: SafeDAssDepth_def)
apply (simp only: SafeDAssDepth_def)
apply (elim conjE)
(** Proof fv e ⊆ L : P4_e1 ;P4_e2 ==> P4let *)
apply (rule conjI)
apply (erule P4_LET, assumption+)
(** Proof L ⊆ dom Γ : P3_e1 ;P3_e2 ==> P3let *)
apply (rule conjI)
apply (simp,rule conjI)
apply (erule P3_LET_e1)
apply (erule P3_LET_e2, assumption+)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (frule P1_f_n_LET,simp)
apply (elim exE,elim conjE)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E1(x1 \<mapsto> v1)" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (rotate_tac 13)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v1" in allE)
apply (erule_tac x="v" in allE)
(** Proof dom Γ ⊆ dom E : P2let ==> P2_e1 ;P2_e2 *)
apply (frule_tac r="v1" in P2_LET, assumption+)
apply (elim conjE)
apply (drule mp,simp)
apply (drule mp,simp)
apply (elim conjE)
(** Proof shareRec ∧ ¬ identityClosure:
P5_P6e_1; P5_P6e_2 ==> P5_P6_let *)
apply (rule conjI)
apply (erule P5_P6_LET, assumption+,simp)
apply (rule impI)
apply (elim conjE)
(** Proof closed: P8_let ==> P8_e1 *)
apply (frule P8_LET_e1,simp)
(** Proof S ∩ R={}: P7_let ==> P7_e1 *)
apply (frule P7_LET_e1, assumption+, simp)
(** Proof closed: P8_let ==> P8_e2 *)
apply (frule P8_LET_e2, assumption+, simp)
(** Proof S ∩ R={}: P7_let ==> P7_e2 *)
apply (frule P7_LET1_e2, assumption+)
(** Proof closed_f: P9_e1; P9_e2 ==> P9_let *)
by (rule P9_LET, assumption+, simp)
(********** Assert: LET1C ***********)
declare atom.simps [simp del]
lemma SafeDADepth_LET1C:
"[| L1 = set (map atom2var as); ∀a∈set as. atom a;
Γ1 = map_of (zip (map atom2var as) (replicate (length as) s''));
x1 ∉ L1;
e2 :f , n \<lbrace> L2, disjointUnionEnv Γ2 (empty(x1\<mapsto>s'')) \<rbrace>;
def_disjointUnionEnv Γ2 (empty(x1\<mapsto>s''));
def_pp Γ1 Γ2 L2;
L = L1 ∪ (L2-{x1});
Γ = pp Γ1 Γ2 L2 |]
==> Let x1 = ConstrE C as r a' In e2 a :f , n \<lbrace> L, Γ \<rbrace>"
apply (simp only: SafeDAssDepth_def)
apply (elim conjE)
(* Premises for LET1C *)
(* L1 ⊆ Γ1 *)
apply (frule set_atom2var_as_subeteq_Γ1)
(** Proof fv e ⊆ L :P4_e2 ==> P4_let *)
apply (rule conjI)
apply (frule fvs_as_subseteq_L1)
apply (rule P4_LET, simp, assumption+)
(** Proof L ⊆ Γ : P3_e2 ==> P3_let *)
apply (rule conjI)
apply (rule P3_LET,assumption+)
(** Assuming P1 for let, we show P1 for e2 *)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (frule P1_f_n_LETC,simp)
apply (elim exE,elim conjE)
apply (erule_tac x="E1(x1 \<mapsto> Loc p)" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h(p \<mapsto> (j, C, map (atom2val E1) as))" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v" in allE)
apply (drule mp,simp)
(* Proof dom Γ ⊆ dom E: P2_let ==> P2_e2 *)
apply (rule P2_LET_e2,assumption+)
(* By hypothesis, we get P5, P6,
and P7 ∧ P8 --> P9 for e2 *)
apply (elim conjE)
(* Proof shareRec ∧ ¬ identityClosure:
P5_P6_e2 ==> P5_P6_let *)
apply (rule conjI)
apply (frule P5_P6_f_n_LETC_e1,assumption+,simp,assumption+,simp)
apply (frule P2_LET_e1)
apply (rule P5_P6_LET,assumption+)
(* Assuming P8 for let *)
apply (rule impI,elim conjE)
(* Proof closed: P8_let ==> P8_e2 *)
apply (frule P5_P6_f_n_LETC_e1 [where ?L1.0=L1 and ?Γ1.0=Γ1])
apply (assumption+,simp,assumption+,simp,assumption+)
apply (frule P8_LET_e1)
apply (frule P9_LETC_e1,assumption+,simp)
apply (frule P2_LET_e2,assumption+)
apply (frule P8_LET_e2)
apply (assumption+,force,assumption+)
apply simp
(* Proof S ∩ R: P7_let ==> P7_e2 *)
apply (frule P5_P6_f_n_LETC_e1,assumption+,simp,assumption+,simp)
apply (frule P2_LET_e1)
apply (frule P7_LET1_e2,assumption+)
(* Now, for hypothesis e2, we get P9 *)
apply (drule mp)
apply force
(* Finally, using P9_e2 is trivial to show P9_let *)
by simp
(********** Assert: LET2 ***********)
lemma SafeDADepth_LET2:
"[| ∀ C as r a'. e1 ≠ ConstrE C as r a';
e1 :f , n \<lbrace> L1 , Γ1 \<rbrace>;
e2 :f , n \<lbrace> L2, disjointUnionEnv Γ2 (empty(x1\<mapsto>d'')) \<rbrace>;
def_disjointUnionEnv Γ2 (empty(x1\<mapsto>d''));
def_pp Γ1 Γ2 L2;
x1 ∉ L1|]
==> Let x1 = e1 In e2 a :f , n \<lbrace> L1 ∪ (L2-{x1}) , pp Γ1 Γ2 L2 \<rbrace>"
apply (simp (no_asm) only: SafeDAssDepth_def)
apply (simp only: SafeDAssDepth_def)
apply (elim conjE)
(** Proof fv e ⊆ L : P4_e1 ;P4_e2 ==> P4let *)
apply (rule conjI)
apply (erule P4_LET, assumption+)
(** Proof L ⊆ dom Γ : P3_e1 ;P3_e2 ==> P3let *)
apply (rule conjI)
apply (simp,rule conjI)
apply (erule P3_LET_e1)
apply (erule P3_LET_e2, assumption+)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (frule P1_f_n_LET,simp)
apply (elim exE,elim conjE)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E1(x1 \<mapsto> v1)" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v1" in allE)
apply (erule_tac x="v" in allE)
(** Proof dom Γ ⊆ dom E : P2let ==> P2_e1 ;P2_e2 *)
apply (frule_tac r="v1" in P2_LET, assumption+)
apply (elim conjE)
apply (drule mp,simp)
apply (drule mp,simp)
apply (elim conjE)
(** Proof shareRec ∧ ¬ identityClosure:
P5_P6e_1; P5_P6e_2 ==> P5_P6_let *)
apply (rule conjI)
apply (erule P5_P6_LET, assumption+)
apply (rule impI)
apply (elim conjE)
(** Proof closed: P8_let ==> P8_e1 *)
apply (frule P8_LET_e1,simp)
(** Proof S ∩ R={}: P7_let ==> P7_e1 *)
apply (frule P7_LET_e1, assumption+, simp)
(** Proof closed: P8_let ==> P8_e2 *)
apply (frule P8_LET_e2, assumption+, simp)
(** Proof S ∩ R={}: P7_let ==> P7_e2 *)
apply (frule P7_LET2_e2, assumption+)
(** Proof closed_f: P9_e1; P9_e2 ==> P9_let *)
by (rule P9_LET, assumption+, simp)
(********** Assert: LET2C ***********)
lemma SafeDADepth_LET2C:
"[| L1 = set (map atom2var as); ∀a∈set as. atom a;
Γ1 = map_of (zip (map atom2var as) (replicate (length as) s''));
x1 ∉ L1;
e2 :f , n \<lbrace> L2, disjointUnionEnv Γ2 (empty(x1\<mapsto>d'')) \<rbrace>;
def_disjointUnionEnv Γ2 (empty(x1\<mapsto>d''));
def_pp Γ1 Γ2 L2;
L = L1 ∪ (L2-{x1});
Γ = pp Γ1 Γ2 L2 |]
==> Let x1 = ConstrE C as r a' In e2 a :f , n \<lbrace> L, Γ \<rbrace>"
apply (simp only: SafeDAssDepth_def)
apply (elim conjE)
(* Premises for LET1C *)
(* L1 ⊆ Γ1 *)
apply (frule set_atom2var_as_subeteq_Γ1)
(** Proof fv e ⊆ L :P4_e2 ==> P4_let *)
apply (rule conjI)
apply (frule fvs_as_subseteq_L1)
apply (rule P4_LET, simp, assumption+)
(** Proof L ⊆ Γ : P3_e2 ==> P3_let *)
apply (rule conjI)
apply (rule P3_LET,assumption+)
(** Assuming P1 for let, we show P1 for e2 *)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (frule P1_f_n_LETC,simp)
apply (elim exE,elim conjE)
apply (erule_tac x="E1(x1 \<mapsto> Loc p)" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h(p \<mapsto> (j, C, map (atom2val E1) as))" in allE)
apply (erule_tac x="k" in allE)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v" in allE)
apply (drule mp,simp)
(* Proof dom Γ ⊆ dom E: P2_let ==> P2_e2 *)
apply (rule P2_LET_e2,assumption+)
(* By hypothesis, we get P5, P6,
and P7 ∧ P8 --> P9 for e2 *)
apply (elim conjE)
(* Proof shareRec ∧ ¬ identityClosure:
P5_P6_e2 ==> P5_P6_let *)
apply (rule conjI)
apply (frule P5_P6_f_n_LETC_e1,assumption+,simp,assumption+,simp)
apply (frule P2_LET_e1)
apply (rule P5_P6_LET,assumption+)
(* Assuming P8 for let *)
apply (rule impI,elim conjE)
(* Proof closed: P8_let ==> P8_e2 *)
apply (frule P5_P6_f_n_LETC_e1 [where ?L1.0=L1 and ?Γ1.0=Γ1])
apply (assumption+,simp,assumption+,simp,assumption+)
apply (frule P8_LET_e1)
apply (frule P9_LETC_e1,assumption+,simp)
apply (frule P2_LET_e2,assumption+)
apply (frule P8_LET_e2)
apply (assumption+,force,assumption+)
apply simp
(* Proof S ∩ R: P7_let ==> P7_e2 *)
apply (frule P5_P6_f_n_LETC_e1,assumption+,simp,assumption+,simp)
apply (frule P2_LET_e1)
apply (frule P7_LET2_e2,assumption+)
(* Now, for hypothesis e2, we get P9 *)
apply (drule mp)
apply force
(* Finally, using P9_e2 is trivial to show P9_let *)
by simp
(********** Assert: CASE ***********)
declare fv_fvs_fvs'_fvAlts_fvTup_fvAlts'_fvTup'.simps [simp del]
lemma SafeDADepth_CASE:
"[| def_nonDisjointUnionEnvList (map snd assert);
length (map snd assert) > 0; length assert = length alts;
∀ i < length alts. ∀ j < length alts. i ≠ j --> (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j))))) = {};
∀ i < length alts. ∀x∈set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
∀ i < length assert. snd (alts ! i) :f , n \<lbrace> fst (assert!i), snd (assert!i) \<rbrace>;
∀ i < length alts. x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
x ∈ dom Γ;
wellFormedDepth f n L Γ (Case (VarE x a) Of alts a');
L = (\<Union>i < length assert. fst (assert!i) - set (snd (extractP (fst (alts ! i))))) ∪ {x};
Γ = nonDisjointUnionEnvList (map snd assert)|]
==> Case (VarE x a) Of alts a' :f , n \<lbrace> L, Γ \<rbrace>"
apply (simp (no_asm) only: SafeDAssDepth_def)
apply (simp only: SafeDAssDepth_def)
(** Proof fv e ⊆ L : P4_ei ==> P4_case *)
apply (rule conjI)
apply (rule P4_CASE,simp,simp,simp)
(** Proof L ⊆ dom Γ : P3_ei ==> P3_case *)
apply (rule conjI)
apply (rule P3_CASE,simp,simp,simp,simp)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (case_tac "E1 x")
(* E1 x = None *)
apply (subgoal_tac "x ∈ dom E1")
prefer 2 apply force
apply (simp add: dom_def)
(* E1 x = Some aa *)
apply (case_tac aa)
(* E1 x = Some (Loc p) *)
apply (rename_tac p)
(* Premises for CASE *)
apply (subgoal_tac "0 < length assert")
prefer 2 apply simp
apply (frule P3_CASE,simp,simp,simp)
apply (frule P4_CASE,simp,simp)
apply (subgoal_tac
"∃ j C vs. h p = Some (j,C,vs) ∧
(∃ i < length alts.
def_extend E1 (snd (extractP (fst (alts ! i)))) vs
∧ (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) \<turnstile> h , k , snd (alts ! i) \<Down>(f, n) hh , k , v)")
prefer 2 apply (rule P1_f_n_CASE)
apply (simp,simp)
apply (subgoal_tac
" ∀i<length alts. fv (snd (alts ! i)) ⊆ fst (assert ! i)")
prefer 2 apply clarsimp
apply (subgoal_tac
" ∀i<length alts. fst (assert ! i) ⊆ dom (snd (assert ! i))")
prefer 2 apply clarsimp
apply (elim exE,elim conjE)
apply (elim exE, elim conjE)
apply (rotate_tac 5)
apply (erule_tac x="i" in allE)
apply (drule mp, simp)
apply (elim conjE)
apply (erule_tac x="extend E1 (snd (extractP (fst (alts ! i)))) vs" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (rotate_tac 25)
apply (erule_tac x="k" in allE)
apply (rotate_tac 25)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v" in allE)
apply (drule mp)
(** Proof semantic: P1 *)
apply (rule conjI,simp)
(** Proof dom Γ ⊆ dom E : P2case ==> P2ei *)
apply (rule P2_CASE,assumption+,simp)
(** Proof shareRec ∧ ¬identityClosure:
P5_P6_ei ==> P5_P6_case *)
apply (rule conjI) apply simp
apply (rule P5_P6_f_n_CASE)
apply (assumption+,simp,simp,assumption+,simp)
apply (rule impI)
apply (elim conjE)
apply (drule mp)
(** Proof closed: P8_case ==> P8_ei *)
apply (rule conjI) apply simp
apply (rule P8_CASE)
apply (assumption+,simp,simp,simp,simp,force,simp,assumption+,simp,assumption+)
(** Proof S ∩ R = {}: P7_case ==> P7_ei *)
apply (frule P2_CASE,assumption+,simp)
apply (simp add: def_extend_def)
apply (elim conjE)
apply (rule P7_CASE)
apply (assumption+,simp,simp,assumption+,simp,simp,simp,simp)
(** Proof closed_f: P9_ei ==> P9_case *)
apply simp
(************ E1 x = Some IntT int ********************)
apply (subgoal_tac
"(∃ i < length alts.
(E1, E2) \<turnstile> h , k , snd (alts ! i) \<Down> (f, n) hh , k , v
∧ fst (alts ! i) = ConstP (LitN int))")
prefer 2 apply (rule P1_f_n_CASE_1_1,simp,assumption+)
apply (elim exE, elim conjE)+
(* Premises for CASE *)
apply (subgoal_tac "0 < length assert")
prefer 2 apply simp
apply (frule P3_CASE,simp,simp,simp)
apply (frule P4_CASE,simp,simp)
apply (rotate_tac 5)
apply (erule_tac x="i" in allE)
apply (drule mp, simp)
apply (elim conjE)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (rotate_tac 22)
apply (erule_tac x="k" in allE)
apply (rotate_tac 22)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v" in allE)
(** Proof semantic: P1 *)
apply (drule mp)
apply (rule conjI,simp)
(** Proof dom Γ ⊆ dom E : P2case ==> P2ei *)
apply (rule P2_CASE_1_1, assumption+,simp)
(** Proof shareRec ∧ ¬identityClosure:
P5_P6_ei ==> P5_P6_case *)
apply (rule conjI) apply simp
apply (rule P5_P6_f_n_CASE_1_1)
apply (assumption+,simp,assumption+,simp)
apply (rule impI)
apply (elim conjE)
apply (drule mp)
(** Proof closed: P8_case ==> P8_ei *)
apply (rule conjI)
apply (rule P8_CASE_1_1)
apply (assumption+,simp,assumption+,simp)
(** Proof S ∩ R = {}: P7_case ==> P7_ei *)
apply (frule P2_CASE_1_1,assumption+,simp)
apply (rule P7_CASEL,assumption+,force)
apply (simp,simp,simp,simp,simp,simp,simp,simp)
(** Proof closed_f: P9_ei ==> P9_case *)
apply simp
(************** E1 x = Some BoolT bool **********************)
apply (subgoal_tac
"(∃ i < length alts.
(E1, E2) \<turnstile> h , k , snd (alts ! i) \<Down> (f, n) hh , k , v
∧ fst (alts ! i) = ConstP (LitB bool))")
prefer 2 apply (rule P1_f_n_CASE_1_2,simp,assumption+)
apply (elim exE, elim conjE)+
(* Premises for CASE *)
apply (subgoal_tac "0 < length assert")
prefer 2 apply simp
apply (frule P3_CASE,simp,simp,simp)
apply (frule P4_CASE,simp,simp)
apply (rotate_tac 5)
apply (erule_tac x="i" in allE)
apply (drule mp, simp)
apply (elim conjE)
apply (erule_tac x="E1" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h" in allE)
apply (rotate_tac 22)
apply (erule_tac x="k" in allE)
apply (rotate_tac 22)
apply (erule_tac x="hh" in allE)
apply (rotate_tac 22)
apply (erule_tac x="v" in allE)
(** Proof semantic: P1 *)
apply (drule mp)
apply (rule conjI,simp)
(** Proof dom Γ ⊆ dom E : P2case ==> P2ei *)
apply (rule P2_CASE_1_1,assumption+,simp)
(** Proof shareRec ∧ ¬identityClosure:
P5_P6_ei ==> P5_P6_case *)
apply (rule conjI) apply simp
apply (rule P5_P6_f_n_CASE_1_2)
apply (assumption+,simp,assumption+,simp)
apply (rule impI)
apply (elim conjE)
apply (drule mp)
(** Proof closed: P8_case ==> P8_ei *)
apply (rule conjI)
apply (rule P8_CASE_1_2)
apply (assumption+,simp,assumption+,simp)
(** Proof S ∩ R = {}: P7_case ==> P7_ei *)
apply (frule P2_CASE_1_1,assumption+,simp)
apply (rule P7_CASEL,assumption+,force)
apply (simp,simp,simp,simp,simp,simp,simp,simp)
(** Proof P9_ei ==> P9_case *)
by simp
(********** Assert: CASED ***********)
lemma SafeDADepth_CASED:
"[| length (map snd assert) > 0; length assert = length alts;
∀ i < length alts. ∀j. ∀x∈set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x = Some d'' --> j ∈ RecPos Ci;
∀ i < length assert. snd (alts ! i) :f , n \<lbrace> fst (assert!i), snd (assert!i) \<rbrace>;
∀ z ∈ dom Γ. Γ z ≠ Some s'' --> (∀i<length alts. z ∉ fst (assert ! i));
def_nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert)));
def_disjointUnionEnv
(nonDisjointUnionEnvList ((map (λ(Li,Γi). restrict_neg_map Γi (set Li∪{x})))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
[x \<mapsto> d''];
∀ i < length alts. ∀ j < length alts. i ≠ j --> (fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j))))) = {};
L = (\<Union>i < length assert. fst (assert!i) - set (snd (extractP (fst (alts ! i))))) ∪ {x};
wellFormedDepth f n L Γ (CaseD (VarE x a) Of alts a');
Γ = 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'')) |]
==> CaseD (VarE x a) Of alts a' :f , n \<lbrace> L , Γ \<rbrace>"
apply (simp (no_asm) only: SafeDAssDepth_def)
apply (simp only: SafeDAssDepth_def)
(** Proof fv e ⊆ L : P4_ei ==> P4_cased *)
apply (rule conjI,simp)
apply (rule P4_CASED,simp,simp)
(** Proof L ⊆ dom Γ : P3_ei ==> P3_case *)
apply (rule conjI,simp,rule conjI)
apply (rule P3_1_CASED,simp,simp,simp)
apply (rule P3_2_CASED,simp,simp,simp,simp,simp)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
(* Premises for CASED *)
apply (subgoal_tac "0 < length assert")
prefer 2 apply simp
apply (frule P3_1_CASED [where x="x"],simp,simp)
apply (frule P3_2_CASED [where x="x"],simp,simp,simp,simp)
apply (subgoal_tac
" ∀i<length alts. fv (snd (alts ! i)) ⊆ fst (assert ! i)")
prefer 2 apply clarsimp
apply (subgoal_tac
" ∀i<length alts. fst (assert ! i) ⊆ dom (snd (assert ! i))")
prefer 2 apply clarsimp
apply (frule P4_CASED,simp)
apply (subgoal_tac
"∃ p j C vs. E1 x = Some (Loc p) ∧ h p = Some (j,C,vs) ∧
(∃ i < length alts.
def_extend E1 (snd (extractP (fst (alts ! i)))) vs
∧ (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) \<turnstile>
h(p := None), k, snd (alts ! i) \<Down>(f,n) hh,k , v)")
prefer 2 apply (rule P1_f_n_CASED,simp)
apply (elim exE,elim conjE)
apply (elim exE, elim conjE)
apply (rotate_tac 3)
apply (erule_tac x="i" in allE)
apply (drule mp, simp)
apply (elim conjE)
apply (erule_tac x="extend E1 (snd (extractP (fst (alts ! i)))) vs" in allE)
apply (erule_tac x="E2" in allE)
apply (erule_tac x="h(p:=None)" in allE)
apply (rotate_tac 25)
apply (erule_tac x="k" in allE)
apply (rotate_tac 25)
apply (erule_tac x="hh" in allE)
apply (erule_tac x="v" in allE)
(** Proof semantic: P1 *)
apply (drule mp)
apply (rule conjI,simp)
(** Proof dom Γ ⊆ dom E : P2_cased ==> P2_ei *)
apply (frule_tac vs="vs" and ?E1.0="E1" in P2_CASED)
apply (assumption+,simp,clarsimp,force,simp)
apply (simp add: def_extend_def,force,assumption+,simp,simp)
apply (simp add: def_extend_def,simp,clarsimp)
(** Proof shareRec ∧ ¬identityClosure:
P5_P6_ei ==> P5_P6_cased *)
apply (rule conjI,simp)
apply (rule P5_P6_f_n_CASED)
apply (assumption+,simp,simp,assumption+,force)
apply (rule impI)
apply (elim conjE)
apply (drule mp)
(** Proof closed: P8_cased ==> P8_ei *)
apply (rule conjI)
apply (simp,frule P5_P6_f_n_CASED)
apply (simp,assumption+)
apply (simp only: def_extend_def, elim conjE)
apply (rule P8_CASED)
apply (assumption+,simp,assumption+,simp,simp,assumption+)
(** Proof S ∩ R: P7_case ==> P7_ei *)
apply (frule_tac vs="vs" and ?E1.0="E1" in P2_CASED)
apply (assumption+,simp,clarsimp,force,simp)
apply (simp add: def_extend_def,force,assumption+,simp,simp)
apply (simp add: def_extend_def) apply simp apply simp
apply (frule P5_P6_f_n_CASED)
apply (simp,simp,assumption+)
apply (simp add: def_extend_def)
apply (elim conjE)
apply (rule P7_CASED)
apply (simp,assumption+,simp,simp,simp,assumption+,simp)
apply (assumption+,simp,assumption+,simp)
(** Proof P9_ei ==> P9_case *)
by simp
(********** Assert: APP ***********)
declare nonDisjointUnionSafeEnvList.simps [simp del]
declare fv_fvs_fvs'_fvAlts_fvTup_fvAlts'_fvTup'.simps [simp add]
declare atom.simps [simp del]
(**** Auxiliary lemmas ****)
lemma lemma_19_aux [rule_format]:
"\<Turnstile> Σm
--> Σm g = Some ms
--> (bodyAPP Σf g): \<lbrace> set (varsAPP Σf g) , [varsAPP Σf g [\<mapsto>] ms] \<rbrace>"
apply (rule impI)
apply (erule ValidGlobalMarkEnv.induct,simp_all)
apply (rule impI)+
by simp
lemma equiv_SafeDAss_all_n_SafeDAssDepth:
"e : \<lbrace> L , Γ \<rbrace> ==> ∀n. SafeDAssDepth e f n L Γ"
apply (simp only: SafeDAss_def)
apply (simp only: SafeDAssDepth_def)
apply clarsimp
apply (simp only: SafeBoundSem_def)
apply (simp add: Let_def)
apply (elim exE)
apply (elim conjE)
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 (frule_tac td=td in eqSemDepthRA)
apply (elim exE)
apply (drule mp,force)
by simp
lemma map_le_x_in_dom_m2:
"[| m1 ⊆m m2; x ∈ dom m1; m1 x ≠ Some y |]
==> x ∈ dom m2 ∧ m2 x ≠ Some y"
apply (rule conjI)
apply (simp add: map_le_def,force)
by (simp add: map_le_def)
lemma shareRec_map_le_Γ:
"[| [xs [\<mapsto>] ms] ⊆m Γg; shareRec (set xs) [xs [\<mapsto>] ms] (E1, E2) (h, k) (hh, k);
length xs = length ms |]
==> shareRec (set xs) Γg (E1, E2) (h, k) (hh, k)"
apply (simp add: shareRec_def)
apply (rule conjI)
(* shareRec *)
apply (rule ballI,rule impI)
apply (elim conjE)
apply (erule_tac x=x in ballE)
prefer 2 apply simp
apply (elim bexE, elim conjE)
apply (drule mp)
apply (rule_tac x=z in bexI,simp)
apply (simp add: map_le_def,assumption+)
apply (elim conjE)
apply (simp add: map_le_def)
apply (subgoal_tac "x ∈ dom [xs [\<mapsto>] ms]")
prefer 2 apply simp
apply (erule_tac x=x in ballE,force,simp)
(* identityClosure *)
apply (rule ballI, rule impI)
apply (elim conjE)
apply (erule_tac x=x in ballE)+
apply simp
apply (elim conjE)
apply (rule map_le_x_in_dom_m2,assumption+,simp,assumption)
apply simp
by simp
lemma RSet_subseteq_RSet_map_le_Γ:
"[|[xs [\<mapsto>] ms] ⊆m Γg; length xs = length ms|]
==> RSet (set xs) [xs [\<mapsto>] ms] (E1, E2) (h, k) ⊆ RSet (set xs) Γg (E1, E2) (h, k)"
apply (rule subsetI)
apply (simp add: RSet_def)
apply (elim conjE, elim bexE, elim conjE)
apply (rule_tac x=z in bexI)
apply (simp add: map_le_def)
by simp
lemma SSet_subseteq_SSet_map_le_Γ:
"[|[xs [\<mapsto>] ms] ⊆m Γg; length xs = length ms|]
==> SSet (set xs) [xs [\<mapsto>] ms] (E1, E2) (h, k) ⊆ SSet (set xs) Γg (E1, E2) (h, k)"
apply (rule subsetI)
apply (simp add: SSet_def)
apply (simp add: Let_def)
apply (elim exE, elim conjE)
apply (rule_tac x=xa in exI)
by (simp add: map_le_def)
lemma SSet_RSet_map_le_Γ:
"[| [xs [\<mapsto>] ms] ⊆m Γg; length xs = length ms;
SSet (set xs) Γg (E1, E2) (h, k) ∩ RSet (set xs) Γg (E1, E2) (h, k) = {}|]
==> SSet (set xs) [xs [\<mapsto>] ms] (E1, E2) (h, k) ∩ RSet (set xs) [xs [\<mapsto>] ms] (E1, E2) (h, k) = {}"
apply (frule SSet_subseteq_SSet_map_le_Γ, assumption+)
apply (frule RSet_subseteq_RSet_map_le_Γ, assumption+)
by blast
lemma SafeDAssDepth_map_le_Γ:
"[| Lg = set xs; [xs [\<mapsto>] ms] ⊆m Γg; Σf g = Some (xs,rs,eg); length xs = length ms;
bodyAPP Σf g :f , n \<lbrace> set (varsAPP Σf g) , [varsAPP Σf g [\<mapsto>] ms] \<rbrace>|]
==> eg :f , n \<lbrace> Lg , Γg \<rbrace>"
apply (simp add: bodyAPP_def)
apply (simp add: varsAPP_def)
apply (simp add: SafeDAssDepth_def)
apply (subgoal_tac "set xs ⊆ dom [xs [\<mapsto>] ms]")
prefer 2 apply simp
apply (rule conjI)
apply (frule map_le_implies_dom_le,simp)
apply (rule allI)+
apply (rule impI, elim conjE)
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)
apply (rule conjI,simp)
apply (frule map_le_implies_dom_le,simp)
apply (elim conjE)
apply (rule conjI)
apply (rule shareRec_map_le_Γ,assumption+)
apply (rule impI)+
apply (drule mp)
apply (rule conjI,simp)
apply (rule SSet_RSet_map_le_Γ, assumption+,simp)
by simp
lemma SafeDAss_map_le_Γ:
"[| Lg = set xs; [xs [\<mapsto>] ms] ⊆m Γg; Σf g = Some (xs,rs,eg); length xs = length ms;
bodyAPP Σf g : \<lbrace> set (varsAPP Σf g) , [varsAPP Σf g [\<mapsto>] ms] \<rbrace>|]
==> eg :f , n \<lbrace> Lg , Γg \<rbrace>"
apply (frule_tac f=f in equiv_SafeDAss_all_n_SafeDAssDepth)
apply (erule_tac x=n in allE)
by (rule SafeDAssDepth_map_le_Γ,simp_all)
lemma lemma_19 [rule_format]:
" \<Turnstile>f , n Σm
--> Σf g = Some (xs,rs,eg)
--> Σm g = Some ms
--> g ≠ f
--> length xs = length ms
--> Lg = set xs
--> [xs [\<mapsto>] ms] ⊆m Γg
--> eg :f , n \<lbrace> Lg ,Γg \<rbrace>"
apply (rule impI)
apply (erule ValidGlobalMarkEnvDepth.induct)
(* [| \<Turnstile> Σm; f ∉ dom Σm|] ==> \<Turnstile>f,n Σm *)
apply (rule impI)+
apply (frule lemma_19_aux,force)
apply (rule SafeDAss_map_le_Γ,assumption+)
(* [| \<Turnstile> Σm; f ∉ dom Σm|] ==> \<Turnstile>f,0 Σm(f\<mapsto>ms) *)
apply (rule impI)+
apply (frule lemma_19_aux,force)
apply (rule SafeDAss_map_le_Γ,assumption+)
(* \<Turnstile>f,Suc n Σm(f\<mapsto>ms) *)
apply (rule impI)+
apply (frule lemma_19_aux,force)
apply (rule SafeDAss_map_le_Γ,assumption+)
(* \<Turnstile>f, n Σm(g\<mapsto>ms) *)
apply (case_tac "ga=g",simp_all)
apply (rule impI)+
apply (rule SafeDAss_map_le_Γ,simp_all)
done
lemma lemma_20 [rule_format]:
" \<Turnstile>f , n Σm
--> Σf f = Some (xs,rs,ef)
--> Σm f = Some ms
--> length xs = length ms
--> Lf = set xs
--> [xs [\<mapsto>] ms] ⊆m Γf
--> n = Suc n'
--> ef :f , n' \<lbrace> Lf ,Γf \<rbrace>"
apply (rule impI)
apply (erule ValidGlobalMarkEnvDepth.induct)
(* [| \<Turnstile> Σm; f ∉ dom Σm|] ==> \<Turnstile>f,n Σm *)
apply (rule impI)+
apply (frule lemma_19_aux,force)
apply (rule SafeDAss_map_le_Γ,assumption+)
(* [| \<Turnstile> Σm; f ∉ dom Σm|] ==> \<Turnstile>f,0 Σm(f\<mapsto>ms) *)
apply simp
(* \<Turnstile>f,Suc n Σm(f\<mapsto>ms) *)
apply (rule impI)+
apply simp
apply (rule SafeDAssDepth_map_le_Γ)
apply (simp,simp,simp,simp,simp)
(* \<Turnstile>f, n Σm(g\<mapsto>ms) *)
apply simp
done
lemma map_upds_equals_map_of_distinct_xs:
"[| distinct xs; length xs = length ms |]
==> [xs [\<mapsto>] ms] = map_of (zip xs ms)"
by (induct xs ms rule: list_induct2',simp_all)
lemma SafeDADepth_APP:
"[| length xs = length ms; primops g = None;
∀a∈set as. atom a; length as = length ms;
Σf g = Some (xs,rs,ef);
L = fvs' as;
Γ0 = nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
def_nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
Γ0 ⊆m Γ;
Σm g = Some ms;
wellFormedDepth f n L Γ ( AppE g as rs' a);
\<Turnstile>f , n Σm |]
==> AppE g as rs' a :f , n \<lbrace> L , Γ \<rbrace>"
apply (case_tac "g≠f")
(* g ≠ f *)
apply (frule_tac Γg="[xs [\<mapsto>] ms]" in lemma_19)
apply (assumption+,simp,simp add: map_le_def)
apply (simp only: SafeDAssDepth_def)
apply (elim conjE)
(* 5.- P4 for APP, i.e. fv (AppE f as rs' ()) ⊆ L *)
apply (rule conjI,simp)
(* 4.- P3 for APP, i.e. fvs' as ⊆ dom Γ *)
apply (rule conjI)
apply (rule P3_APP,simp,simp,simp)
(* implication for APP *)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
(* (E1, E2) \<turnstile> h , k , td , ef \<Down> hh , k , v , r *)
apply (frule P1_f_n_APP_2,simp,force,simp,force)
apply (elim exE)
apply (erule_tac x="map_of (zip xs (map (atom2val E1) as))" in allE)
apply (erule_tac x="map_of (zip rs (map (the o E2) rs'))(self \<mapsto>
Suc k)" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="Suc k" in allE)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="v" in allE)
apply (elim conjE)
apply (drule mp)
apply (rule conjI,simp)
(* 2.- Assuming P2 for APP, we get P2 for ef,
i.e. dom (map_of (zip xs ms)) ⊆ dom E1' *)
apply (simp)
(* P3 to P6 and P7 ∧ P8 -> P9 for ef *)
apply (elim conjE)
(* P5 and P6 for APP *)
apply (rule conjI)
apply (frule P3_APP,simp,simp)
apply (rule P5_P6_f_n_APP_2)
apply (simp,assumption+,simp,assumption+)
(* Assuming P7 and P8 for APP *)
apply (rule impI)
apply (elim conjE)
(* 8.- P7 for ef *)
apply (subst (asm) map_upds_equals_map_of_distinct_xs,assumption+)+
apply (frule P3_APP,simp,simp)
apply (subgoal_tac "length xs=length as")
prefer 2 apply simp
apply (frule P7_APP_ef,assumption+)
(* 9.- Let us assume P8 for APP, i.e, closed (E1, E2) (fvs' as) (h, k)
then P8 for ef *)
apply (frule P3_APP,simp,simp)
apply (frule P8_APP_ef,assumption+)
(* 10.- We get P9 for ef *)
apply (drule mp)
apply (rule conjI,simp)
apply simp
(* 11.- P9 for APP *)
apply (rule P9_APP,assumption+)
(* g = f *)
apply simp
apply (case_tac n)
(* n = 0 *)
apply (simp only: SafeDAssDepth_def)
(* 5.- P4 for APP, i.e. fv (AppE f as rs' ()) ⊆ L *)
apply (rule conjI,simp)
(* 4.- P3 for APP, i.e. fvs' as ⊆ dom Γ *)
apply (rule conjI)
apply (rule P3_APP,simp,simp,simp)
(* implication for APP.
P1(f,0) is false (at least one call to f is being made
by the expression AppE f as rs' () *)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (frule P1_f_n_APP,assumption+,simp)
(* case n > 0 *)
apply (frule_tac Γf="[xs [\<mapsto>] ms]" in lemma_20)
apply (assumption+,simp,simp,simp)
apply simp
apply (simp only: SafeDAssDepth_def)
apply (elim conjE)
(* 5.- P4 for APP, i.e. fv (AppE f as rs' ()) ⊆ L *)
apply (rule conjI,simp)
(* 4.- P3 for APP, i.e. fvs' as ⊆ dom Γ *)
apply (rule conjI)
apply (rule P3_APP,simp,simp,simp)
(* implication for APP *)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
(* (E1, E2) \<turnstile> h , k , td , ef \<Down> hh , k , v , r *)
apply (frule P1_f_n_ge_0_APP,simp,force)
apply (elim exE)
apply (erule_tac x="map_of (zip xs (map (atom2val E1) as))" in allE)
apply (erule_tac x="map_of (zip rs (map (the o E2) rs'))(self \<mapsto>
Suc k)" in allE)
apply (erule_tac x="h" in allE)
apply (erule_tac x="Suc k" in allE)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="v" in allE)
apply (elim conjE)
apply (drule mp)
apply (rule conjI,simp)
(* 2.- Assuming P2 for APP, we get P2 for ef,
i.e. dom (map_of (zip xs ms)) ⊆ dom E1' *)
apply (simp)
(* P3 to P6 and P7 ∧ P8 -> P9 for ef *)
apply (elim conjE)
(* P5 and P6 for APP *)
apply (rule conjI)
apply (frule P3_APP,simp,simp)
apply (rule P5_P6_f_n_APP,assumption+)
(* Assuming P7 and P8 for APP *)
apply (rule impI)
apply (elim conjE)
(* 8.- P7 for ef *)
apply (subst (asm) map_upds_equals_map_of_distinct_xs,assumption+)+
apply (frule P3_APP,simp,simp)
apply (frule P7_APP_ef,assumption+)
(* 9.- Let us assume P8 for APP, i.e, closed (E1, E2) (fvs' as) (h, k)
then P8 for ef *)
apply (frule P3_APP,simp,simp)
apply (frule P8_APP_ef,assumption+)
(* 10.- We get P9 for ef *)
apply (drule mp)
apply (rule conjI,simp)
apply simp
(* 11.- P9 for APP *)
apply (rule P9_APP,assumption+)
done
end
lemma SafeDADepth_LitInt:
ConstE (LitN i) a :f , n \<lbrace> {} , empty \<rbrace>
lemma SafeDADepth_LitBool:
ConstE (LitB b) a :f , n \<lbrace> {} , empty \<rbrace>
lemma SafeDADepth_Var1:
Γ x = Some s'' ==> VarE x a :f , n \<lbrace> {x} , Γ \<rbrace>
lemma SafeDADepth_Var2:
[| x ∈ dom Γ; wellFormed {x} Γ (x @ r d) |]
==> x @ r d :f , n \<lbrace> {x} , Γ \<rbrace>
lemma SafeDADepth_Var3:
[| Γ x = Some d''; wellFormed {x} Γ (ReuseE x a) |]
==> ReuseE x a :f , n \<lbrace> {x} , Γ \<rbrace>
lemma SafeDADepth_APP_PRIMOP:
[| atom a1.0; atom a2.0; primops g = Some oper;
L = {atom2var a1.0, atom2var a2.0};
Γ0.0 = [atom2var a1.0 |-> s'', atom2var a2.0 |-> s'']; Γ0.0 ⊆m Γ |]
==> AppE g [a1.0, a2.0] [] a :f , n \<lbrace> L , Γ \<rbrace>
lemma SafeDADepth_LET1:
[| e1.0 :f , n \<lbrace> L1.0 , Γ1.0 \<rbrace>;
e2.0 :f , n \<lbrace> L2.0 , Γ2' \<rbrace>; Γ2' = Γ2.0 + [x1.0 |-> s''];
def_disjointUnionEnv Γ2.0 [x1.0 |-> s'']; def_pp Γ1.0 Γ2.0 L2.0; x1.0 ∉ L1.0;
L = L1.0 ∪ (L2.0 - {x1.0}); Γ = Γ1.0\<triangleright>Γ2.0 L2.0;
∀C as r a'. e1.0 ≠ ConstrE C as r a' |]
==> Let x1.0 = e1.0 In e2.0 a :f , n \<lbrace> L , Γ \<rbrace>
lemma SafeDADepth_LET1C:
[| L1.0 = set (map atom2var as); ∀a∈set as. atom a;
Γ1.0 = map_of (zip (map atom2var as) (replicate (length as) s''));
x1.0 ∉ L1.0; e2.0 :f , n \<lbrace> L2.0 , Γ2.0 + [x1.0 |-> s''] \<rbrace>;
def_disjointUnionEnv Γ2.0 [x1.0 |-> s'']; def_pp Γ1.0 Γ2.0 L2.0;
L = L1.0 ∪ (L2.0 - {x1.0}); Γ = Γ1.0\<triangleright>Γ2.0 L2.0 |]
==> Let x1.0 = ConstrE C as r a' In e2.0 a :f , n \<lbrace> L , Γ \<rbrace>
lemma SafeDADepth_LET2:
[| ∀C as r a'. e1.0 ≠ ConstrE C as r a';
e1.0 :f , n \<lbrace> L1.0 , Γ1.0 \<rbrace>;
e2.0 :f , n \<lbrace> L2.0 , Γ2.0 + [x1.0 |-> d''] \<rbrace>;
def_disjointUnionEnv Γ2.0 [x1.0 |-> d'']; def_pp Γ1.0 Γ2.0 L2.0;
x1.0 ∉ L1.0 |]
==> Let x1.0 = e1.0 In e2.0 a :f , n \<lbrace> L1.0 ∪
(L2.0 - {x1.0}) , Γ1.0\<triangleright>Γ2.0 L2.0 \<rbrace>
lemma SafeDADepth_LET2C:
[| L1.0 = set (map atom2var as); ∀a∈set as. atom a;
Γ1.0 = map_of (zip (map atom2var as) (replicate (length as) s''));
x1.0 ∉ L1.0; e2.0 :f , n \<lbrace> L2.0 , Γ2.0 + [x1.0 |-> d''] \<rbrace>;
def_disjointUnionEnv Γ2.0 [x1.0 |-> d'']; def_pp Γ1.0 Γ2.0 L2.0;
L = L1.0 ∪ (L2.0 - {x1.0}); Γ = Γ1.0\<triangleright>Γ2.0 L2.0 |]
==> Let x1.0 = ConstrE C as r a' In e2.0 a :f , n \<lbrace> L , Γ \<rbrace>
lemma SafeDADepth_CASE:
[| def_nonDisjointUnionEnvList (map snd assert); 0 < length (map snd assert);
length assert = length alts;
∀i<length alts.
∀j<length alts.
i ≠ j -->
fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j)))) = {};
∀i<length alts.
∀x∈set (snd (extractP (fst (alts ! i)))). snd (assert ! i) x ≠ Some d'';
∀i<length assert.
snd (alts !
i) :f , n \<lbrace> fst (assert ! i) , snd (assert ! i) \<rbrace>;
∀i<length alts.
x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
x ∈ dom Γ; wellFormedDepth f n L Γ (Case VarE x a Of alts a');
L = (UN i<length assert.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪
{x};
Γ = nonDisjointUnionEnvList (map snd assert) |]
==> Case VarE x a Of alts a' :f , n \<lbrace> L , Γ \<rbrace>
lemma SafeDADepth_CASED:
[| 0 < length (map snd assert); length assert = length alts;
∀i<length alts.
∀j. ∀x∈set (snd (extractP (fst (alts ! i)))).
snd (assert ! i) x = Some d'' --> j ∈ RecPos Ci;
∀i<length assert.
snd (alts !
i) :f , n \<lbrace> fst (assert ! i) , snd (assert ! i) \<rbrace>;
∀z∈dom Γ. Γ z ≠ Some s'' --> (∀i<length alts. z ∉ fst (assert ! i));
def_nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (insert x (set Li)))
(zip (map (snd o extractP o fst) alts) (map snd assert)));
def_disjointUnionEnv
(nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (set Li ∪ {x}))
(zip (map (snd o extractP o fst) alts) (map snd assert))))
[x |-> d''];
∀i<length alts.
∀j<length alts.
i ≠ j -->
fst (assert ! i) ∩ set (snd (extractP (fst (alts ! j)))) = {};
L = (UN i<length assert.
fst (assert ! i) - set (snd (extractP (fst (alts ! i))))) ∪
{x};
wellFormedDepth f n L Γ (CaseD VarE x a Of alts a');
Γ = nonDisjointUnionEnvList
(map (λ(Li, Γi). restrict_neg_map Γi (set Li ∪ {x}))
(zip (map (snd o extractP o fst) alts) (map snd assert))) +
[x |-> d''] |]
==> CaseD VarE x a Of alts a' :f , n \<lbrace> L , Γ \<rbrace>
lemma lemma_19_aux:
[| \<Turnstile> Σm ; Σm g = Some ms |]
==> bodyAPP Σf
g : \<lbrace> set (varsAPP Σf g) , [varsAPP Σf g [|->] ms] \<rbrace>
lemma equiv_SafeDAss_all_n_SafeDAssDepth:
e : \<lbrace> L , Γ \<rbrace> ==> ∀n. e :f , n \<lbrace> L , Γ \<rbrace>
lemma map_le_x_in_dom_m2:
[| m1.0 ⊆m m2.0; x ∈ dom m1.0; m1.0 x ≠ Some y |]
==> x ∈ dom m2.0 ∧ m2.0 x ≠ Some y
lemma shareRec_map_le_Γ:
[| [xs [|->] ms] ⊆m Γg;
shareRec (set xs) [xs [|->] ms] (E1.0, E2.0) (h, k) (hh, k);
length xs = length ms |]
==> shareRec (set xs) Γg (E1.0, E2.0) (h, k) (hh, k)
lemma RSet_subseteq_RSet_map_le_Γ:
[| [xs [|->] ms] ⊆m Γg; length xs = length ms |]
==> RSet (set xs) [xs [|->] ms] (E1.0, E2.0) (h, k)
⊆ RSet (set xs) Γg (E1.0, E2.0) (h, k)
lemma SSet_subseteq_SSet_map_le_Γ:
[| [xs [|->] ms] ⊆m Γg; length xs = length ms |]
==> SSet (set xs) [xs [|->] ms] (E1.0, E2.0) (h, k)
⊆ SSet (set xs) Γg (E1.0, E2.0) (h, k)
lemma SSet_RSet_map_le_Γ:
[| [xs [|->] ms] ⊆m Γg; length xs = length ms;
SSet (set xs) Γg (E1.0, E2.0) (h, k) ∩ RSet (set xs) Γg (E1.0, E2.0) (h, k) =
{} |]
==> SSet (set xs) [xs [|->] ms] (E1.0, E2.0) (h, k) ∩
RSet (set xs) [xs [|->] ms] (E1.0, E2.0) (h, k) =
{}
lemma SafeDAssDepth_map_le_Γ:
[| Lg = set xs; [xs [|->] ms] ⊆m Γg; Σf g = Some (xs, rs, eg);
length xs = length ms;
bodyAPP Σf
g :f , n \<lbrace> set (varsAPP Σf g) , [varsAPP Σf g [|->] ms] \<rbrace> |]
==> eg :f , n \<lbrace> Lg , Γg \<rbrace>
lemma SafeDAss_map_le_Γ:
[| Lg = set xs; [xs [|->] ms] ⊆m Γg; Σf g = Some (xs, rs, eg);
length xs = length ms;
bodyAPP Σf
g : \<lbrace> set (varsAPP Σf g) , [varsAPP Σf g [|->] ms] \<rbrace> |]
==> eg :f , n \<lbrace> Lg , Γg \<rbrace>
lemma lemma_19:
[| \<Turnstile>f , n Σm ; Σf g = Some (xs, rs, eg); Σm g = Some ms; g ≠ f;
length xs = length ms; Lg = set xs; [xs [|->] ms] ⊆m Γg |]
==> eg :f , n \<lbrace> Lg , Γg \<rbrace>
lemma lemma_20:
[| \<Turnstile>f , n Σm ; Σf f = Some (xs, rs, ef); Σm f = Some ms;
length xs = length ms; Lf = set xs; [xs [|->] ms] ⊆m Γf; n = Suc n' |]
==> ef :f , n' \<lbrace> Lf , Γf \<rbrace>
lemma map_upds_equals_map_of_distinct_xs:
[| distinct xs; length xs = length ms |] ==> [xs [|->] ms] = map_of (zip xs ms)
lemma SafeDADepth_APP:
[| length xs = length ms; primops g = None; ∀a∈set as. atom a;
length as = length ms; Σf g = Some (xs, rs, ef); L = fvs' as;
Γ0.0 = nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
def_nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
Γ0.0 ⊆m Γ; Σm g = Some ms; wellFormedDepth f n L Γ (AppE g as rs' a);
\<Turnstile>f , n Σm |]
==> AppE g as rs' a :f , n \<lbrace> L , Γ \<rbrace>