Theory ProofRulesRegions

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

header {* Proof rules for region deallocation *}

theory ProofRulesRegions
imports SafeRegionDepth
begin


inductive
  ProofRulesREG :: "[unit Exp, RegionEnv, string, ThetaMapping, TypeExpression] => bool"   
             ( "_ , _ \<turnstile>_  _ \<leadsto>  _ " [71,71,71,71,71] 70)
where
   litInt : "ConstE (LitN i) a, Σt \<turnstile>f (ϑ1,ϑ2) \<leadsto> (ConstrT intType [] [])"

|  litBool: "ConstE (LitB b) a, Σt \<turnstile>f (ϑ1,ϑ2) \<leadsto> (ConstrT boolType [] [])" 

|  var1   : "[| ϑ1 x = Some t |] 
             ==> VarE x a, Σt \<turnstile>f (ϑ1,ϑ2) \<leadsto> t"

|  var2   : "[| ϑ1 x = Some (ConstrT T ti ρl); 
               ϑ2 r = Some ρ';
               coherent constructorSignature Tc|] 
             ==> CopyE x r d, Σt \<turnstile>f (ϑ1,ϑ2) \<leadsto> ConstrT T ti ((butlast ρl)@[ρ'])"

|  var3   : "[| ϑ1 x = Some t; coherent constructorSignature Tc |]
             ==> ReuseE x a, Σt \<turnstile>f (ϑ1,ϑ2) \<leadsto> t"


|  let1    : "[| ∀ C as r a'. e1 ≠  ConstrE C as r a'; 
               x1 ∉ dom ϑ1; x1 ∉ fv e1;
               e1, Σt \<turnstile>f  (ϑ1,ϑ2) \<leadsto> t1; 
                e2, Σt \<turnstile>f (ϑ1(x1\<mapsto>t1),ϑ2) \<leadsto> t2 |] 
              ==> Let x1 = e1 In e2 a, Σt \<turnstile>f (ϑ1,ϑ2) \<leadsto> t2"

|  letc  :  "[| x1 ∉ fvs as;  x1 ∉ dom ϑ1;
               constructorSignature C = Some (ti,ρ,t);
               t = ConstrT T tn ρs; 
               t' = mu_ext (μ1,μ2) t;
               argP (map (mu_ext (μ1,μ2)) ti) ((the o μ2) ρ) as r (ϑ1,ϑ2);
               wellT ti ρ t;
               e2, Σt \<turnstile>f (ϑ1(x1\<mapsto>t'),ϑ2) \<leadsto> t''|] 
              ==> Let x1 = ConstrE C as r a' In e2 a, Σt \<turnstile>f (ϑ1,ϑ2) \<leadsto> t''"

|  case1  : "[| length assert = length alts; length alts > 0;
                ∀ i < length alts. constructorSignature (fst (extractP (fst (alts ! i)))) 
                           = Some (ti,ρ,t) ∧
                        t = ConstrT T tn ρs ∧
                        length (snd (extractP (fst (alts ! i)))) = length ti ∧
                        wellT ti ρ t ∧
               fst (assert ! i) = ϑ1 ++ (map_of (zip (snd (extractP (fst (alts ! i)))) 
                                                (map (mu_ext μ) ti))) ∧ 
                  dom ϑ1 ∩ dom (map_of (zip (snd (extractP (fst (alts ! i)))) 
                                             (map (mu_ext μ) ti))) = {} ∧
                  ϑ1 x = Some (mu_ext μ t)  ∧
                  snd (assert ! i) = ϑ2;
              ∀ i < length alts. snd (alts ! i), Σt 
                    \<turnstile>f  (fst (assert!i), snd (assert!i)) \<leadsto> t';
              ∀ i < length alts. x ∉ set (snd (extractP (fst (alts ! i))))|] 
             ==>  Case (VarE x a) Of alts a', Σt \<turnstile>f (ϑ1,ϑ2) \<leadsto> t'"

|  case2  : "[| length assert = length alts; length alts > 0;
               coherent constructorSignature Tc;
               ∀ i < length alts. constructorSignature 
                                  (fst (extractP (fst (alts ! i)))) = Some (ti,ρ,t) ∧
                        t = ConstrT T tn ρs ∧
                        length (snd (extractP (fst (alts ! i)))) = length ti ∧
                        wellT ti ρ t ∧
               fst (assert ! i) = ϑ1 ++ (map_of (zip (snd (extractP (fst (alts ! i)))) 
                                                     (map (mu_ext μ) ti))) ∧ 
                    dom ϑ1 ∩ dom (map_of (zip (snd (extractP (fst (alts ! i)))) 
                                              (map (mu_ext μ) ti))) = {} ∧
                    ϑ1 x = Some (mu_ext μ t)  ∧
                    snd (assert ! i) = ϑ2;
               ∀ i < length alts. snd (alts ! i), Σt 
                       \<turnstile>f  (fst (assert!i), snd (assert!i)) \<leadsto> t';
               ∀ i < length alts. x ∉ set (snd (extractP (fst (alts ! i))))|] 
               ==>  CaseD (VarE x a) Of alts a', Σt \<turnstile>f (ϑ1,ϑ2) \<leadsto> t'"

|  app    :  "[| Σt g = Some (ti,ρs,tg); primops g = None;
                ρself ∉ regions tg ∪ (\<Union> set (map regions ti)) ∪ set ρs;
                length as = length ti; length ρs = length rr; 
                ∀i<length ρs. ∃t. μ2 (ρs ! i) = Some t;
                ρfake ∉ ran μ2; μ_ren_dom (μ1, μ2);

                t = mu_ext (μ1,μ2) tg; mu_ext_def (μ1,μ2) tg;
                Σf g = Some (xs,rs,e); fv e ⊆ set xs; fvReg e ⊆ set rs ∪ {self};
                argP_app (map (mu_ext (μ1,μ2)) ti) (map (the o μ2) ρs) as rr (ϑ1,ϑ2) |] 
               ==>  AppE g as rr a, Σt \<turnstile>f (ϑ1,ϑ2) \<leadsto> t"


|  rec    : "[| Σf f = Some (xs,rs,ef); 
               f ∉ dom Σt;
               ϑ1f = map_of (zip xs ti);
               ϑ2f = map_of (zip rs ρs) ++ [self \<mapsto> ρself];   
               ef, Σt(f\<mapsto>(ti,ρs,tf)) \<turnstile>f (ϑ1f,ϑ2f) \<leadsto> tf |] 
             ==>  ef, Σt \<turnstile>f (ϑ1f,ϑ2f) \<leadsto> tf"


declare SafeRegionDAss.simps [simp del]
declare SafeRegionDAssDepth.simps [simp del]

(* Lemma 5 *)

lemma equiv_all_n_SafeRegionDAssDepth_SafeRegionDAss:
  "∀n. SafeRegionDAssDepth e f n ϑ t ==> e : \<lbrace> ϑ , t \<rbrace>"
apply (case_tac ϑ)
apply (simp only: SafeRegionDAss.simps)
apply (simp only: SafeRegionDAssDepth.simps)
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 (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' in allE)
apply (erule_tac x=v in allE)
apply (erule_tac x=η in allE)

apply (simp add: Let_def)
apply (drule mp,force)
by simp


lemma equiv_SafeRegionDAss_all_n_SafeRegionDAssDepth:
  "e : \<lbrace> ϑ , t \<rbrace> ==> ∀n. SafeRegionDAssDepth e f n ϑ t"
apply (case_tac ϑ)
apply (simp only: SafeRegionDAss.simps)
apply (simp only: SafeRegionDAssDepth.simps)
apply clarsimp
apply (simp only: SafeBoundSem_def)
apply (simp add: Let_def)
apply (elim exE)
apply (elim conjE)
apply (frule_tac td=td in eqSemDepthRA)
apply (elim exE)
apply (case_tac x,case_tac ba)
apply (erule_tac x=E1 in allE)
apply (erule_tac x=E2 in allE)
apply (erule_tac x=h in allE)
apply (erule_tac x=k in allE)
apply (erule_tac x=td in allE)
apply (erule_tac x=h' in allE)
apply (erule_tac x=v in allE)
apply (erule_tac x=aa in allE)
apply (erule_tac x=ab in allE)
apply (erule_tac x=bb in allE)
apply (erule_tac x=η in allE)
apply (drule mp,force)
by simp


lemma lemma_5:
  "∀ n. SafeRegionDAssDepth e f n ϑ t ≡  e : \<lbrace> ϑ , t \<rbrace>"
apply (rule eq_reflection)
apply (rule iffI)
(* forward implication *)
 apply (rule equiv_all_n_SafeRegionDAssDepth_SafeRegionDAss,force)
(* backwards implication *)
by (rule equiv_SafeRegionDAss_all_n_SafeRegionDAssDepth,force)


(* Lemma 6 *)

declare fun_upd_apply [simp del]

lemma imp_ValidGlobalRegionEnv_all_n_ValidGlobalRegionEnvDepth:
  "ValidGlobalRegionEnv Σt ==> ∀ n. \<Turnstile>f,n Σt"
apply (erule ValidGlobalRegionEnv.induct,simp_all)
 apply (rule allI)
 apply (rule ValidGlobalRegionEnvDepth.base) 
  apply (rule ValidGlobalRegionEnv.base)
 apply simp
apply (rule allI)
apply (case_tac "fa=f",simp)
 apply (induct_tac n)
  apply (rule ValidGlobalRegionEnvDepth.depth0,simp,simp)
 apply (rule ValidGlobalRegionEnvDepth.step)
 apply (simp,simp,simp,simp,simp)
 apply (frule_tac f=f in  equiv_SafeRegionDAss_all_n_SafeRegionDAssDepth,simp)  
apply (rule ValidGlobalRegionEnvDepth.g)
apply (simp,simp,simp,simp,simp)
by (frule_tac f=fa in  equiv_SafeRegionDAss_all_n_SafeRegionDAssDepth,simp)


lemma imp_ValidRegionDepth_n_SigmaRegion_Valid_Sigma [rule_format]:
  "\<Turnstile>f , n  Σt 
  --> f ∉ dom Σt
  --> ValidGlobalRegionEnv Σt"
apply (rule impI)
apply (erule ValidGlobalRegionEnvDepth.induct,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 ValidGlobalRegionEnv.step,simp_all) 


lemma imp_f_notin_SigmaRegion_ValidDepth_n_SigmaRegion_Valid_Sigma:
  "[| f ∉ dom Σt; ∀ n. \<Turnstile>f , n  Σt |]   
  ==> ValidGlobalRegionEnv Σt"
apply (erule_tac x=n in allE)
by (rule imp_ValidRegionDepth_n_SigmaRegion_Valid_Sigma,assumption+)



lemma Theorem_4_aux [rule_format]:
  " ValidGlobalRegionEnvDepth f n Σt
   --> n = Suc n' 
   --> f ∈ dom Σt
   --> (bodyAPP Σf f)  :f ,  n'  \<lbrace> (map_of (zip (varsAPP Σf f) (typesArgAPP Σt f)), map_of (zip (regionsAPP Σf f) (regionsArgAPP Σt f)) ++ [self \<mapsto> ρself]), 
                                 (typeResAPP Σt f) \<rbrace>"
apply (rule impI)
apply (erule ValidGlobalRegionEnvDepth.induct,simp_all)
 apply (rule impI)+
 apply (subgoal_tac "typesArgAPP (Σt(f \<mapsto> (ti, ρs, tf))) f = ti",simp)
 apply (subgoal_tac "regionsArgAPP (Σt(f \<mapsto> (ti, ρs, tf))) f = ρs",simp)
 apply (subgoal_tac "typeResAPP (Σt(f \<mapsto> (ti, ρs, tf))) f = tf",simp)
 apply (unfold typeResAPP_def regionsArgAPP_def typesArgAPP_def)
by (simp add: fun_upd_apply add: dom_def)+



lemma Theorem_4:
  "[| ∀ n > 0. ValidGlobalRegionEnvDepth f n Σt; f ∈ dom Σt |] 
   ==> ∀ n.  (bodyAPP Σf f)  :f ,  n  \<lbrace> (map_of (zip (varsAPP Σf f) (typesArgAPP Σt f)), 
                                       map_of (zip (regionsAPP Σf f) (regionsArgAPP Σt f)) ++ [self \<mapsto> ρself]), 
                                       (typeResAPP Σt f) \<rbrace>"
apply (rule allI)
apply (rule_tac n="Suc n" in Theorem_4_aux)
by simp_all 


lemma Theorem_5_aux [rule_format]:
  "\<Turnstile>f , n  Σt 
   --> n = Suc n' 
   --> f ∈ dom Σt
   --> (bodyAPP Σf f) : \<lbrace> (map_of (zip (varsAPP Σf f) (typesArgAPP Σt f)), 
                            map_of (zip (regionsAPP Σf f) (regionsArgAPP Σt f)) ++ [self \<mapsto> ρself]), 
                           (typeResAPP Σt f) \<rbrace>
   --> \<Turnstile> Σt"
apply (rule impI)
apply (erule ValidGlobalRegionEnvDepth.induct,simp_all)
 apply (rule impI)+
 apply (rule ValidGlobalRegionEnv.step) 
 apply (simp,simp,simp,simp,simp)
 apply (subgoal_tac "typesArgAPP (Σt(f \<mapsto> (ti, ρs, tf))) f = ti",simp)
 apply (subgoal_tac "regionsArgAPP (Σt(f \<mapsto> (ti, ρs, tf))) f = ρs",simp)
 apply (subgoal_tac "typeResAPP (Σt(f \<mapsto> (ti, ρs, tf))) f = tf",simp)
 apply (simp add: typeResAPP_def add: fun_upd_apply add: dom_def)
 apply (simp add: regionsArgAPP_def add: fun_upd_apply add: dom_def)
 apply (simp add: typesArgAPP_def add: fun_upd_apply add: dom_def)
apply (rule impI)+
apply (case_tac "g=f",simp_all)
apply (rule ValidGlobalRegionEnv.step,simp_all) 
apply (subgoal_tac "f ∈ dom Σt",simp)
 prefer 2 apply (simp add: fun_upd_apply add: dom_def)
apply (subgoal_tac "typesArgAPP (Σt(g \<mapsto> (ti, ρs, tf))) f = typesArgAPP Σt f",simp)
apply (subgoal_tac "regionsArgAPP (Σt(g \<mapsto> (ti, ρs, tf))) f = regionsArgAPP Σt f",simp)
apply (subgoal_tac "typeResAPP (Σt(g \<mapsto> (ti, ρs, tf))) f =  typeResAPP Σt f",simp)
apply (unfold typeResAPP_def regionsArgAPP_def typesArgAPP_def)
by (simp add: fun_upd_apply add: dom_def)+


lemma Theorem_5:
  "[| ∀ n > 0. \<Turnstile>f , n Σt; f ∈ dom Σt;
     (bodyAPP Σf f) : \<lbrace> (map_of (zip (varsAPP Σf f) (typesArgAPP Σt f)), 
                          map_of (zip (regionsAPP Σf f) (regionsArgAPP Σt f)) ++ [self \<mapsto> ρself]), 
                        (typeResAPP Σt f) \<rbrace>|] 
   ==> \<Turnstile> Σt"
apply (rule_tac n="Suc n" in Theorem_5_aux)
by simp_all 



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



lemma imp_all_n_ValidGlobalRegionEnvDepth_ValidGlobalRegionEnv:
  "[| ∀ n. \<Turnstile>f,n Σt |] ==> ValidGlobalRegionEnv Σt"
apply (case_tac "f ∉ dom Σt",simp_all)
 apply (rule imp_f_notin_SigmaRegion_ValidDepth_n_SigmaRegion_Valid_Sigma,assumption+)
by (rule imp_f_in_SigmaRegion_ValidDepth_n_SigmaRegion_Valid_Sigma,assumption+)


lemma lemma_6:
  "∀ n. \<Turnstile>f,n Σt ≡ ValidGlobalRegionEnv Σt"
apply (rule eq_reflection)
apply (rule iffI)
(* forward implication *)
 apply (rule_tac f=f in imp_all_n_ValidGlobalRegionEnvDepth_ValidGlobalRegionEnv,force)
(* backwards implication *)
by (rule imp_ValidGlobalRegionEnv_all_n_ValidGlobalRegionEnvDepth,force)
 


(* Lemma 7 *)

lemma lemma_7:
  "[| ∀ n.  e, Σt :f,n \<lbrace> ϑ , t \<rbrace> |] 
   ==> SafeRegionDAssCntxt e Σt ϑ t"
apply (simp only: SafeRegionDAssDepthCntxt_def)
apply (subgoal_tac "(∀n. \<Turnstile>f , n  Σt) --> (∀n. e :f , n \<lbrace> ϑ , t \<rbrace>)")
 apply (erule thin_rl)
 apply (subst (asm) lemma_5)
 apply (subst (asm) lemma_6)
 apply (simp add: SafeRegionDAssCntxt_def)
by force




(* Lemma 8 *)


lemma lemma_8_REC [rule_format]:
  "(∀n. (ValidGlobalRegionEnvDepth f n (Σt(f \<mapsto> (ti,ρs,tf)))  
         --> (bodyAPP Σf f) :f,n \<lbrace> (map_of (zip (varsAPP Σf f) ti), map_of (zip (regionsAPP Σf f) ρs)(self \<mapsto> ρself)), tf \<rbrace>))
   --> f ∉ dom Σt
   --> ValidGlobalRegionEnvDepth f n Σt
   --> (bodyAPP Σf f) :f,n \<lbrace> (map_of (zip (varsAPP Σf f) ti), map_of (zip (regionsAPP Σf f) ρs)(self \<mapsto> ρself)), tf \<rbrace>"
apply (rule impI)
apply (induct_tac n)
 (* n = 0 *)
 apply (rule impI)+
 apply (erule_tac x=0 in allE)
 apply (frule imp_ValidRegionDepth_n_SigmaRegion_Valid_Sigma,assumption+)
 apply (subgoal_tac "\<Turnstile>f , 0  Σt(f \<mapsto> (ti,ρs,tf))",simp)
 apply (rule ValidGlobalRegionEnvDepth.depth0,assumption+)
(* n > 0 *)
apply (erule_tac x="Suc n" in allE)
apply (rule impI)+
apply (frule imp_ValidRegionDepth_n_SigmaRegion_Valid_Sigma,assumption+)
apply (subgoal_tac "\<Turnstile>f , n  Σt",simp)
 apply (subgoal_tac "\<Turnstile>f , Suc n  Σt(f \<mapsto> (ti,ρs,tf))",simp)
 apply (rule ValidGlobalRegionEnvDepth.step,simp_all)
by (rule ValidGlobalRegionEnvDepth.base,assumption+)




lemma lemma_8:
  "e, Σt \<turnstile>f ϑ \<leadsto> t
   ==> ∀ n.  e, Σt :f,n \<lbrace> ϑ , t \<rbrace>"
apply (erule ProofRulesREG.induct)
 (* ConstE (LitN i) *)
 apply (simp only: SafeRegionDAssDepthCntxt_def)
 apply (rule allI, rule impI) 
 apply (rule SafeDARegionDepth_LitInt)
 
 (* ConstE (LitB b) *)
 apply (simp only: SafeRegionDAssDepthCntxt_def)
 apply (rule allI, rule impI) 
 apply (rule SafeDARegionDepth_LitBool)

 (* VarE x *)
 apply (simp only: SafeRegionDAssDepthCntxt_def)
 apply (rule allI, rule impI) 
 apply (rule SafeDARegionDepth_Var1,force)

 (* x @ r *)
 apply (simp only: SafeRegionDAssDepthCntxt_def)
 apply (rule allI, rule impI) 
 apply (rule SafeDARegionDepth_Var2,force,force,force)

 (* ReuseE x *)
 apply (simp only: SafeRegionDAssDepthCntxt_def) 
 apply (rule allI, rule impI)
 apply (rule SafeDARegionDepth_Var3,force,force)

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

 (* Let x1 = e1 In e2. LETC *)
 apply (rule allI)
 apply (simp only: SafeRegionDAssDepthCntxt_def)
 apply (rule impI)
 apply (erule_tac x=n in allE)+
 apply (drule mp, simp)+
 apply (rule SafeDARegionDepth_LETC)
 apply (assumption+,force,assumption+,simp)

 (* Case VarE x a Of alts *)
 apply (rule allI)
 apply (simp only: SafeRegionDAssDepthCntxt_def)
 apply (rule impI)
 apply (subgoal_tac
   " ∀i<length alts. snd (alts ! i) :f , n \<lbrace> (fst (assert ! i), snd (assert ! i)) , t' \<rbrace>")
 prefer 2 apply force
 apply (rule SafeDARegionDepth_CASE)
 apply assumption+

 (* CaseD VarE x a Of alts *)
 apply (rule allI)
 apply (simp only: SafeRegionDAssDepthCntxt_def)
 apply (rule impI)
 apply (subgoal_tac
   " ∀i<length alts. snd (alts ! i) :f , n \<lbrace> (fst (assert ! i), snd (assert ! i)) , t' \<rbrace>")
 prefer 2 apply force
 apply (rule SafeDARegionDepth_CASED)
 apply assumption+

 (* AppE fa as rs' a. APP *)
 apply (rule allI)
 apply (simp only: SafeRegionDAssDepthCntxt_def)
 apply (rule impI)
 apply (rule SafeDARegionDepth_APP)
 apply (assumption+,simp,assumption+,simp,assumption+,simp)

 (* Rec *)
 apply (simp only: SafeRegionDAssDepthCntxt_def)
 apply (rule allI,rule impI)
 apply (subgoal_tac 
   "ef = (bodyAPP Σf f) ∧
    xs = (varsAPP Σf f) ∧
    rs = (regionsAPP Σf f)",simp)
  apply (rule lemma_8_REC,force,force,force)
 by (simp add: bodyAPP_def add: varsAPP_def add: regionsAPP_def)



(* Lemma 2 *)

lemma lemma_2:
  "e, Σt \<turnstile>f ϑ \<leadsto> t
  ==> e, Σt : \<lbrace> ϑ , t \<rbrace> "
apply (rule lemma_7)
by (rule lemma_8,assumption)


end