Theory ProofRulesCostes

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

header {* Proof-rules for certifying memory bounds, and soundness theorem *}

theory ProofRulesCostes
imports CostesDepth Finite_Set
begin


(* Auxiliary definitions *)
constdefs costs_le:: "Cost => Cost => bool"  ("_ \<sqsubseteq>c _" 1000)
 "costs_le c1 c2 ≡ (dom c1 = dom c2) ∧ (∀ x ∈ dom c1. the (c1 x) ≤ the (c2 x))"

constdefs abstractDelta_le:: "AbstractDelta => AbstractDelta => bool"  
                             ("_ \<sqsubseteq>Δ _" 1000)
 "abstractDelta_le Δ1 Δ2 ≡ (dom Δ1 = dom Δ2) ∧ 
  (∀ ρ ∈ dom Δ1. (the (Δ1 ρ)) \<sqsubseteq>c (the (Δ2 ρ)))"

constdefs resources_le :: "AbstractDelta => AbstractMu => AbstractSigma 
                          => AbstractDelta => AbstractMu => AbstractSigma => bool"
   ("'( _ , _ , _ ') \<sqsubseteq>R '( _ , _ , _ ')" 1000)
 "( Δ' , μ' , σ' )  \<sqsubseteq>R ( Δ , μ , σ ) ≡ 
  Δ'  \<sqsubseteq>Δ Δ ∧ μ' \<sqsubseteq>c μ ∧ σ' \<sqsubseteq>c σ"

inductive
  ProofRulesCostes :: 
  "unit Exp => FunctionResourcesSignature =>
   FunName => ThetaMapping => PhiMapping => real => 
   AbstractDelta => AbstractMu => AbstractSigma => bool"
    ("_ , _  \<turnstile>_ _ _ _ '( _ , _ , _ ')" 1000)
where
   litInt : "ConstE (LitN i) a, Σb 
   \<turnstile>f (ϑ1, ϑ2) Φ td ([]f , 
   []0, []1)"

|  litBool: "ConstE (LitB b) a, Σb 
   \<turnstile>f (ϑ1, ϑ2) Φ td ([]f , 
   []0, []1)" 

|  var1   : "VarE x a, Σb 
   \<turnstile>f (ϑ1, ϑ2) Φ td ([]f , 
   []0, []1)"

|  var2   : "[|(typesRegsAPP Σϑ f) r = Some ρ; 
              (sizesAPP ΣΦ f) x = Some η |] 
              ==> CopyE x r d, Σb 
                  \<turnstile>f  (typesAPP Σϑ f) (sizesAPP ΣΦ f) td ([ρ \<mapsto> η], η, []2)"

|  var3   : "[| (typesRegsAPP Σϑ f) r = Some ρ; 
               (sizesAPP ΣΦ f) x = Some η |] 
             ==> ReuseE x a, Σb 
                 \<turnstile>f  (typesAPP Σϑ f) (sizesAPP ΣΦ f) td ([]f , 
                 []0, []1)"

|  let1   : "[| ∀C as r a'. e1 ≠ ConstrE C as r a'; 
               x1 ∉ fv e1; 
               x1 ∉ set (varsAPP Σd f);
               defined_AbstractDelta Δ1 f;
               defined_bound |Δ1| f;
               defined_bound μ1 f;
               defined_bound σ1 f;
               defined_AbstractDelta Δ2 f;
               defined_bound μ2 f;
               defined_bound σ2 f;
               e1, Σb \<turnstile>f (ϑ1, ϑ2) Φ 0 (Δ1, μ1, σ1);
               e2, Σb \<turnstile>f (ϑ1, ϑ2) Φ (td+1) (Δ2, μ2, σ2);
               Δ = Δ1  +Δ  Δ2; 
               μ = \<Squnion>c {μ1,|Δ1|+c  μ2}; 
               σ = \<Squnion>c 
                     {[]2 +c  σ1, 
                      []1 +c  σ2} |] 
             ==> Let x1 = e1 In e2 a, Σb \<turnstile>f (ϑ1, ϑ2) Φ td 
                                          ( Δ, μ , σ )"

|  let1c  : "[| (typesRegsAPP Σϑ f) r = Some ρ; ρ ∉ dom Δ;
              e2, Σb \<turnstile>f  (typesAPP Σϑ f) (sizesAPP ΣΦ f) td 
             (Δ, μ, σ) |] 
             ==> Let x1 = ConstrE C as r a' In e2 a, Σb
             \<turnstile>f  (typesAPP Σϑ f) (sizesAPP ΣΦ f) td 
                (Δ ++ [ρ \<mapsto> []1], 
                 μ +c  []1, 
                 σ2 +c []1)"

|  case1  : "[| length alts = length assert; 
               length alts > 0;
              (∀ i < length assert. 
                     defined_AbstractDelta (AbstractDeltaSpaceCost (assert ! i)) f);
              (∀ i < length assert. 
                     monotonic_AbstractDelta (AbstractDeltaSpaceCost (assert ! i)));
              (∀ i < length assert. 
                     defined_bound (AbstractMuSpaceCost (assert ! i)) f);
              (∀ i < length assert. 
                     monotonic_bound (AbstractMuSpaceCost (assert ! i)));
              (∀ i < length assert. 
                     defined_bound (AbstractSigmaSpaceCost (assert ! i)) f);
              (∀ i < length assert. 
                     monotonic_bound (AbstractSigmaSpaceCost (assert ! i)));
              ∀ i < length alts. 
              snd (alts ! i), Σb 
                   \<turnstile>f (ϑ1, ϑ2) Φ (td+ real (length (snd (extractP (fst (alts ! i)))))) 
                     (AbstractDeltaSpaceCost (assert!i), 
                      AbstractMuSpaceCost (assert!i), 
                      AbstractSigmaSpaceCost (assert!i));
               Δ = \<Squnion>Δ f (map AbstractDeltaSpaceCost assert);
               μ = \<Squnion>c (map AbstractMuSpaceCost assert);
               σ = \<Squnion>c (map (λ (Δ,n). addCostReal Δ n) 
                   (zip (map AbstractSigmaSpaceCost assert) 
                         (map num_r alts))) |] 
            ==> Case (VarE x a) Of alts a', Σb 
            \<turnstile>f (ϑ1, ϑ2) Φ td (Δ,μ,σ)"

|  app_primop :  "[| primops g = Some oper |] 
                   ==> AppE g [a1,a2] [] a, Σb 
                      \<turnstile>f (ϑ1, ϑ2) Φ td  
                      ([]g, 
                       []0, []2)"

|  app    :  "[| Σd g = Some (xs,rs,eg); Σb g = Some (projection g Δg,μg,σg);  
                primops g = None;
                l = real (length as); q = real (length rs');
                argP ψ (R_Args Σt g) (typesRegsAPP Σϑ f) rs';
                ∀i<length as. atom (as ! i);
                monotonic_bound μg; defined_bound μg g; 
                monotonic_bound σg; defined_bound σg g;
                monotonic_AbstractDelta Δg; defined_AbstractDelta Δg g;
                f ∈ dom Σd;
                Σt g = Some(ti,ρs,t);
                fv eg ⊆ set xs; fvReg eg ⊆ set rs; 
                fv eg ⊆ dom (sizesAPP ΣΦ f);
                length xs = length ti; 
                Δ = instance_f f g Δg ψ (sizesAPP ΣΦ f) as;
                μ = mu_app μg as (sizesAPP ΣΦ f);
                σ = \<Squnion>c  {[]l + q, 
                (substCostReal (addCostReal (addCostReal 
                   (sigma_app σg as (sizesAPP ΣΦ f))  l)  q) td)}|] 
               ==> AppE g as rs' a, Σb \<turnstile>f (typesAPP Σϑ f) 
                   (sizesAPP ΣΦ f) td  (Δ, μ, σ)"

|  rec    : "[| Σd f = Some (xs,rs,ef);  
               f ∉ dom Σb;
               (ρself_f f) ∉ dom Δ;
               finite (dom Δ);
               ef, Σb(f\<mapsto>(Δ,μ,σ)) 
               \<turnstile>f (typesAPP Σϑ f) (sizesAPP ΣΦ f) real(length 
               (varsAPP Σd f) + length (regionsAPP Σd f))  
               (Δ', μ', σ');
               (projection f Δ', μ', σ')  \<sqsubseteq>R  (Δ, μ, σ)|] 
             ==>  ef, Σb \<turnstile>f (typesAPP Σϑ f) (sizesAPP ΣΦ f) 
                  real(length (varsAPP Σd f)+length(regionsAPP Σd f)) 
                  (Δ', μ', σ')"


(* ∀n.  e :f typesAPP Σϑ f sizesAPP ΣΦ f td , n    \<lbrace> Δ , μ , σ \<rbrace> ≡ 
    e :f typesAPP Σϑ f sizesAPP ΣΦ f td  \<lbrace> Δ , μ , σ \<rbrace> *)

lemma equiv_all_n_SafeResourcesDAssDepth_SafeResourcesDAss:
  "∀n. SafeResourcesDAssDepth e f (typesAPP Σϑ f) (sizesAPP ΣΦ f) td n Δ μ σ 
  ==> e :f (typesAPP Σϑ f) (sizesAPP ΣΦ f) td \<lbrace>Δ, μ, σ\<rbrace>"
apply (simp only: typesAPP_def)
apply (simp only: SafeResourcesDAss.simps)
apply (simp only: SafeResourcesDAssDepth.simps)
apply (rule impI)
apply (rule conjI,simp)+
apply (intro allI, 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 (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 (erule_tac x=k in allE)
apply (erule_tac x=hh in allE)
apply (erule_tac x=v in allE)
apply (erule_tac x=δ in allE)
apply (erule_tac x=m in allE)
apply (erule_tac x=s in allE)
apply (erule_tac x=η in allE)
apply (erule_tac x=si in allE)
apply (drule mp)
 apply (rule conjI, simp add: Let_def, force)
 apply (rule conjI, simp)
 apply (rule conjI, simp)
 apply (rule conjI, simp)
 apply (rule conjI, simp)
 apply simp
by simp


lemma equiv_SafeResourcesDAss_all_n_SafeResourcesDAssDepth:
  "e :f (typesAPP Σϑ g) (sizesAPP ΣΦ g) td \<lbrace>Δ, μ, σ\<rbrace>
   ==> ∀n. SafeResourcesDAssDepth e f (typesAPP Σϑ g) (sizesAPP ΣΦ g) td n Δ μ σ"
apply (simp only: typesAPP_def)
apply (simp only: SafeResourcesDAss.simps)
apply (simp only: SafeResourcesDAssDepth.simps)
apply clarsimp
apply (simp only: SafeBoundSem_def)
apply (simp add: Let_def)
apply (elim exE)
apply (elim conjE)
apply (rotate_tac 7)
apply (erule_tac x=E1 in allE)
apply (erule_tac x=E2 in allE)
apply (erule_tac x=h in allE)
apply (rotate_tac 9)
apply (erule_tac x=k in allE)
apply (erule_tac x=hh in allE)
apply (erule_tac x=v in allE)
apply (erule_tac x=δ in allE)
apply (erule_tac x=m in allE)
apply (erule_tac x=s in allE)
apply (erule_tac x=η in allE)
apply (frule_tac td=td in eqSemDepthRA)
apply (drule mp,force)
by simp


lemma lemma_5:
  "∀ n. SafeResourcesDAssDepth e f (typesAPP Σϑ f) (sizesAPP ΣΦ f) td n Δ μ σ ≡  
   e :f (typesAPP Σϑ f) (sizesAPP ΣΦ f) td \<lbrace>Δ, μ, σ\<rbrace>"
apply (rule eq_reflection)
apply (rule iffI)
(* forward implication *)
 apply (rule equiv_all_n_SafeResourcesDAssDepth_SafeResourcesDAss,force)
(* backwards implication *)
by (rule equiv_SafeResourcesDAss_all_n_SafeResourcesDAssDepth,force)




(* ∀ n. \<Turnstile>\<Turnstile>f,n Σb ≡ ValidGlobalResourcesEnv Σb*)

declare fun_upd_apply [simp del]
declare SafeResourcesDAss.simps [simp del]
declare SafeResourcesDAssDepth.simps [simp del]

lemma imp_ValidGlobalResourcesEnv_all_n_ValidGlobalResourcesEnvDepth:
  "ValidGlobalResourcesEnv Σb
   ==> ∀ n. \<Turnstile>\<Turnstile>f,n Σb"
apply (erule ValidGlobalResourcesEnv.induct) 
 apply (rule allI)
 apply (rule ValidGlobalResourcesEnvDepth.base) 
  apply (rule ValidGlobalResourcesEnv.base)
 apply simp
apply (rule allI)
apply (case_tac "fa=f",simp)
 apply (induct_tac n)
  apply (rule ValidGlobalResourcesEnvDepth.depth0,simp,simp)
 apply (rule_tac ValidGlobalResourcesEnvDepth.step)
 apply (simp,simp,simp)
 apply (frule_tac f=f in equiv_SafeResourcesDAss_all_n_SafeResourcesDAssDepth,force)
apply (rule ValidGlobalResourcesEnvDepth.g)
by (simp,simp,simp,simp)



lemma imp_ValidGlobalResourcesEnv_all_n_ValidGlobalResourcesEnvDepth:
  "ValidGlobalResourcesEnv Σb
   ==> ∀ n. \<Turnstile>\<Turnstile>f,n Σb"
apply (erule ValidGlobalResourcesEnv.induct) 
 apply (rule allI)
 apply (rule ValidGlobalResourcesEnvDepth.base) 
  apply (rule ValidGlobalResourcesEnv.base)
 apply simp
apply (rule allI)
apply (case_tac "fa=f",simp)
 apply (induct_tac n)
  apply (rule ValidGlobalResourcesEnvDepth.depth0,simp,simp)
 apply (rule_tac ValidGlobalResourcesEnvDepth.step)
 apply (simp,simp,simp)
 apply (frule_tac f=f in equiv_SafeResourcesDAss_all_n_SafeResourcesDAssDepth,force)
apply (rule ValidGlobalResourcesEnvDepth.g)
by (simp,simp,simp,simp) 



lemma imp_ValidResourcesDepth_n_SigmaResources_Valid_Sigma [rule_format]:
  "\<Turnstile>\<Turnstile>f,n Σb
  --> f ∉ dom Σb
  --> ValidGlobalResourcesEnv Σb"
apply (rule impI)
apply (erule ValidGlobalResourcesEnvDepth.induct,simp_all)
apply (rule impI)
by (rule ValidGlobalResourcesEnv.step,simp_all) 



lemma imp_f_notin_SigmaResources_ValiddDepth_n_SigmaResources_Valid_Sigma:
  "[| f ∉ dom Σb; ∀ n. \<Turnstile>\<Turnstile>f,n Σb|]   
  ==> ValidGlobalResourcesEnv Σb"
apply (erule_tac x=n in allE)
by (rule imp_ValidResourcesDepth_n_SigmaResources_Valid_Sigma,assumption+)

lemma the_AbstractDeltaSpaceCost_upd:
  "AbstractDeltaSpaceCost (the ((Σ(f \<mapsto> (Δ,μ,σ))) f))= Δ"
by (simp add: fun_upd_apply add: dom_def)

lemma the_AbstractMuSpaceCost_upd:
  "AbstractMuSpaceCost (the ((Σ(f \<mapsto> (Δ,μ,σ))) f))= μ"
by (simp add: fun_upd_apply add: dom_def)

lemma the_AbstractSigmaSpaceCost_upd:
  "AbstractSigmaSpaceCost (the ((Σ(f \<mapsto> (Δ,μ,σ))) f))= σ"
by (simp add: fun_upd_apply add: dom_def)

lemma the_AbstractDeltaSpaceCost_other_upd:
  "g ≠ f
   ==> AbstractDeltaSpaceCost (the ((Σ(g \<mapsto> (Δ,μ,σ))) f)) = AbstractDeltaSpaceCost (the (Σ f))"
by (simp add: fun_upd_apply add: dom_def)

lemma the_AbstractMuSpaceCost_other_upd:
  "g ≠ f
   ==> AbstractMuSpaceCost (the ((Σ(g \<mapsto> (Δ,μ,σ))) f)) = AbstractMuSpaceCost (the (Σ f))"
by (simp add: fun_upd_apply add: dom_def)

lemma the_AbstractSigmaSpaceCost_other_upd:
  "g ≠ f 
   ==> AbstractSigmaSpaceCost (the ((Σ(g \<mapsto> (Δ,μ,σ))) f)) = AbstractSigmaSpaceCost (the (Σ f))"
by (simp add: fun_upd_apply add: dom_def)

lemma the_AbstractDeltaSpaceCost_other_projection_upd:
  "g ≠ f
   ==> AbstractDeltaSpaceCost (the ((Σ(g \<mapsto> (projection g Δ,μ,σ))) f)) = AbstractDeltaSpaceCost (the (Σ f))"
by (simp add: fun_upd_apply add: dom_def)


lemma the_AbstractMuSpaceCost_other_projection_upd:
  "g ≠ f
   ==> AbstractMuSpaceCost (the ((Σ(g \<mapsto> (projection g Δ,μ,σ))) f)) = AbstractMuSpaceCost (the (Σ f))"
by (simp add: fun_upd_apply add: dom_def)

lemma the_AbstractSigmaSpaceCost_other_projection_upd:
  "g ≠ f 
   ==> AbstractSigmaSpaceCost (the ((Σ(g \<mapsto> (projection g Δ,μ,σ))) f)) = AbstractSigmaSpaceCost (the (Σ f))"
by (simp add: fun_upd_apply add: dom_def)


axioms equals_projection:
  "projection f Δ' = projection f Δ
   ==> Δ' = Δ"


lemma Theorem_4_aux [rule_format]:
  " \<Turnstile>\<Turnstile>f,n Σb
   --> n = Suc n' 
   --> f ∈ dom Σb
   --> Σb f = Some (projection f Δ, μ ,σ)
   -->  (bodyAPP Σd f)  :f (typesAPP Σϑ f) (sizesAPP ΣΦ f) real(length (varsAPP Σd f) + length (regionsAPP Σd f)), n' 
            \<lbrace> Δ, μ, σ \<rbrace>"
apply (rule impI)
apply (erule ValidGlobalResourcesEnvDepth.induct) 
 apply simp apply simp
 apply (rule impI)+
 apply (subst (asm) map_upd_Some_unfold,simp)
 apply (elim conjE, frule equals_projection,simp)
apply clarsimp
by  (simp add: fun_upd_apply add: dom_def)


lemma Theorem_4:
  "[| ∀ n > 0. \<Turnstile>\<Turnstile>f,n Σb; f ∈ dom Σb; Σb f = Some (projection f Δ, μ ,σ) |] 
   ==> ∀ n. (bodyAPP Σd f) :f (typesAPP Σϑ f) (sizesAPP ΣΦ f) real(length (varsAPP Σd f) + length (regionsAPP Σd f)), n 
            \<lbrace> Δ , μ, σ \<rbrace>"
apply (rule allI)
apply (rule_tac n="Suc n" in Theorem_4_aux)
by (force,simp,simp,simp)



lemma Theorem_5_aux [rule_format]:
  "\<Turnstile>\<Turnstile>f,n Σb
   --> n = Suc n' 
   --> f ∈ dom Σb
   --> Σb f = Some (projection f Δ, μ ,σ)
   -->  (bodyAPP Σd f) :f  (typesAPP Σϑ f) (sizesAPP ΣΦ f) real(length (varsAPP Σd f) + length (regionsAPP Σd f))    
            \<lbrace> Δ, μ, σ \<rbrace>
   --> \<Turnstile>\<Turnstile> Σb"
apply (rule impI)
apply (erule ValidGlobalResourcesEnvDepth.induct,simp_all)
 apply (rule impI)+
 apply (rule ValidGlobalResourcesEnv.step) 
 apply (simp,simp)
 apply (subst (asm) map_upd_Some_unfold,simp)
 apply (elim conjE, frule equals_projection,simp)
apply (rule impI)+
apply (case_tac "g=f",simp_all)
apply (rule ValidGlobalResourcesEnv.step,simp_all) 
apply (subgoal_tac "f ∈ dom Σb",simp)
 prefer 2 apply (simp add: fun_upd_apply add: dom_def)
by (simp add: fun_upd_apply add: dom_def)+


lemma Theorem_5:
  "[| ∀ n > 0. \<Turnstile>\<Turnstile>f,n Σb; f ∈ dom Σb; Σb f = Some (projection f Δ, μ ,σ);
     (bodyAPP Σd f) :f  (typesAPP Σϑ f) (sizesAPP ΣΦ f) real(length (varsAPP Σd f) + length (regionsAPP Σd f))    
             \<lbrace> Δ, μ ,σ \<rbrace>|] 
   ==> \<Turnstile>\<Turnstile> Σb"
apply (rule_tac n="Suc n" in Theorem_5_aux)
by simp_all



lemma signature_correct [rule_format]:
  "\<Turnstile>\<Turnstile>f,n Σb 
  --> f ∈ dom Σb
  --> (∃ Δ. (AbstractDeltaSpaceCost (the (Σb f))) = projection f Δ)"
apply (rule impI)
apply (erule ValidGlobalResourcesEnvDepth.induct,simp_all)
  apply (simp add: fun_upd_apply add: dom_def,force)
 apply (rule_tac x="Δ" in exI)
 apply (simp add: fun_upd_apply add: dom_def)
apply (rule impI)
apply (drule mp,simp)
apply (elim exE)
apply (rule_tac x="Δ'" in exI)
by (simp add: fun_upd_apply add: dom_def)



lemma imp_f_in_SigmaResources_ValidDepth_n_SigmaResources_Valid_Sigma:
  "[| ∀ n. \<Turnstile>\<Turnstile>f,n Σb; f ∈ dom Σb |] 
   ==> ValidGlobalResourcesEnv Σb"
apply (subgoal_tac "\<Turnstile>\<Turnstile>f,n Σb")
 prefer 2 apply simp
apply (frule signature_correct,assumption)
apply (elim exE)
apply (frule domD) 
apply (elim exE, case_tac b, case_tac ba,simp,clarsimp)
apply (subgoal_tac "f ∈ dom Σb")
 apply (subgoal_tac "\<Turnstile>\<Turnstile>f,0 Σb ∧ (∀n > 0. \<Turnstile>\<Turnstile>f,n Σb)",elim conjE)
  prefer 2 apply simp
 apply (frule Theorem_4,simp_all,force) 
 apply (subgoal_tac "\<Turnstile>\<Turnstile>f,0 Σb ∧ (∀n > 0. \<Turnstile>\<Turnstile>f,n Σb)",elim conjE)
  prefer 2 apply simp
 apply (frule Theorem_5,simp_all,force) 
 apply (rule equiv_all_n_SafeResourcesDAssDepth_SafeResourcesDAss,simp) 
by (simp add: dom_def)



lemma imp_all_n_ValidGlobalResourcesEnvDepth_ValidGlobalResourcesEnv:
  "[| ∀ n. \<Turnstile>\<Turnstile>f,n Σb |] 
   ==> ValidGlobalResourcesEnv Σb"
apply (case_tac "f ∉ dom Σb",simp_all)
 apply (rule imp_f_notin_SigmaResources_ValiddDepth_n_SigmaResources_Valid_Sigma,assumption+)
by (rule imp_f_in_SigmaResources_ValidDepth_n_SigmaResources_Valid_Sigma,assumption+)


lemma lemma_6:
  "∀ n. \<Turnstile>\<Turnstile>f,n Σb ≡ 
   ValidGlobalResourcesEnv Σb"
apply (rule eq_reflection)
apply (rule iffI)
(* forward implication *)
 apply (rule_tac f=f in imp_all_n_ValidGlobalResourcesEnvDepth_ValidGlobalResourcesEnv,force)
(* backwards implication *)
by (rule imp_ValidGlobalResourcesEnv_all_n_ValidGlobalResourcesEnvDepth,force)



(* ∀n.  e , Σb :f typesAPP Σϑ f sizesAPP ΣΦ f td , n  \<lbrace> Δ , μ , σ \<rbrace> 
   ==> e , Σb : f typesAPP Σϑ f sizesAPP ΣΦ f  \<lbrace> td , Δ , μ \<rbrace> σ *)


lemma lemma_7:
  "[| ∀ n. e, Σb :f (typesAPP Σϑ f) (sizesAPP ΣΦ f) td, n \<lbrace> Δ , μ , σ \<rbrace> |] 
   ==> SafeResourcesDAssCntxt e Σb f (typesAPP Σϑ f) (sizesAPP ΣΦ f) td Δ μ σ"
apply (simp only: typesAPP_def)
apply (simp only: SafeResourcesDAssDepthCntxt.simps)
apply (subgoal_tac 
  "(∀n. \<Turnstile>\<Turnstile>f,n Σb) --> 
   (∀n.  e :f (typesAPP Σϑ f) (sizesAPP ΣΦ f) td, n \<lbrace> Δ , μ , σ \<rbrace>)")
 apply (erule thin_rl)
 apply (subst (asm) lemma_5)
 apply (subst (asm) lemma_6)
 apply (simp add: SafeResourcesDAssCntxt.simps)
apply (simp only: typesAPP_def)
apply (rule impI)
apply (simp only: typesAPP_def)
by force



(*  e, Σb \<turnstile>f  (typesAPP Σϑ f) (sizesAPP ΣΦ f) td  (Δ,μ,σ)
   ==> ∀ n. e , Σb :f  (typesAPP Σϑ f) (sizesAPP ΣΦ f) td,n \<lbrace> Δ , μ , σ \<rbrace> *)

lemma fold_op_plus_le [rule_format]:
  "finite ({ρ. η ρ = Some j})
   --> Δ' \<sqsubseteq>Δ Δ
   --> fold op + (λρ. the (the (Δ' ρ) si)) (0::real) ({ρ. η ρ = Some j}) ≤ 
       fold op + (λρ. the (the (Δ ρ) si)) (0::real) ({ρ. η ρ = Some j})"
apply (rule impI)
apply (induct rule: finite_induct)
 apply (rule impI)
 apply simp 
apply (rule impI)+
apply (simp add: ran_def)
apply (simp add: abstractDelta_le_def)
apply (subgoal_tac "the (the (Δ' x) si) ≤ the (the (Δ x) si)")
 apply clarsimp
apply (elim conjE)
apply (case_tac "x ∈ dom Δ")
 apply (simp add: costs_le_def)
 apply (case_tac "si ∈dom (the (Δ' x))",force,force)
apply (subgoal_tac "Δ x = None",simp) 
 apply (subgoal_tac "Δ' x = None",simp,force) 
by force



lemma sizeAbstractDelta_si_le:
  "[| finite ({ρ. η ρ = Some j ∧ ρ ∈ dom Δ});
     Δ' \<sqsubseteq>Δ  Δ |] 
   ==> sizeAbstractDelta_si Δ' si j η ≤ 
       sizeAbstractDelta_si Δ si j η"
apply (simp add: sizeAbstractDelta_si_def)
apply (simp add: setsum_def)
apply (rule impI)
by (rule fold_op_plus_le,assumption+)


lemma resources_le_Delta_ge:
 "[| ∀j∈{0..k}. finite ({ρ. η ρ = Some j ∧ ρ ∈ dom Δ});
    Delta_ge Δ' si k η δ;  Δ' \<sqsubseteq>Δ  Δ|] 
  ==> Delta_ge Δ si k η δ"
apply (simp add: Delta_ge_def)
apply (rule ballI)
apply (subgoal_tac "dom Δ' = dom Δ")
 prefer 2 apply (simp add: abstractDelta_le_def)
apply (erule_tac x=j in ballE,simp)
 apply (frule_tac η=η and j=j and si=si in sizeAbstractDelta_si_le,assumption+) 
 apply force
by simp


lemma resources_le_Mu_ge:
 "[| mu_ge μ' si s; μ' \<sqsubseteq>c μ |] 
  ==> mu_ge μ si s"
apply (simp add: mu_ge_def)
apply (simp add: costs_le_def)
apply (erule real_le_trans) 
apply (elim conjE)
by (erule_tac x=si in ballE,simp,force)


lemma resources_le_Sigma_ge:
 "[| sigma_ge σ' si s;  σ' \<sqsubseteq>c σ |] 
  ==> sigma_ge σ si s"
apply (simp add: sigma_ge_def)
apply (simp add: costs_le_def)
apply (erule real_le_trans) 
apply (elim conjE)
by (erule_tac x=si in ballE,simp,force)




lemma dom_projection_Delta:
  "dom (projection f Δ) = dom Δ - {(ρself_f f)}"
apply (rule equalityI)
 apply (rule subsetI)
 apply (simp add: projection_def,clarsimp)
 apply (split split_if_asm,simp,force)
apply (rule subsetI)
apply (simp add: projection_def)
by clarsimp


lemma dom_delta'_equals_dom_delta_ρself:
  "[| insert (ρself_f f) (set (R_Args Σt f)) = dom Δ';
     projection f Δ' \<sqsubseteq>Δ Δ |] 
   ==> dom Δ' = insert (ρself_f f) (dom Δ)"
apply (rule equalityI)
 apply (rule subsetI)
 apply (simp add: abstractDelta_le_def)
 apply (subst (asm) dom_projection_Delta)
 apply blast
apply (rule subsetI)
apply (simp add: abstractDelta_le_def)
apply (subst (asm) dom_projection_Delta)
by blast


lemma projection_prop:
  "[| insert (ρself_f f) (set (R_Args Σt f)) = dom Δ';
      projection f Δ' \<sqsubseteq>Δ Δ |] 
   ==> Δ' \<sqsubseteq>Δ Δ(ρself_f f \<mapsto> the (Δ' (ρself_f f)))"
apply (simp (no_asm) add: abstractDelta_le_def)
apply (rule conjI)
 apply (rule dom_delta'_equals_dom_delta_ρself,simp,simp) 
apply (subst dom_delta'_equals_dom_delta_ρself,simp,simp)
apply (rule ballI)
apply (simp only: abstractDelta_le_def)
apply (elim conjE,clarsimp,erule disjE)
 apply (simp add: fun_upd_apply add: dom_def) 
 apply (simp add: costs_le_def)
apply (erule_tac x=ρ in ballE)
 prefer 2 apply simp
apply (subst (asm) dom_projection_Delta)
apply (subgoal_tac "ρ ≠ (ρself_f f)")
 apply (simp add: projection_def)
 apply (simp add: fun_upd_apply add: dom_def)
by blast



lemma sizeAbstractDelta_si_le:
  "[| insert (ρself_f f) (set (R_Args Σt f)) = dom Δ';
     finite ({ρ. η ρ = Some j ∧ ρ ∈ dom Δ});
     projection f Δ' \<sqsubseteq>Δ  Δ |] 
   ==> sizeAbstractDelta_si Δ' si j η ≤ 
       sizeAbstractDelta_si (Δ(ρself_f f \<mapsto> the (Δ' (ρself_f f)))) si j η"
apply (simp add: sizeAbstractDelta_si_def)
apply (simp add: setsum_def)
apply (rule impI)
apply (rule fold_op_plus_le,assumption+)
by (rule projection_prop,assumption+)


lemma resources_le_Delta_ge:
 "[| insert (ρself_f f) (set (R_Args Σt f)) = dom Δ';
    ∀j∈{0..k}. finite ({ρ. η ρ = Some j ∧ ρ ∈ dom Δ});
    Delta_ge Δ' si k η δ;  projection f Δ' \<sqsubseteq>Δ  Δ|] 
  ==> Delta_ge (Δ(ρself_f f \<mapsto> the (Δ' (ρself_f f)))) si k η δ"
apply (simp add: Delta_ge_def)
apply (rule ballI)
apply (erule_tac x=j in ballE,simp)
 apply (frule_tac η=η and j=j and si=si in sizeAbstractDelta_si_le,assumption+) 
 apply force
by simp

lemma finite_dom_Δ_finite_η:
  "finite (dom Δ)
   ==> (∀j∈{0..k}. finite ({ρ. η ρ = Some j ∧ ρ ∈ dom Δ}))"
apply (rule ballI)
apply (rule_tac B="{ρ. ρ ∈ dom Δ}" in finite_subset)
by (blast,simp)


lemma resources_le_SafeResourcesDAssDepth:
  "[| ( projection f Δ' , μ' , σ' )  \<sqsubseteq>R ( Δ , μ , σ );
      finite (dom Δ);
       bodyAPP Σd f :f (typesAPP Σϑ f) (sizesAPP ΣΦ f) td, n  \<lbrace> Δ' , μ' , σ' \<rbrace> |] 
   ==> bodyAPP Σd f :f (typesAPP Σϑ f) (sizesAPP ΣΦ f) td, n  \<lbrace> Δ((ρself_f f) \<mapsto> the (Δ' (ρself_f f))), μ , σ \<rbrace>"
apply (simp only: resources_le_def)
apply (simp only: typesAPP_def)
apply (simp only: SafeResourcesDAssDepth.simps)
apply (elim conjE)
apply (rule impI)
apply (rule conjI,simp)+
 apply (rule dom_delta'_equals_dom_delta_ρself,simp,simp) 
apply (drule mp,simp)
apply (elim conjE)
apply (rule allI)+
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 (erule_tac x=δ in allE)
apply (erule_tac x=m in allE)
apply (erule_tac x=s in allE)
apply (erule_tac x=η in allE)
apply (erule_tac x=si in allE)
apply (rule impI)
apply (elim conjE)
apply (drule mp)
 apply (rule conjI,simp)+
 apply (subst dom_delta'_equals_dom_delta_ρself,simp,simp,simp)
 apply (rule conjI,simp)
 apply simp
apply (elim conjE)
apply (frule_tac η=η and k=k in finite_dom_Δ_finite_η)
apply (rule conjI, rule resources_le_Delta_ge,simp,simp,simp,simp)
apply (rule conjI, rule resources_le_Mu_ge,simp,simp)
by (rule resources_le_Sigma_ge,simp,simp)



lemma projection_prop2:
  "(ρself_f f) ∉ dom Δ
   ==> Δ = projection f (Δ(ρself_f f \<mapsto> the (Δ' (ρself_f f))))"
apply (rule map_le_antisym)
 apply (simp add: projection_def)
 apply (simp add: map_le_def,clarsimp)
 apply (rule sym)
 apply (subst map_upd_Some_unfold,simp)
apply (simp add: projection_def)
apply (simp add: map_le_def,clarsimp)
by (subst (asm) map_upd_Some_unfold,simp)


lemma lemma_8_REC [rule_format]:
  "(∀n. (ValidGlobalResourcesEnvDepth f n (Σb(f \<mapsto> (Δ, μ, σ))))  
         -->  SafeResourcesDAssDepth (bodyAPP Σd f) f (typesAPP Σϑ f) (sizesAPP ΣΦ f) 
                                     (real (length (varsAPP Σd f)) + real (length (regionsAPP Σd f)))  n Δ' μ' σ')
   --> f ∉ dom Σb
   --> (ρself_f f) ∉ dom Δ
   --> finite (dom Δ)
   --> ( projection f Δ' , μ' , σ' ) \<sqsubseteq>R ( Δ , μ , σ )
   --> ValidGlobalResourcesEnvDepth f n Σb
   --> SafeResourcesDAssDepth (bodyAPP Σd f) f (typesAPP Σϑ f) (sizesAPP ΣΦ f) 
                              (real (length (varsAPP Σd f)) + real (length (regionsAPP Σd f)))  n Δ' μ' σ' "
apply (rule impI)
apply (induct_tac n)
 (* n = 0 *)
 apply (rule impI)+
 apply (erule_tac x=0 in allE)
 apply (frule imp_ValidResourcesDepth_n_SigmaResources_Valid_Sigma,assumption+)
 apply (subgoal_tac "\<Turnstile>\<Turnstile>f,0 Σb(f \<mapsto> (Δ, μ, σ))",simp)
 apply (subst projection_prop2,assumption)
 apply (rule ValidGlobalResourcesEnvDepth.depth0,assumption+)
(* n > 0 *)
apply (erule_tac x="Suc n" in allE)
apply (rule impI)+
apply (drule mp,simp)
apply (frule imp_ValidResourcesDepth_n_SigmaResources_Valid_Sigma,assumption+)
apply (frule_tac f=f in imp_ValidGlobalResourcesEnv_all_n_ValidGlobalResourcesEnvDepth)
apply (erule_tac x=n in allE,simp)
apply (frule resources_le_SafeResourcesDAssDepth,assumption+)
apply (subgoal_tac "\<Turnstile>\<Turnstile>f,Suc n Σb(f \<mapsto> (Δ, μ, σ))",simp) 
apply (subst projection_prop2,assumption)
by (rule ValidGlobalResourcesEnvDepth.step,simp_all)



lemma lemma_8:
  " e, Σb \<turnstile>f  (typesAPP Σϑ f) (sizesAPP ΣΦ f) td  (Δ,μ,σ)
   ==> ∀ n. e , Σb :f  (typesAPP Σϑ f) (sizesAPP ΣΦ f) td,n \<lbrace> Δ , μ , σ \<rbrace>"
apply (simp only: typesAPP_def)
apply (erule ProofRulesCostes.induct)
 (* ConstE (LitN i) *)
 apply (simp only: SafeResourcesDAssDepthCntxt.simps)
 apply (rule allI, rule impI) 
 apply (rule SafeResourcesDADepth_LitInt)
 
 (* ConstE (LitB b) *)
 apply (simp only: SafeResourcesDAssDepthCntxt.simps)
 apply (rule allI, rule impI) 
 apply (rule SafeResourcesDADepth_LitBool)

 (* VarE x *)
 apply (simp only: SafeResourcesDAssDepthCntxt.simps)
 apply (rule allI, rule impI)
 apply (rule SafeResourcesDADepth_Var1)

 (* x @ r *)
 apply (simp only: typesAPP_def)
 apply (simp only: SafeResourcesDAssDepthCntxt.simps)
 apply (rule allI, rule impI) 
 apply (rule SafeResourcesDADepth_Var2,force,force)

 (* ReuseE x *)
 apply (simp only: typesAPP_def)
 apply (simp only: SafeResourcesDAssDepthCntxt.simps)
 apply (rule allI, rule impI) 
 apply (rule SafeResourcesDADepth_Var3,force,force)

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

 (* Let x1 = e1 In e2. LET2 *)
 apply (rule allI)
 apply (simp only: typesAPP_def)
 apply (simp only: SafeResourcesDAssDepthCntxt.simps)
 apply (rule impI)
 apply (erule_tac x=n in allE)+
 apply (drule mp, simp)+
 apply (rule SafeResourcesDADepth_Let2)
 apply assumption+

 (* Case VarE x a Of alts *)
 apply (rule allI)
 apply (simp only: SafeResourcesDAssDepthCntxt.simps)
 apply (rule impI)
 apply (rule SafeResourcesDADepth_CASE) 
 apply (assumption+,simp,assumption+,simp,simp,simp,simp)

 (* AppE fa [a1, a2] [] a *)
 apply (rule allI)
 apply (simp only: SafeResourcesDAssDepthCntxt.simps)
 apply (rule impI)
 apply (rule SafeResourcesDADepth_APP_PRIMOP)
 apply (assumption+)

 (* AppE fa as rs' a. APP *)
 apply (rule allI)
 apply (simp only: typesAPP_def)
 apply (simp only: SafeResourcesDAssDepthCntxt.simps)
 apply (rule impI)
 apply (fold typesAPP_def)
 apply (frule_tac  σg=σg  in SafeResourcesDADepth_APP) 
 apply (assumption+,simp,assumption+,simp)

 (* Rec *)
 apply (simp only: typesAPP_def)
 apply (simp only: SafeResourcesDAssDepthCntxt.simps)
 apply (rule allI)
 apply (rule impI)
 apply (subgoal_tac 
   "ef = (bodyAPP Σd f) ∧
    xs = (varsAPP Σd f) ∧
    rs = (regionsAPP Σd f)",simp)
 apply (fold typesAPP_def)
 apply (rule_tac f=f and Σb=Σb in lemma_8_REC)
 apply (simp only: typesAPP_def)
 apply (force,simp,simp,simp,simp,simp)
 apply (simp add: bodyAPP_def)
 apply (simp add: varsAPP_def)
 apply (simp add: regionsAPP_def)
done





(* Soundness theorem *)


lemma lemma_2:
  "e, Σb \<turnstile>f  (typesAPP Σϑ f) (sizesAPP ΣΦ f)  td (Δ,μ,σ) 
  ==> SafeResourcesDAssCntxt e Σb f  (typesAPP Σϑ f) (sizesAPP ΣΦ f)  td Δ μ σ"
apply (rule lemma_7)
by (rule lemma_8,assumption)


end