Up to index of Isabelle/HOL/Bounds
theory Costes_definitions(* Title:
Author: Ricardo Pe{\~n}a and Javier de Dios
Copyright: June 2010, Universidad Complutense de Madrid
*)
header {* Definitions for certifying memory bounds *}
theory Costes_definitions
imports SafeRASemanticsReal SafeDepthSemanticsReal
"~~/src/HOL/Real/Real"
begin
(* ρ *)
types RegionTypeVariable = "string"
(* ρself *)
constdefs
ρself :: RegionTypeVariable
"ρself ≡ ''rho_self''"
constdefs ρself_f :: "FunName => RegionTypeVariable"
"ρself_f f ≡ ρself @ ''_'' @ f"
(* Polynomial *)
types Cost = "real list \<rightharpoonup> real"
(* Types of abstract resources *)
types AbstractDelta = "RegionTypeVariable \<rightharpoonup> Cost"
AbstractMu = "Cost"
AbstractSigma = "Cost"
types VarType = "string"
(* Type Expressions *)
datatype TypeExpression = VarT VarType
| ConstrT string "TypeExpression list" "VarType list"
(* Function Signatures *)
types FunctionResourcesSignature = "FunName \<rightharpoonup> AbstractDelta × AbstractMu
× AbstractSigma"
FunctionTypesSignature = "FunName \<rightharpoonup> (TypeExpression list × VarType list
× TypeExpression)"
FunctionDefinitionSignature= "FunName \<rightharpoonup> (ProgVar list × RegVar list
× unit Exp)"
(* Region Enviroment type *)
types RegionEnv = "string \<rightharpoonup> TypeExpression list × VarType list × TypeExpression"
consts Σt :: FunctionTypesSignature
(* constructorSignature *)
types ConstructorSignatureFun = "string \<rightharpoonup> TypeExpression list × VarType
× TypeExpression"
consts constructorSignature :: ConstructorSignatureFun
(* PhiMapping *)
types PhiMapping = "(string \<rightharpoonup> Cost)"
(* ϑ (x) = T ti ρi *)
types TypeMapping = "(string \<rightharpoonup> TypeExpression)"
types RegMapping = "(string \<rightharpoonup> string)"
types ThetaMapping = "TypeMapping × RegMapping"
(* η *)
types InstantiationMapping = "VarType \<rightharpoonup> nat"
(* (μ1,μ2) *)
types TypeMu = "(string \<rightharpoonup> TypeExpression) × (string \<rightharpoonup> string)"
(* mu_ext *)
consts mu_ext :: "TypeMu => TypeExpression => TypeExpression"
mu_exts :: "TypeMu => TypeExpression list => TypeExpression list"
primrec
"mu_ext μ (VarT a) = the ((fst μ) a)"
"mu_ext μ (ConstrT T tm ρs) = (ConstrT T (mu_exts μ tm) (map (the o (snd μ)) ρs))"
"mu_exts μ [] = []"
"mu_exts μ (x#xs) = mu_ext μ x # (mu_exts μ xs)"
(* Regions of ϑ
fun regionsThetaMapping :: "ThetaMapping => RegionTypeVariable set"
where
"regionsThetaMapping (ϑ1,ϑ2) = (\<Union>t ∈ ran ϑ1. regions t) ∪ ran ϑ2"
*)
(* Get recursive positions of value list *)
constdefs
RecPos :: "Val list => TypeExpression list => TypeExpression => Val list"
"RecPos vn tn t == map fst (filter (λ(vi,ti). ti=t) (zip vn tn))"
(* Get size of value in a heap *)
function size :: "Val => HeapMap => real"
where
"size (IntT i) h = 0"
| "size (BoolT b) h = 0"
| "size (Loc p) h = (case (h p) of Some (j,C,vn) =>
(case Σt C of Some (ti,ρs,t)
=> 1 + (∑ v ∈ set (RecPos vn ti t). size v h)
| _ => 0)
| _ => 0)"
by pat_completeness auto
(* Get size of an environment variable in a heap *)
constdefs sizeEnv :: "(ProgVar \<rightharpoonup> Val) => ProgVar => HeapMap => real"
"sizeEnv E x h ≡ (case E x of Some v => size v h
| _ => 0)"
(* Δ is upper bound for δ *)
constdefs
sizeAbstractDelta_si :: "AbstractDelta => real list => nat => InstantiationMapping
=> real"
"sizeAbstractDelta_si Δ si j η ≡ ∑ρ∈{ρ. η ρ = Some j}. the (the (Δ ρ) si)"
constdefs
Delta_ge :: "AbstractDelta => real list => nat => InstantiationMapping
=> Delta => bool"
"Delta_ge Δ si k η δ ≡ (∀ j ∈ {0..k}. sizeAbstractDelta_si Δ si j η ≥ the (δ j))"
(* μ is upper bound for m *)
constdefs
mu_ge :: "AbstractMu => real list => MinimumFreshCells => bool"
"mu_ge μ si m ≡ the (μ si) ≥ m"
(* σ is upper bound for s *)
constdefs
sigma_ge :: "AbstractSigma => real list => MinimumWords => bool"
"sigma_ge σ si s == the (σ si) ≥ s"
(* Auxiliary function to build si *)
fun build_si :: "(ProgVar \<rightharpoonup> Val) => HeapMap => ProgVar list => real list"
where
"build_si E h [] = []"
| "build_si E h (x#xs) = (sizeEnv E x h) # build_si E h xs"
(* Δ, μ and σ are defined for sizes *)
constdefs defined :: "AbstractDelta => AbstractMu => AbstractSigma => real list => bool"
"defined Δ μ σ si ≡
(∀ ρ ∈ dom Δ. (∀ si'. length si = length si' --> si' ∈ dom (the (Δ ρ))))
∧ (∀ si'. length si = length si' --> si' ∈ dom μ)
∧ (∀ si'. length si = length si' --> si' ∈ dom σ)"
types FunTypesEnv = "string \<rightharpoonup> ThetaMapping"
FunSizesEnv = "string \<rightharpoonup> PhiMapping"
(* Global types and sizes environments *)
consts Σϑ :: FunTypesEnv
consts ΣΦ :: FunSizesEnv
constdefs typesVarsAPP :: "FunTypesEnv => string => TypeMapping"
"typesVarsAPP Σ f ≡ (case Σ f of Some (ϑ1,ϑ2) => ϑ1)"
constdefs typesRegsAPP :: "FunTypesEnv => string => RegMapping"
"typesRegsAPP Σ f ≡ (case Σ f of Some (ϑ1,ϑ2) => ϑ2)"
constdefs typesAPP :: "FunTypesEnv => string => ThetaMapping"
"typesAPP Σ f ≡ (typesVarsAPP Σ f,typesRegsAPP Σ f)"
constdefs typesArgAPP :: "RegionEnv => string => TypeExpression list"
"typesArgAPP Σ f == (case Σ f of Some (ti,ρs,tf) => ti)"
constdefs regionsArgAPP :: "RegionEnv => string => string list"
"regionsArgAPP Σ f ≡ (case Σ f of Some (ti,ρs,tf) => ρs)"
constdefs typeResAPP :: "RegionEnv => string => TypeExpression"
"typeResAPP Σ f ≡ (case Σ f of Some (ti,ρs,tf) => tf)"
constdefs sizesAPP :: "FunSizesEnv => string => PhiMapping"
"sizesAPP Σ f ≡ (case Σ f of Some φ => φ)"
constdefs R_Args :: " RegionEnv => FunName => string list"
"R_Args Σ f ≡ (case Σ f of Some (ts,ρs,t) => ρs)"
(* admissible *)
constdefs
admissible :: "FunName => InstantiationMapping => nat => bool"
"admissible f η k ≡
ρself_f f ∈ dom η ∧
(∀ ρ ∈ dom η.
∃ k'.
η ρ = Some k' ∧
(ρ = ρself_f f --> k' = k) ∧
(ρ ≠ ρself_f f --> k' < k))"
(* regions *)
consts regions :: "TypeExpression => string set"
regions' :: "TypeExpression list => string set"
primrec
"regions (VarT a) = {}"
"regions (ConstrT T tm ρs) = (regions' tm) ∪ set ρs"
"regions' [] = {}"
"regions' (t#ts) = regions t ∪ regions' ts"
(* variables *)
consts variables :: "TypeExpression => string set"
variables' :: "TypeExpression list => string set"
primrec
"variables (VarT a) = {a}"
"variables (ConstrT T tm ρs) = (variables' tm)"
"variables' [] = {}"
"variables' (t#ts) = variables t ∪ variables' ts"
(* wellT *)
fun
wellT :: " TypeExpression list => VarType => TypeExpression => bool"
where
"wellT tn ρ (ConstrT T tm ρs) =
((length ρs > 0 ∧ ρ = last ρs ∧ distinct ρs ∧ last ρs ∉ regions' tm)
∧ (∀ i < length tn. regions (tn!i) ⊆ regions (ConstrT T tm ρs) ∧
variables (tn!i) ⊆ variables (ConstrT T tm ρs)))"
(* consistent_v *)
inductive
consistent_v :: "[TypeExpression, InstantiationMapping, Val, HeapMap ] => bool"
where
primitiveI : "consistent_v (ConstrT intType [] []) η (IntT i) h"
| primitiveB : "consistent_v (ConstrT boolType [] []) η (BoolT b) h"
| variable : "consistent_v (VarT a) η v h"
| algebraic_None : "p ∉ dom h ==> consistent_v t η (Loc p) h"
| algebraic : "[| h p = Some (j,C,vn);
ρl = last ρs;
ρl ∈ dom η; η (ρl) = Some j;
constructorSignature C = Some (tn',ρ',ConstrT T tm' ρs');
wellT tn' (last ρs') (TypeExpression.ConstrT T tm' ρs');
length vn = length tn';
∃ μ1 μ2. (((the (μ2 (last ρs'))), mu_ext (μ1,μ2) (ConstrT T tm' ρs')) =
(ρl,ConstrT T tm ρs) ∧
(∀ i < length vn. consistent_v ((map (mu_ext (μ1,μ2)) tn')!i) η (vn!i) h)) |]
==> consistent_v (ConstrT T tm ρs) η (Loc p) h"
(* consistent *)
fun
consistent :: "ThetaMapping => InstantiationMapping => Environment => HeapMap => bool"
where
"consistent (ϑ1,ϑ2) η (E1,E2) h =
((∀ x ∈ dom E1. ∃ t v. ϑ1 x = Some t
∧ E1 x = Some v
∧ consistent_v t η v h)
∧ (∀ r ∈ dom E2 . ∃ r' r''. ϑ2 r = Some r'
∧ η r' = Some r''
∧ E2 r = Some r'')
∧ self ∈ dom E2
∧ ϑ2 self = Some ρself)"
fun valid_f :: "FunName => ThetaMapping => PhiMapping => bool"
where
"valid_f f (ϑ1,ϑ2) Φ =
(∀ e. (set (varsAPP Σd f)) ∪ fv (e ()::unit Exp) ⊆ dom ϑ1
∧ fvReg (e ()::unit Exp) ∪ {ρself_f f} ⊆ dom ϑ2
∧ (set (varsAPP Σd f)) ∪ fv (e ()::unit Exp) ⊆ dom Φ
∧ (∀ E1 E2 h k td hh v r η si .
SafeRASem (E1,E2) h k td (e ()::unit Exp) hh k v r
∧ si = build_si E1 h (varsAPP Σd f)
∧ admissible f η k
--> consistent (ϑ1,ϑ2) η (E1,E2) h
∧ (∀ y ∈ dom Φ. the ((the (Φ y)) si) >= sizeEnv E1 y h)))"
constdefs valid :: " FunDefEnv => FunTypesEnv => FunSizesEnv => bool"
"valid Σ_d Σ_ϑ Σ_Φ ≡ (∀ f ∈ dom Σ_d. valid_f f (typesAPP Σ_ϑ f) (sizesAPP Σ_Φ f))"
declare valid_f.simps [simp del]
declare valid_def [simp del]
(* Assert definition *)
fun SafeResourcesDAss::
"unit Exp =>
FunName => ThetaMapping => PhiMapping => real =>
AbstractDelta => AbstractMu => AbstractSigma => bool"
("_ :_ _ _ _ \<lbrace> _ , _ , _ \<rbrace>" 1000)
where
" SafeResourcesDAss e f (ϑ1,ϑ2) Φ td Δ μ σ =
(valid Σd Σϑ ΣΦ --> (* valid *)
(set (R_Args Σt f)) ∪ {ρself_f f} = dom Δ (* P_static *)
∧ (∀ E1 E2 h k hh v δ m s η si.
SafeRASemanticsReal.SafeRASem (E1,E2) h k td e hh k v (δ,m,s)
∧ (set (varsAPP Σd f))∪fv e ⊆ dom E1 ∧ fvReg e ⊆ dom E2 (* P_dyn *)
∧ dom Δ = dom η
∧ si = build_si E1 h (varsAPP Σd f) (* P_size *)
∧ admissible f η k (* P_η *)
--> Delta_ge Δ si k η δ (* P_Δ *)
∧ mu_ge μ si m (* P_μ *)
∧ sigma_ge σ si s))" (* P_σ *)
(* Auxiliary definitions *)
constdefs regionsType :: "string => string set"
"regionsType f ≡ (case Σt f of Some (ti, ρs, t) => regions' ti ∪ regions t ∪ set ρs)"
constdefs constantCost :: "real => Cost" ("[]_" 1000)
"constantCost r ≡ (λxs. Some r)"
constdefs emptyAbstractDelta :: "string => AbstractDelta"
("[]_" 1000)
"emptyAbstractDelta f ==
(%ρ . if ρ ∈ (set (R_Args Σt f)) ∪ {ρself_f f}
then Some []0
else None)"
(**** Definitions for LET ***)
fun foldr1 :: "('a => 'a => 'a) => 'a list => 'a"
where
"foldr1 f [x] = x"
| "foldr1 f (x#xs) = f x (foldr1 f xs)"
constdefs addCost :: "Cost => Cost => Cost" (" _ +c _ " 1000)
"c1 +c c2 ≡ (λ x. if (x ∈ dom c1 ∩ dom c2) then Some (the (c1 x) + the (c2 x))
else None)"
constdefs addCostList :: "Cost list => Cost"
"addCostList ≡ foldr1 addCost"
constdefs addAbstractDelta :: "AbstractDelta => AbstractDelta => AbstractDelta"
(" _ +Δ _ " 1000)
"addAbstractDelta Δ1 Δ2 ==
(%ρ . if (ρ ∈ dom Δ1 ∩ dom Δ2)
then Some ((the (Δ1 ρ)) +c (the (Δ2 ρ)))
else None)"
constdefs addCostReal :: "Cost => real => Cost"
"addCostReal c r ≡ (λ x. if x ∈ dom c then Some (the (c x) + r)
else None)"
constdefs substCostReal :: "Cost => real => Cost"
"substCostReal c r ≡ (λ x. if x ∈ dom c then Some (the (c x) - r)
else None)"
constdefs maxCost :: "Cost => Cost => Cost" ("\<Squnion>c { _ , _ }" 1000)
"\<Squnion>c { c1 , c2 } ≡ (λ x. if x ∈ dom c1 ∩ dom c2 then Some (max (the (c1 x)) (the (c2 x)))
else None)"
constdefs maxAbstractDelta :: "AbstractDelta => AbstractDelta => AbstractDelta"
"maxAbstractDelta Δ1 Δ2 ≡ (%ρ . if (ρ ∈ dom Δ1 ∩ dom Δ2)
then Some \<Squnion>c { the (Δ1 ρ) , the (Δ2 ρ) }
else None)"
constdefs maxCostList :: "Cost list => Cost" ("\<Squnion>c _ " 1000)
"maxCostList xs ≡ foldr maxCost xs []0"
constdefs maxAbstractDeltaList :: "FunName => AbstractDelta list => AbstractDelta"
("\<Squnion>Δ _ _ " 1000)
"maxAbstractDeltaList f xs ≡ foldr maxAbstractDelta xs (emptyAbstractDelta f)"
constdefs sizeAbstractDelta :: "AbstractDelta => Cost" ("|_|" 1000)
"sizeAbstractDelta d ≡ fold addCost (%x. x) []0 (ran d)"
(***** Definitions for CASE ****)
fun AbstractDeltaSpaceCost :: "AbstractDelta × AbstractMu × AbstractSigma => AbstractDelta"
where
"AbstractDeltaSpaceCost (Δ, μ, σ) = Δ"
fun AbstractMuSpaceCost :: "AbstractDelta × AbstractMu × AbstractSigma => AbstractMu"
where
"AbstractMuSpaceCost (Δ, μ, σ) = μ"
fun AbstractSigmaSpaceCost :: "AbstractDelta × AbstractMu × AbstractSigma => AbstractSigma"
where
"AbstractSigmaSpaceCost (Δ, μ, σ) = σ"
constdefs num_r :: "('a Patron × 'a Exp) => real"
"num_r alt ≡ real (length (snd (extractP (fst alt))))"
(***** Definitions for APP ****)
constdefs list_ge :: "real list => real list => bool"
"list_ge xs ys == (∀ i < length xs. xs!i ≥ ys!i)"
constdefs monotonic_bound :: "(real list \<rightharpoonup> real) => bool"
"monotonic_bound b == (∀ x ∈ dom b. (∀ y ∈ dom b. list_ge x y --> the (b x) ≥ the (b y)))"
constdefs monotonic_AbstractDelta :: "AbstractDelta => bool"
"monotonic_AbstractDelta Δ ≡ (∀ ρ ∈ dom Δ. monotonic_bound (the (Δ ρ)))"
constdefs defined_bound :: "(real list \<rightharpoonup> real) => FunName => bool"
"defined_bound b f ≡ (∀ xs. length xs = length (varsAPP Σd f) --> xs ∈ dom b)"
constdefs defined_AbstractDelta :: "AbstractDelta => FunName => bool"
"defined_AbstractDelta Δ f ≡ (∀ ρ ∈ dom Δ. defined_bound (the (Δ ρ)) f)"
(* argP_aux *)
fun argP_aux :: "(string \<rightharpoonup> TypeExpression) => TypeExpression => 'a Exp => bool"
where
"argP_aux ϑ t (ConstE (LitN _) _) = (t = (ConstrT intType [] []))"
| "argP_aux ϑ t (ConstE (LitB _) _) = (t = (ConstrT boolType [] []))"
| "argP_aux ϑ t (VarE x _) = (ϑ x = Some t)"
fun argP :: "(string \<rightharpoonup> string) => string list => RegMapping => string list => bool"
where
"argP ψ ρs ϑ2 rs = (length ρs = length rs
∧ (∀ i < length ρs. ψ (ρs!i) = ϑ2 (rs!i)))"
constdefs η_ef :: "InstantiationMapping => (string \<rightharpoonup> string) => string list
=> InstantiationMapping"
"η_ef η φ ρs ≡ (%ρ. η (the (φ ρ))) |` (set ρs)"
consts phiMapping_app :: "(Cost option) list => real list => real list"
primrec
"phiMapping_app [] xs = []"
"phiMapping_app (c#cs) xs = (case c of Some c' => the (c' xs)# (phiMapping_app cs xs))"
constdefs cost_PhiMapping :: "Cost => ('a Exp) list => PhiMapping => Cost"
"cost_PhiMapping c as φ ≡ (λ xs. c (phiMapping_app (map φ (map atom2var as)) xs))"
constdefs mu_app :: "AbstractMu => ('a Exp) list => PhiMapping => AbstractMu"
"mu_app μg as φ ≡ cost_PhiMapping μg as φ"
constdefs sigma_app :: "AbstractSigma => ('a Exp) list => PhiMapping => AbstractSigma"
"sigma_app σg as φ ≡ cost_PhiMapping σg as φ"
constdefs
setsumCost :: "('a => Cost) => 'a set => Cost"
"setsumCost f A ≡ if finite A then fold addCost f []0 A else []0"
constdefs sum_rho :: "FunName => AbstractDelta => (string \<rightharpoonup> string) => PhiMapping
=> ('a Exp) list => string => Cost"
"sum_rho g Δg ψ Φ as ρ ≡ (%xs. (setsumCost
(λ ρ. the (Δg ρ))
{ρ'. ψ ρ' = Some ρ ∧ ρ' ∈ set (R_Args Σt g)})
(phiMapping_app (map Φ (map atom2var as)) xs))"
constdefs instance_f ::
"FunName => FunName => AbstractDelta => (string \<rightharpoonup> string) => PhiMapping
=> ('a Exp) list => AbstractDelta"
"instance_f f g Δg ψ Φ as ≡
(%ρ. Some (sum_rho g Δg ψ Φ as ρ)) |` ((set (R_Args Σt f)) ∪ {ρself_f f})"
consts varToExp :: "string list => 'a => 'a Exp list"
primrec
"varToExp [] a = []"
"varToExp (v#vs) a = VarE v a # varToExp vs a"
(* Projection of Δ *)
constdefs projection :: "FunName => AbstractDelta => AbstractDelta"
"projection f Δ ≡ (%ρ. if (ρ = ρself_f f) then None else Δ ρ)"
(* A costs environment ΣB is valid. \<Turnstile> ΣB *)
inductive
ValidGlobalResourcesEnv :: "FunctionResourcesSignature => bool"
("\<Turnstile>\<Turnstile> _ " 1000)
where
base: " \<Turnstile>\<Turnstile> empty"
| step: "[| \<Turnstile>\<Turnstile> Σb; f ∉ dom Σb;
(bodyAPP Σd f) :f (typesAPP Σϑ f) (sizesAPP ΣΦ f) real(length (varsAPP Σd f) + length (regionsAPP Σd f))
\<lbrace> Δ, μ, σ \<rbrace> |] ==> \<Turnstile>\<Turnstile> Σb(f\<mapsto>(projection f Δ,μ,σ))"
(* e satisfies the static assertion \<lbrace>Δ,μ,σ\<rbrace> in the context of ΣB *)
fun SafeResourcesDAssCntxt ::
"unit Exp => FunctionResourcesSignature =>
FunName => ThetaMapping => PhiMapping => real =>
AbstractDelta => AbstractMu => AbstractSigma => bool"
("_ , _ : _ _ _ \<lbrace> _ , _ , _ \<rbrace>" 1000)
where
"SafeResourcesDAssCntxt e Σb f (ϑ1,ϑ2) Φ td Δ μ σ =
( \<Turnstile>\<Turnstile> Σb --> e :f (ϑ1,ϑ2) Φ td \<lbrace> Δ, μ, σ \<rbrace>)"
(* The subexpresion e of f's body satisfies the static assertion \<lbrace>Δ,μ,σ\<rbrace>
up to depth n *)
fun SafeResourcesDAssDepth::
"unit Exp =>
FunName => ThetaMapping => PhiMapping => real => nat =>
AbstractDelta => AbstractMu => AbstractSigma => bool"
(" _ :_ _ _ _ , _ \<lbrace> _ , _ , _ \<rbrace>" 1000)
where
" SafeResourcesDAssDepth e f (ϑ1,ϑ2) Φ td n Δ μ σ =
(valid Σd Σϑ ΣΦ --> (* valid *)
(set (R_Args Σt f)) ∪ {ρself_f f} = dom Δ (* P_static *)
∧ (∀ E1 E2 h k hh v δ m s η si.
SafeDepthSemanticsReal.SafeBoundSem (E1,E2) h k td e (f,n) hh k v (δ,m,s)
∧ (set (varsAPP Σd f)) ∪ fv e ⊆ dom E1 ∧ fvReg e ⊆ dom E2 (* P_dyn *)
∧ dom Δ = dom η
∧ si = build_si E1 h (varsAPP Σd f) (* P_size *)
∧ admissible f η k (* P_η *)
--> Delta_ge Δ si k η δ (* P_Δ *)
∧ mu_ge μ si m (* P_μ *)
∧ sigma_ge σ si s))" (* P_σ *)
(* A costs environment ΣB is valid up to depth n for function f.
\<Turnstile>f,n ΣB *)
inductive ValidGlobalResourcesEnvDepth ::
"string => nat => FunctionResourcesSignature => bool"
("\<Turnstile>\<Turnstile>_ , _ _ " 1000)
where
base : "[| \<Turnstile>\<Turnstile> Σb; f ∉ dom Σb|] ==> \<Turnstile>\<Turnstile>f,n Σb"
| depth0 : "[| \<Turnstile>\<Turnstile> Σb; f ∉ dom Σb|] ==> \<Turnstile>\<Turnstile>f,0 Σb(f\<mapsto> (projection f Δ,μ,σ))"
| step : "[| \<Turnstile>\<Turnstile> Σb; f ∉ dom Σb;
(bodyAPP Σd f) :f (typesAPP Σϑ f) (sizesAPP ΣΦ f) real(length (varsAPP Σd f) + length (regionsAPP Σd f)), n
\<lbrace> Δ, μ, σ \<rbrace> |] ==> \<Turnstile>\<Turnstile>f,Suc n Σb(f\<mapsto>(projection f Δ,μ,σ))"
| g : "[| \<Turnstile>\<Turnstile>f,n Σb; g ∉ dom Σb; g≠f;
(bodyAPP Σd g) :g (typesAPP Σϑ g) (sizesAPP ΣΦ g) real(length (varsAPP Σd g) + length (regionsAPP Σd g))
\<lbrace> Δ, μ, σ \<rbrace> |] ==> \<Turnstile>\<Turnstile>f, n Σb(g\<mapsto>(projection g Δ,μ,σ))"
(* The subexpresion e of f's body satisfies the static assertion \<lbrace>ϑ,t\<rbrace>
up to depth n in the context of ΣT *)
fun SafeResourcesDAssDepthCntxt ::
"unit Exp => FunctionResourcesSignature =>
FunName => ThetaMapping => PhiMapping => real => nat =>
AbstractDelta => AbstractMu => AbstractSigma => bool"
(" _ , _ :_ _ _ _ , _ \<lbrace> _ , _ , _ \<rbrace>" 1000)
where
"SafeResourcesDAssDepthCntxt e Σb f (ϑ1,ϑ2) Φ td n Δ μ σ =
( \<Turnstile>\<Turnstile>f,n Σb --> e :f (ϑ1,ϑ2) Φ td, n \<lbrace> Δ, μ, σ \<rbrace>)"
end