Up to index of Isabelle/HOL/Bounds
theory CostesDepth(* Title:
Author: Ricardo Pe{\~n}a and Javier de Dios
Copyright: June 2010, Universidad Complutense de Madrid
*)
header {* Auxiliary lemmas of the soundness theorem *}
theory CostesDepth
imports Costes_definitions
begin
(********** Assert: (ConstE (LitN i) a) ***********)
lemma dom_emptyAbstractDelta:
"dom []f = (set (R_Args Σt f)) ∪ {ρself_f f}"
apply (rule equalityI)
apply (rule subsetI)
apply (simp add: emptyAbstractDelta_def,clarsimp)
apply (split split_if_asm,simp,simp)
apply (simp add: emptyAbstractDelta_def)
by (rule conjI,force,force)
lemma Delta_ge_emptyAbstractDelta_emptyDelta:
"[| dom []f = dom η |]
==> Delta_ge []f si k η (SafeRASemanticsReal.emptyDelta k)"
apply (subst (asm) dom_emptyAbstractDelta)
apply (simp add: Delta_ge_def)
apply (simp add: sizeAbstractDelta_si_def)
apply (simp add: emptyDelta_def)
apply (simp add: emptyAbstractDelta_def)
apply (rule ballI)
apply (rule setsum_nonneg)
apply (simp add: constantCost_def)
apply (rule allI, intro impI)
by clarsimp
lemma mu_ge_constantCost:
"mu_ge []0 si 0"
by (simp add: mu_ge_def add: constantCost_def)
lemma sigma_ge_constantCost:
"sigma_ge []1 si 1"
by (simp add: sigma_ge_def add: constantCost_def)
lemma SafeResourcesDADepth_LitInt:
"ConstE (LitN i) a :f (ϑ1, ϑ2) φ td, n
\<lbrace>[]f , []0, []1\<rbrace>"
apply (simp only: SafeResourcesDAssDepth.simps)
apply (rule impI)
apply (rule conjI)
(* P_stat *)
apply (subst dom_emptyAbstractDelta,simp)
(* Let us assume P\<Down>(f,n) *)
apply (intro allI,rule impI)
apply (elim conjE)
apply (frule impSemBoundRA [where td=td])
apply (erule SafeRASem.cases,simp_all)
apply clarsimp
apply (rule conjI)
(* P_Δ *)
apply (rule Delta_ge_emptyAbstractDelta_emptyDelta,assumption+)
apply (rule conjI)
(* P_μ *)
apply (rule mu_ge_constantCost)
(* P_σ *)
by (rule sigma_ge_constantCost)
(********** (ConstE (LitB b) a) ***********)
lemma SafeResourcesDADepth_LitBool:
"ConstE (LitB b) a :f (ϑ1, ϑ2) φ td, n \<lbrace>[]f , []0, []1\<rbrace>"
apply (simp only: SafeResourcesDAssDepth.simps)
apply (rule impI)
apply (rule conjI)
(* P_stat *)
apply (subst dom_emptyAbstractDelta,simp)
(* Let us assume P\<Down>(f,n) *)
apply (intro allI,rule impI)
apply (elim conjE)
apply (frule impSemBoundRA [where td=td])
apply (erule SafeRASem.cases,simp_all)
apply clarsimp
apply (rule conjI)
(* P_Δ *)
apply (rule Delta_ge_emptyAbstractDelta_emptyDelta,assumption+)
apply (rule conjI)
(* P_μ *)
apply (rule mu_ge_constantCost)
(* P_σ *)
by (rule sigma_ge_constantCost)
(********** VarE x a ***********)
axioms SafeResourcesDADepth_Var1:
"VarE x a :f (ϑ1, ϑ2) φ td, n
\<lbrace>[]f , []0, []1\<rbrace>"
(********** CopyE x r d ***********)
axioms SafeResourcesDADepth_Var2:
"[| ϑ2 r = Some ρ; φ x = Some η |]
==> CopyE x r d :f (ϑ1, ϑ2) φ td, n \<lbrace>[ρ \<mapsto> η], η, []2\<rbrace>"
(********** Reuse x a ***********)
axioms SafeResourcesDADepth_Var3:
"[| ϑ2 r = Some ρ; φ x = Some η |]
==> ReuseE x a :f (ϑ1, ϑ2) φ td, n
\<lbrace>[]f , []0, []1\<rbrace>"
(********** App_PRIMOP ***********)
axioms SafeResourcesDADepth_APP_PRIMOP:
"[| primops g = Some oper |]
==> AppE g [a1,a2] [] a :f (ϑ1, ϑ2) φ td, n
\<lbrace>[]g , []0, []2\<rbrace>"
(********** Let x1 = e1 In e2 a ***********)
lemma dom_addAbstractDelta:
"dom (Δ1 +Δ Δ2) = dom Δ1 ∩ dom Δ2"
apply (simp add: addAbstractDelta_def)
apply auto
by (split split_if_asm,force,force)+
lemma P_static_dom_Δ_Let:
"[| set (R_Args Σt f) ∪ {ρself_f f} = dom Δ1;
set (R_Args Σt f) ∪ {ρself_f f} = dom Δ2 |]
==> set (R_Args Σt f) ∪ {ρself_f f} = dom Δ1 +Δ Δ2"
by (subst dom_addAbstractDelta,simp)
lemma P1_f_n_LET:
" [|∀C as r a'. e1 ≠ ConstrE C as r a';
SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (Let x1 = e1 In e2 a)
(f, n) hh k v (δ, m, s)|]
==> ∃h' v1 v2 δ1 m1 s1 δ2 m2 s2 n1 n2.
SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k 0 e1
(f, n) h' k v1 (δ1, m1, s1)
∧ SafeDepthSemanticsReal.SafeBoundSem (E1(x1 \<mapsto> v1), E2) h' k (td + 1) e2
(f, n) hh k v2 (δ2, m2, s2)
∧ δ = SafeRASemanticsReal.addDelta δ1 δ2
∧ m = max m1 (m2 + SafeRASemanticsReal.balanceCells δ1)
∧ s = max (s1 + 2) (s2 + 1)
∧ x1 ∉ dom E1"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
apply (elim conjE)
apply (rule_tac x=h' in exI)
apply (rule_tac x=v1 in exI)
apply (rule_tac x=v2 in exI)
apply (rule_tac x=δ1 in exI)
apply (rule_tac x=m1 in exI)
apply (rule_tac x=s1 in exI)
apply (rule conjI)
apply (rule_tac x=n1 in exI)+
apply simp
apply (rule_tac x=δ2 in exI)
apply (rule_tac x=m2 in exI)
apply (rule_tac x=s2 in exI)
apply (rule conjI)
apply (rule_tac x=n2 in exI)+
apply simp
by simp
lemma P_dyn_dom_E1_Let_e1:
"[| set (varsAPP Σd f) ∪ fv (Let x1 = e1 In e2 a) ⊆ dom E1;
x1 ∉ fv e1 |]
==> set (varsAPP Σd f) ∪ fv e1 ⊆ dom E1"
by (simp,elim conjE, blast)
lemma P_dyn_dom_E1_Let_e2:
"[| set (varsAPP Σd f) ∪ fv (Let x1 = e1 In e2 a) ⊆ dom E1;
x1 ∉ fv e1 |]
==> set (varsAPP Σd f) ∪ fv e2 ⊆ dom (E1(x1 \<mapsto> v1))"
by (simp,elim conjE, blast)
lemma P_dyn_dom_Δ_Let_e1:
"[| set (R_Args Σt f) ∪ {ρself_f f} = dom Δ1;
set (R_Args Σt f) ∪ {ρself_f f} = dom Δ2;
dom Δ1 +Δ Δ2 = dom η |]
==> dom Δ1 = dom η"
by (subst (asm) dom_addAbstractDelta,simp)
lemma P_dyn_dom_Δ_Let_e2:
"[| set (R_Args Σt f) ∪ {ρself_f f} = dom Δ1;
set (R_Args Σt f) ∪ {ρself_f f} = dom Δ2;
dom Δ1 +Δ Δ2 = dom η |]
==> dom Δ1 = dom η"
by (subst (asm) dom_addAbstractDelta,simp)
lemma length_build_si:
"length (build_si E1 h xs) = length xs"
by (induct xs,simp_all)
lemma sizeAbstractDelta_si_addf:
"[| set (R_Args Σt f) ∪ {ρself_f f} = dom Δ1; defined_AbstractDelta Δ1 f;
set (R_Args Σt f) ∪ {ρself_f f} = dom Δ2; defined_AbstractDelta Δ2 f;
dom Δ1 +Δ Δ2 = dom η |]
==> sizeAbstractDelta_si Δ1 +Δ Δ2 (build_si E1 h (varsAPP Σd f)) j η
= sizeAbstractDelta_si Δ1 (build_si E1 h (varsAPP Σd f)) j η + sizeAbstractDelta_si Δ2 (build_si E1 h (varsAPP Σd f)) j η"
apply (frule P_static_dom_Δ_Let,simp)
apply (subgoal_tac " dom Δ1 +Δ Δ2 = dom Δ2")
apply (subgoal_tac "dom Δ1 = dom Δ2",simp)
apply (simp only: sizeAbstractDelta_si_def)
apply (subgoal_tac "(∑ρ | η ρ = Some j. the (the ( Δ1 +Δ Δ2 ρ) (build_si E1 h (varsAPP Σd f)))) =
(∑ρ | η ρ = Some j. the (the (Δ1 ρ) (build_si E1 h (varsAPP Σd f))) + the (the (Δ2 ρ) (build_si E1 h (varsAPP Σd f))))",simp)
apply (subst setsum_addf)
apply (simp only: addAbstractDelta_def)
apply (rule setsum_cong2)
apply (simp add: addAbstractDelta_def)
apply (rule conjI)
apply (rule impI)+
apply (simp add: addCost_def)
apply (rule impI)
apply (simp add: defined_AbstractDelta_def)
apply (erule_tac x=x in ballE)
prefer 2 apply simp
apply (simp add: defined_bound_def)
apply (erule_tac x="(build_si E1 h (varsAPP Σd f))" in allE)
apply (subst (asm) length_build_si)
apply simp
apply (erule_tac x=x in ballE)
prefer 2 apply simp
apply (erule_tac x="(build_si E1 h (varsAPP Σd f))" in allE)
apply (subst (asm) length_build_si)
apply simp
apply (simp add: dom_def)
apply simp
by simp
lemma sizeAbstractDelta_si_nonneg:
"[| dom Δ = dom η;
∀ρ∈dom Δ. 0 ≤ the (the (Δ ρ) si) |]
==> sizeAbstractDelta_si Δ si j η ≥ 0"
apply (simp add: sizeAbstractDelta_si_def)
by (rule setsum_nonneg,simp,force)
axioms wellFormed_Δ:
"∀ρ ∈ dom Δ.
0 ≤ the (the (Δ ρ) (build_si E1 h (varsAPP Σd f)))"
axioms semantic_no_capture_E1:
"[| SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td e (f, n) h' k v (δ, m, s);
E1 x = Some (Loc p);
p ∉ dom h |]
==> p ∉ dom h'"
axioms semantic_extend_pointers:
" SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td e (f, n) h' k v (δ, m, s)
==> (∀p∈dom h. h p = h' p)"
axioms size_equals_h_h':
"v = Loc p
==> size v h' = Costes_definitions.size v h"
axioms axiom_size_dom:
"(∀ x ∈ set (varsAPP Σd f). size_dom (the (E1 x), h))"
lemma sizeEnv_equals_h_h':
"[| x1 ∉ dom E1;
SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td e (f, n) h' k v (δ, m, s);
x1 ∉ set xs; x1 ≠ x;
size_dom (the (E1 x), h); size_dom (the (E1 x), h');
(∀ x ∈ set xs. size_dom (the (E1 x), h) ∧ size_dom (the (E1 x),h'))|]
==> sizeEnv E1 x h = sizeEnv (E1(x1 \<mapsto> v1)) x h'"
apply (subgoal_tac "sizeEnv (E1(x1 \<mapsto> v1)) x h' = sizeEnv E1 x h'",simp)
prefer 2 apply (simp add: sizeEnv_def)
apply (frule semantic_extend_pointers)
apply (simp add: sizeEnv_def)
apply (case_tac "E1 x",simp_all)
apply (case_tac a)
(* Loc p *)
apply (rename_tac v' p)
apply (case_tac "p ∉ dom h")
(* p ∉ dom h *)
apply (frule semantic_no_capture_E1,simp,assumption+)
apply (subgoal_tac "h p = None ∧ h' p = None")
apply (simp add: size.psimps(3))
apply force
(* p ∈ dom h *)
apply (subgoal_tac "∃ j C vn. h p = Some (j,C,vn)")
prefer 2 apply force
apply (elim exE)
apply (rule size_equals_h_h',assumption)
(* IntT *)
apply simp
(* BoolT *)
by simp
lemma build_si_equals_h_h' [rule_format]:
"x1 ∉ dom E1
--> SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td e (f, n) h' k v (δ, m, s)
--> x1 ∉ set xs
--> (∀ x ∈ set xs. size_dom (the (E1 x), h) ∧ size_dom (the (E1 x),h'))
--> (build_si E1 h xs) = (build_si (E1(x1 \<mapsto> v1)) h' xs)"
apply (rule impI)
apply (induct xs,simp_all)
apply (intro impI)
apply (drule mp,simp)+
apply (elim conjE)
by (rule sizeEnv_equals_h_h',assumption+)
lemma P_Δ_Let:
"[| set (R_Args Σt f) ∪ {ρself_f f} = dom Δ1; defined_AbstractDelta Δ1 f;
set (R_Args Σt f) ∪ {ρself_f f} = dom Δ2; defined_AbstractDelta Δ2 f;
dom Δ1 +Δ Δ2 = dom η;
Delta_ge Δ1 (build_si E1 h (varsAPP Σd f)) k η δ1;
Delta_ge Δ2 (build_si E1 h (varsAPP Σd f)) k η δ2 |]
==> Delta_ge Δ1 +Δ Δ2 (build_si E1 h (varsAPP Σd f)) k η (δ1 ⊕ δ2)"
apply (unfold Delta_ge_def)
apply (rule ballI)
apply (subst sizeAbstractDelta_si_addf,simp,simp,simp,simp,simp)
apply (erule_tac x=j in ballE)
prefer 2 apply simp
apply (erule_tac x=j in ballE)
prefer 2 apply simp
apply (simp add: addDelta_def)
apply (rule conjI)
apply (rule impI)
apply (rule conjI)
apply (rule impI,clarsimp)
apply (rule impI)
apply (subgoal_tac "0 ≤ sizeAbstractDelta_si Δ1 (build_si E1 h (varsAPP Σd f)) j η",simp)
apply (rule sizeAbstractDelta_si_nonneg)
apply (subst (asm) dom_addAbstractDelta,simp)
apply (rule wellFormed_Δ)
apply (rule impI)
apply (rule conjI)
apply (rule impI)
apply (subgoal_tac "0 ≤ sizeAbstractDelta_si Δ2 (build_si E1 h (varsAPP Σd f)) j η",simp)
apply (rule sizeAbstractDelta_si_nonneg)
apply (subst (asm) dom_addAbstractDelta,simp)
apply (rule wellFormed_Δ)
apply (rule impI)
apply (subgoal_tac "0 ≤ sizeAbstractDelta_si Δ2 (build_si E1 h (varsAPP Σd f)) j η")
apply (subgoal_tac "0 ≤ sizeAbstractDelta_si Δ1 (build_si E1 h (varsAPP Σd f)) j η")
apply clarsimp
apply (rule sizeAbstractDelta_si_nonneg)
apply (subst (asm) dom_addAbstractDelta,simp)
apply (rule wellFormed_Δ)
apply (rule sizeAbstractDelta_si_nonneg)
apply (subst (asm) dom_addAbstractDelta,simp)
by (rule wellFormed_Δ)
axioms sizeAbstractDelta_Δ1_ge_balanceCells_δ1:
"Delta_ge Δ1 si k η δ1
==> the (sizeAbstractDelta Δ1 si) ≥
SafeRASemanticsReal.balanceCells δ1"
lemma defined_AbstractDelta_si_in_dom_Δ1:
"defined_bound |Δ1| f
==> build_si E1 h (varsAPP Σd f) ∈ dom |Δ1|"
apply (simp add: defined_bound_def)
apply (erule_tac x="build_si E1 h (varsAPP Σd f)" in allE)
by (subst (asm) length_build_si,simp)
lemma P_μ_Let:
"[| Delta_ge Δ1 (build_si E1 h (varsAPP Σd f)) k η δ1;
defined_AbstractDelta Δ1 f; defined_bound |Δ1| f;
mu_ge μ1 (build_si E1 h (varsAPP Σd f)) m1; defined_bound μ1 f;
mu_ge μ2 (build_si E1 h (varsAPP Σd f)) m2; defined_bound μ2 f |]
==> mu_ge \<Squnion>c { μ1 , |Δ1| +c μ2 } (build_si E1 h (varsAPP Σd f)) (max m1 (m2 + SafeRASemanticsReal.balanceCells δ1))"
apply (simp add: mu_ge_def)
apply (rule conjI)
apply (simp add: maxCost_def)
apply (rule conjI)
apply (rule impI)
apply (simp add: maxCost_def)
apply (rule impI)+
apply (simp add: defined_bound_def [where b=μ1])
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (simp add: defined_bound_def [where b=μ2])
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (frule_tac ?E1.0=E1 and h=h in defined_AbstractDelta_si_in_dom_Δ1)
apply (simp add: addCost_def)
apply (simp add: dom_def)
apply (frule sizeAbstractDelta_Δ1_ge_balanceCells_δ1)
apply (simp add: maxCost_def)
apply (rule conjI,rule impI)
apply (simp add: addCost_def)
apply (rule conjI,rule impI)
apply (frule sizeAbstractDelta_Δ1_ge_balanceCells_δ1,simp)
apply (rule impI)
apply (simp add: defined_bound_def [where b=μ1])
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (simp add: defined_bound_def [where b=μ2])
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (frule_tac ?E1.0=E1 and h=h in defined_AbstractDelta_si_in_dom_Δ1)
apply simp
apply (rule impI)
apply (simp add: addCost_def)
apply (simp add: defined_bound_def [where b=μ1])
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (simp add: defined_bound_def [where b=μ2])
apply (subst (asm) length_build_si,simp)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (frule_tac ?E1.0=E1 and h=h in defined_AbstractDelta_si_in_dom_Δ1)
by (simp add: dom_def)
lemma P_σ_Let:
"[| sigma_ge σ1 (build_si E1 h (varsAPP Σd f)) s1; defined_bound σ1 f;
sigma_ge σ2 (build_si E1 h (varsAPP Σd f)) s2; defined_bound σ2 f |]
==> sigma_ge \<Squnion>c { []2 +c σ1 , []1 +c σ2 } (build_si E1 h (varsAPP Σd f)) (max (s1 + 2) (s2 + 1))"
apply (simp add: sigma_ge_def)
apply (rule conjI)
apply (simp add: maxCost_def)
apply (rule conjI)
apply (rule impI)
apply (simp add: constantCost_def)
apply (simp add: addCost_def)
apply (rule conjI)
apply (rule impI)+
apply (rule conjI)
apply (rule impI,simp)
apply (rule impI)
apply (simp add: defined_bound_def)
apply (rule impI)
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply clarsimp
apply (rule impI)+
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (simp add: constantCost_def)
apply (simp add: addCost_def)
apply (simp add: dom_def)
apply (simp add: maxCost_def)
apply (rule conjI)
apply (rule impI)
apply (simp add: constantCost_def)
apply (simp add: addCost_def)
apply (rule conjI)
apply (rule impI)+
apply (rule conjI)
apply (rule impI,simp)
apply (rule impI)
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply clarsimp
apply (rule impI)+
apply (rule conjI)
apply (rule impI)
apply (simp add: defined_bound_def)
apply (rule impI)+
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply clarsimp
apply (rule impI)+
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (simp add: constantCost_def)
apply (simp add: addCost_def)
by (simp add: dom_def)
lemma SafeResourcesDADepth_Let1:
"[| ∀C as r a'. e1 ≠ ConstrE C as r a';
x1 ∉ fv e1;
x1 ∉ set (varsAPP Σd f);
e1 :f (ϑ1, ϑ2) Φ 0, n \<lbrace>Δ1, μ1, σ1\<rbrace>;
defined_AbstractDelta Δ1 f; defined_bound |Δ1| f;
defined_bound μ1 f; defined_bound σ1 f;
e2 :f (ϑ1, ϑ2) Φ (td+1), n \<lbrace>Δ2, μ2, σ2\<rbrace>;
defined_AbstractDelta Δ2 f; defined_bound μ2 f; defined_bound σ2 f;
Δ = Δ1 +Δ Δ2;
μ = \<Squnion>c {μ1, |Δ1| +c μ2};
σ = \<Squnion>c {[]2 +c σ1,
[]1 +c σ2} |]
==> Let x1 = e1 In e2 a :f (ϑ1, ϑ2) Φ td, n \<lbrace> Δ, μ , σ \<rbrace>"
apply (simp only: SafeResourcesDAssDepth.simps)
(* Assuming valid_f for let,
we have valid_f for both e1 and e2 *)
apply (rule impI)
apply (drule mp, simp)
apply (drule mp, simp)
(* We get P_static for e1 and e2 *)
apply (elim conjE)
(* 2. P_static for Let *)
(* 2. P_static_dom_Δ for Let *)
apply (rule conjI)
apply (rule P_static_dom_Δ_Let,simp,simp)
(* 3. Assuming P\<Down>(f,n) for let, and using the
semantic rule Let, we get P\<Down>(f,n) for
e1 and e2 and appropiate heaps and
runtime environments *)
apply (intro allI, rule impI)
apply (elim conjE)
apply (frule P1_f_n_LET,simp)
apply (elim exE)
(* P\<Down>(f,n) for e1 *)
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=v1 in allE)
apply (erule_tac x=δ1 in allE)
apply (erule_tac x=m1 in allE)
apply (erule_tac x=s1 in allE)
apply (erule_tac x=η in allE)
apply (erule_tac x=si in allE)
apply (drule mp)
apply (rule conjI,simp)
(* 4.1. Assuming P_dyn, P_size and P_η for Let,
we get P_dyn, P_size and P_η for e1 *)
apply (rule conjI, rule P_dyn_dom_E1_Let_e1, assumption+)
apply (rule conjI, simp)
apply (rule conjI, frule P_dyn_dom_Δ_Let_e1,simp,simp,simp)
apply (rule conjI, simp)
apply simp
(* P\<Down>(f,n) for e2 *)
apply (erule_tac x="E1(x1 \<mapsto> v1)" 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=v2 in allE)
apply (erule_tac x=δ2 in allE)
apply (erule_tac x=m2 in allE)
apply (erule_tac x=s2 in allE)
apply (erule_tac x=η in allE)
apply (erule_tac x="build_si (E1(x1 \<mapsto> v1)) h' (varsAPP Σd f)" in allE)
apply (drule mp)
apply (rule conjI,simp)
(* 4.2. Assuming P_dyn, P_size and P_η for Let,
we get P_dyn, P_size and P_η for e2 *)
apply (rule conjI, rule P_dyn_dom_E1_Let_e2, assumption+)
apply (rule conjI, simp)
apply (rule conjI, frule P_dyn_dom_Δ_Let_e2, simp,simp,simp)
apply (rule conjI, simp)
apply simp
(* 5. We get P_Δ, P_μ and P_σ for
the bound (Δ1,μ1,σ1) w.r.t (δ1,m1,s1) of e1 and
the bound (Δ2,μ2,σ2) w.r.t (δ2,m2,s2) of e2 *)
(* sizes are equals *)
apply (subgoal_tac "(∀ x ∈ set (varsAPP Σd f). size_dom (the (E1 x), h) ∧
size_dom (the (E1 x),h'))")
prefer 2 apply (insert axiom_size_dom,force)
apply (subgoal_tac
"build_si E1 h (varsAPP Σd f) =
build_si (E1(x1 \<mapsto> v1)) h' (varsAPP Σd f)")
prefer 2 apply (rule build_si_equals_h_h', simp,force,assumption+, simp,simp)
(* 6.1. (Δ1 +Δ Δ2) is bound for (δ1 ⊕ δ2) *)
apply (rule conjI)
apply (rule P_Δ_Let)
apply (simp,simp,simp,simp,simp,simp,simp)
(* 6.2. \<Squnion>{μ1,|Δ1|+μ2) is bound for \<Squnion>{m1,|δ1|+m2} *)
apply (rule conjI,rule P_μ_Let)
apply (force,simp,simp,simp,simp,simp,simp)
(* 6.3. \<Squnion>{2+σ1,1+σ2) is bound for \<Squnion>{2+s1,1+s2} *)
apply (rule P_σ_Let)
by (simp,simp,simp,simp)
(********** Let x1 = ConstrE C as r a' ***********)
axioms SafeResourcesDADepth_Let2:
"[| ϑ2 r = Some ρ; ρ ∉ dom Δ;
e2 :f (ϑ1, ϑ2) φ td, n \<lbrace>Δ, μ, σ\<rbrace> |]
==>Let x1 = ConstrE C as r a' In e2 a :f (ϑ1, ϑ2) φ td, n \<lbrace>Δ ++ [ρ \<mapsto> []1], μ +c []1, σ2 +c []1\<rbrace>"
(********** Case (VarE x a) Of alts a' ***********)
lemma dom_maxCost:
"dom (maxCost c1 c2) = dom c1 ∩ dom c2"
apply (rule equalityI)
apply (rule subsetI)
apply (simp add: maxCost_def,clarsimp)
apply (split split_if_asm,simp)
apply (simp add: maxCost_def)
apply (rule subsetI)
apply (simp add: maxCost_def,clarsimp)
apply (simp add: dom_def)
done
lemma dom_maxAbstractDelta:
"dom (maxAbstractDelta c1 c2) = dom c1 ∩ dom c2"
apply (rule equalityI)
apply (rule subsetI)
apply (simp add: maxAbstractDelta_def,clarsimp)
apply (split split_if_asm,simp,simp)
apply (rule subsetI)
apply (simp add: maxAbstractDelta_def)
by (clarsimp,simp add: dom_def)
lemma dom_maxCostList:
"dom (foldr maxCost (map AbstractMuSpaceCost xs) []0) =
(\<Inter> i < length xs. dom (AbstractMuSpaceCost (xs! i)))"
apply (induct xs)
apply (simp add: constantCost_def,force)
apply clarsimp
apply (simp add: maxCost_def)
apply (rule equalityI)
apply (rule subsetI,simp)
apply (rule ballI,clarsimp)
apply (split split_if_asm,simp)
apply (case_tac i)
apply (simp add: dom_def)
apply simp
apply (erule_tac x=nat in ballE)
apply (simp add: dom_def)
apply simp
apply simp
apply clarsimp
apply (rule conjI)
apply force
by force
lemma P_static_dom_Δ_Case [rule_format]:
"length xs > 0
--> (∀i<length xs.
insert (ρself_f f) (set (R_Args Σt f)) = dom (AbstractDeltaSpaceCost (xs ! i)) )
--> insert (ρself_f f) (set (R_Args Σt f)) = dom \<Squnion>Δ f map AbstractDeltaSpaceCost xs"
apply (simp add: maxAbstractDeltaList_def)
apply (induct xs,clarsimp,clarsimp)
apply (subst dom_maxAbstractDelta)
apply (case_tac xs)
apply (simp add: maxAbstractDelta_def)
apply (subst dom_emptyAbstractDelta,simp)
apply (subgoal_tac "dom a = insert (ρself_f f) (set (R_Args Σt f))")
prefer 2 apply (erule_tac x=0 in allE,simp)
apply clarsimp
apply (drule mp)
apply (rule allI,rule impI)
apply (erule_tac x="Suc i" in allE,simp)
by simp
lemma P_dyn_dom_E1_Case_ej:
"[| set (varsAPP Σd f) ⊆ dom E1;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs |]
==> set (varsAPP Σd f) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)"
apply (simp add: extend_def)
apply (simp add: def_extend_def)
by blast
lemma P_dyn_fv_dom_E1_Case_ej [rule_format]:
" fvAlts alts ⊆ dom E1
--> i < length alts
--> def_extend E1 (snd (extractP (fst (alts ! i)))) vs
--> fv (snd (alts ! i)) ⊆ dom (extend E1 (snd (extractP (fst (alts ! i)))) vs)"
apply (induct alts arbitrary: i ,simp_all)
apply (rule impI)+
apply (elim conjE)
apply (case_tac "alts = []",simp_all)
apply (simp add: def_extend_def)
apply (case_tac a, simp_all)
apply (elim conjE)
apply (simp add: extend_def)
apply blast
apply (case_tac i,simp_all)
apply (case_tac a, simp_all)
apply (simp add: def_extend_def)
apply (simp add: extend_def)
apply (case_tac aa,simp_all)
apply (simp add: Let_def)
by blast
lemma P_dyn_fvReg_dom_E2_Case_ej:
"[| fvAltsReg alts ⊆ dom E2; i < length alts |]
==> fvReg (snd (alts ! i)) ⊆ dom E2"
apply (induct alts arbitrary: i,simp_all)
apply (case_tac i,simp)
by (case_tac a, simp_all)
lemma P_dyn_fv_dom_E1_Case_LitN_ej [rule_format]:
"fvAlts alts ⊆ dom E1
--> i < length alts
--> fst (alts ! i) = ConstP (LitN n)
--> fv (snd (alts ! i)) ⊆ dom E1"
apply (induct alts arbitrary: i ,simp_all)
apply (rule impI)+
apply (elim conjE)
apply (case_tac "alts = []",simp_all)
apply (case_tac a, simp_all)
apply (case_tac i,simp_all)
by (case_tac a, simp_all)
lemma P_dyn_fv_dom_E1_Case_LitB_ej [rule_format]:
"fvAlts alts ⊆ dom E1
--> i < length alts
--> fst (alts ! i) = ConstP (LitB b)
--> fv (snd (alts ! i)) ⊆ dom E1"
apply (induct alts arbitrary: i ,simp_all)
apply (rule impI)+
apply (elim conjE)
apply (case_tac "alts = []",simp_all)
apply (case_tac a, simp_all)
apply (case_tac i,simp_all)
by (case_tac a, simp_all)
(* Properties for sizeEnv *)
lemma si_in_dom_AbstractDeltaSpaceCost:
"[| defined_AbstractDelta (AbstractDeltaSpaceCost x) f; ρ ∈ dom (AbstractDeltaSpaceCost x) |]
==> build_si E1 h (varsAPP Σd f) ∈ dom (the (AbstractDeltaSpaceCost x ρ))"
apply (simp add: defined_AbstractDelta_def)
apply (erule_tac x=ρ in ballE)
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
by simp
lemma si_in_dom_emptyAbstractDelta:
"ρ ∈ dom []f
==> build_si E1 h (varsAPP Σd f) ∈ dom (the ([]f ρ))"
apply (simp add: emptyAbstractDelta_def, clarsimp)
apply (split split_if_asm)
apply clarsimp
apply (rule conjI)
apply (simp add: constantCost_def,force)
apply (rule conjI)
apply (simp add: constantCost_def,force)
apply force
by simp
lemma defined_AbstracDelta_imp_defined_bound:
"[| (∀i<length assert.
insert (ρself_f f) (set (R_Args Σt f)) = dom (AbstractDeltaSpaceCost (assert ! i)) );
ρ ∈ insert (ρself_f f) (set (R_Args Σt f));
(∀ i < length assert. defined_AbstractDelta (AbstractDeltaSpaceCost (assert ! i)) f) |]
==> (∀ i < length assert. defined_bound (the (AbstractDeltaSpaceCost (assert ! i) ρ)) f) "
apply (rule allI,rule impI)
apply (erule_tac x=i in allE,simp)
apply (simp only: defined_AbstractDelta_def)
done
lemma all_i_defined_bound_all_si_in_dom_Delta:
"(∀ i < length xs. defined_bound (the (AbstractDeltaSpaceCost (xs ! i) ρ)) f)
==> ∀ i < length xs. build_si E1 h (varsAPP Σd f) ∈ dom (the (AbstractDeltaSpaceCost (xs ! i) ρ))"
apply (rule allI,rule impI)
apply (erule_tac x=i in allE,simp)
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si)
by simp
lemma all_i_si_in_Delta_si_in_dom_maxCost_Delta:
"∀ i < length xs. build_si E1 h (varsAPP Σd f) ∈ dom (the (AbstractDeltaSpaceCost (xs ! i) ρ))
==> build_si E1 h (varsAPP Σd f) ∈ (\<Inter> i < length xs. dom (the (AbstractDeltaSpaceCost (xs ! i) ρ)))"
by (induct xs,simp,simp)
lemma dom_maxCostDeltaList [rule_format]:
"ρ ∈ insert (ρself_f f) (set (R_Args Σt f))
--> ρ ∈ dom (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f)
--> dom (the (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f ρ)) =
(\<Inter> i < length xs. dom (the (AbstractDeltaSpaceCost (xs ! i) ρ)))"
apply (rule impI)
apply (induct xs)
apply (simp add: emptyAbstractDelta_def)
apply (simp add: constantCost_def)
apply force
apply clarsimp
apply (rule equalityI)
apply (rule subsetI,simp)
apply (rule ballI,clarsimp)
apply (case_tac i)
apply (simp add: maxAbstractDelta_def)
apply (split split_if_asm)
apply (simp add: maxCost_def)
apply clarsimp
apply (split split_if_asm)
apply (simp add: dom_def)
apply simp
apply simp
apply clarsimp
apply (simp add: maxAbstractDelta_def)
apply (split split_if_asm)
apply (simp add: maxCost_def)
apply clarsimp
apply (split split_if_asm)
apply (erule_tac x=nat in ballE)
apply (simp add: dom_def)
apply simp
apply simp
apply simp
apply (rule subsetI,simp)
apply (simp add: maxAbstractDelta_def)
apply (split split_if_asm)
apply (simp add: maxCost_def)
apply clarsimp
apply (rule conjI)
apply (simp add: dom_def)
apply force
apply (rule ballI)
apply (erule_tac x="Suc i" in ballE)
apply simp
apply simp
by simp
lemma si_dom_Delta_si_dom_maxCost_Delta:
"[| ρ ∈ insert (ρself_f f) (set (R_Args Σt f));
ρ ∈ dom (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f);
∀ i < length xs. build_si E1 h (varsAPP Σd f) ∈ dom (the (AbstractDeltaSpaceCost (xs ! i) ρ)) |]
==> build_si E1 h (varsAPP Σd f) ∈ dom (the (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f ρ))"
apply (frule all_i_si_in_Delta_si_in_dom_maxCost_Delta)
by (subst dom_maxCostDeltaList,simp,simp,simp)
lemma ρ_in_dom_AbstractDeltaSpaceCost:
"[| ρ ∈ insert (ρself_f f) (set (R_Args Σt f));
ρ ∈ dom (maxAbstractDelta (AbstractDeltaSpaceCost x) (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f)) |]
==> ρ ∈ dom (AbstractDeltaSpaceCost x) ∧ ρ ∈ dom (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f)"
apply (simp add: maxAbstractDelta_def,clarsimp)
by (split split_if_asm,simp,simp)
lemma si_in_dom_AbstractDeltaSpaceCost:
"[| ρ ∈ insert (ρself_f f) (set (R_Args Σt f));
si ∈ dom (the (maxAbstractDelta (AbstractDeltaSpaceCost x) (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f) ρ));
ρ ∈ dom (maxAbstractDelta (AbstractDeltaSpaceCost x) (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f)) |]
==> si ∈ dom (the (AbstractDeltaSpaceCost x ρ)) ∩
dom (the (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f ρ))"
apply (frule ρ_in_dom_AbstractDeltaSpaceCost,simp,clarsimp)
apply (simp add: maxAbstractDelta_def)
apply (split split_if_asm)
apply (simp add: maxCost_def,clarsimp)
apply (split split_if_asm,simp,simp)
by simp
lemma maxAbstractDeltaSpaceCost_ge_AbstractDeltaSpaceCost [rule_format]:
"i < length assert
--> ρ ∈ insert (ρself_f f) (set (R_Args Σt f))
--> ρ ∈ dom (foldr maxAbstractDelta (map AbstractDeltaSpaceCost assert) []f)
--> build_si E1 h (varsAPP Σd f) ∈ dom (the (foldr maxAbstractDelta (map AbstractDeltaSpaceCost assert) []f ρ))
--> the (the (AbstractDeltaSpaceCost (assert ! i) ρ) (build_si E1 h (varsAPP Σd f)))
≤ the (the (\<Squnion>Δ f map AbstractDeltaSpaceCost assert ρ) (build_si E1 h (varsAPP Σd f)))"
apply (rule impI)
apply (induct assert i rule: list_induct3,simp_all)
apply (rule conjI)
apply (rule impI)+
apply (simp only: maxAbstractDeltaList_def)
apply (simp (no_asm) add: maxAbstractDelta_def)
apply (rule conjI)
apply (rule impI)
apply (simp add: maxCost_def)
apply (rule impI)+
apply (subgoal_tac
"build_si E1 h (varsAPP Σd f) ∈
dom (the (AbstractDeltaSpaceCost x (ρself_f f))) ∩
dom (the (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f (ρself_f f)))", simp)
apply (rule si_in_dom_AbstractDeltaSpaceCost,simp,simp,simp)
apply (rule impI)+
apply (subgoal_tac "ρself_f f ∈ dom (AbstractDeltaSpaceCost x) ∧
ρself_f f ∈ dom (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f)",simp)
apply (rule ρ_in_dom_AbstractDeltaSpaceCost,simp,simp)
apply (rule impI)+
apply (simp only: maxAbstractDeltaList_def)
apply (simp (no_asm) add: maxAbstractDelta_def)
apply (rule conjI)
apply (rule impI)
apply (simp add: maxCost_def)
apply (rule impI)+
apply (subgoal_tac "build_si E1 h (varsAPP Σd f) ∈ dom (the (AbstractDeltaSpaceCost x ρ)) ∩
dom (the (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f ρ))", simp)
apply (rule si_in_dom_AbstractDeltaSpaceCost,simp,force,simp)
apply (rule impI)+
apply (subgoal_tac "ρ ∈ dom (AbstractDeltaSpaceCost x) ∧
ρ ∈ dom (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f)",simp)
apply (rule ρ_in_dom_AbstractDeltaSpaceCost,simp,simp)
apply (rule conjI)
apply (rule impI)+
apply clarsimp
apply (simp only: maxAbstractDeltaList_def)
apply (simp (no_asm) add: maxAbstractDelta_def)
apply (rule conjI)
apply (rule impI)
apply (simp add: maxCost_def)
apply (rule conjI)
apply (rule impI)+
apply simp
apply (rule impI)+
apply (simp add: maxAbstractDelta_def)
apply (simp add: maxCost_def)
apply clarsimp
apply (split split_if_asm,simp,simp)
apply (rule impI)+
apply (simp add: maxAbstractDelta_def)
apply (split split_if_asm,simp,simp)
apply clarsimp
apply (simp only: maxAbstractDeltaList_def)
apply (simp (no_asm) add: maxAbstractDelta_def)
apply (rule conjI)
apply (rule impI)
apply (simp add: maxCost_def)
apply (rule conjI)
apply (rule impI)+
apply simp
apply (rule impI)+
apply (simp add: maxAbstractDelta_def)
apply (simp add: maxCost_def)
apply clarsimp
apply (split split_if_asm,simp,simp)
apply (rule impI)+
apply (simp add: maxAbstractDelta_def)
by (split split_if_asm,simp,simp)
lemma all_i_defined_bound_all_si_in_dom_mu:
"∀ i < length xs. defined_bound (AbstractMuSpaceCost (xs! i)) f
==> ∀ i < length xs. build_si E1 h (varsAPP Σd f) ∈ dom (AbstractMuSpaceCost (xs! i))"
apply (rule allI,rule impI)
apply (erule_tac x=i in allE,simp)
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si)
by simp
lemma all_i_si_in_dom_mu_si_in_dom_maxCost_mu:
"∀ i < length xs. build_si E1 h (varsAPP Σd f) ∈ dom (AbstractMuSpaceCost (xs! i))
==> build_si E1 h (varsAPP Σd f) ∈ (\<Inter> i < length xs. dom (AbstractMuSpaceCost (xs! i)))"
by (induct xs,simp,simp)
lemma si_dom_mu_si_dom_maxCost_mu:
"∀ i < length xs. build_si E1 h (varsAPP Σd f) ∈ dom (AbstractMuSpaceCost (xs! i))
==> build_si E1 h (varsAPP Σd f) ∈ dom (foldr maxCost (map AbstractMuSpaceCost xs) []0)"
apply (frule all_i_si_in_dom_mu_si_in_dom_maxCost_mu)
by (subst dom_maxCostList,simp)
lemma maxAbstractMuSpaceCost_ge_AbstractMuSpaceCost [rule_format]:
"i < length assert
--> (∀ i < length assert. defined_bound (AbstractMuSpaceCost (assert ! i)) f)
--> the (AbstractMuSpaceCost (assert ! i) (build_si E1 h (varsAPP Σd f)))
≤ the (\<Squnion>c map AbstractMuSpaceCost assert (build_si E1 h (varsAPP Σd f)))"
apply (rule impI)
apply (simp add: maxCostList_def)
apply (induct assert i rule: list_induct3, simp_all)
apply (case_tac xs,simp)
apply (rule impI)
apply (simp only: maxCost_def)
apply (simp (no_asm) add: maxCost_def)
apply (simp add: constantCost_def)
apply (simp add: dom_def)
apply clarsimp
apply (simp add: maxCost_def)
apply (rule impI)+
apply (drule mp)
apply (erule_tac x=0 in allE,simp)
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply clarsimp
apply (rule conjI)
apply (erule_tac x="Suc 0" in allE,simp)
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (rule si_dom_mu_si_dom_maxCost_mu)
apply (rule all_i_defined_bound_all_si_in_dom_mu,force)
apply (rule impI,clarsimp)
apply (drule mp)
apply force
apply (simp add: maxCost_def)
apply (rule conjI)
apply (rule impI)+
apply simp
apply (rule impI)+
apply (drule mp)
apply (erule_tac x="0" in allE,simp)
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (subgoal_tac
"build_si E1 h (varsAPP Σd f) ∈ dom (foldr maxCost (map AbstractMuSpaceCost xs) []0)",simp)
apply (rule si_dom_mu_si_dom_maxCost_mu)
apply (rule all_i_defined_bound_all_si_in_dom_mu)
by force
lemma sizeAbstractDelta_si_case_Lit_ge_sizeAbstracDelta_si_alt:
"[| i < length assert;
insert (ρself_f f) (set (R_Args Σt f)) = dom \<Squnion>Δ f map AbstractDeltaSpaceCost assert;
(∀i<length assert.
insert (ρself_f f) (set (R_Args Σt f)) = dom (AbstractDeltaSpaceCost (assert ! i)) );
(∀ i < length assert. defined_AbstractDelta (AbstractDeltaSpaceCost (assert ! i)) f);
insert (ρself_f f) (set (R_Args Σt f)) = dom η |]
==> sizeAbstractDelta_si (AbstractDeltaSpaceCost (assert ! i)) (build_si E1 h (varsAPP Σd f)) j η
≤ sizeAbstractDelta_si \<Squnion>Δ f map AbstractDeltaSpaceCost assert (build_si E1 h (varsAPP Σd f)) j η"
apply (simp (no_asm) only: sizeAbstractDelta_si_def)
apply (rule setsum_mono)
apply (subgoal_tac "ρ ∈ insert (ρself_f f) (set (R_Args Σt f))")
prefer 2 apply (simp add: dom_def,blast)
apply (rule maxAbstractDeltaSpaceCost_ge_AbstractDeltaSpaceCost,simp,simp)
apply (simp add: maxAbstractDeltaList_def)
apply (subst dom_maxCostDeltaList,simp)
apply (simp add: maxAbstractDeltaList_def)
apply (rule all_i_si_in_Delta_si_in_dom_maxCost_Delta)
apply (rule all_i_defined_bound_all_si_in_dom_Delta)
apply (frule defined_AbstracDelta_imp_defined_bound,simp,simp)
by simp
lemma P_Δ_Case_Lit:
"[| i < length assert;
insert (ρself_f f) (set (R_Args Σt f)) = dom \<Squnion>Δ f map AbstractDeltaSpaceCost assert;
∀i<length assert. insert (ρself_f f) (set (R_Args Σt f)) = dom (AbstractDeltaSpaceCost (assert ! i));
∀i<length assert. defined_AbstractDelta (AbstractDeltaSpaceCost (assert ! i)) f;
insert (ρself_f f) (set (R_Args Σt f)) = dom η;
Delta_ge (AbstractDeltaSpaceCost (assert ! i)) (build_si E1 h (varsAPP Σd f)) k η δ |]
==> Delta_ge \<Squnion>Δ f map AbstractDeltaSpaceCost assert (build_si E1 h (varsAPP Σd f)) k η δ"
apply (simp (no_asm) only: Delta_ge_def)
apply (rule ballI)
apply (frule_tac
?E1.0=E1 and h =h and j=j
in sizeAbstractDelta_si_case_Lit_ge_sizeAbstracDelta_si_alt, assumption+)
apply (simp add: Delta_ge_def)
by (erule_tac x=j in ballE,simp,simp)
lemma nth_build_si:
"i< length xs
==> build_si E1 h xs!i = sizeEnv E1 (xs!i) h"
apply (induct xs arbitrary:i, simp_all)
by (case_tac i,simp_all)
lemma sizeEnv_alt_equals_sizeEnv_Case:
"[| set (varsAPP Σd f) ⊆ dom E1; ia < length (varsAPP Σd f);
def_extend E1 (snd (extractP (fst (alts ! i)))) vs |]
==> sizeEnv (extend E1 (snd (extractP (fst (alts ! i)))) vs) (varsAPP Σd f ! ia) h = sizeEnv E1 (varsAPP Σd f ! ia) h"
apply (subgoal_tac
"extend E1 (snd (extractP (fst (alts ! i)))) vs (varsAPP Σd f ! ia) =
E1 (varsAPP Σd f ! ia)")
apply (simp add: sizeEnv_def)
apply (simp add: def_extend_def)
apply (elim conjE)
apply (subgoal_tac "(varsAPP Σd f ! ia) ∉ set (snd (extractP (fst (alts ! i)))) ")
apply (rule sym)
apply (subst extend_monotone,simp,simp)
apply (subgoal_tac "varsAPP Σd f ! ia ∈ dom E1",blast)
by (subst (asm) set_conv_nth,blast)
lemma build_si_Case_ge_build_si_alt:
"[| set (varsAPP Σd f) ⊆ dom E1; ia < length (varsAPP Σd f);
def_extend E1 (snd (extractP (fst (alts ! i)))) vs |]
==> build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h (varsAPP Σd f) ! ia = build_si E1 h (varsAPP Σd f) ! ia"
apply (subst nth_build_si,simp)+
by (rule sizeEnv_alt_equals_sizeEnv_Case,assumption+)
lemma sizeEnv_alt_equals_sizeEnv_Case_2:
"[| x ∈ dom E1;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs |]
==> sizeEnv (extend E1 (snd (extractP (fst (alts ! i)))) vs) x h = sizeEnv E1 x h"
apply (subgoal_tac
"extend E1 (snd (extractP (fst (alts ! i)))) vs x =
E1 x")
apply (simp add: sizeEnv_def)
apply (simp add: def_extend_def)
apply (elim conjE)
apply (subgoal_tac "x ∉ set (snd (extractP (fst (alts ! i)))) ")
apply (rule sym)
apply (subst extend_monotone,simp,simp)
by blast
lemma build_si_Case_ge_build_si_alt_2 [rule_format]:
"set xs ⊆ dom E1
--> def_extend E1 (snd (extractP (fst (alts ! i)))) vs
--> build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h xs = build_si E1 h xs"
apply (induct_tac xs,simp_all)
apply clarsimp
by (rule sizeEnv_alt_equals_sizeEnv_Case_2,force,simp)
lemma list_ge_build_si_alt_build_si_Case:
"[| set (varsAPP Σd f) ⊆ dom E1;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs |]
==> list_ge (build_si E1 h (varsAPP Σd f)) (build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h (varsAPP Σd f))"
apply (simp add: list_ge_def,clarsimp)
apply (subst (asm) length_build_si)
apply (frule_tac ?E1.0=E1 and h=h in build_si_Case_ge_build_si_alt,assumption+)
by simp
lemma sizeAbstractDelta_si_Case_ge_sizeAbstractDelta_si_alt:
"[| i < length assert; set (varsAPP Σd f) ⊆ dom E1;
∀i<length assert. insert (ρself_f f) (set (R_Args Σt f)) = dom (AbstractDeltaSpaceCost (assert ! i));
(∀i<length assert.
insert (ρself_f f) (set (R_Args Σt f)) = dom (AbstractDeltaSpaceCost (assert ! i)) );
∀i<length assert. defined_AbstractDelta (AbstractDeltaSpaceCost (assert ! i)) f;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
monotonic_AbstractDelta (AbstractDeltaSpaceCost (assert ! i));
insert (ρself_f f) (set (R_Args Σt f)) = dom η |]
==> sizeAbstractDelta_si (AbstractDeltaSpaceCost (assert ! i)) (build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h (varsAPP Σd f)) j η
≤ sizeAbstractDelta_si (AbstractDeltaSpaceCost (assert ! i)) (build_si E1 h (varsAPP Σd f)) j η"
apply (simp (no_asm) only: sizeAbstractDelta_si_def)
apply (rule setsum_mono,clarsimp)
by (subst build_si_Case_ge_build_si_alt_2,simp,simp,simp)
lemma sizeAbstractDelta_si_Case_equals_sizeAbstractDelta_si_alt:
"[| i < length assert; set (varsAPP Σd f) ⊆ dom E1;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs |]
==> sizeAbstractDelta_si (AbstractDeltaSpaceCost (assert ! i)) (build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h (varsAPP Σd f)) j η
= sizeAbstractDelta_si (AbstractDeltaSpaceCost (assert ! i)) (build_si E1 h (varsAPP Σd f)) j η"
apply (simp (no_asm) only: sizeAbstractDelta_si_def)
by (subst build_si_Case_ge_build_si_alt_2,simp,simp,simp)
lemma P_Δ_Case:
"[| i < length assert;
insert (ρself_f f) (set (R_Args Σt f)) = dom \<Squnion>Δ f map AbstractDeltaSpaceCost assert;
∀i<length assert. insert (ρself_f f) (set (R_Args Σt f)) = dom (AbstractDeltaSpaceCost (assert ! i));
∀i<length assert. defined_AbstractDelta (AbstractDeltaSpaceCost (assert ! i)) f;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
insert (ρself_f f) (set (R_Args Σt f)) = dom η;
set (varsAPP Σd f) ⊆ dom E1;
insert (ρself_f f) (set (R_Args Σt f)) = dom η;
monotonic_AbstractDelta (AbstractDeltaSpaceCost (assert ! i));
Delta_ge (AbstractDeltaSpaceCost (assert ! i)) (build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h (varsAPP Σd f)) k η δ |]
==> Delta_ge \<Squnion>Δ f map AbstractDeltaSpaceCost assert (build_si E1 h (varsAPP Σd f)) k η δ"
apply (simp (no_asm) only: Delta_ge_def)
apply (rule ballI)
apply (frule_tac
?E1.0=E1 and h =h and j=j
in sizeAbstractDelta_si_case_Lit_ge_sizeAbstracDelta_si_alt, assumption+)
apply (subgoal_tac
" sizeAbstractDelta_si (AbstractDeltaSpaceCost (assert ! i)) (build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h (varsAPP Σd f)) j η =
sizeAbstractDelta_si (AbstractDeltaSpaceCost (assert ! i)) (build_si E1 h (varsAPP Σd f)) j η")
apply (simp add: Delta_ge_def)
apply (erule_tac x=j in ballE,simp,simp)
by (rule sizeAbstractDelta_si_Case_equals_sizeAbstractDelta_si_alt,assumption+)
lemma AbstractMuSpaceCost_Case_equals_AbstractMuSpaceCost_alt:
"[| set (varsAPP Σd f) ⊆ dom E1;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs |]
==> the (AbstractMuSpaceCost (assert ! i) (build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h (varsAPP Σd f)))
= the (AbstractMuSpaceCost (assert ! i) (build_si E1 h (varsAPP Σd f)))"
by (subst build_si_Case_ge_build_si_alt_2,simp,simp,simp)
lemma P_μ_Case:
"[| set (varsAPP Σd f) ⊆ dom E1;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
monotonic_bound (AbstractMuSpaceCost (assert ! i));
(∀ i < length assert. defined_bound (AbstractMuSpaceCost (assert ! i)) f);
i < length assert;
mu_ge (AbstractMuSpaceCost (assert ! i)) (build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h (varsAPP Σd f)) m |]
==> mu_ge \<Squnion>c map AbstractMuSpaceCost assert (build_si E1 h (varsAPP Σd f)) m"
apply (simp add: mu_ge_def)
apply (frule_tac
?E1.0=E1 and h =h
in maxAbstractMuSpaceCost_ge_AbstractMuSpaceCost,force)
apply (subgoal_tac
"the (AbstractMuSpaceCost (assert ! i) (build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h (varsAPP Σd f))) =
the (AbstractMuSpaceCost (assert ! i) (build_si E1 h (varsAPP Σd f)))")
apply force
by (rule AbstractMuSpaceCost_Case_equals_AbstractMuSpaceCost_alt,assumption,simp)
lemma P_μ_Case_Lit:
"[| (∀ i < length assert. defined_bound (AbstractMuSpaceCost (assert ! i)) f);
i < length assert;
mu_ge (AbstractMuSpaceCost (assert ! i)) (build_si E1 h (varsAPP Σd f)) m |]
==> mu_ge \<Squnion>c map AbstractMuSpaceCost assert (build_si E1 h (varsAPP Σd f)) m"
apply (simp add: mu_ge_def)
apply (subgoal_tac
"the (\<Squnion>c map AbstractMuSpaceCost assert (build_si E1 h (varsAPP Σd f))) ≥
the (AbstractMuSpaceCost (assert ! i) (build_si E1 h (varsAPP Σd f)))")
apply force
by (rule maxAbstractMuSpaceCost_ge_AbstractMuSpaceCost,assumption,simp)
lemma all_i_defined_bound_all_si_in_dom_sigma:
"∀ i < length xs. defined_bound (AbstractSigmaSpaceCost (xs! i)) f
==> ∀ i < length xs. build_si E1 h (varsAPP Σd f) ∈ dom (AbstractSigmaSpaceCost (xs! i))"
apply (rule allI,rule impI)
apply (erule_tac x=i in allE,simp)
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si)
by simp
lemma all_i_si_in_dom_sigma_si_in_dom_maxCost_sigma:
"∀ i < length xs. build_si E1 h (varsAPP Σd f) ∈ dom (AbstractSigmaSpaceCost (xs! i))
==> build_si E1 h (varsAPP Σd f) ∈ (\<Inter> i < length xs. dom (AbstractSigmaSpaceCost (xs! i)))"
by (induct xs,simp,simp)
lemma dom_maxCostSigmaList:
" length xs = length ys
--> dom (foldr maxCost (map (λ(x, y). addCostReal x y) (zip (map AbstractSigmaSpaceCost xs) (map num_r ys))) []0) =
(\<Inter> i < length xs. dom (AbstractSigmaSpaceCost (xs! i)))"
apply (induct xs ys rule:list_induct2',simp_all)
apply (simp add: constantCost_def)
apply force
apply clarsimp
apply (simp add: maxCost_def)
apply (rule equalityI)
apply (rule subsetI,simp)
apply (rule ballI,clarsimp)
apply (split split_if_asm,simp)
apply (case_tac i)
apply (simp add: dom_def)
apply (simp add: addCostReal_def)
apply clarsimp
apply (split split_if_asm)
apply clarsimp
apply simp
apply clarsimp
apply (erule_tac x=nat in ballE)
apply (simp add: dom_def)
apply simp
apply simp
apply clarsimp
apply (rule conjI)
apply (simp add:addCostReal_def)
apply force
by force
lemma si_dom_sigma_si_dom_maxCost_sigma:
"[| length xs = length ys;
∀ i < length xs. build_si E1 h (varsAPP Σd f) ∈ dom (AbstractSigmaSpaceCost (xs! i)) |]
==> build_si E1 h (varsAPP Σd f) ∈
dom (foldr maxCost (map (λ(x, y). addCostReal x y) (zip (map AbstractSigmaSpaceCost xs) (map num_r ys))) []0)"
apply (frule all_i_si_in_dom_sigma_si_in_dom_maxCost_sigma)
by (subst dom_maxCostSigmaList,simp)
lemma maxAbstractSigmaSpaceCost_ge_AbstractSigmaSpaceCost [rule_format]:
"length assert = length alts
--> (∀ i < length assert. defined_bound (AbstractSigmaSpaceCost (assert ! i)) f)
--> (∀ i < length assert. the (AbstractSigmaSpaceCost (assert ! i) (build_si E1 h (varsAPP Σd f)))
≤ the (\<Squnion>c map (λ(x, y). addCostReal x y) (zip (map AbstractSigmaSpaceCost assert) (map num_r alts)) (build_si E1 h (varsAPP Σd f))))"
apply (induct assert alts rule: list_induct2',simp_all)
apply clarsimp
apply (drule mp,force)
apply (simp add: maxCostList_def)
apply (simp add: maxCost_def)
apply (rule conjI)
apply (rule impI,clarsimp)
apply (case_tac i,simp)
apply (simp add: addCostReal_def)
apply (split split_if_asm,simp)
apply (subgoal_tac "num_r (ab,ba) >= 0",simp)
apply (simp add: num_r_def)
apply simp
apply simp
apply (erule_tac x=nat in allE,simp)
apply (erule_tac x=nat in allE,simp)
apply clarsimp
apply (drule mp)
apply (erule_tac x=0 in allE,simp)
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (simp add: addCostReal_def)
apply (simp add: dom_def)
apply (subgoal_tac
"build_si E1 h (varsAPP Σd f) ∈
dom (foldr maxCost (map (λ(x, y). addCostReal x y) (zip (map AbstractSigmaSpaceCost xs) (map num_r ys))) []0)",simp)
apply (rule si_dom_sigma_si_dom_maxCost_sigma,assumption+)
apply (rule all_i_defined_bound_all_si_in_dom_sigma)
by force
lemma maxAbstractSigmaSpaceCost_ge_AbstractSigmaSpaceCost_2 [rule_format]:
"length assert = length alts
--> (∀ i < length assert. defined_bound (AbstractSigmaSpaceCost (assert ! i)) f)
--> (∀ i < length assert. the (AbstractSigmaSpaceCost (assert ! i) (build_si E1 h (varsAPP Σd f))) + num_r (alts!i)
≤ the (\<Squnion>c map (λ(x, y). addCostReal x y) (zip (map AbstractSigmaSpaceCost assert) (map num_r alts)) (build_si E1 h (varsAPP Σd f))))"
apply (induct assert alts rule: list_induct2',simp_all)
apply clarsimp
apply (drule mp,force)
apply (simp add: maxCostList_def)
apply (simp add: maxCost_def)
apply (rule conjI)
apply (rule impI,clarsimp)
apply (case_tac i,simp)
apply (simp add: addCostReal_def)
apply (split split_if_asm,simp)
apply simp
apply force
apply clarsimp
apply (drule mp)
apply (erule_tac x=0 in allE,simp)
apply (simp add: defined_bound_def)
apply (erule_tac x=" build_si E1 h (varsAPP Σd f)" in allE)
apply (subst (asm) length_build_si,simp)
apply (simp add: addCostReal_def)
apply (simp add: dom_def)
apply (subgoal_tac
"build_si E1 h (varsAPP Σd f) ∈
dom (foldr maxCost (map (λ(x, y). addCostReal x y) (zip (map AbstractSigmaSpaceCost xs) (map num_r ys))) []0)",simp)
apply (rule si_dom_sigma_si_dom_maxCost_sigma,assumption+)
apply (rule all_i_defined_bound_all_si_in_dom_sigma)
by force
lemma P_σ_Case_Lit:
"[| i < length assert; length assert = length alts;
(∀ i < length assert. defined_bound (AbstractSigmaSpaceCost (assert ! i)) f);
sigma_ge (AbstractSigmaSpaceCost (assert ! i)) (build_si E1 h (varsAPP Σd f)) s |]
==> sigma_ge \<Squnion>c map (λ(x, y). addCostReal x y) (zip (map AbstractSigmaSpaceCost assert) (map num_r alts)) (build_si E1 h (varsAPP Σd f)) s"
apply (simp add: sigma_ge_def)
apply (subgoal_tac
"the (AbstractSigmaSpaceCost (assert ! i) (build_si E1 h (varsAPP Σd f)))
≤ the (\<Squnion>c map (λ(x, y). addCostReal x y) (zip (map AbstractSigmaSpaceCost assert) (map num_r alts)) (build_si E1 h (varsAPP Σd f)))")
apply force
apply (rule maxAbstractSigmaSpaceCost_ge_AbstractSigmaSpaceCost,assumption+, simp)
by simp
lemma AbstractSigmaSpaceCost_Case_equals_AbstractSigmaSpaceCost_alt:
"[| set (varsAPP Σd f) ⊆ dom E1;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs |]
==> the (AbstractSigmaSpaceCost (assert ! i) (build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h (varsAPP Σd f)))
= the (AbstractSigmaSpaceCost (assert ! i) (build_si E1 h (varsAPP Σd f)))"
by (subst build_si_Case_ge_build_si_alt_2,simp,simp,simp)
lemma P_σ_Case:
"[| i < length assert; length assert = length alts;
s = s' + nr; nr = real (length vs);
set (varsAPP Σd f) ⊆ dom E1;
def_extend E1 (snd (extractP (fst (alts ! i)))) vs;
(∀ i < length assert. defined_bound (AbstractSigmaSpaceCost (assert ! i)) f);
sigma_ge (AbstractSigmaSpaceCost (assert ! i)) (build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h (varsAPP Σd f)) s' |]
==> sigma_ge \<Squnion>c map (λ(x, y). addCostReal x y) (zip (map AbstractSigmaSpaceCost assert) (map num_r alts)) (build_si E1 h (varsAPP Σd f)) s"
apply (simp add: sigma_ge_def)
apply (frule_tac
?E1.0=E1 and h =h
in maxAbstractSigmaSpaceCost_ge_AbstractSigmaSpaceCost_2,force,simp)
apply (subgoal_tac "num_r (alts ! i) = real (length vs)")
apply (subgoal_tac
"the (AbstractSigmaSpaceCost (assert ! i) (build_si (extend E1 (snd (extractP (fst (alts ! i)))) vs) h (varsAPP Σd f))) =
the (AbstractSigmaSpaceCost (assert ! i) (build_si E1 h (varsAPP Σd f)))")
apply simp
apply (rule AbstractSigmaSpaceCost_Case_equals_AbstractSigmaSpaceCost_alt,assumption+)
apply (simp add: num_r_def)
by (simp add: def_extend_def)
lemma P1_f_n_CASE:
"[| E1 x = Some (Val.Loc p);
SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (Case VarE x () Of alts ()) (f, n) hh k v (δ, m, s)|]
==> ∃ j C vs nr s'.
h p = Some (j,C,vs) ∧
s = (s' + nr) ∧
nr = real (length vs) ∧
(∃ i < length alts.
def_extend E1 (snd (extractP (fst (alts ! i)))) vs
∧ SafeDepthSemanticsReal.SafeBoundSem (extend E1 (snd (extractP (fst (alts ! i)))) vs, E2) h k (td + nr) (snd (alts ! i))
(f, n) hh k v (δ, m, s'))"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
by force
lemma P1_f_n_CASE_1_1:
"[| E1 x = Some (IntT n');
SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (Case VarE x () Of alts ()) (f, n) hh k v (δ, m, s)|]
==> (∃ i < length alts.
(SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (snd (alts ! i)) (f, n) hh k v (δ, m, s))
∧ fst (alts ! i) = ConstP (LitN n'))"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
by force
lemma P1_f_n_CASE_1_2:
"[| E1 x = Some (BoolT b);
SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (Case VarE x () Of alts ()) (f, n) hh k v (δ, m, s)|]
==> (∃ i < length alts.
(SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (snd (alts ! i)) (f, n) hh k v (δ, m, s))
∧ fst (alts ! i) = ConstP (LitB b))"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
by force
lemma nr_Case:
"[| nr = real (length vs); def_extend E1 (snd (extractP (fst (alts ! i)))) vs |]
==> td + nr = td + num_r (alts!i)"
by (simp add: num_r_def, simp add: def_extend_def)
lemma SafeResourcesDADepth_CASE:
"[| 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) :f (ϑ1, ϑ2) φ (td+ real (length (snd (extractP (fst (alts ! i)))))), n \<lbrace>AbstractDeltaSpaceCost (assert!i),
AbstractMuSpaceCost (assert!i),
AbstractSigmaSpaceCost (assert!i)\<rbrace>;
Δ = \<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' :f (ϑ1, ϑ2) φ td, n \<lbrace>Δ,μ,σ\<rbrace>"
apply (simp only: SafeResourcesDAssDepth.simps)
(* Assuming valid_f for case,
we have valid_f for all ei *)
apply (rule impI)
apply (subgoal_tac "∀ i < length alts. valid Σd Σϑ ΣΦ")
prefer 2 apply simp
apply simp
(* 2. P_static for Case *)
(* 2. P_static_dom_Δ for Case *)
apply (rule conjI)
apply (rule P_static_dom_Δ_Case)
apply (simp,simp)
apply (intro allI, rule impI)
apply (elim conjE)
(* cases for E1 x *)
apply (case_tac "E1 x")
(* E1 x = None *)
apply (simp add: dom_def)
(* E1 x = Some x *)
apply (case_tac a)
apply (rename_tac p,simp)
(* 3. Assuming P\<Down>(f,n) for Case, and using the
semantic rule Case, we get P\<Down>(f,n) for
one ej, j ∈ {1..m} for appropiate heaps and
runtime environments *)
apply (frule P1_f_n_CASE,assumption)
apply (elim exE, elim conjE)
apply (elim exE, elim conjE)
apply (subgoal_tac
"insert (ρself_f f) (set (R_Args Σt f))
= dom \<Squnion>Δ f map AbstractDeltaSpaceCost assert")
prefer 2 apply (rule P_static_dom_Δ_Case,simp)
apply (rotate_tac 8)
apply (erule_tac x=ia in allE,simp)
apply (subgoal_tac
"∀i<length assert.
insert (ρself_f f) (set (R_Args Σt f)) = dom (AbstractDeltaSpaceCost (assert ! i))")
prefer 2 apply force
apply (rotate_tac 8)
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 30)
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 (rotate_tac 19)
apply (drule mp)
apply (rule conjI)
apply (subst (asm) nr_Case,assumption+)+
apply (simp add: num_r_def)
(* 4. Assuming P_dyn, P_size and P_η for Case,
we get P_dyn, P_size and P_η for ej *)
apply (rule conjI, rule P_dyn_dom_E1_Case_ej,assumption+)
apply (rule conjI, rule P_dyn_fv_dom_E1_Case_ej,assumption+)
apply (rule conjI, rule P_dyn_fvReg_dom_E2_Case_ej,assumption+)
apply (rule conjI, simp)
apply simp
(* 5. We get P_Δ, P_μ and P_σ for
the bound (Δj,μj,σj) w.r.t (δj,mj,sj) of ej's
evaluation *)
(* 5.1. \<Squnion>Δ (Δi) is bound for δj *)
apply (rule conjI, rule P_Δ_Case)
apply (simp,assumption+,force,assumption+,force,simp,simp)
(* 5.2. \<Squnion>μ (μi) is bound for mj *)
apply (rule conjI, rule P_μ_Case)
apply (simp,assumption+,force,assumption+,force,simp)
(* 5.3. \<Squnion>σ (σi + ni) is bound for (sj+nj) *)
apply (rule P_σ_Case)
apply (simp,simp,simp,force,simp,assumption+,simp)
(***** case for E1 x = IntT n *****)
(* 3. Assuming P\<Down>(f,n) for Case, and using the
semantic rule Case, we get P\<Down>(f,n) for
one ej, j ∈ {1..m} for appropiate heaps and
runtime environments *)
apply simp
apply (frule P1_f_n_CASE_1_1,assumption)
apply (elim exE, elim conjE)
apply (subgoal_tac
"insert (ρself_f f) (set (R_Args Σt f))
= dom \<Squnion>Δ f map AbstractDeltaSpaceCost assert")
prefer 2 apply (rule P_static_dom_Δ_Case,simp)
apply (rotate_tac 8)
apply (erule_tac x=ia in allE,simp)
apply (subgoal_tac
"∀i<length assert.
insert (ρself_f f) (set (R_Args Σt f)) = dom (AbstractDeltaSpaceCost (assert ! i))")
prefer 2 apply force
apply (rotate_tac 8)
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 27)
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 (rotate_tac 18)
apply (drule mp)
apply (rule conjI,simp)
(* 4. Assuming P_dyn, P_size and P_η for Case,
we get P_dyn, P_size and P_η for ej *)
apply (rule conjI,assumption)
apply (rule conjI, rule P_dyn_fv_dom_E1_Case_LitN_ej,assumption+)
apply (rule conjI, rule P_dyn_fvReg_dom_E2_Case_ej,assumption+)
apply (rule conjI,simp)
apply assumption
(* 5. We get P_Δ, P_μ and P_σ for
the bound (Δj,μj,σj) w.r.t (δj,mj,sj) of ej's
evaluation *)
(* 5.1. \<Squnion>Δ (Δi) is bound for δj *)
apply (rule conjI)
apply (rule P_Δ_Case_Lit,simp,assumption+,simp,simp)
(* 5.2. \<Squnion>μ (μi) is bound for mj *)
apply (rule conjI, rule P_μ_Case_Lit,force,force,force)
(* 5.3. \<Squnion>σ (σi + ni) is bound for (sj+nj) *)
apply (rule P_σ_Case_Lit,force,force,force,force)
(***** case for E1 x = BoolT b *****)
(* 3. Assuming P\<Down>(f,n) for Case, and using the
semantic rule Case, we get P\<Down>(f,n) for
one ej, j ∈ {1..m} for appropiate heaps and
runtime environments *)
apply simp
apply (frule P1_f_n_CASE_1_2,assumption)
apply (elim exE, elim conjE)
apply (subgoal_tac
"insert (ρself_f f) (set (R_Args Σt f))
= dom \<Squnion>Δ f map AbstractDeltaSpaceCost assert")
prefer 2 apply (rule P_static_dom_Δ_Case,simp)
apply (rotate_tac 8)
apply (erule_tac x=ia in allE,simp)
apply (subgoal_tac
"∀i<length assert.
insert (ρself_f f) (set (R_Args Σt f)) = dom (AbstractDeltaSpaceCost (assert ! i))")
prefer 2 apply force
apply (rotate_tac 8)
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 27)
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 (rotate_tac 18)
apply (drule mp)
apply (rule conjI,simp)
(* 4. Assuming P_dyn, P_size and P_η for Case,
we get P_dyn, P_size and P_η for ej *)
apply (rule conjI,simp)
apply (rule conjI, rule P_dyn_fv_dom_E1_Case_LitB_ej,assumption+)
apply (rule conjI, rule P_dyn_fvReg_dom_E2_Case_ej,assumption+)
apply (rule conjI, simp)
apply simp
(* 5. We get P_Δ, P_μ and P_σ for
the bound (Δj,μj,σj) w.r.t (δj,mj,sj) of ej's
evaluation *)
(* 5.1. \<Squnion>Δ (Δi) is bound for δj *)
apply (rule conjI)
apply (rule P_Δ_Case_Lit,simp,assumption+,simp,simp)
(* 5.2. \<Squnion>μ (μi) is bound for mj *)
apply (rule conjI, rule P_μ_Case_Lit,force,force,force)
(* 5.3. \<Squnion>σ (σi + ni) is bound for (sj+nj) *)
apply (rule P_σ_Case_Lit,force,force,force,force)
done
(***********************************************)
declare atom.simps [simp del]
declare consistent.simps [simp del]
declare SafeResourcesDAssDepth.simps [simp del]
declare valid_def [simp del]
declare SafeResourcesDAss.simps [simp del]
declare argP.simps [simp del]
declare η_ef_def [simp del]
(* Auxiliary Lemmas for ef *)
axioms equals_projection:
"projection f Δ' = projection f Δ
==> Δ' = Δ"
lemma lemma_19_aux [rule_format]:
"\<Turnstile>\<Turnstile> Σb
--> Σb g = Some (projection g Δg,μg,σg)
--> Σd g = Some (xs,rs,eg)
--> (bodyAPP Σd g):g (typesAPP Σϑ g) (sizesAPP ΣΦ g) real(length (varsAPP Σd g) + length (regionsAPP Σd g)) \<lbrace> Δg,μg,σg \<rbrace>"
apply (rule impI)
apply (erule ValidGlobalResourcesEnv.induct)
apply simp
apply (rule impI)+
apply (case_tac "g=f")
(* g = f *)
apply (simp add: typeResAPP_def regionsArgAPP_def typesArgAPP_def)
apply (elim conjE, frule equals_projection,simp)
(* g ≠ f *)
by (simp add: typeResAPP_def regionsArgAPP_def typesArgAPP_def)
lemma equiv_SafeResourcesDAss_all_n_SafeResourcesDAssDepth:
"e :f (typesAPP Σϑ f) (sizesAPP ΣΦ f) td \<lbrace>Δ, μ, σ\<rbrace>
==> ∀n. SafeResourcesDAssDepth e f (typesAPP Σϑ f) (sizesAPP ΣΦ f) 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 (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 (frule_tac td=td in eqSemDepthRA)
apply (drule mp,force)
by simp
lemma lemma_19 [rule_format]:
"ValidGlobalResourcesEnvDepth f n Σb
--> Σd g = Some (xs,rs,eg)
--> Σb g = Some (projection g Δg,μg,σg)
--> g ≠ f
--> SafeResourcesDAss eg g (typesAPP Σϑ g) (sizesAPP ΣΦ g) (real (length xs) + real (length rs)) Δg μg σg"
apply (rule impI)
apply (erule ValidGlobalResourcesEnvDepth.induct)
(* [| \<Turnstile>\<Turnstile> Σb; f ∉ dom Σb|] ==> \<Turnstile>\<Turnstile>f,n Σb *)
apply (rule impI)+
apply (frule lemma_19_aux,force,force)
apply (simp add: bodyAPP_def varsAPP_def regionsAPP_def)
(* [| \<Turnstile>\<Turnstile> Σb; f ∉ dom Σb|] ==> \<Turnstile>\<Turnstile>f,0 Σb(f\<mapsto>(Δg,μg,σg)) *)
apply (rule impI)+
apply (frule lemma_19_aux, simp add: fun_upd_apply, force)
apply (subst (asm) fun_upd_apply, simp)
apply (simp add: bodyAPP_def varsAPP_def regionsAPP_def)
(* \<Turnstile>\<Turnstile>f,Suc n Σb(f\<mapsto>(Δg,μg,σg)) *)
apply (rule impI)+
apply (frule lemma_19_aux, simp add: fun_upd_apply, force)
apply (subst (asm) fun_upd_apply, simp)
apply (simp add: bodyAPP_def varsAPP_def regionsAPP_def)
(* \<Turnstile>\<Turnstile>f, n Σb(g\<mapsto>(Δg,μg,σg)) *)
apply (case_tac "ga=g",simp_all)
apply (rule impI)+
apply (simp add: bodyAPP_def varsAPP_def regionsAPP_def)
apply (elim conjE, frule equals_projection,simp)
done
lemma lemma_20 [rule_format]:
"ValidGlobalResourcesEnvDepth f n Σb
--> Σd f = Some (xs,rs,ef)
--> Σb f = Some (projection f Δf,μf,σf)
--> n = Suc n'
--> SafeResourcesDAssDepth ef f (typesAPP Σϑ f) (sizesAPP ΣΦ f) (real (length xs) + real (length rs)) n' Δf μf σf"
apply (rule impI)
apply (erule ValidGlobalResourcesEnvDepth.induct)
(* [| \<Turnstile>\<Turnstile> Σb; f ∉ dom Σb|] ==> \<Turnstile>\<Turnstile>f,n Σb *)
apply (rule impI)+
apply (frule lemma_19_aux, simp add: fun_upd_apply, force)
apply (frule equiv_SafeResourcesDAss_all_n_SafeResourcesDAssDepth)
apply (simp add: bodyAPP_def varsAPP_def regionsAPP_def)
(* [| \<Turnstile>\<Turnstile> Σb; f ∉ dom Σb|] ==> \<Turnstile>\<Turnstile>f,0 Σb(f\<mapsto>(Δg,μg,σg)) *)
apply simp
(* \<Turnstile>\<Turnstile>f,Suc n Σb(f\<mapsto>(Δg,μg,σg)) *)
apply (rule impI)+
apply (simp add: bodyAPP_def varsAPP_def regionsAPP_def)
apply (elim conjE, frule equals_projection,simp)
(* \<Turnstile>\<Turnstile>f, n Σb(g\<mapsto>(Δg,μg,σg)) *)
apply (rule impI)+
apply simp
done
(***** P_sem *******)
lemma P1_f_n_APP:
"[| (E1, E2) \<turnstile> h, k, td, AppE f as rs' a \<Down>(f,n) hh , k , v, (δ,m,s); primops f = None;
Σd f = Some (xs, rs, ef)|]
==> ∃ h' δ' s'.
(map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) \<turnstile>
h, (Suc k), (real (length as) + real (length rs')), ef \<Down>(f,n) h', (Suc k), v, (δ',m,s')
∧ s = max( real (length xs) + real (length rs)) ((s'+ real (length xs))+real (length rs) - td)
∧ δ = δ'(k+1:=None)
∧ length xs = length as
∧ distinct xs
∧ length rs = length rs'
∧ distinct rs
∧ hh = h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}
∧ dom E1 ∩ set xs = {}
∧ n > 0"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
apply clarsimp
apply (rule_tac x=h' in exI)
apply (rule_tac x=δ in exI)
apply (rule_tac x=s in exI)
apply (rule conjI)
apply (rule_tac x=nfa in exI)
apply (rule conjI)
apply force
apply force
by force
lemma P1_f_n_APP_2:
"[| (E1, E2) \<turnstile> h , k , td, AppE g as rs' a \<Down>(f,n) hh , k , v, (δ,m,s); primops g = None; f≠g;
Σd g = Some (xs, rs, eg) |]
==> ∃ h' δ' s'.
(map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) \<turnstile>
h, (Suc k), (real (length as) + real (length rs')), eg \<Down>(f,n) h', (Suc k), v, (δ',m,s')
∧ s = max( real (length xs) + real (length rs)) ((s'+ real (length xs))+real (length rs) - td)
∧ δ = δ'(k+1:=None)
∧ length xs = length as
∧ distinct xs
∧ length rs = length rs'
∧ distinct rs
∧ hh = h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}
∧ dom E1 ∩ set xs = {}"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
apply clarsimp
apply (rule_tac x=h' in exI)
apply (rule_tac x=δ in exI)
apply (rule_tac x=s in exI)
apply (rule conjI)
apply (rule_tac x=nfa in exI)
apply (rule conjI)
apply force
apply force
by force
lemma P1_f_n_ge_0_APP:
"[| (E1, E2) \<turnstile> h , k , td, AppE f as rs' a \<Down>(f,Suc n) hh , k , v, (δ,m,s); primops f = None;
Σd f = Some (xs, rs, ef) |]
==> ∃ h' δ' s'.
(map_of (zip xs (map (atom2val E1) as)), map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k)) \<turnstile>
h , Suc k , (real (length as) + real (length rs')), ef \<Down>(f,n) h' , Suc k , v, (δ',m,s')
∧ s = max( real (length xs) + real (length rs)) ((s'+ real (length xs))+real (length rs) - td)
∧ δ = δ'(k+1:=None)
∧ length xs = length as
∧ distinct xs
∧ length rs = length rs'
∧ distinct rs
∧ hh = h' |` {p. p ∈ dom h' & fst (the (h' p)) ≤ k}
∧ dom E1 ∩ set xs = {}"
apply (simp add: SafeBoundSem_def)
apply (elim exE, elim conjE)
apply (erule SafeDepthSem.cases,simp_all)
apply clarsimp
apply (rule_tac x=h' in exI)
apply (rule_tac x=δ in exI)
apply (rule_tac x=s in exI)
apply (rule conjI)
apply (rule_tac x=nfa in exI)
apply (rule conjI)
apply force
apply force
by force
(* Auxiliary lemmas *)
lemma dom_map_of_zip:
"length xs = length ys
==> set xs ⊆ dom (map_of (zip xs ys))"
apply (induct xs ys rule:list_induct2',simp_all)
by blast
lemma xs_in_dom_f:
"[| length xs = length ys;
(∀ i < length ys. f (xs!i) = g (ys!i));
set ys ⊆ dom g |]
==> ∀ i < length xs. (xs!i) ∈ dom f"
by force
lemma nth_in_dom_map:
" set xs ⊆ dom m
==> ∀ i < length xs. xs!i ∈ dom m"
by force
lemma set_xs_subseteq_dom_m:
"[| x ∈ set xs; (∀i<length xs. xs ! i ∈ dom m) |]
==> x ∈ dom m"
by (subst (asm) in_set_conv_nth,force)
(**** Auxiliary lemmas for instance_f *****)
lemma dom_instance_f:
"dom (instance_f f Δg φ as rs Φ) = (set (R_Args Σt f)) ∪ {ρself_f f}"
apply (simp add: instance_f_def)
apply (rule equalityI)
apply (rule subsetI)
apply (simp add: instance_f_def)
apply clarsimp
apply (rule conjI)
apply clarsimp
by clarsimp
(**** Auxiliary lemmas for η_g *****)
lemma dom_η_ef:
"[| Σd g = Some (xs,rs,eg); fvReg (AppE g as rs' ()) ⊆ dom E2;
SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (AppE g as rs' ()) (f, n) hh k v (δ, m, s);
valid Σd Σϑ ΣΦ; admissible f η k; f ∈ dom Σd;
argP φ (R_Args Σt g) (typesRegsAPP Σϑ f) rs'|]
==> dom (η_ef η φ (R_Args Σt g) ++ [ρself_f g \<mapsto> Suc k]) = set (R_Args Σt g) ∪ {ρself_f g}"
apply (simp add: argP.simps)
apply (simp add: valid_def)
apply (erule_tac x=f in ballE)
prefer 2 apply force
apply (simp only: typesAPP_def)
apply (simp add: valid_f.simps)
apply (elim conjE)
apply (erule_tac x="AppE g as rs'" in allE)
apply (elim conjE,simp)
apply (erule_tac x=E1 in allE)
apply (erule_tac x=E2 in allE)
apply (erule_tac x=h in allE)
apply (rotate_tac 13)
apply (erule_tac x=k in allE)
apply (erule_tac x=td in allE)
apply (erule_tac x=hh in allE)
apply (erule_tac x=v in allE)
apply (erule_tac x=δ in allE)
apply (erule_tac x=m in allE)
apply (erule_tac x=s in allE)
apply (erule_tac x=η in allE)
apply (drule mp, simp)
apply (subst eqSemRABound,force)
apply (elim conjE)
apply (simp add: consistent.simps)
apply (elim conjE)
apply (rule equalityI)
apply (rule subsetI)
apply (simp add: η_ef_def)
apply force
apply (rule subsetI)
apply (simp add: η_ef_def,clarsimp)
apply (frule xs_in_dom_f,simp,simp)
apply (frule set_xs_subseteq_dom_m, simp)
apply (subst (asm) in_set_conv_nth)
apply (elim exE)
apply (rotate_tac 5)
apply (erule_tac x=i in allE)
apply (drule mp,simp,simp)
apply (rotate_tac 7)
apply (erule_tac x="rs'!i" in ballE)
apply (elim exE, elim conjE)+
apply simp
by (frule nth_in_dom_map,simp)
(**** Lemmas for properties ****)
(* P_dyn: xs ∪ fv eg ⊆ dom E1_g *)
lemma P_dyn_xs_subseteq_dom_E1_g:
"[| Σd g = Some (xs, rs, eg); fv eg ⊆ set xs;
∀i<length as. atom (as ! i);length xs = length as |]
==> set (varsAPP Σd g) ∪ fv eg ⊆ dom (map_of (zip xs (map (atom2val E1) as)))"
apply (subgoal_tac "length xs = length (map (atom2val E1) as)")
prefer 2 apply (induct xs, simp,clarsimp)
apply (frule_tac ys="(map (atom2val E1) as)" in dom_map_of_zip)
by (simp add: varsAPP_def)
(* P_dyn: fvReg eg ⊆ dom E2_g*)
lemma P_dyn_fvReg_eg_subseteq_dom_E2_g:
"[| fvReg eg ⊆ set rs; length rs = length rs';
set rs' ⊆ dom E2 |]
==> fvReg eg ⊆ dom (map_of (zip rs (map (the o E2) rs'))(self \<mapsto> Suc k))"
apply (subgoal_tac "set rs ⊆ dom (map_of (zip rs (map (the o E2) rs')))",simp)
apply blast
by (rule dom_map_of_zip,simp)
(* P_dyn: dom η = dom Δ *)
lemma P_dyn_dom_η_ef:
"[| Σd g = Some (xs,rs,eg); fvReg (AppE g as rs' ()) ⊆ dom E2;
SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (AppE g as rs' ()) (f, n) hh k v (δ, m, s);
valid Σd Σϑ ΣΦ; argP ψ (R_Args Σt g) (typesRegsAPP Σϑ f) rs';
admissible f η k; f ∈ dom Σd;
set (R_Args Σt g) ∪ {ρself_f g} = dom Δg;
dom (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) = dom η |]
==> dom Δg = dom (η_ef η ψ (R_Args Σt g) ++ [ρself_f g \<mapsto> Suc k])"
by (subst dom_η_ef,assumption+,simp)
(* P_η *)
lemma P_η_ef:
"[| admissible f η k |]
==> admissible g (η_ef η φ (R_Args Σt g) ++ [ρself_f g \<mapsto> Suc k]) (Suc k)"
apply (simp only: admissible_def)
apply (rule conjI,simp)
apply (elim conjE)
apply (rule ballI,simp)
apply (rule impI,simp)
apply (erule_tac x="the (φ ρ)" in ballE)
apply (elim exE, elim conjE)
apply (simp add: η_ef_def)
apply force
by (simp add: η_ef_def, simp add: dom_def)
lemma length_phiMapping_equals_length_as:
"[| atom2var ` set as ⊆ dom Φ |]
==> length (phiMapping_app (map Φ (map atom2var as)) si) = length as"
by (induct as,simp,clarsimp)
lemma length_build_si:
"length (build_si E1 h xs) = length xs"
by (induct xs,simp_all)
lemma valid_fv_APP_subseteq_Φ:
"[| SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (AppE g as rs' ()) (f, n) hh k v (δ, m, s);
valid Σd Σϑ ΣΦ; f ∈ dom Σd |]
==> fv (AppE g as rs' ()) ⊆ dom (sizesAPP ΣΦ f)"
apply (simp add: valid_def)
apply (erule_tac x=f in ballE)
apply (simp add: typesAPP_def add: valid_f.simps)
apply (elim conjE)
apply (erule_tac x="AppE g as rs'" in allE,simp)
by force
lemma as_subseteq_dom_Φ [rule_format]:
"fvs' as ⊆ dom Φ
--> (∀i<length as. atom (as ! i))
--> atom2var ` set as ⊆ dom Φ"
apply (rule impI)
apply (induct as,simp,clarsimp)
apply (drule mp,force,simp)
apply (erule_tac x=0 in allE,simp)
apply (simp add: atom.simps)
by (case_tac a, simp_all)
lemma nth_map_of_xs_atom2val:
"[| length xs = length as;
distinct xs |]
==> ∀ i < length xs.
map_of (zip xs (map (atom2val E1) as)) (xs!i) =
Some (atom2val E1 (as!i))"
apply clarsimp
apply (induct xs as rule: list_induct2',simp_all)
by (case_tac i,simp,clarsimp)
lemma nth_atom2val_in_dom_E:
"[| atom2var ` set as ⊆ dom E1;
i < length as; as ! i = VarE x a |]
==> Some (atom2val E1 (as ! i)) = E1 x"
apply (subgoal_tac "i < length (map atom2var as)")
apply (frule_tac xs="(map atom2var as)" in nth_mem,simp)
apply (subgoal_tac "x ∈ dom E1")
apply (frule domD,elim exE,simp)
apply blast
by (induct as, simp, simp)
lemma nth_build_si:
"i< length xs
==> build_si E1 h xs!i = sizeEnv E1 (xs!i) h"
apply (induct xs arbitrary:i, simp_all)
by (case_tac i,simp_all)
lemma sizeEnv_equals_build_si_i:
"[|length xs = length as; distinct xs; (∀i<length as. atom (as ! i));
Σd g = Some (xs,rs,eg); i < length as; atom2var ` set as ⊆ dom E1|]
==> sizeEnv E1 (map atom2var as ! i) h
= build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g) ! i"
apply (simp add: varsAPP_def)
apply (subst nth_build_si,simp)
apply (frule_tac ?E1.0="E1" in nth_map_of_xs_atom2val,simp)
apply (erule_tac x=i in allE)
apply (drule mp,simp)
apply (erule_tac x=i in allE)
apply (drule mp,simp)
apply (simp add: atom.simps)
apply (case_tac "as!i",simp_all)
apply (frule_tac ?E1.0="E1" in nth_map_of_xs_atom2val,simp)
apply (erule_tac x=i in allE)
apply (drule mp,simp)
apply (subst (asm) nth_atom2val_in_dom_E,assumption+)
apply (subgoal_tac "sizeEnv (map_of (zip xs (map (atom2val E1) as))) (xs ! i) h =
sizeEnv E1 list h",simp)
by (simp add: sizeEnv_def)
lemma fv_as_in_dom_E1 [rule_format]:
"fvs' as ⊆ dom E1
--> (∀i<length as. atom (as ! i))
--> atom2var ` set as ⊆ dom E1"
apply (rule impI)
apply (induct as,simp,clarsimp)
apply (drule mp,force,simp)
apply (erule_tac x=0 in allE,simp)
apply (simp add: atom.simps)
by (case_tac a, simp_all)
lemma nth_phiMapping_app:
"set ys ⊆ dom φ
==> ∀ i < length ys. phiMapping_app (map φ ys) si ! i =
the (the (φ (ys!i)) si)"
apply (rule allI, rule impI)
apply (induct ys arbitrary: i, simp_all)
apply (elim conjE)
apply (frule domD, elim exE,simp)
by (case_tac i,simp,simp)
lemma list_ge_phiMapping_app_build_si:
"[| (∀ i < length as. atom (as!i)); length xs = length as; distinct xs;
fv (AppE g as rs' a) ⊆ dom E1;
SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (AppE g as rs' ()) (f, n) hh k v (δ, m, s);
admissible f η k; f ∈ dom Σd;
Σd g = Some (xs,rs,eg); valid Σd Σϑ ΣΦ |]
==> list_ge (phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f)))
(build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g))"
apply (simp add: list_ge_def)
apply (rule allI, rule impI)
apply (simp only: valid_def)
apply (erule_tac x=f in ballE)
prefer 2 apply force
apply (simp add: typesAPP_def)
apply (simp add: valid_f.simps)
apply (elim conjE)
apply (erule_tac x="AppE g as rs'" in allE)
apply (elim conjE,simp)
apply (erule_tac x=E1 in allE)
apply (erule_tac x=E2 in allE)
apply (erule_tac x=h in allE)
apply (rotate_tac 15)
apply (erule_tac x=k in allE)
apply (erule_tac x=td in allE)
apply (erule_tac x=hh in allE)
apply (erule_tac x=v in allE)
apply (erule_tac x=δ in allE)
apply (erule_tac x=m in allE)
apply (erule_tac x=s in allE)
apply (rotate_tac 15)
apply (erule_tac x=η in allE)
apply (drule mp,simp)
apply (subst eqSemRABound,force)
apply (elim conjE)
apply (frule_tac Φ="(sizesAPP ΣΦ f)" in as_subseteq_dom_Φ,simp)
apply (frule_tac Φ="(sizesAPP ΣΦ f)" and
si="(build_si E1 h (varsAPP Σd f))" in length_phiMapping_equals_length_as)
apply (subst nth_phiMapping_app,simp,simp)
apply (erule_tac x="map atom2var as ! i" in ballE)
apply (subgoal_tac "sizeEnv E1 (map atom2var as ! i) h
= build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g) ! i",simp)
apply (frule fv_as_in_dom_E1,simp)
apply (rule sizeEnv_equals_build_si_i,assumption+,simp,simp)
apply (subgoal_tac "set (map atom2var as) ⊆ dom (sizesAPP ΣΦ f)")
apply (frule_tac xs="map atom2var as" in nth_in_dom_map,simp)
by simp
lemma Phi_Mapping_app_ge_build_si_ef:
"[| SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (AppE g as rs' ()) (f, n) hh k v (δ, m, s);
(∀i<length as. atom (as ! i)); length xs = length as; distinct xs;
valid Σd Σϑ ΣΦ; Σd g = Some (xs, rs, ef); fv (AppE g as rs' a) ⊆ dom E1;
monotonic_bound μg; f ∈ dom Σd; admissible f η k;
defined_bound μg g|]
==> the (μg (phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f)))) ≥
the (μg (build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g)))"
apply (frule valid_fv_APP_subseteq_Φ,assumption+)
apply (subgoal_tac "phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f)) ∈ dom μg")
prefer 2 apply (simp only: defined_bound_def)
apply (erule_tac x="phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f))" in allE)
apply (drule mp)
apply (simp add: varsAPP_def)
apply (rule length_phiMapping_equals_length_as)
apply (rule as_subseteq_dom_Φ, assumption+,force)
apply simp
apply (subgoal_tac "build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g) ∈ dom μg")
prefer 2 apply (simp only: defined_bound_def)
apply (erule_tac x="build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g)" in allE)
apply (drule mp)
apply (subst length_build_si,simp)
apply simp
apply (simp add: monotonic_bound_def)
apply (erule_tac x="phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f))" in ballE)
prefer 2 apply simp
apply (erule_tac x="build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g)" in ballE)
prefer 2 apply simp
apply (drule mp)
by (rule list_ge_phiMapping_app_build_si,assumption+,simp,assumption+)
lemma P_μ_APP:
"[| SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (AppE g as rs' ()) (f, n) hh k v (δ, m, s);
(∀ i < length as. atom (as!i));
distinct xs; length xs = length as;
monotonic_bound μg; defined_bound μg g;
Σd g = Some (xs, rs, ef);
f ∈ dom Σd;
admissible f η k;
valid Σd Σϑ ΣΦ;
set (varsAPP Σd f) ∪ fv (AppE g as rs' ()) ⊆ dom E1;
mu_ge μg (build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g)) m |]
==> mu_ge (mu_app μg as (sizesAPP ΣΦ f)) (build_si E1 h (varsAPP Σd f)) m"
apply (simp only: mu_ge_def)
apply (simp only: mu_app_def)
apply (simp only: cost_PhiMapping_def)
apply (subgoal_tac "the (μg (phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f)))) >=
the (μg (build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g)))",simp)
apply (rule Phi_Mapping_app_ge_build_si_ef)
by (assumption+,simp,assumption+)
lemma fvs_in_dom_sizesAPP:
"[| (∀i<length as. atom (as ! i));
SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (AppE g as rs' ()) (f, n) hh k v (δ, m,s);
f ∈ dom Σd; admissible f η k;
valid Σd Σϑ ΣΦ |]
==> atom2var ` set as ⊆ dom (sizesAPP ΣΦ f)"
apply (simp only: valid_def)
apply (erule_tac x=f in ballE)
prefer 2 apply force
apply (simp add: typesAPP_def)
apply (simp add: valid_f.simps)
apply (elim conjE)
apply (erule_tac x="AppE g as rs'" in allE)
apply (elim conjE,simp)
apply (erule_tac x=E1 in allE)
apply (erule_tac x=E2 in allE)
apply (erule_tac x=h in allE)
apply (rotate_tac 10)
apply (erule_tac x=k in allE)
apply (erule_tac x=td in allE)
apply (erule_tac x=hh in allE)
apply (erule_tac x=v in allE)
apply (erule_tac x=δ in allE)
apply (erule_tac x=m in allE)
apply (erule_tac x=s in allE)
apply (erule_tac x=η in allE)
apply (drule mp,simp)
apply (subst eqSemRABound,force)
apply (elim conjE)
by (rule as_subseteq_dom_Φ,simp,simp)
lemma P_σ_APP:
"[| SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (AppE g as rs' ()) (f, n) hh k v (δ, m, s);
(∀i<length as. atom (as ! i)); length xs = length as; distinct xs;
valid Σd Σϑ ΣΦ; Σd g = Some (xs, rs, ef); fv (AppE g as rs' a) ⊆ dom E1;
monotonic_bound σg; f ∈ dom Σd; admissible f η k;
defined_bound σg g;
s = max (l + q) (s' + l + q - td);
sigma_ge σg (build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g)) s' |]
==> sigma_ge \<Squnion>c {[]l + q, substCostReal (addCostReal (addCostReal (sigma_app σg as (sizesAPP ΣΦ f)) l) q) td} (build_si E1 h (varsAPP Σd f)) s"
apply (frule fvs_in_dom_sizesAPP, assumption+)
apply (simp only: sigma_ge_def)
apply (simp only: sigma_app_def)
apply (simp only: cost_PhiMapping_def)
apply (subgoal_tac
"the (σg (phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f)))) ≥
the (σg (build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g)))",simp)
apply (rule conjI)
apply (simp add: constantCost_def)
apply (simp add: maxCost_def)
apply (rule impI)+
apply (drule mp,force)
apply (subgoal_tac
" build_si E1 h (varsAPP Σd f) ∈
dom (substCostReal (addCostReal (addCostReal (λxs. σg (phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) xs)) l) q) td)",simp)
apply (simp add: substCostReal_def)
apply (simp add: addCostReal_def)
apply clarsimp
apply (subgoal_tac "phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f)) ∈ dom σg")
prefer 2 apply (simp only: defined_bound_def)
apply (erule_tac x="phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f))" in allE)
apply (drule mp)
apply (subst length_phiMapping_equals_length_as,simp)
apply (simp add: varsAPP_def)
apply simp
apply (subgoal_tac "phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f)) ∈ dom σg")
prefer 2 apply (simp only: defined_bound_def)
apply (simp add: dom_def)
apply (simp add: maxCost_def)
apply (rule conjI)
apply (rule impI)+
apply clarsimp
apply (simp add: substCostReal_def)
apply (split split_if_asm,simp,simp add: addCostReal_def)
apply clarsimp
apply (split split_if_asm,simp,clarsimp)
apply (split split_if_asm,simp,simp)
apply simp
apply simp
apply (rule impI)+
apply (drule mp)
apply (simp add: constantCost_def)
apply (simp add: dom_def)
apply (subgoal_tac
"build_si E1 h (varsAPP Σd f) ∈
dom (substCostReal (addCostReal (addCostReal (λxs. σg (phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) xs)) l) q) td)",simp)
apply (simp add: substCostReal_def)
apply (simp add: addCostReal_def)
apply clarsimp
apply (subgoal_tac "phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f)) ∈ dom σg")
prefer 2 apply (simp only: defined_bound_def)
apply (erule_tac x="phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f))" in allE)
apply (drule mp)
apply (subst length_phiMapping_equals_length_as,simp)
apply (simp add: varsAPP_def)
apply simp
apply (subgoal_tac "phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f)) ∈ dom σg")
prefer 2 apply (simp only: defined_bound_def)
apply (simp add: dom_def)
by (rule Phi_Mapping_app_ge_build_si_ef,assumption+)
lemma setsumCost_empty: "setsumCost f {} = []0"
by (simp add: setsumCost_def)
lemma sumcost_conm:
"x +c y = y +c x"
apply (simp add: addCost_def)
apply (rule ext)
apply simp
done
lemma sumcost_dist:
"addCost (addCost x y) z = addCost x (addCost y z)"
apply (simp add: addCost_def)
apply (rule ext,clarsimp)
apply (rule conjI, rule impI)
apply (rule conjI,clarsimp)
apply (split split_if_asm,simp add:dom_def,simp)
apply clarsimp
apply (split split_if_asm,simp add:dom_def,simp)
apply (rule impI)
apply (rule conjI,clarsimp)
apply (split split_if_asm,simp add:dom_def,simp)
apply (rule impI,clarsimp)
by (split split_if_asm,simp add:dom_def,simp)
lemma setsumCost_insert [simp]:
"finite F ==> a ∉ F ==> setsumCost f (insert a F) = addCost (f a) (setsumCost f F)"
apply (simp add: setsumCost_def)
apply (subst ACf.fold_insert,simp_all)
apply (rule ACf.intro)
apply (rule sumcost_conm)
apply (rule sumcost_dist)
done
axioms setsumCost_setsum:
"the ((setsumCost (λx. the (f x)) A) xs) = setsum (λx. the (the (f x) xs)) A"
lemma sumset_instance_f_equals_sumset_phiMapping:
"dom (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) = dom η
==>
(∑ρ | η ρ = Some j.
the (the (instance_f f g Δg ψ (sizesAPP ΣΦ f) as ρ) (build_si E1 h (varsAPP Σd f))))
= (∑ρ | η ρ = Some j.
∑ρ∈{ρ'. ψ ρ' = Some ρ ∧ ρ' ∈ set (R_Args Σt g)}.
the (the (Δg ρ) (phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f)))))"
apply (simp (no_asm) only: instance_f_def)
apply (subgoal_tac
"(∑ρ | η ρ = Some j.
the (the (((λρ. Some (sum_rho g Δg ψ (sizesAPP ΣΦ f) as ρ)) |` (set (R_Args Σt f) ∪ {ρself_f f})) ρ)
(build_si E1 h (varsAPP Σd f)))) =
(∑ρ | η ρ = Some j. the (the (Some (sum_rho g Δg ψ (sizesAPP ΣΦ f) as ρ)) (build_si E1 h (varsAPP Σd f))))",simp)
apply (simp add: sum_rho_def)
apply (subst setsumCost_setsum,simp)
apply (rule setsum_cong2,simp)
apply (simp only: sum_rho_def)
apply (simp add: restrict_map_def)
apply (simp add: instance_f_def)
by force
lemma setsum_build_si_le_setsum_phiMapping:
"[| SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (AppE g as rs' ()) (f, n) hh k v (δ, m, s);
(∀i<length as. atom (as ! i)); length xs = length as; distinct xs;
valid Σd Σϑ ΣΦ; Σd g = Some (xs, rs, ef); fv (AppE g as rs' a) ⊆ dom E1;
monotonic_AbstractDelta Δg; f ∈ dom Σd; admissible f η k;
set (R_Args Σt g) ∪ {ρself_f g} = dom Δg;
dom (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) = dom η;
defined_AbstractDelta Δg g|]
==> (∑ρ | η ρ = Some j.
∑ρ∈{ρ'. ψ ρ' = Some ρ ∧ ρ' ∈ set (R_Args Σt g)}.
the (the (Δg ρ) (phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1 h (varsAPP Σd f)))))
≥
(∑ρ | η ρ = Some j.
∑ρ∈{ρ'. ψ ρ' = Some ρ ∧ ρ' ∈ set (R_Args Σt g)}.
the (the (Δg ρ) (build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g))))"
apply (rule setsum_mono)
apply (rule setsum_mono)
apply (subgoal_tac "ρ' ∈ dom Δg")
apply (subgoal_tac "monotonic_bound (the (Δg ρ'))")
apply (subgoal_tac "defined_bound (the (Δg ρ')) g")
apply (rule Phi_Mapping_app_ge_build_si_ef,assumption+)
apply (simp add: defined_AbstractDelta_def)
apply (simp add: monotonic_AbstractDelta_def)
by blast
axioms setsum_η_ef_equals_setsum_η:
"[| SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (AppE g as rs' ()) (f, n) hh k v (δ, m, s);
(∀i<length as. atom (as ! i)); length xs = length as; distinct xs;
valid Σd Σϑ ΣΦ; Σd g = Some (xs, rs, ef); fv (AppE g as rs' a) ⊆ dom E1;
monotonic_AbstractDelta Δg; f ∈ dom Σd; admissible f η k;
set (R_Args Σt g) ∪ {ρself_f g} = dom Δg;
dom (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) = dom η;
defined_AbstractDelta Δg g|]
==> (∑ρ | (η_ef η ψ (R_Args Σt g)(ρself_f g \<mapsto> Suc k)) ρ = Some j.
the (the (Δg ρ) (build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g)))) =
(∑ρ | η ρ = Some j. ∑ρ∈{ρ'. ψ ρ' = Some ρ ∧ ρ' ∈ set (R_Args Σt g)}.
the (the (Δg ρ) (build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g))))"
lemma sizeAbstractDelta_si_APP_ge_sizeAbstractDelta_si_eg:
"[| SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (AppE g as rs' ()) (f, n) hh k v (δ, m, s);
(∀i<length as. atom (as ! i)); length xs = length as; distinct xs;
valid Σd Σϑ ΣΦ; Σd g = Some (xs, rs, ef); fv (AppE g as rs' a) ⊆ dom E1;
monotonic_AbstractDelta Δg; f ∈ dom Σd; admissible f η k;
set (R_Args Σt g) ∪ {ρself_f g} = dom Δg;
dom (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) = dom η;
defined_AbstractDelta Δg g|]
==> sizeAbstractDelta_si (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) (build_si E1 h (varsAPP Σd f)) j η >=
sizeAbstractDelta_si Δg (build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g)) j (η_ef η ψ (R_Args Σt g)(ρself_f g \<mapsto> Suc k))"
apply (simp only: sizeAbstractDelta_si_def)
apply (subst sumset_instance_f_equals_sumset_phiMapping,simp)
apply (frule_tac j=j in setsum_build_si_le_setsum_phiMapping,assumption+)
by (subst setsum_η_ef_equals_setsum_η,assumption+)
lemma P_Δ_APP:
"[| SafeDepthSemanticsReal.SafeBoundSem (E1, E2) h k td (AppE g as rs' ()) (f, n) hh k v (δ, m, s);
(∀i<length as. atom (as ! i)); length xs = length as; distinct xs;
valid Σd Σϑ ΣΦ; Σd g = Some (xs, rs, ef); fv (AppE g as rs' a) ⊆ dom E1;
monotonic_AbstractDelta Δg; f ∈ dom Σd; admissible f η k;
defined_AbstractDelta Δg g;
set (R_Args Σt g) ∪ {ρself_f g} = dom Δg;
Delta_ge Δg (build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g)) (Suc k)
(η_ef η ψ (R_Args Σt g) ++ [ρself_f g \<mapsto> Suc k]) δ';
dom (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) = dom η;
δ = δ'(k + 1 := None) |]
==> Delta_ge (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) (build_si E1 h (varsAPP Σd f)) k η δ"
apply (simp add: Delta_ge_def)
apply (rule ballI)
apply (erule_tac x=j in ballE)
prefer 2 apply simp
apply (frule_tac j=j and ψ=ψ in sizeAbstractDelta_si_APP_ge_sizeAbstractDelta_si_eg)
by (assumption+,simp,assumption+,simp,assumption+,simp)
(** main theorem **)
lemma SafeResourcesDADepth_APP:
"[| ∀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;
Σ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';
Δ = 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)};
\<Turnstile>\<Turnstile>f , n Σb |]
==> AppE g as rs' a :f (typesAPP Σϑ f) (sizesAPP ΣΦ f) td, n \<lbrace>Δ, μ, σ\<rbrace>"
apply (case_tac "g≠f")
(* g ≠ f *)
apply (frule lemma_19,assumption+)
apply (simp add: typesAPP_def)
apply (simp only: SafeResourcesDAssDepth.simps)
(* implication P_est for APP *)
apply (rule impI)
apply (rule conjI, subst dom_instance_f,simp)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
(* valid *)
apply (simp only: SafeResourcesDAss.simps)
apply (drule mp,simp)
(* SafeRASemanticsReal.SafeRASem (E1,E2) h k td e hh k v (δ,m,s) *)
apply (frule P1_f_n_APP_2,simp,force,force)
apply (elim exE, elim conjE)
apply (rotate_tac 29)
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 (rotate_tac 38)
apply (erule_tac x="Suc k" in allE)
apply (rotate_tac 38)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="v" in allE)
apply (rotate_tac 38)
apply (erule_tac x="δ'" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="s'" in allE)
apply (erule_tac x="(η_ef η ψ (R_Args Σt g) ++ [ρself_f g \<mapsto> Suc k])" in allE)
apply (erule_tac x=" build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd g)" in allE)
apply (drule mp)
(* SafeDepthSemanticsReal.SafeBoundSem *)
apply (rule conjI)
apply (subst eqSemRABound [where f=f],force)
(* Assuming P_dyn for APP, we get P_dyn for ef *)
(* set (varsAPP Σd g) ∪ fv eg ⊆ dom (map_of (zip xs (map (atom2val E1) as))) *)
apply (rule conjI)
apply (rule P_dyn_xs_subseteq_dom_E1_g, assumption+)
(* fvReg eg ⊆ dom (map_of (zip rs (map (the o E2) rr))(self \<mapsto> Suc k)) *)
apply (rule conjI)
apply (rule P_dyn_fvReg_eg_subseteq_dom_E2_g,assumption+,simp)
(* dom Δg = dom (η_ren η ++ [ρself \<mapsto> Suc k]) *)
apply (rule conjI, rule P_dyn_dom_η_ef,assumption+)
(* Assuming P_xs for APP, we get P_xs for ef
si = build_si E1 h ϑ1 xs *)
apply (rule conjI, simp)
(* Assuming P_η for APP, we get P_η for ef,
admissible η k *)
apply (rule P_η_ef,simp)
(* Premises for validity eg *)
apply (elim conjE)
(* Delta_ge Δ si k η δ *)
apply (rule conjI, rule P_Δ_APP)
apply (assumption+,simp,assumption+)
(* mu_ge μ si m *)
apply (rule conjI)
apply (rule P_μ_APP,assumption+)
(* sigma_ge σ si s *)
apply (rule P_σ_APP)
apply (assumption+,simp,assumption+,simp,simp)
(* g = f *)
apply simp
apply (case_tac n)
(* n = 0 *)
apply (simp only: typesAPP_def)
apply (simp only: SafeResourcesDAssDepth.simps)
apply (rule impI)
apply (rule conjI, subst dom_instance_f,simp)
apply (rule allI)+
apply (rule impI)
apply (elim conjE)
apply (frule P1_f_n_APP,assumption+,simp)
(* case n > 0 *)
apply (frule lemma_20)
apply (force,force,simp,simp)
apply (simp only: typesAPP_def)
apply (simp only: SafeResourcesDAssDepth.simps)
apply (rule impI)
apply (drule mp,simp)
apply (elim conjE)
apply (rule conjI, subst dom_instance_f, simp)
apply (intro allI, rule impI)
apply (elim conjE)
apply (frule P1_f_n_ge_0_APP,simp,force)
apply (elim exE, elim conjE)
apply (rotate_tac 25)
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 (rotate_tac 40)
apply (erule_tac x="Suc k" in allE)
apply (rotate_tac 40)
apply (erule_tac x="h'" in allE)
apply (erule_tac x="v" in allE)
apply (rotate_tac 40)
apply (erule_tac x="δ'" in allE)
apply (erule_tac x="m" in allE)
apply (erule_tac x="s'" in allE)
apply (erule_tac x="(η_ef η ψ (R_Args Σt g) ++ [ρself_f g \<mapsto> Suc k])" in allE)
apply (erule_tac x=" build_si (map_of (zip xs (map (atom2val E1) as))) h (varsAPP Σd f)" in allE)
apply (drule mp)
(* afeDepthSemanticsReal.SafeBoundSem *)
apply (rule conjI,simp)
(* Assuming P_dyn for APP, we get P_dyn for ef *)
(* set (varsAPP Σd g) ∪ fv eg ⊆ dom (map_of (zip xs (map (atom2val E1) as))) *)
apply (rule conjI)
apply (rule P_dyn_xs_subseteq_dom_E1_g, assumption+)
(* fvReg eg ⊆ dom (map_of (zip rs (map (the o E2) rr))(self \<mapsto> Suc k)) *)
apply (rule conjI)
apply (rule P_dyn_fvReg_eg_subseteq_dom_E2_g,assumption+,simp)
(* dom Δg = dom (η_ren η ++ [ρself \<mapsto> Suc k]) *)
apply (rule conjI, rule P_dyn_dom_η_ef)
apply (force,simp,simp,assumption+,simp,assumption+,simp,simp)
(* Assuming P_xs for APP, we get P_xs for ef
si = build_si E1 h ϑ1 xs *)
apply (rule conjI, simp)
(* Assuming P_η for APP, we get P_η for ef,
admissible η k *)
apply (frule P_η_ef,simp)
(* Premises for validity eg *)
apply (elim conjE)
(* Delta_ge Δ si k η δ *)
apply (rule conjI)
apply (frule P_Δ_APP)
apply (assumption+,simp,assumption+,simp,assumption+,simp)
(* mu_ge μ si m *)
apply (rule conjI)
apply (frule P_μ_APP,assumption+,simp)
(* sigma_ge σ si s *)
apply (frule_tac σg="σg" in P_σ_APP)
by (assumption+,simp,assumption+,simp)
end
lemma dom_emptyAbstractDelta:
dom []f = set (R_Args Σt f) ∪ {ρself_f f}
lemma Delta_ge_emptyAbstractDelta_emptyDelta:
dom []f = dom η ==> Delta_ge []f si k η ([]\<^sub>k)
lemma mu_ge_constantCost:
mu_ge []0 si 0
lemma sigma_ge_constantCost:
sigma_ge []1 si 1
lemma SafeResourcesDADepth_LitInt:
ConstE (LitN i)
a :f (ϑ1.0, ϑ2.0) φ td , n \<lbrace> []f , []0 , []1 \<rbrace>
lemma SafeResourcesDADepth_LitBool:
ConstE (LitB b)
a :f (ϑ1.0, ϑ2.0) φ td , n \<lbrace> []f , []0 , []1 \<rbrace>
lemma dom_addAbstractDelta:
dom Δ1.0 +Δ Δ2.0 = dom Δ1.0 ∩ dom Δ2.0
lemma P_static_dom_Δ_Let:
[| set (R_Args Σt f) ∪ {ρself_f f} = dom Δ1.0;
set (R_Args Σt f) ∪ {ρself_f f} = dom Δ2.0 |]
==> set (R_Args Σt f) ∪ {ρself_f f} = dom Δ1.0 +Δ Δ2.0
lemma P1_f_n_LET:
[| ∀C as r a'. e1.0 ≠ ConstrE C as r a';
(E1.0,
E2.0) \<turnstile> h , k , td , Let x1.0 = e1.0 In e2.0 a \<Down> (f,
n) hh , k , v , (δ, m, s) |]
==> ∃h' v1 v2 δ1 m1 s1 δ2 m2 s2 n1 n2.
(E1.0,
E2.0) \<turnstile> h , k , 0 , e1.0 \<Down> (f,
n) h' , k , v1 , (δ1, m1, s1) ∧
(E1.0(x1.0 |-> v1),
E2.0) \<turnstile> h' , k , (td +
1) , e2.0 \<Down> (f,
n) hh , k , v2 , (δ2, m2, s2) ∧
δ = δ1 ⊕ δ2 ∧
m = max m1 (m2 + \<parallel> δ1 \<parallel>) ∧
s = max (s1 + 2) (s2 + 1) ∧ x1.0 ∉ dom E1.0
lemma P_dyn_dom_E1_Let_e1:
[| set (varsAPP Σd f) ∪ fv (Let x1.0 = e1.0 In e2.0 a) ⊆ dom E1.0;
x1.0 ∉ fv e1.0 |]
==> set (varsAPP Σd f) ∪ fv e1.0 ⊆ dom E1.0
lemma P_dyn_dom_E1_Let_e2:
[| set (varsAPP Σd f) ∪ fv (Let x1.0 = e1.0 In e2.0 a) ⊆ dom E1.0;
x1.0 ∉ fv e1.0 |]
==> set (varsAPP Σd f) ∪ fv e2.0 ⊆ dom (E1.0(x1.0 |-> v1.0))
lemma P_dyn_dom_Δ_Let_e1:
[| set (R_Args Σt f) ∪ {ρself_f f} = dom Δ1.0;
set (R_Args Σt f) ∪ {ρself_f f} = dom Δ2.0; dom Δ1.0 +Δ Δ2.0 = dom η |]
==> dom Δ1.0 = dom η
lemma P_dyn_dom_Δ_Let_e2:
[| set (R_Args Σt f) ∪ {ρself_f f} = dom Δ1.0;
set (R_Args Σt f) ∪ {ρself_f f} = dom Δ2.0; dom Δ1.0 +Δ Δ2.0 = dom η |]
==> dom Δ1.0 = dom η
lemma length_build_si:
length (build_si E1.0 h xs) = length xs
lemma sizeAbstractDelta_si_addf:
[| set (R_Args Σt f) ∪ {ρself_f f} = dom Δ1.0; defined_AbstractDelta Δ1.0 f;
set (R_Args Σt f) ∪ {ρself_f f} = dom Δ2.0; defined_AbstractDelta Δ2.0 f;
dom Δ1.0 +Δ Δ2.0 = dom η |]
==> sizeAbstractDelta_si Δ1.0 +Δ Δ2.0 (build_si E1.0 h (varsAPP Σd f)) j η =
sizeAbstractDelta_si Δ1.0 (build_si E1.0 h (varsAPP Σd f)) j η +
sizeAbstractDelta_si Δ2.0 (build_si E1.0 h (varsAPP Σd f)) j η
lemma sizeAbstractDelta_si_nonneg:
[| dom Δ = dom η; ∀ρ∈dom Δ. 0 ≤ the (the (Δ ρ) si) |]
==> 0 ≤ sizeAbstractDelta_si Δ si j η
lemma sizeEnv_equals_h_h':
[| x1.0 ∉ dom E1.0;
(E1.0,
E2.0) \<turnstile> h , k , td , e \<Down> (f, n) h' , k , v , (δ, m, s) ;
x1.0 ∉ set xs; x1.0 ≠ x; size_dom (the (E1.0 x), h);
size_dom (the (E1.0 x), h');
∀x∈set xs. size_dom (the (E1.0 x), h) ∧ size_dom (the (E1.0 x), h') |]
==> sizeEnv E1.0 x h = sizeEnv (E1.0(x1.0 |-> v1.0)) x h'
lemma build_si_equals_h_h':
[| x1.0 ∉ dom E1.0;
(E1.0,
E2.0) \<turnstile> h , k , td , e \<Down> (f, n) h' , k , v , (δ, m, s) ;
x1.0 ∉ set xs;
!!x. x ∈ set xs
==> size_dom (the (E1.0 x), h) ∧ size_dom (the (E1.0 x), h') |]
==> build_si E1.0 h xs = build_si (E1.0(x1.0 |-> v1.0)) h' xs
lemma P_Δ_Let:
[| set (R_Args Σt f) ∪ {ρself_f f} = dom Δ1.0; defined_AbstractDelta Δ1.0 f;
set (R_Args Σt f) ∪ {ρself_f f} = dom Δ2.0; defined_AbstractDelta Δ2.0 f;
dom Δ1.0 +Δ Δ2.0 = dom η;
Delta_ge Δ1.0 (build_si E1.0 h (varsAPP Σd f)) k η δ1.0;
Delta_ge Δ2.0 (build_si E1.0 h (varsAPP Σd f)) k η δ2.0 |]
==> Delta_ge Δ1.0 +Δ Δ2.0 (build_si E1.0 h (varsAPP Σd f)) k η (δ1.0 ⊕ δ2.0)
lemma defined_AbstractDelta_si_in_dom_Δ1:
defined_bound |Δ1.0| f ==> build_si E1.0 h (varsAPP Σd f) ∈ dom |Δ1.0|
lemma P_μ_Let:
[| Delta_ge Δ1.0 (build_si E1.0 h (varsAPP Σd f)) k η δ1.0;
defined_AbstractDelta Δ1.0 f; defined_bound |Δ1.0| f;
mu_ge μ1.0 (build_si E1.0 h (varsAPP Σd f)) m1.0; defined_bound μ1.0 f;
mu_ge μ2.0 (build_si E1.0 h (varsAPP Σd f)) m2.0; defined_bound μ2.0 f |]
==> mu_ge \<Squnion>c { μ1.0 , |Δ1.0| +c μ2.0 }
(build_si E1.0 h (varsAPP Σd f))
(max m1.0 (m2.0 + \<parallel> δ1.0 \<parallel>))
lemma P_σ_Let:
[| sigma_ge σ1.0 (build_si E1.0 h (varsAPP Σd f)) s1.0; defined_bound σ1.0 f;
sigma_ge σ2.0 (build_si E1.0 h (varsAPP Σd f)) s2.0; defined_bound σ2.0 f |]
==> sigma_ge \<Squnion>c { []2 +c σ1.0 , []1 +c σ2.0 }
(build_si E1.0 h (varsAPP Σd f)) (max (s1.0 + 2) (s2.0 + 1))
lemma SafeResourcesDADepth_Let1:
[| ∀C as r a'. e1.0 ≠ ConstrE C as r a'; x1.0 ∉ fv e1.0;
x1.0 ∉ set (varsAPP Σd f);
e1.0 :f (ϑ1.0, ϑ2.0) Φ 0 , n \<lbrace> Δ1.0 , μ1.0 , σ1.0 \<rbrace>;
defined_AbstractDelta Δ1.0 f; defined_bound |Δ1.0| f; defined_bound μ1.0 f;
defined_bound σ1.0 f;
e2.0 :f (ϑ1.0, ϑ2.0) Φ td + 1 , n \<lbrace> Δ2.0 , μ2.0 , σ2.0 \<rbrace>;
defined_AbstractDelta Δ2.0 f; defined_bound μ2.0 f; defined_bound σ2.0 f;
Δ = Δ1.0 +Δ Δ2.0 ; μ = \<Squnion>c { μ1.0 , |Δ1.0| +c μ2.0 };
σ = \<Squnion>c { []2 +c σ1.0 , []1 +c σ2.0 } |]
==> Let x1.0 = e1.0 In e2.0 a :f (ϑ1.0,
ϑ2.0) Φ td , n \<lbrace> Δ , μ , σ \<rbrace>
lemma dom_maxCost:
dom \<Squnion>c { c1.0 , c2.0 } = dom c1.0 ∩ dom c2.0
lemma dom_maxAbstractDelta:
dom (maxAbstractDelta c1.0 c2.0) = dom c1.0 ∩ dom c2.0
lemma dom_maxCostList:
dom (foldr maxCost (map AbstractMuSpaceCost xs) []0) =
(INT i<length xs. dom (AbstractMuSpaceCost (xs ! i)))
lemma P_static_dom_Δ_Case:
[| 0 < length xs;
!!i. i < length xs
==> insert (ρself_f f) (set (R_Args Σt f)) =
dom (AbstractDeltaSpaceCost (xs ! i)) |]
==> insert (ρself_f f) (set (R_Args Σt f)) =
dom \<Squnion>Δ f map AbstractDeltaSpaceCost xs
lemma P_dyn_dom_E1_Case_ej:
[| set (varsAPP Σd f) ⊆ dom E1.0;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> set (varsAPP Σd f) ⊆ dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs)
lemma P_dyn_fv_dom_E1_Case_ej:
[| fvAlts alts ⊆ dom E1.0; i < length alts;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> fv (snd (alts ! i)) ⊆ dom (extend E1.0 (snd (extractP (fst (alts ! i)))) vs)
lemma P_dyn_fvReg_dom_E2_Case_ej:
[| fvAltsReg alts ⊆ dom E2.0; i < length alts |]
==> fvReg (snd (alts ! i)) ⊆ dom E2.0
lemma P_dyn_fv_dom_E1_Case_LitN_ej:
[| fvAlts alts ⊆ dom E1.0; i < length alts; fst (alts ! i) = ConstP (LitN n) |]
==> fv (snd (alts ! i)) ⊆ dom E1.0
lemma P_dyn_fv_dom_E1_Case_LitB_ej:
[| fvAlts alts ⊆ dom E1.0; i < length alts; fst (alts ! i) = ConstP (LitB b) |]
==> fv (snd (alts ! i)) ⊆ dom E1.0
lemma si_in_dom_AbstractDeltaSpaceCost:
[| defined_AbstractDelta (AbstractDeltaSpaceCost x) f;
ρ ∈ dom (AbstractDeltaSpaceCost x) |]
==> build_si E1.0 h (varsAPP Σd f) ∈ dom (the (AbstractDeltaSpaceCost x ρ))
lemma si_in_dom_emptyAbstractDelta:
ρ ∈ dom []f ==> build_si E1.0 h (varsAPP Σd f) ∈ dom (the ([]f ρ))
lemma defined_AbstracDelta_imp_defined_bound:
[| ∀i<length assert.
insert (ρself_f f) (set (R_Args Σt f)) =
dom (AbstractDeltaSpaceCost (assert ! i));
ρ ∈ insert (ρself_f f) (set (R_Args Σt f));
∀i<length assert.
defined_AbstractDelta (AbstractDeltaSpaceCost (assert ! i)) f |]
==> ∀i<length assert.
defined_bound (the (AbstractDeltaSpaceCost (assert ! i) ρ)) f
lemma all_i_defined_bound_all_si_in_dom_Delta:
∀i<length xs. defined_bound (the (AbstractDeltaSpaceCost (xs ! i) ρ)) f
==> ∀i<length xs.
build_si E1.0 h (varsAPP Σd f)
∈ dom (the (AbstractDeltaSpaceCost (xs ! i) ρ))
lemma all_i_si_in_Delta_si_in_dom_maxCost_Delta:
∀i<length xs.
build_si E1.0 h (varsAPP Σd f)
∈ dom (the (AbstractDeltaSpaceCost (xs ! i) ρ))
==> build_si E1.0 h (varsAPP Σd f)
∈ (INT i<length xs. dom (the (AbstractDeltaSpaceCost (xs ! i) ρ)))
lemma dom_maxCostDeltaList:
[| ρ ∈ insert (ρself_f f) (set (R_Args Σt f));
ρ ∈ dom (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f) |]
==> dom (the (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f ρ)) =
(INT i<length xs. dom (the (AbstractDeltaSpaceCost (xs ! i) ρ)))
lemma si_dom_Delta_si_dom_maxCost_Delta:
[| ρ ∈ insert (ρself_f f) (set (R_Args Σt f));
ρ ∈ dom (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f);
∀i<length xs.
build_si E1.0 h (varsAPP Σd f)
∈ dom (the (AbstractDeltaSpaceCost (xs ! i) ρ)) |]
==> build_si E1.0 h (varsAPP Σd f)
∈ dom (the (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f ρ))
lemma ρ_in_dom_AbstractDeltaSpaceCost:
[| ρ ∈ insert (ρself_f f) (set (R_Args Σt f));
ρ ∈ dom (maxAbstractDelta (AbstractDeltaSpaceCost x)
(foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f)) |]
==> ρ ∈ dom (AbstractDeltaSpaceCost x) ∧
ρ ∈ dom (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f)
lemma si_in_dom_AbstractDeltaSpaceCost:
[| ρ ∈ insert (ρself_f f) (set (R_Args Σt f));
si ∈ dom (the (maxAbstractDelta (AbstractDeltaSpaceCost x)
(foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f)
ρ));
ρ ∈ dom (maxAbstractDelta (AbstractDeltaSpaceCost x)
(foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f)) |]
==> si ∈ dom (the (AbstractDeltaSpaceCost x ρ)) ∩
dom (the (foldr maxAbstractDelta (map AbstractDeltaSpaceCost xs) []f
ρ))
lemma maxAbstractDeltaSpaceCost_ge_AbstractDeltaSpaceCost:
[| i < length assert; ρ ∈ insert (ρself_f f) (set (R_Args Σt f));
ρ ∈ dom (foldr maxAbstractDelta (map AbstractDeltaSpaceCost assert) []f);
build_si E1.0 h (varsAPP Σd f)
∈ dom (the (foldr maxAbstractDelta (map AbstractDeltaSpaceCost assert) []f
ρ)) |]
==> the (the (AbstractDeltaSpaceCost (assert ! i) ρ)
(build_si E1.0 h (varsAPP Σd f)))
≤ the (the (\<Squnion>Δ f map AbstractDeltaSpaceCost assert ρ)
(build_si E1.0 h (varsAPP Σd f)))
lemma all_i_defined_bound_all_si_in_dom_mu:
∀i<length xs. defined_bound (AbstractMuSpaceCost (xs ! i)) f
==> ∀i<length xs.
build_si E1.0 h (varsAPP Σd f) ∈ dom (AbstractMuSpaceCost (xs ! i))
lemma all_i_si_in_dom_mu_si_in_dom_maxCost_mu:
∀i<length xs.
build_si E1.0 h (varsAPP Σd f) ∈ dom (AbstractMuSpaceCost (xs ! i))
==> build_si E1.0 h (varsAPP Σd f)
∈ (INT i<length xs. dom (AbstractMuSpaceCost (xs ! i)))
lemma si_dom_mu_si_dom_maxCost_mu:
∀i<length xs.
build_si E1.0 h (varsAPP Σd f) ∈ dom (AbstractMuSpaceCost (xs ! i))
==> build_si E1.0 h (varsAPP Σd f)
∈ dom (foldr maxCost (map AbstractMuSpaceCost xs) []0)
lemma maxAbstractMuSpaceCost_ge_AbstractMuSpaceCost:
[| i < length assert;
!!i. i < length assert
==> defined_bound (AbstractMuSpaceCost (assert ! i)) f |]
==> the (AbstractMuSpaceCost (assert ! i) (build_si E1.0 h (varsAPP Σd f)))
≤ the (\<Squnion>c map AbstractMuSpaceCost assert
(build_si E1.0 h (varsAPP Σd f)))
lemma sizeAbstractDelta_si_case_Lit_ge_sizeAbstracDelta_si_alt:
[| i < length assert;
insert (ρself_f f) (set (R_Args Σt f)) =
dom \<Squnion>Δ f map AbstractDeltaSpaceCost assert ;
∀i<length assert.
insert (ρself_f f) (set (R_Args Σt f)) =
dom (AbstractDeltaSpaceCost (assert ! i));
∀i<length assert.
defined_AbstractDelta (AbstractDeltaSpaceCost (assert ! i)) f;
insert (ρself_f f) (set (R_Args Σt f)) = dom η |]
==> sizeAbstractDelta_si (AbstractDeltaSpaceCost (assert ! i))
(build_si E1.0 h (varsAPP Σd f)) j η
≤ sizeAbstractDelta_si \<Squnion>Δ f map AbstractDeltaSpaceCost assert
(build_si E1.0 h (varsAPP Σd f)) j η
lemma P_Δ_Case_Lit:
[| i < length assert;
insert (ρself_f f) (set (R_Args Σt f)) =
dom \<Squnion>Δ f map AbstractDeltaSpaceCost assert ;
∀i<length assert.
insert (ρself_f f) (set (R_Args Σt f)) =
dom (AbstractDeltaSpaceCost (assert ! i));
∀i<length assert.
defined_AbstractDelta (AbstractDeltaSpaceCost (assert ! i)) f;
insert (ρself_f f) (set (R_Args Σt f)) = dom η;
Delta_ge (AbstractDeltaSpaceCost (assert ! i))
(build_si E1.0 h (varsAPP Σd f)) k η δ |]
==> Delta_ge \<Squnion>Δ f map AbstractDeltaSpaceCost assert
(build_si E1.0 h (varsAPP Σd f)) k η δ
lemma nth_build_si:
i < length xs ==> build_si E1.0 h xs ! i = sizeEnv E1.0 (xs ! i) h
lemma sizeEnv_alt_equals_sizeEnv_Case:
[| set (varsAPP Σd f) ⊆ dom E1.0; ia < length (varsAPP Σd f);
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> sizeEnv (extend E1.0 (snd (extractP (fst (alts ! i)))) vs)
(varsAPP Σd f ! ia) h =
sizeEnv E1.0 (varsAPP Σd f ! ia) h
lemma build_si_Case_ge_build_si_alt:
[| set (varsAPP Σd f) ⊆ dom E1.0; ia < length (varsAPP Σd f);
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> build_si (extend E1.0 (snd (extractP (fst (alts ! i)))) vs) h
(varsAPP Σd f) !
ia =
build_si E1.0 h (varsAPP Σd f) ! ia
lemma sizeEnv_alt_equals_sizeEnv_Case_2:
[| x ∈ dom E1.0; def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> sizeEnv (extend E1.0 (snd (extractP (fst (alts ! i)))) vs) x h =
sizeEnv E1.0 x h
lemma build_si_Case_ge_build_si_alt_2:
[| set xs ⊆ dom E1.0; def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> build_si (extend E1.0 (snd (extractP (fst (alts ! i)))) vs) h xs =
build_si E1.0 h xs
lemma list_ge_build_si_alt_build_si_Case:
[| set (varsAPP Σd f) ⊆ dom E1.0;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> list_ge (build_si E1.0 h (varsAPP Σd f))
(build_si (extend E1.0 (snd (extractP (fst (alts ! i)))) vs) h
(varsAPP Σd f))
lemma sizeAbstractDelta_si_Case_ge_sizeAbstractDelta_si_alt:
[| i < length assert; set (varsAPP Σd f) ⊆ dom E1.0;
∀i<length assert.
insert (ρself_f f) (set (R_Args Σt f)) =
dom (AbstractDeltaSpaceCost (assert ! i));
∀i<length assert.
insert (ρself_f f) (set (R_Args Σt f)) =
dom (AbstractDeltaSpaceCost (assert ! i));
∀i<length assert.
defined_AbstractDelta (AbstractDeltaSpaceCost (assert ! i)) f;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs;
monotonic_AbstractDelta (AbstractDeltaSpaceCost (assert ! i));
insert (ρself_f f) (set (R_Args Σt f)) = dom η |]
==> sizeAbstractDelta_si (AbstractDeltaSpaceCost (assert ! i))
(build_si (extend E1.0 (snd (extractP (fst (alts ! i)))) vs) h
(varsAPP Σd f))
j η
≤ sizeAbstractDelta_si (AbstractDeltaSpaceCost (assert ! i))
(build_si E1.0 h (varsAPP Σd f)) j η
lemma sizeAbstractDelta_si_Case_equals_sizeAbstractDelta_si_alt:
[| i < length assert; set (varsAPP Σd f) ⊆ dom E1.0;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> sizeAbstractDelta_si (AbstractDeltaSpaceCost (assert ! i))
(build_si (extend E1.0 (snd (extractP (fst (alts ! i)))) vs) h
(varsAPP Σd f))
j η =
sizeAbstractDelta_si (AbstractDeltaSpaceCost (assert ! i))
(build_si E1.0 h (varsAPP Σd f)) j η
lemma P_Δ_Case:
[| i < length assert;
insert (ρself_f f) (set (R_Args Σt f)) =
dom \<Squnion>Δ f map AbstractDeltaSpaceCost assert ;
∀i<length assert.
insert (ρself_f f) (set (R_Args Σt f)) =
dom (AbstractDeltaSpaceCost (assert ! i));
∀i<length assert.
defined_AbstractDelta (AbstractDeltaSpaceCost (assert ! i)) f;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs;
insert (ρself_f f) (set (R_Args Σt f)) = dom η;
set (varsAPP Σd f) ⊆ dom E1.0;
insert (ρself_f f) (set (R_Args Σt f)) = dom η;
monotonic_AbstractDelta (AbstractDeltaSpaceCost (assert ! i));
Delta_ge (AbstractDeltaSpaceCost (assert ! i))
(build_si (extend E1.0 (snd (extractP (fst (alts ! i)))) vs) h
(varsAPP Σd f))
k η δ |]
==> Delta_ge \<Squnion>Δ f map AbstractDeltaSpaceCost assert
(build_si E1.0 h (varsAPP Σd f)) k η δ
lemma AbstractMuSpaceCost_Case_equals_AbstractMuSpaceCost_alt:
[| set (varsAPP Σd f) ⊆ dom E1.0;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> the (AbstractMuSpaceCost (assert ! i)
(build_si (extend E1.0 (snd (extractP (fst (alts ! i)))) vs) h
(varsAPP Σd f))) =
the (AbstractMuSpaceCost (assert ! i) (build_si E1.0 h (varsAPP Σd f)))
lemma P_μ_Case:
[| set (varsAPP Σd f) ⊆ dom E1.0;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs;
monotonic_bound (AbstractMuSpaceCost (assert ! i));
∀i<length assert. defined_bound (AbstractMuSpaceCost (assert ! i)) f;
i < length assert;
mu_ge (AbstractMuSpaceCost (assert ! i))
(build_si (extend E1.0 (snd (extractP (fst (alts ! i)))) vs) h
(varsAPP Σd f))
m |]
==> mu_ge \<Squnion>c map AbstractMuSpaceCost assert
(build_si E1.0 h (varsAPP Σd f)) m
lemma P_μ_Case_Lit:
[| ∀i<length assert. defined_bound (AbstractMuSpaceCost (assert ! i)) f;
i < length assert;
mu_ge (AbstractMuSpaceCost (assert ! i)) (build_si E1.0 h (varsAPP Σd f))
m |]
==> mu_ge \<Squnion>c map AbstractMuSpaceCost assert
(build_si E1.0 h (varsAPP Σd f)) m
lemma all_i_defined_bound_all_si_in_dom_sigma:
∀i<length xs. defined_bound (AbstractSigmaSpaceCost (xs ! i)) f
==> ∀i<length xs.
build_si E1.0 h (varsAPP Σd f) ∈ dom (AbstractSigmaSpaceCost (xs ! i))
lemma all_i_si_in_dom_sigma_si_in_dom_maxCost_sigma:
∀i<length xs.
build_si E1.0 h (varsAPP Σd f) ∈ dom (AbstractSigmaSpaceCost (xs ! i))
==> build_si E1.0 h (varsAPP Σd f)
∈ (INT i<length xs. dom (AbstractSigmaSpaceCost (xs ! i)))
lemma dom_maxCostSigmaList:
length xs = length ys -->
dom (foldr maxCost
(map (λ(x, y). addCostReal x y)
(zip (map AbstractSigmaSpaceCost xs) (map num_r ys)))
[]0) =
(INT i<length xs. dom (AbstractSigmaSpaceCost (xs ! i)))
lemma si_dom_sigma_si_dom_maxCost_sigma:
[| length xs = length ys;
∀i<length xs.
build_si E1.0 h (varsAPP Σd f) ∈ dom (AbstractSigmaSpaceCost (xs ! i)) |]
==> build_si E1.0 h (varsAPP Σd f)
∈ dom (foldr maxCost
(map (λ(x, y). addCostReal x y)
(zip (map AbstractSigmaSpaceCost xs) (map num_r ys)))
[]0)
lemma maxAbstractSigmaSpaceCost_ge_AbstractSigmaSpaceCost:
[| length assert = length alts;
!!i. i < length assert
==> defined_bound (AbstractSigmaSpaceCost (assert ! i)) f;
i < length assert |]
==> the (AbstractSigmaSpaceCost (assert ! i) (build_si E1.0 h (varsAPP Σd f)))
≤ the (\<Squnion>c map (λ(x, y). addCostReal x y)
(zip (map AbstractSigmaSpaceCost assert)
(map num_r alts))
(build_si E1.0 h (varsAPP Σd f)))
lemma maxAbstractSigmaSpaceCost_ge_AbstractSigmaSpaceCost_2:
[| length assert = length alts;
!!i. i < length assert
==> defined_bound (AbstractSigmaSpaceCost (assert ! i)) f;
i < length assert |]
==> the (AbstractSigmaSpaceCost (assert ! i) (build_si E1.0 h (varsAPP Σd f))) +
num_r (alts ! i)
≤ the (\<Squnion>c map (λ(x, y). addCostReal x y)
(zip (map AbstractSigmaSpaceCost assert)
(map num_r alts))
(build_si E1.0 h (varsAPP Σd f)))
lemma P_σ_Case_Lit:
[| i < length assert; length assert = length alts;
∀i<length assert. defined_bound (AbstractSigmaSpaceCost (assert ! i)) f;
sigma_ge (AbstractSigmaSpaceCost (assert ! i))
(build_si E1.0 h (varsAPP Σd f)) s |]
==> sigma_ge
\<Squnion>c map (λ(x, y). addCostReal x y)
(zip (map AbstractSigmaSpaceCost assert) (map num_r alts))
(build_si E1.0 h (varsAPP Σd f)) s
lemma AbstractSigmaSpaceCost_Case_equals_AbstractSigmaSpaceCost_alt:
[| set (varsAPP Σd f) ⊆ dom E1.0;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> the (AbstractSigmaSpaceCost (assert ! i)
(build_si (extend E1.0 (snd (extractP (fst (alts ! i)))) vs) h
(varsAPP Σd f))) =
the (AbstractSigmaSpaceCost (assert ! i) (build_si E1.0 h (varsAPP Σd f)))
lemma P_σ_Case:
[| i < length assert; length assert = length alts; s = s' + nr;
nr = real (length vs); set (varsAPP Σd f) ⊆ dom E1.0;
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs;
∀i<length assert. defined_bound (AbstractSigmaSpaceCost (assert ! i)) f;
sigma_ge (AbstractSigmaSpaceCost (assert ! i))
(build_si (extend E1.0 (snd (extractP (fst (alts ! i)))) vs) h
(varsAPP Σd f))
s' |]
==> sigma_ge
\<Squnion>c map (λ(x, y). addCostReal x y)
(zip (map AbstractSigmaSpaceCost assert) (map num_r alts))
(build_si E1.0 h (varsAPP Σd f)) s
lemma P1_f_n_CASE:
[| E1.0 x = Some (Loc p);
(E1.0,
E2.0) \<turnstile> h , k , td , Case VarE x
() Of alts () \<Down> (f, n) hh , k , v , (δ, m, s) |]
==> ∃j C vs nr s'.
h p = Some (j, C, vs) ∧
s = s' + nr ∧
nr = real (length vs) ∧
(∃i<length alts.
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs ∧
(extend E1.0 (snd (extractP (fst (alts ! i)))) vs,
E2.0) \<turnstile> h , k , (td +
nr) , snd (alts ! i) \<Down> (f, n) hh , k , v , (δ, m, s') )
lemma P1_f_n_CASE_1_1:
[| E1.0 x = Some (IntT n');
(E1.0,
E2.0) \<turnstile> h , k , td , Case VarE x
() Of alts () \<Down> (f, n) hh , k , v , (δ, m, s) |]
==> ∃i<length alts.
(E1.0,
E2.0) \<turnstile> h , k , td , snd
(alts ! i) \<Down> (f, n) hh , k , v , (δ, m, s) ∧
fst (alts ! i) = ConstP (LitN n')
lemma P1_f_n_CASE_1_2:
[| E1.0 x = Some (BoolT b);
(E1.0,
E2.0) \<turnstile> h , k , td , Case VarE x
() Of alts () \<Down> (f, n) hh , k , v , (δ, m, s) |]
==> ∃i<length alts.
(E1.0,
E2.0) \<turnstile> h , k , td , snd
(alts ! i) \<Down> (f, n) hh , k , v , (δ, m, s) ∧
fst (alts ! i) = ConstP (LitB b)
lemma nr_Case:
[| nr = real (length vs);
def_extend E1.0 (snd (extractP (fst (alts ! i)))) vs |]
==> td + nr = td + num_r (alts ! i)
lemma SafeResourcesDADepth_CASE:
[| length alts = length assert; 0 < length alts;
∀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) :f (ϑ1.0,
ϑ2.0) φ td +
real (length
(snd (extractP
(fst (alts !
i))))) , n \<lbrace> AbstractDeltaSpaceCost
(assert !
i) , AbstractMuSpaceCost
(assert !
i) , AbstractSigmaSpaceCost (assert ! i) \<rbrace>;
Δ = \<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' :f (ϑ1.0,
ϑ2.0) φ td , n \<lbrace> Δ , μ , σ \<rbrace>
lemma lemma_19_aux:
[| \<Turnstile>\<Turnstile> Σb ; Σb g = Some (projection g Δg, μg, σg);
Σd g = Some (xs, rs, eg) |]
==> bodyAPP Σd
g :g typesAPP Σϑ
g sizesAPP ΣΦ
g real (length (varsAPP Σd g) +
length
(regionsAPP Σd g)) \<lbrace> Δg , μg , σg \<rbrace>
lemma equiv_SafeResourcesDAss_all_n_SafeResourcesDAssDepth:
e :f typesAPP Σϑ f sizesAPP ΣΦ f td \<lbrace> Δ , μ , σ \<rbrace>
==> ∀n. e :f typesAPP Σϑ
f sizesAPP ΣΦ f td , n \<lbrace> Δ , μ , σ \<rbrace>
lemma lemma_19:
[| \<Turnstile>\<Turnstile>f , n Σb ; Σd g = Some (xs, rs, eg);
Σb g = Some (projection g Δg, μg, σg); g ≠ f |]
==> eg :g typesAPP Σϑ
g sizesAPP ΣΦ
g real (length xs) +
real (length rs) \<lbrace> Δg , μg , σg \<rbrace>
lemma lemma_20:
[| \<Turnstile>\<Turnstile>f , n Σb ; Σd f = Some (xs, rs, ef);
Σb f = Some (projection f Δf, μf, σf); n = Suc n' |]
==> ef :f typesAPP Σϑ
f sizesAPP ΣΦ
f real (length xs) +
real (length rs) , n' \<lbrace> Δf , μf , σf \<rbrace>
lemma P1_f_n_APP:
[| (E1.0,
E2.0) \<turnstile> h , k , td , AppE f as rs'
a \<Down> (f, n) hh , k , v , (δ, m, s) ;
primops f = None; Σd f = Some (xs, rs, ef) |]
==> ∃h' δ' s'.
(map_of (zip xs (map (atom2val E1.0) as)),
map_of (zip rs (map (the o E2.0) rs'))(self |->
Suc k)) \<turnstile> h , Suc k , (real (length as) +
real (length rs')) , ef \<Down> (f, n) h' , Suc k , v , (δ', m, s') ∧
s = max (real (length xs) + real (length rs))
(s' + real (length xs) + real (length rs) - td) ∧
δ = δ'(k + 1 := None) ∧
length xs = length as ∧
distinct xs ∧
length rs = length rs' ∧
distinct rs ∧
hh = h' |` {p : dom h'. fst (the (h' p)) ≤ k} ∧
dom E1.0 ∩ set xs = {} ∧ 0 < n
lemma P1_f_n_APP_2:
[| (E1.0,
E2.0) \<turnstile> h , k , td , AppE g as rs'
a \<Down> (f, n) hh , k , v , (δ, m, s) ;
primops g = None; f ≠ g; Σd g = Some (xs, rs, eg) |]
==> ∃h' δ' s'.
(map_of (zip xs (map (atom2val E1.0) as)),
map_of (zip rs (map (the o E2.0) rs'))(self |->
Suc k)) \<turnstile> h , Suc k , (real (length as) +
real (length rs')) , eg \<Down> (f, n) h' , Suc k , v , (δ', m, s') ∧
s = max (real (length xs) + real (length rs))
(s' + real (length xs) + real (length rs) - td) ∧
δ = δ'(k + 1 := None) ∧
length xs = length as ∧
distinct xs ∧
length rs = length rs' ∧
distinct rs ∧
hh = h' |` {p : dom h'. fst (the (h' p)) ≤ k} ∧ dom E1.0 ∩ set xs = {}
lemma P1_f_n_ge_0_APP:
[| (E1.0,
E2.0) \<turnstile> h , k , td , AppE f as rs'
a \<Down> (f,
Suc n) hh , k , v , (δ, m, s) ;
primops f = None; Σd f = Some (xs, rs, ef) |]
==> ∃h' δ' s'.
(map_of (zip xs (map (atom2val E1.0) as)),
map_of (zip rs (map (the o E2.0) rs'))(self |->
Suc k)) \<turnstile> h , Suc k , (real (length as) +
real (length rs')) , ef \<Down> (f, n) h' , Suc k , v , (δ', m, s') ∧
s = max (real (length xs) + real (length rs))
(s' + real (length xs) + real (length rs) - td) ∧
δ = δ'(k + 1 := None) ∧
length xs = length as ∧
distinct xs ∧
length rs = length rs' ∧
distinct rs ∧
hh = h' |` {p : dom h'. fst (the (h' p)) ≤ k} ∧ dom E1.0 ∩ set xs = {}
lemma dom_map_of_zip:
length xs = length ys ==> set xs ⊆ dom (map_of (zip xs ys))
lemma xs_in_dom_f:
[| length xs = length ys; ∀i<length ys. f (xs ! i) = g (ys ! i);
set ys ⊆ dom g |]
==> ∀i<length xs. xs ! i ∈ dom f
lemma nth_in_dom_map:
set xs ⊆ dom m ==> ∀i<length xs. xs ! i ∈ dom m
lemma set_xs_subseteq_dom_m:
[| x ∈ set xs; ∀i<length xs. xs ! i ∈ dom m |] ==> x ∈ dom m
lemma dom_instance_f:
dom (instance_f f Δg φ as rs Φ) = set (R_Args Σt f) ∪ {ρself_f f}
lemma dom_η_ef:
[| Σd g = Some (xs, rs, eg); fvReg (AppE g as rs' ()) ⊆ dom E2.0;
(E1.0,
E2.0) \<turnstile> h , k , td , AppE g as rs'
() \<Down> (f, n) hh , k , v , (δ, m, s) ;
valid Σd Σϑ ΣΦ; admissible f η k; f ∈ dom Σd;
argP φ (R_Args Σt g) (typesRegsAPP Σϑ f) rs' |]
==> dom (η_ef η φ (R_Args Σt g) ++ [ρself_f g |-> Suc k]) =
set (R_Args Σt g) ∪ {ρself_f g}
lemma P_dyn_xs_subseteq_dom_E1_g:
[| Σd g = Some (xs, rs, eg); fv eg ⊆ set xs; ∀i<length as. atom (as ! i);
length xs = length as |]
==> set (varsAPP Σd g) ∪ fv eg ⊆ dom (map_of (zip xs (map (atom2val E1.0) as)))
lemma P_dyn_fvReg_eg_subseteq_dom_E2_g:
[| fvReg eg ⊆ set rs; length rs = length rs'; set rs' ⊆ dom E2.0 |]
==> fvReg eg ⊆ dom (map_of (zip rs (map (the o E2.0) rs'))(self |-> Suc k))
lemma P_dyn_dom_η_ef:
[| Σd g = Some (xs, rs, eg); fvReg (AppE g as rs' ()) ⊆ dom E2.0;
(E1.0,
E2.0) \<turnstile> h , k , td , AppE g as rs'
() \<Down> (f, n) hh , k , v , (δ, m, s) ;
valid Σd Σϑ ΣΦ; argP ψ (R_Args Σt g) (typesRegsAPP Σϑ f) rs';
admissible f η k; f ∈ dom Σd; set (R_Args Σt g) ∪ {ρself_f g} = dom Δg;
dom (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) = dom η |]
==> dom Δg = dom (η_ef η ψ (R_Args Σt g) ++ [ρself_f g |-> Suc k])
lemma P_η_ef:
admissible f η k
==> admissible g (η_ef η φ (R_Args Σt g) ++ [ρself_f g |-> Suc k]) (Suc k)
lemma length_phiMapping_equals_length_as:
atom2var ` set as ⊆ dom Φ
==> length (phiMapping_app (map Φ (map atom2var as)) si) = length as
lemma length_build_si:
length (build_si E1.0 h xs) = length xs
lemma valid_fv_APP_subseteq_Φ:
[| (E1.0,
E2.0) \<turnstile> h , k , td , AppE g as rs'
() \<Down> (f, n) hh , k , v , (δ, m, s) ;
valid Σd Σϑ ΣΦ; f ∈ dom Σd |]
==> fv (AppE g as rs' ()) ⊆ dom (sizesAPP ΣΦ f)
lemma as_subseteq_dom_Φ:
[| fvs' as ⊆ dom Φ; !!i. i < length as ==> atom (as ! i) |]
==> atom2var ` set as ⊆ dom Φ
lemma nth_map_of_xs_atom2val:
[| length xs = length as; distinct xs |]
==> ∀i<length xs.
map_of (zip xs (map (atom2val E1.0) as)) (xs ! i) =
Some (atom2val E1.0 (as ! i))
lemma nth_atom2val_in_dom_E:
[| atom2var ` set as ⊆ dom E1.0; i < length as; as ! i = VarE x a |]
==> Some (atom2val E1.0 (as ! i)) = E1.0 x
lemma nth_build_si:
i < length xs ==> build_si E1.0 h xs ! i = sizeEnv E1.0 (xs ! i) h
lemma sizeEnv_equals_build_si_i:
[| length xs = length as; distinct xs; ∀i<length as. atom (as ! i);
Σd g = Some (xs, rs, eg); i < length as; atom2var ` set as ⊆ dom E1.0 |]
==> sizeEnv E1.0 (map atom2var as ! i) h =
build_si (map_of (zip xs (map (atom2val E1.0) as))) h (varsAPP Σd g) ! i
lemma fv_as_in_dom_E1:
[| fvs' as ⊆ dom E1.0; !!i. i < length as ==> atom (as ! i) |]
==> atom2var ` set as ⊆ dom E1.0
lemma nth_phiMapping_app:
set ys ⊆ dom φ
==> ∀i<length ys. phiMapping_app (map φ ys) si ! i = the (the (φ (ys ! i)) si)
lemma list_ge_phiMapping_app_build_si:
[| ∀i<length as. atom (as ! i); length xs = length as; distinct xs;
fv (AppE g as rs' a) ⊆ dom E1.0;
(E1.0,
E2.0) \<turnstile> h , k , td , AppE g as rs'
() \<Down> (f, n) hh , k , v , (δ, m, s) ;
admissible f η k; f ∈ dom Σd; Σd g = Some (xs, rs, eg); valid Σd Σϑ ΣΦ |]
==> list_ge
(phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as))
(build_si E1.0 h (varsAPP Σd f)))
(build_si (map_of (zip xs (map (atom2val E1.0) as))) h (varsAPP Σd g))
lemma Phi_Mapping_app_ge_build_si_ef:
[| (E1.0,
E2.0) \<turnstile> h , k , td , AppE g as rs'
() \<Down> (f, n) hh , k , v , (δ, m, s) ;
∀i<length as. atom (as ! i); length xs = length as; distinct xs;
valid Σd Σϑ ΣΦ; Σd g = Some (xs, rs, ef); fv (AppE g as rs' a) ⊆ dom E1.0;
monotonic_bound μg; f ∈ dom Σd; admissible f η k; defined_bound μg g |]
==> the (μg (build_si (map_of (zip xs (map (atom2val E1.0) as))) h
(varsAPP Σd g)))
≤ the (μg (phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as))
(build_si E1.0 h (varsAPP Σd f))))
lemma P_μ_APP:
[| (E1.0,
E2.0) \<turnstile> h , k , td , AppE g as rs'
() \<Down> (f, n) hh , k , v , (δ, m, s) ;
∀i<length as. atom (as ! i); distinct xs; length xs = length as;
monotonic_bound μg; defined_bound μg g; Σd g = Some (xs, rs, ef); f ∈ dom Σd;
admissible f η k; valid Σd Σϑ ΣΦ;
set (varsAPP Σd f) ∪ fv (AppE g as rs' ()) ⊆ dom E1.0;
mu_ge μg
(build_si (map_of (zip xs (map (atom2val E1.0) as))) h (varsAPP Σd g)) m |]
==> mu_ge (mu_app μg as (sizesAPP ΣΦ f)) (build_si E1.0 h (varsAPP Σd f)) m
lemma fvs_in_dom_sizesAPP:
[| ∀i<length as. atom (as ! i);
(E1.0,
E2.0) \<turnstile> h , k , td , AppE g as rs'
() \<Down> (f, n) hh , k , v , (δ, m, s) ;
f ∈ dom Σd; admissible f η k; valid Σd Σϑ ΣΦ |]
==> atom2var ` set as ⊆ dom (sizesAPP ΣΦ f)
lemma P_σ_APP:
[| (E1.0,
E2.0) \<turnstile> h , k , td , AppE g as rs'
() \<Down> (f, n) hh , k , v , (δ, m, s) ;
∀i<length as. atom (as ! i); length xs = length as; distinct xs;
valid Σd Σϑ ΣΦ; Σd g = Some (xs, rs, ef); fv (AppE g as rs' a) ⊆ dom E1.0;
monotonic_bound σg; f ∈ dom Σd; admissible f η k; defined_bound σg g;
s = max (l + q) (s' + l + q - td);
sigma_ge σg
(build_si (map_of (zip xs (map (atom2val E1.0) as))) h (varsAPP Σd g)) s' |]
==> sigma_ge
\<Squnion>c { []l + q , substCostReal
(addCostReal
(addCostReal (sigma_app σg as (sizesAPP ΣΦ f))
l)
q)
td }
(build_si E1.0 h (varsAPP Σd f)) s
lemma setsumCost_empty:
setsumCost f {} = []0
lemma sumcost_conm:
x +c y = y +c x
lemma sumcost_dist:
x +c y +c z = x +c y +c z
lemma setsumCost_insert:
[| finite F; a ∉ F |] ==> setsumCost f (insert a F) = f a +c setsumCost f F
lemma sumset_instance_f_equals_sumset_phiMapping:
dom (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) = dom η
==> (∑ρ | η ρ = Some j.
the (the (instance_f f g Δg ψ (sizesAPP ΣΦ f) as ρ)
(build_si E1.0 h (varsAPP Σd f)))) =
(∑ρ | η ρ = Some j.
∑ρ∈{ρ'. ψ ρ' = Some ρ ∧
ρ' ∈ set (R_Args Σt
g)}. the (the (Δg ρ)
(phiMapping_app
(map (sizesAPP ΣΦ f) (map atom2var as)) (build_si E1.0 h (varsAPP Σd f)))))
lemma setsum_build_si_le_setsum_phiMapping:
[| (E1.0,
E2.0) \<turnstile> h , k , td , AppE g as rs'
() \<Down> (f, n) hh , k , v , (δ, m, s) ;
∀i<length as. atom (as ! i); length xs = length as; distinct xs;
valid Σd Σϑ ΣΦ; Σd g = Some (xs, rs, ef); fv (AppE g as rs' a) ⊆ dom E1.0;
monotonic_AbstractDelta Δg; f ∈ dom Σd; admissible f η k;
set (R_Args Σt g) ∪ {ρself_f g} = dom Δg;
dom (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) = dom η;
defined_AbstractDelta Δg g |]
==> (∑ρ | η ρ = Some j.
∑ρ∈{ρ'. ψ ρ' = Some ρ ∧
ρ' ∈ set (R_Args Σt
g)}. the (the (Δg ρ)
(build_si
(map_of (zip xs (map (atom2val E1.0) as))) h (varsAPP Σd g))))
≤ (∑ρ | η ρ = Some j.
∑ρ∈{ρ'. ψ ρ' = Some ρ ∧
ρ' ∈ set (R_Args Σt
g)}. the (the (Δg ρ)
(phiMapping_app (map (sizesAPP ΣΦ f) (map atom2var as))
(build_si E1.0 h (varsAPP Σd f)))))
lemma sizeAbstractDelta_si_APP_ge_sizeAbstractDelta_si_eg:
[| (E1.0,
E2.0) \<turnstile> h , k , td , AppE g as rs'
() \<Down> (f, n) hh , k , v , (δ, m, s) ;
∀i<length as. atom (as ! i); length xs = length as; distinct xs;
valid Σd Σϑ ΣΦ; Σd g = Some (xs, rs, ef); fv (AppE g as rs' a) ⊆ dom E1.0;
monotonic_AbstractDelta Δg; f ∈ dom Σd; admissible f η k;
set (R_Args Σt g) ∪ {ρself_f g} = dom Δg;
dom (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) = dom η;
defined_AbstractDelta Δg g |]
==> sizeAbstractDelta_si Δg
(build_si (map_of (zip xs (map (atom2val E1.0) as))) h (varsAPP Σd g)) j
(η_ef η ψ (R_Args Σt g)(ρself_f g |-> Suc k))
≤ sizeAbstractDelta_si (instance_f f g Δg ψ (sizesAPP ΣΦ f) as)
(build_si E1.0 h (varsAPP Σd f)) j η
lemma P_Δ_APP:
[| (E1.0,
E2.0) \<turnstile> h , k , td , AppE g as rs'
() \<Down> (f, n) hh , k , v , (δ, m, s) ;
∀i<length as. atom (as ! i); length xs = length as; distinct xs;
valid Σd Σϑ ΣΦ; Σd g = Some (xs, rs, ef); fv (AppE g as rs' a) ⊆ dom E1.0;
monotonic_AbstractDelta Δg; f ∈ dom Σd; admissible f η k;
defined_AbstractDelta Δg g; set (R_Args Σt g) ∪ {ρself_f g} = dom Δg;
Delta_ge Δg
(build_si (map_of (zip xs (map (atom2val E1.0) as))) h (varsAPP Σd g))
(Suc k) (η_ef η ψ (R_Args Σt g) ++ [ρself_f g |-> Suc k]) δ';
dom (instance_f f g Δg ψ (sizesAPP ΣΦ f) as) = dom η;
δ = δ'(k + 1 := None) |]
==> Delta_ge (instance_f f g Δg ψ (sizesAPP ΣΦ f) as)
(build_si E1.0 h (varsAPP Σd f)) k η δ
lemma SafeResourcesDADepth_APP:
[| ∀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; Σ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';
Δ = 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 };
\<Turnstile>\<Turnstile>f , n Σb |]
==> AppE g as rs'
a :f typesAPP Σϑ f sizesAPP ΣΦ f td , n \<lbrace> Δ , μ , σ \<rbrace>