Theory ProofRules

(*  Title:      Proof Rules
    Author:     Ricardo Peña and Javier de Dios
    Copyright:  June 2010, Universidad Complutense de Madrid
*)

header {* Proof rules for explicit deallocation *}

theory ProofRules
imports SafeDAssDepth
begin


consts RecPos :: "string => nat set"

inductive
  ProofRulesED :: "[unit Exp, MarkEnv, string, string set, TypeEnvironment] => bool"   
             ( "_ , _ \<turnstile>_  '( _ , _ ')" [71,71,71,71,71] 70)
where
   litInt : "ConstE (LitN i) a, Σm \<turnstile>f ({} , empty)"

|  litBool: "ConstE (LitB b) a, Σm \<turnstile>f ({} , empty)" 

|  var1   : "[|Γ x = Some s''|] 
             ==> VarE x a, Σm \<turnstile>f ( {x} , Γ )"

|  var2   : "[|x ∈ dom Γ; wellFormed {x} Γ (CopyE x r d)|] 
             ==> CopyE x r d, Σm \<turnstile>f ( {x} , Γ )"

|  var3   : "[|Γ x = Some d''; wellFormed {x} Γ (ReuseE x a)|] 
             ==> ReuseE x a, Σm \<turnstile>f ( {x} , Γ )"

|  let1   : "[| e1, Σm \<turnstile>f ( L1 , Γ1 );
               e2, Σm \<turnstile>f ( L2, Γ2' );
               Γ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, Σm \<turnstile>f ( L , Γ )"

|  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, Σm \<turnstile>f ( L2, disjointUnionEnv Γ2 (empty(x1\<mapsto>s'')));
               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, Σm \<turnstile>f ( L, Γ )"

|  let2   : "[| ∀   C as r a'.  e1 ≠ ConstrE C as r a';
               e1, Σm \<turnstile>f ( L1 , Γ1 );
               e2, Σm \<turnstile>f ( L2, disjointUnionEnv Γ2 (empty(x1\<mapsto>d'')));
               def_disjointUnionEnv Γ2 (empty(x1\<mapsto>d''));
               def_pp Γ1 Γ2 L2;
               x1 ∉ L1|] 
             ==> Let x1 = e1 In e2 a, Σm \<turnstile>f ( (L1 ∪ (L2-{x1})) , (pp Γ1 Γ2 L2))"

|  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, Σm \<turnstile>f ( L2, disjointUnionEnv Γ2 (empty(x1\<mapsto>d'')));
               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, Σm \<turnstile>f ( L, Γ )"

|  case1  : "[| 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), Σm \<turnstile>f ( fst (assert!i), snd (assert!i));
               ∀ i < length alts. x ∈ fst (assert ! i) ∧ x ∉ set (snd (extractP (fst (alts ! i))));
               x ∈ dom Γ;
               wellFormed 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', Σm \<turnstile>f ( L, Γ )"

|  case2  : "[| 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), Σm \<turnstile>f ( fst (assert!i), snd (assert!i) );
               ∀ 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};
               wellFormed 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', Σm \<turnstile>f ( L , Γ )"

|  app_primop : "[| atom a1; atom a2; primops f = Some oper;
                   L = {atom2var a1, atom2var a2};
                   Γ0 = [atom2var a1 \<mapsto> s'',atom2var a2 \<mapsto> s'']; 
                   Γ0 ⊆m Γ |] 
                  ==>  AppE f [a1,a2] [] a, Σm \<turnstile>f ( L , Γ )"

|  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;
                Σm g = Some ms;
                Γ0 = nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms)); 
                def_nonDisjointUnionSafeEnvList (maps_of (zip (map atom2var as) ms));
                Γ0 ⊆m Γ; 
                wellFormed L Γ ( AppE g as rs' a) |] 
               ==>  AppE g as rs' a, Σm \<turnstile>f ( L , Γ )"

|  rec    : "[| Σf f = Some (xs,rs,ef); 
               f ∉ dom Σm;
               Lf = set xs;
               Γf = empty (xs [\<mapsto>] ms);
               ef, Σm(f\<mapsto>ms) \<turnstile>f ( Lf , Γf ) |] 
             ==>  ef, Σm \<turnstile>f ( Lf , Γf )"




(* Lemma equivalent satisfaction with/without depth, part 1 *)

lemma equiv_all_n_SafeDAssDepth_SafeDAss:
  "∀n. SafeDAssDepth e f n L Γ ==> e : \<lbrace> L , Γ \<rbrace>"
apply (simp only: SafeDAss_def)
apply (simp only: SafeDAssDepth_def)
apply (rule conjI,simp)+
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (frule_tac f=f in eqSemRADepth)
apply (simp only: SafeBoundSem_def)
apply (elim exE)
apply (rename_tac n)
apply (erule_tac x=n in allE)
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=hh in allE)
apply (erule_tac x=v in allE)
apply (simp add: Let_def)
apply (drule mp,force)
by simp

(* Lemma equivalent satisfaction with/without depth, part 2 *)


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 equivalent satisfaction with/without depth, both parts *)

lemma lemma_5:
  "∀ n. SafeDAssDepth e f n L Γ ≡  e : \<lbrace> L , Γ \<rbrace>"
apply (rule eq_reflection)
apply (rule iffI)
(* forward implication *)
 apply (rule equiv_all_n_SafeDAssDepth_SafeDAss,force)
(* backwards implication *)
by (rule equiv_SafeDAss_all_n_SafeDAssDepth,force)


(* Lemma equivalent environment validity with/without depth, part 1 *)

declare fun_upd_apply [simp del]

lemma imp_ValidGlobalMarkEnv_all_n_ValidGlobalMarkEnvDepth:
  "ValidGlobalMarkEnv Σ ==> ∀ n. \<Turnstile>f,n Σ"
apply (erule ValidGlobalMarkEnv.induct,simp_all)
 apply (rule allI)
 apply (rule ValidGlobalMarkEnvDepth.base) 
  apply (rule ValidGlobalMarkEnv.base)
 apply simp
apply (rule allI)
apply (case_tac "fa=f",simp)
 apply (induct_tac n)
  apply (rule ValidGlobalMarkEnvDepth.depth0,simp,simp)
 apply (rule ValidGlobalMarkEnvDepth.step)
 apply (simp,simp,simp,simp,simp)
 apply (frule_tac f=f in  equiv_SafeDAss_all_n_SafeDAssDepth,simp)  
apply (rule ValidGlobalMarkEnvDepth.g)
apply (simp,simp,simp,simp,simp,simp)
done

(* Lemma equivalent environment validity with/without depth, part 2 *)

lemma imp_ValidDepth_n_Sigma_Valid_Sigma [rule_format]:
  "\<Turnstile>f , n  Σm 
  --> f ∉ dom Σm
  --> ValidGlobalMarkEnv Σm"
apply (rule impI)
apply (erule ValidGlobalMarkEnvDepth.induct) apply(simp_all)
  apply (simp add: fun_upd_apply add: dom_def)
 apply (simp add: fun_upd_apply add: dom_def)
apply (rule impI)
apply (drule mp)
 apply (simp add: fun_upd_apply add: dom_def)
by (rule ValidGlobalMarkEnv.step,simp_all) 

(* Lemma equivalent environment validity with/without depth, part 3 *)

lemma imp_f_notin_Sigma_ValiddDepth_n_Sigma_Valid_Sigma:
  "[| f ∉ dom Σm; ∀ n. \<Turnstile>f , n  Σm |]   
  ==> ValidGlobalMarkEnv Σm"
apply (erule_tac x=n in allE)
by (rule imp_ValidDepth_n_Sigma_Valid_Sigma,assumption+)

(* Lemma equivalent environment validity with/without depth, part 4 *)

lemma Theorem_4_aux [rule_format]:
  " \<Turnstile>f , n Σm
   --> n = Suc n' 
   --> f ∈ dom Σm
   --> (bodyAPP Σf f)  :f ,  n'  \<lbrace> set (varsAPP Σf f) , [(varsAPP Σf f) [\<mapsto>] the (Σm f)] \<rbrace>"
apply (rule impI)
apply (erule ValidGlobalMarkEnvDepth.induct,simp_all)
apply (rule impI)+
apply (subgoal_tac "the ((Σm(f \<mapsto> ms)) f) = ms",simp)
apply (simp add: fun_upd_apply add: dom_def)
apply (rule impI)+
apply (case_tac "g=f",simp_all)
apply (subgoal_tac "f ∈ dom Σm",simp)
 prefer 2 apply (simp add: fun_upd_apply add: dom_def)
apply (subgoal_tac "the ((Σm(g \<mapsto> ms)) f) = the (Σm f)",simp)
by (simp add: fun_upd_apply add: dom_def)


(* Lemma equivalent environment validity with/without depth, part 5 *)


lemma Theorem_4:
  "[| ∀ n > 0. \<Turnstile>f , n Σm; f ∈ dom Σm |] 
   ==> ∀ n.  (bodyAPP Σf f)  :f ,  n  \<lbrace> set (varsAPP Σf f) , [(varsAPP Σf f) [\<mapsto>] the (Σm f)] \<rbrace>"
apply (rule allI)
apply (rule_tac n="Suc n" in Theorem_4_aux)
by simp_all 


(* Lemma equivalent environment validity with/without depth, part 6 *)

lemma Theorem_5_aux [rule_format]:
  "\<Turnstile>f , n  Σm 
   --> n = Suc n' 
   --> f ∈ dom Σm
   --> bodyAPP Σf f : \<lbrace> set (varsAPP Σf f) , [varsAPP Σf f [\<mapsto>] the (Σm f)] \<rbrace>
   --> \<Turnstile> Σm"
apply (rule impI)
apply (erule ValidGlobalMarkEnvDepth.induct,simp_all)
 apply (rule impI)+
 apply (rule ValidGlobalMarkEnv.step) 
 apply (simp,simp,simp,simp,simp)
 apply (subgoal_tac "the ((Σm(f \<mapsto> ms)) f) = ms",simp)
 apply (simp add: fun_upd_apply add: dom_def)
apply (rule impI)+
apply (case_tac "g=f",simp_all)
apply (rule ValidGlobalMarkEnv.step,simp_all) 
apply (subgoal_tac "f ∈ dom Σm",simp)
 prefer 2 apply (simp add: fun_upd_apply add: dom_def)
apply (subgoal_tac "the ((Σm(g \<mapsto> ms)) f) = the (Σm f)",simp)
by (simp add: fun_upd_apply add: dom_def)


(* Lemma equivalent environment validity with/without depth, part 7 *)

lemma Theorem_5:
  "[| ∀ n > 0. \<Turnstile>f , n Σm; f ∈ dom Σm;
     bodyAPP Σf f : \<lbrace> set (varsAPP Σf f) , [varsAPP Σf f [\<mapsto>] the (Σm f)] \<rbrace>|] 
   ==> \<Turnstile> Σm"
apply (rule_tac n="Suc n" in Theorem_5_aux)
by simp_all 


(* Lemma equivalent environment validity with/without depth, part 8 *)


lemma imp_f_in_Sigma_ValidDepth_n_Sigma_Valid_Sigma:
  "[| ∀ n. \<Turnstile>f , n  Σm; f ∈ dom Σm |] 
   ==> ValidGlobalMarkEnv Σm"
apply (subgoal_tac "\<Turnstile>f , n  Σm")
 prefer 2 apply simp
apply (subgoal_tac "\<Turnstile>f , 0  Σm ∧ (∀n > 0. \<Turnstile>f , n  Σm)",elim conjE)
 prefer 2 apply simp
 apply (frule Theorem_4,assumption+)
apply (frule Theorem_5,assumption+)
by (rule equiv_all_n_SafeDAssDepth_SafeDAss,simp,simp)


(* Lemma equivalent environment validity with/without depth, part 9 *)


lemma imp_all_n_ValidGlobalMarkEnvDepth_ValidGlobalMarkEnv:
  "[| ∀ n. \<Turnstile>f,n Σ |] ==> ValidGlobalMarkEnv Σ"
apply (case_tac "f ∉ dom Σ",simp_all)
 apply (rule imp_f_notin_Sigma_ValiddDepth_n_Sigma_Valid_Sigma,assumption+)
by (rule imp_f_in_Sigma_ValidDepth_n_Sigma_Valid_Sigma,assumption+)


(* Lemma equivalent environment validity with/without depth, complete *)


lemma lemma_6:
  "∀ n. \<Turnstile>f,n Σm ≡ ValidGlobalMarkEnv Σm"
apply (rule eq_reflection)
apply (rule iffI)
(* forward implication *)
 apply (rule_tac f=f in imp_all_n_ValidGlobalMarkEnvDepth_ValidGlobalMarkEnv,force)
(* backwards implication *)
by (rule imp_ValidGlobalMarkEnv_all_n_ValidGlobalMarkEnvDepth,force)



(* Lemma implication of assertion satisfaction in a context environment with/without depth *)

lemma lemma_7:
  "[| ∀ n.  e, Σm :f,n \<lbrace> L , Γ \<rbrace> |] 
   ==> SafeDAssCntxt e Σm  L Γ"
apply (simp only: SafeDAssDepthCntxt_def)
apply (subgoal_tac "(∀n. \<Turnstile>f , n  Σm) --> (∀n. e :f , n \<lbrace> L , Γ \<rbrace>)")
 apply (erule thin_rl)
 apply (subst (asm) lemma_5)
 apply (subst (asm) lemma_6)
 apply (simp add: SafeDAssCntxt_def)
by force


(* Auxiliary Lemma for soundness theorem, part 1 *)


lemma lemma_8_REC [rule_format]:
  "(∀n. (ValidGlobalMarkEnvDepth f n (Σm(f \<mapsto> ms)))  --> (bodyAPP Σf f) :f,n \<lbrace> set (varsAPP Σf f) , [(varsAPP Σf f) [\<mapsto>] ms]\<rbrace>)
   --> f ∉ dom Σm
   --> ValidGlobalMarkEnvDepth f n Σm 
   --> (bodyAPP Σf f) :f,n \<lbrace> set (varsAPP Σf f) , [(varsAPP Σf f) [\<mapsto>] ms]\<rbrace>"
apply (rule impI)
apply (induct_tac n)
 (* n = 0 *)
 apply (rule impI)+
 apply (erule_tac x=0 in allE)
 apply (frule imp_ValidDepth_n_Sigma_Valid_Sigma,assumption+)
 apply (subgoal_tac "\<Turnstile>f , 0  Σm(f \<mapsto> ms)",simp)
 apply (rule ValidGlobalMarkEnvDepth.depth0,assumption+)
(* n > 0 *)
apply (erule_tac x="Suc n" in allE)
apply (rule impI)+
apply (frule imp_ValidDepth_n_Sigma_Valid_Sigma,assumption+)
apply (subgoal_tac "\<Turnstile>f , n  Σm",simp)
 apply (subgoal_tac "\<Turnstile>f , Suc n  Σm(f \<mapsto> ms)",simp)
 apply (rule ValidGlobalMarkEnvDepth.step,simp_all)
by (rule ValidGlobalMarkEnvDepth.base,assumption+)


(* Auxiliary lemma for soundness thoerem, part 2 *)


lemma lemma_8:
  "e, Σm \<turnstile>f ( L , Γ )
   ==> ∀ n.  e, Σm :f,n \<lbrace> L , Γ \<rbrace>"
apply (erule ProofRulesED.induct)
 (* ConstE (LitN i) *)
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule allI, rule impI)
 apply (rule SafeDADepth_LitInt)
 
 (* ConstE (LitB b) *)
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule allI, rule impI) 
 apply (rule SafeDADepth_LitBool)

 (* VarE x *)
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule allI, rule impI) 
 apply (rule SafeDADepth_Var1,force)

 (* x @ r *)
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule allI, rule impI) 
 apply (rule SafeDADepth_Var2,force,force)

 (* ReuseE x *)
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule allI, rule impI) 
 apply (rule SafeDADepth_Var3,force,force)

 (* Let x1 = e1 In e2. LET1 *)
 apply (rule allI)
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule impI)
 apply (erule_tac x=n in allE)+
 apply (drule mp, simp)+
 apply (rule SafeDADepth_LET1)
 apply (assumption+,simp,assumption+,simp,simp,assumption+)

 (* Let x1 = e1 In e2. LET1C *)
 apply (rule allI)
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule impI)
 apply (erule_tac x=n in allE)+
 apply (drule mp, simp)+
 apply (rule SafeDADepth_LET1C)
 apply (assumption+,simp,assumption+,simp,simp,simp)

 (* Let x1 = ConstrE C as r. LET2 *)
 apply (rule allI)
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule impI)
 apply (erule_tac x=n in allE)+
 apply (drule mp, simp)+
 apply (rule SafeDADepth_LET2)
 apply assumption+ 

 (* Let x1 = ConstrE C as r. LET2C *)
 apply (rule allI)
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule impI)
 apply (erule_tac x=n in allE)+
 apply (drule mp, simp)+
 apply (rule SafeDADepth_LET2C)
 apply (assumption+,simp,assumption+,simp,simp,simp)

 (* Case VarE x a Of alts *)
 apply (rule allI)
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule impI)
 apply (subgoal_tac
   " ∀i<length alts. snd (alts ! i) :f , n \<lbrace> fst (assert ! i) , snd (assert ! i) \<rbrace>")
 prefer 2 apply force
 apply (frule_tac f=f and n=n in imp_wellFormed_wellFormedDepth)
 apply (rule SafeDADepth_CASE)
 apply (assumption+,simp,assumption+,simp,simp)

 (* CaseD VarE x a Of alts *)
 apply (rule allI)
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule impI)
 apply (subgoal_tac
   " ∀i<length alts. snd (alts ! i) :f , n \<lbrace> fst (assert ! i) , snd (assert ! i) \<rbrace>")
 prefer 2 apply force
 apply (frule_tac f=f and n=n in imp_wellFormed_wellFormedDepth)
 apply (rule SafeDADepth_CASED)
 apply (assumption+,simp,assumption+,simp,simp,simp)

 (* AppE fa [a1, a2] [] a *)
 apply (rule allI)
 apply (simp (no_asm) only: SafeDAssDepthCntxt_def)
 apply (rule impI)
 apply (rule SafeDADepth_APP_PRIMOP)
 apply (assumption+)

 (* AppE fa as rs' a. APP *)
 apply (rule allI)
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule impI)
 apply (frule_tac f=f and n=n in imp_wellFormed_wellFormedDepth)
 apply (rule SafeDADepth_APP)
 apply (assumption+,simp,assumption+,simp,assumption+)

 (* Rec *) 
 apply (simp only: SafeDAssDepthCntxt_def)
 apply (rule allI)
 apply (rule impI)
 apply (subgoal_tac 
   "ef = (bodyAPP Σf f) ∧
    xs = (varsAPP Σf f)",simp)
 apply (rule_tac Σm=Σm in lemma_8_REC)
 apply (simp,simp,simp)
 apply (simp add: bodyAPP_def add: varsAPP_def)
done


(* Soundness Theorem, complete *)


lemma lemma_2:
  "e, Σm \<turnstile>f ( L , Γ ) 
  ==> SafeDAssCntxt e Σm L Γ"
apply (rule lemma_7)
by (rule lemma_8,assumption)


end