Theory CardArityTransformSafe
theory CardArityTransformSafe
imports ArityTransform CardinalityAnalysisSpec AbstractTransform Sestoft SestoftGC ArityEtaExpansionSafe ArityAnalysisStack ArityConsistent
begin
context CardinalityPrognosisSafe
begin
sublocale AbstractTransformBoundSubst
"λ a . inc⋅a"
"λ a . pred⋅a"
"λ Δ e a . (a, Aheap Δ e⋅a)"
"fst"
"snd"
"λ _. 0"
"Aeta_expand"
"snd"
apply standard
apply (simp add: Aheap_subst)
apply (rule subst_Aeta_expand)
done
abbreviation ccTransform where "ccTransform ≡ transform"
lemma supp_transform: "supp (transform a e) ⊆ supp e"
by (induction rule: transform.induct)
(auto simp add: exp_assn.supp Let_supp dest!: subsetD[OF supp_map_transform] subsetD[OF supp_map_transform_step] )
interpretation supp_bounded_transform transform
by standard (auto simp add: fresh_def supp_transform)
type_synonym tstate = "(AEnv × (var ⇒ two) × Arity × Arity list × var list)"
fun transform_alts :: "Arity list ⇒ stack ⇒ stack"
where
"transform_alts _ [] = []"
| "transform_alts (a#as) (Alts e1 e2 # S) = (Alts (ccTransform a e1) (ccTransform a e2)) # transform_alts as S"
| "transform_alts as (x # S) = x # transform_alts as S"
lemma transform_alts_Nil[simp]: "transform_alts [] S = S"
by (induction S) auto
lemma Astack_transform_alts[simp]:
"Astack (transform_alts as S) = Astack S"
by (induction rule: transform_alts.induct) auto
lemma fresh_star_transform_alts[intro]: "a ♯* S ⟹ a ♯* transform_alts as S"
by (induction as S rule: transform_alts.induct) (auto simp add: fresh_star_Cons)
fun a_transform :: "astate ⇒ conf ⇒ conf"
where "a_transform (ae, a, as) (Γ, e, S) =
(map_transform Aeta_expand ae (map_transform ccTransform ae Γ),
ccTransform a e,
transform_alts as S)"
fun restr_conf :: "var set ⇒ conf ⇒ conf"
where "restr_conf V (Γ, e, S) = (restrictA V Γ, e, restr_stack V S)"
fun add_dummies_conf :: "var list ⇒ conf ⇒ conf"
where "add_dummies_conf l (Γ, e, S) = (Γ, e, S @ map Dummy (rev l))"
fun conf_transform :: "tstate ⇒ conf ⇒ conf"
where "conf_transform (ae, ce, a, as, r) c = add_dummies_conf r ((a_transform (ae, a, as) (restr_conf (- set r) c)))"
inductive consistent :: "tstate ⇒ conf ⇒ bool" where
consistentI[intro!]:
"a_consistent (ae, a, as) (restr_conf (- set r) (Γ, e, S))
⟹ edom ae = edom ce
⟹ prognosis ae as a (Γ, e, S) ⊑ ce
⟹ (⋀ x. x ∈ thunks Γ ⟹ many ⊑ ce x ⟹ ae x = up⋅0)
⟹ set r ⊆ (domA Γ ∪ upds S) - edom ce
⟹ consistent (ae, ce, a, as, r) (Γ, e, S)"
inductive_cases consistentE[elim!]: "consistent (ae, ce, a, as) (Γ, e, S)"
lemma closed_consistent:
assumes "fv e = ({}::var set)"
shows "consistent (⊥, ⊥, 0, [], []) ([], e, [])"
proof-
from assms
have "edom (prognosis ⊥ [] 0 ([], e, [])) = {}"
by (auto dest!: subsetD[OF edom_prognosis])
thus ?thesis
by (auto simp add: edom_empty_iff_bot closed_a_consistent[OF assms])
qed
lemma card_arity_transform_safe:
fixes c c'
assumes "c ⇒⇧* c'" and "¬ boring_step c'" and "heap_upds_ok_conf c" and "consistent (ae,ce,a,as,r) c"
shows "∃ae' ce' a' as' r'. consistent (ae',ce',a',as',r') c' ∧ conf_transform (ae,ce,a,as,r) c ⇒⇩G⇧* conf_transform (ae',ce',a',as',r') c'"
using assms(1,2) heap_upds_ok_invariant assms(3-)
proof(induction c c' arbitrary: ae ce a as r rule:step_invariant_induction)
case (app⇩1 Γ e x S)
have "prognosis ae as (inc⋅a) (Γ, e, Arg x # S) ⊑ prognosis ae as a (Γ, App e x, S)" by (rule prognosis_App)
with app⇩1 have "consistent (ae, ce, inc⋅a, as, r) (Γ, e, Arg x # S)"
by (auto intro: a_consistent_app⇩1 elim: below_trans)
moreover
have "conf_transform (ae, ce, a, as, r) (Γ, App e x, S) ⇒⇩G conf_transform (ae, ce, inc⋅a, as, r) (Γ, e, Arg x # S)"
by simp rule
ultimately
show ?case by (blast del: consistentI consistentE)
next
case (app⇩2 Γ y e x S)
have "prognosis ae as (pred⋅a) (Γ, e[y::=x], S) ⊑ prognosis ae as a (Γ, (Lam [y]. e), Arg x # S)"
by (rule prognosis_subst_Lam)
then
have "consistent (ae, ce, pred⋅a, as, r) (Γ, e[y::=x], S)" using app⇩2
by (auto 4 3 intro: a_consistent_app⇩2 elim: below_trans)
moreover
have "conf_transform (ae, ce, a, as, r) (Γ, Lam [y]. e, Arg x # S) ⇒⇩G conf_transform (ae, ce, pred ⋅ a, as, r) (Γ, e[y::=x], S)" by (simp add: subst_transform[symmetric]) rule
ultimately
show ?case by (blast del: consistentI consistentE)
next
case (thunk Γ x e S)
hence "x ∈ thunks Γ" by auto
hence [simp]: "x ∈ domA Γ" by (rule subsetD[OF thunks_domA])
from thunk have "prognosis ae as a (Γ, Var x, S) ⊑ ce" by auto
from below_trans[OF prognosis_called fun_belowD[OF this] ]
have [simp]: "x ∈ edom ce" by (auto simp add: edom_def)
hence [simp]: "x ∉ set r" using thunk by auto
from ‹heap_upds_ok_conf (Γ, Var x, S)›
have "x ∉ upds S" by (auto dest!: heap_upds_okE)
have "x ∈ edom ae" using thunk by auto
then obtain u where "ae x = up⋅u" by (cases "ae x") (auto simp add: edom_def)
show ?case
proof(cases "ce x" rule:two_cases)
case none
with ‹x ∈ edom ce› have False by (auto simp add: edom_def)
thus ?thesis..
next
case once
from ‹prognosis ae as a (Γ, Var x, S) ⊑ ce›
have "prognosis ae as a (Γ, Var x, S) x ⊑ once"
using once by (metis (mono_tags) fun_belowD)
hence "x ∉ ap S" using prognosis_ap[of ae as a Γ "(Var x)" S] by auto
from ‹map_of Γ x = Some e› ‹ae x = up⋅u› ‹¬ isVal e›
have *: "prognosis ae as u (delete x Γ, e, Upd x # S) ⊑ record_call x ⋅ (prognosis ae as a (Γ, Var x, S))"
by (rule prognosis_Var_thunk)
from ‹prognosis ae as a (Γ, Var x, S) x ⊑ once›
have "(record_call x ⋅ (prognosis ae as a (Γ, Var x, S))) x = none"
by (simp add: two_pred_none)
hence **: "prognosis ae as u (delete x Γ, e, Upd x # S) x = none" using fun_belowD[OF *, where x = x] by auto
have eq: "prognosis (env_delete x ae) as u (delete x Γ, e, Upd x # S) = prognosis ae as u (delete x Γ, e, Upd x # S)"
by (rule prognosis_env_cong) simp
have [simp]: "restr_stack (- set r - {x}) S = restr_stack (- set r) S"
using ‹x ∉ upds S› by (auto intro: restr_stack_cong)
have "prognosis (env_delete x ae) as u (delete x Γ, e, Upd x # S) ⊑ env_delete x ce"
unfolding eq
using ** below_trans[OF below_trans[OF * Cfun.monofun_cfun_arg[OF ‹prognosis ae as a (Γ, Var x, S) ⊑ ce›]] record_call_below_arg]
by (rule below_env_deleteI)
moreover
have *: "a_consistent (env_delete x ae, u, as) (delete x (restrictA (- set r) Γ), e, restr_stack (- set r) S)"
using thunk ‹ae x = up⋅u›
by (auto intro!: a_consistent_thunk_once simp del: restr_delete)
ultimately
have "consistent (env_delete x ae, env_delete x ce, u, as, x # r) (delete x Γ, e, Upd x # S)" using thunk
by (auto simp add: restr_delete_twist Compl_insert elim:below_trans )
moreover
from *
have **: "Astack (transform_alts as (restr_stack (- set r) S) @ map Dummy (rev r) @ [Dummy x]) ⊑ u" by (auto elim: a_consistent_stackD)
{
from ‹map_of Γ x = Some e› ‹ae x = up⋅u› once
have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) Γ))) x = Some (Aeta_expand u (transform u e))"
by (simp add: map_of_map_transform)
hence "conf_transform (ae, ce, a, as, r) (Γ, Var x, S) ⇒⇩G
add_dummies_conf r (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) Γ))), Aeta_expand u (ccTransform u e), Upd x # transform_alts as (restr_stack (- set r) S))"
by (auto simp add: map_transform_delete delete_map_transform_env_delete insert_absorb restr_delete_twist simp del: restr_delete)
also
have "… ⇒⇩G⇧* add_dummies_conf (x # r) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) Γ))), Aeta_expand u (ccTransform u e), transform_alts as (restr_stack (- set r) S))"
apply (rule r_into_rtranclp)
apply (simp add: append_assoc[symmetric] del: append_assoc)
apply (rule dropUpd)
done
also
have "… ⇒⇩G⇧* add_dummies_conf (x # r) (delete x (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) Γ))), ccTransform u e, transform_alts as (restr_stack (- set r) S))"
by simp (intro normal_trans Aeta_expand_safe **)
also(rtranclp_trans)
have "… = conf_transform (env_delete x ae, env_delete x ce, u, as, x # r) (delete x Γ, e, Upd x # S)"
by (auto intro!: map_transform_cong simp add: map_transform_delete[symmetric] restr_delete_twist Compl_insert)
finally(back_subst)
have "conf_transform (ae, ce, a, as, r) (Γ, Var x, S) ⇒⇩G⇧* conf_transform (env_delete x ae, env_delete x ce, u, as, x # r) (delete x Γ, e, Upd x # S)".
}
ultimately
show ?thesis by (blast del: consistentI consistentE)
next
case many
from ‹map_of Γ x = Some e› ‹ae x = up⋅u› ‹¬ isVal e›
have "prognosis ae as u (delete x Γ, e, Upd x # S) ⊑ record_call x ⋅ (prognosis ae as a (Γ, Var x, S))"
by (rule prognosis_Var_thunk)
also note record_call_below_arg
finally
have *: "prognosis ae as u (delete x Γ, e, Upd x # S) ⊑ prognosis ae as a (Γ, Var x, S)" by this simp_all
have "ae x = up⋅0" using thunk many ‹x ∈ thunks Γ› by (auto)
hence "u = 0" using ‹ae x = up⋅u› by simp
have "prognosis ae as 0 (delete x Γ, e, Upd x # S) ⊑ ce" using *[unfolded ‹u=0›] thunk by (auto elim: below_trans)
moreover
have "a_consistent (ae, 0, as) (delete x (restrictA (- set r) Γ), e, Upd x # restr_stack (- set r) S)" using thunk ‹ae x = up⋅0›
by (auto intro!: a_consistent_thunk_0 simp del: restr_delete)
ultimately
have "consistent (ae, ce, 0, as, r) (delete x Γ, e, Upd x # S)" using thunk ‹ae x = up⋅u› ‹u = 0›
by (auto simp add: restr_delete_twist)
moreover
from ‹map_of Γ x = Some e› ‹ae x = up⋅0› many
have "map_of (map_transform Aeta_expand ae (map_transform ccTransform ae (restrictA (- set r) Γ))) x = Some (transform 0 e)"
by (simp add: map_of_map_transform)
with ‹¬ isVal e›
have "conf_transform (ae, ce, a, as, r) (Γ, Var x, S) ⇒⇩G conf_transform (ae, ce, 0, as, r) (delete x Γ, e, Upd x # S)"
by (auto intro: gc_step.intros simp add: map_transform_delete restr_delete_twist intro!: step.intros simp del: restr_delete)
ultimately
show ?thesis by (blast del: consistentI consistentE)
qed
next
case (lamvar Γ x e S)
from lamvar(1) have [simp]: "x ∈ domA Γ" by (metis domI dom_map_of_conv_domA)
from lamvar have "prognosis ae as a (Γ, Var x, S) ⊑ ce" by auto
from below_trans[OF prognosis_called fun_belowD[OF this] ]
have [simp]: "x ∈ edom ce" by (auto simp add: edom_def)
then obtain c where "ce x = up⋅c" by (cases "ce x") (auto simp add: edom_def)
from lamvar
have [simp]: "x ∉ set r" by auto
then have "x ∈ edom ae" using lamvar by auto
then obtain u where "ae x = up⋅u" by (cases "ae x") (auto simp add: edom_def)
have "prognosis ae as u ((x, e) # delete x Γ, e, S) = prognosis ae as u (Γ, e, S)"
using ‹map_of Γ x = Some e› by (auto intro!: prognosis_reorder)
also have "… ⊑ record_call x ⋅ (prognosis ae as a (Γ, Var x, S))"
using ‹map_of Γ x = Some e› ‹ae x = up⋅u› ‹isVal e› by (rule prognosis_Var_lam)
also have "… ⊑ prognosis ae as a (Γ, Var x, S)" by (rule record_call_below_arg)
finally have *: "prognosis ae as u ((x, e) # delete x Γ, e, S) ⊑ prognosis ae as a (Γ, Var x, S)" by this simp_all
moreover
have "a_consistent (ae, u, as) ((x,e) # delete x (restrictA (- set r) Γ), e, restr_stack (- set r) S)" using lamvar ‹ae x = up⋅u›
by (auto intro!: a_consistent_lamvar simp del: restr_delete)
ultimately
have "consistent (ae, ce, u, as, r) ((x, e) # delete x Γ, e, S)"
using lamvar edom_mono[OF *] by (auto simp add: thunks_Cons restr_delete_twist elim: below_trans)
moreover
from ‹a_consistent _ _›
have **: "Astack (transform_alts as (restr_stack (- set r) S) @ map Dummy (rev r)) ⊑ u" by (auto elim: a_consistent_stackD)
{
from ‹isVal e›
have "isVal (transform u e)" by simp
hence "isVal (Aeta_expand u (transform u e))" by (rule isVal_Aeta_expand)
moreover
from ‹map_of Γ x = Some e› ‹ae x = up ⋅ u› ‹ce x = up⋅c› ‹isVal (transform u e)›
have "map_of (map_transform Aeta_expand ae (map_transform transform ae (restrictA (- set r) Γ))) x = Some (Aeta_expand u (transform u e))"
by (simp add: map_of_map_transform)
ultimately
have "conf_transform (ae, ce, a, as, r) (Γ, Var x, S) ⇒⇩G⇧*
add_dummies_conf r ((x, Aeta_expand u (transform u e)) # delete x (map_transform Aeta_expand ae (map_transform transform ae (restrictA (- set r) Γ))), Aeta_expand u (transform u e), transform_alts as (restr_stack (- set r) S))"
by (auto intro!: normal_trans[OF lambda_var] simp add: map_transform_delete simp del: restr_delete)
also have "… = add_dummies_conf r ((map_transform Aeta_expand ae (map_transform transform ae ((x,e) # delete x (restrictA (- set r) Γ)))), Aeta_expand u (transform u e), transform_alts as (restr_stack (- set r) S))"
using ‹ae x = up ⋅ u› ‹ce x = up⋅c› ‹isVal (transform u e)›
by (simp add: map_transform_Cons map_transform_delete restr_delete_twist del: restr_delete)
also(subst[rotated]) have "… ⇒⇩G⇧* conf_transform (ae, ce, u, as, r) ((x, e) # delete x Γ, e, S)"
by (simp add: restr_delete_twist) (rule normal_trans[OF Aeta_expand_safe[OF ** ]])
finally(rtranclp_trans)
have "conf_transform (ae, ce, a, as, r) (Γ, Var x, S) ⇒⇩G⇧* conf_transform (ae, ce, u, as, r) ((x, e) # delete x Γ, e, S)".
}
ultimately show ?case by (blast del: consistentI consistentE)
next
case (var⇩2 Γ x e S)
show ?case
proof(cases "x ∈ set r")
case [simp]: False
from var⇩2
have "a_consistent (ae, a, as) (restrictA (- set r) Γ, e, Upd x # restr_stack (-set r) S)" by auto
from a_consistent_UpdD[OF this]
have "ae x = up⋅0" and "a = 0".
from ‹isVal e› ‹x ∉ domA Γ›
have *: "prognosis ae as 0 ((x, e) # Γ, e, S) ⊑ prognosis ae as 0 (Γ, e, Upd x # S)" by (rule prognosis_Var2)
moreover
have "a_consistent (ae, a, as) ((x, e) # restrictA (- set r) Γ, e, restr_stack (- set r) S)"
using var⇩2 by (auto intro!: a_consistent_var⇩2)
ultimately
have "consistent (ae, ce, 0, as, r) ((x, e) # Γ, e, S)"
using var⇩2 ‹a = 0›
by (auto simp add: thunks_Cons elim: below_trans)
moreover
have "conf_transform (ae, ce, a, as, r) (Γ, e, Upd x # S) ⇒⇩G conf_transform (ae, ce, 0, as, r) ((x, e) # Γ, e, S)"
using ‹ae x = up⋅0› ‹a = 0› var⇩2
by (auto intro: gc_step.intros simp add: map_transform_Cons)
ultimately show ?thesis by (blast del: consistentI consistentE)
next
case True
hence "ce x = ⊥" using var⇩2 by (auto simp add: edom_def)
hence "x ∉ edom ce" by (simp add: edomIff)
hence "x ∉ edom ae" using var⇩2 by auto
hence [simp]: "ae x = ⊥" by (auto simp add: edom_def)
note ‹x ∈ set r›[simp]
have "prognosis ae as a ((x, e) # Γ, e, S) ⊑ prognosis ae as a ((x, e) # Γ, e, Upd x # S)" by (rule prognosis_upd)
also have "… ⊑ prognosis ae as a (delete x ((x,e) # Γ), e, Upd x # S)"
using ‹ae x = ⊥› by (rule prognosis_not_called)
also have "delete x ((x,e)#Γ) = Γ" using ‹x ∉ domA Γ› by simp
finally
have *: "prognosis ae as a ((x, e) # Γ, e, S) ⊑ prognosis ae as a (Γ, e, Upd x # S)" by this simp
then
have "consistent (ae, ce, a, as, r) ((x, e) # Γ, e, S)" using var⇩2
by (auto simp add: thunks_Cons elim:below_trans a_consistent_var⇩2)
moreover
have "conf_transform (ae, ce, a, as, r) (Γ, e, Upd x # S) = conf_transform (ae, ce, a, as, r) ((x, e) # Γ, e, S)"
by (auto simp add: map_transform_restrA[symmetric])
ultimately show ?thesis
by (fastforce del: consistentI consistentE simp del:conf_transform.simps)
qed
next
case (let⇩1 Δ Γ e S)
let ?ae = "Aheap Δ e⋅a"
let ?ce = "cHeap Δ e⋅a"
have "domA Δ ∩ upds S = {}" using fresh_distinct_fv[OF let⇩1(2)] by (auto dest: subsetD[OF ups_fv_subset])
hence *: "⋀ x. x ∈ upds S ⟹ x ∉ edom ?ae" by (auto simp add: edom_cHeap dest!: subsetD[OF edom_Aheap])
have restr_stack_simp2: "restr_stack (edom (?ae ⊔ ae)) S = restr_stack (edom ae) S"
by (auto intro: restr_stack_cong dest!: *)
have "edom ce = edom ae" using let⇩1 by auto
have "edom ae ⊆ domA Γ ∪ upds S" using let⇩1 by (auto dest!: a_consistent_edom_subsetD)
from subsetD[OF this] fresh_distinct[OF let⇩1(1)] fresh_distinct_fv[OF let⇩1(2)]
have "edom ae ∩ domA Δ = {}" by (auto dest: subsetD[OF ups_fv_subset])
from ‹edom ae ∩ domA Δ = {}›
have [simp]: "edom (Aheap Δ e⋅a) ∩ edom ae = {}" by (auto dest!: subsetD[OF edom_Aheap])
from fresh_distinct[OF let⇩1(1)]
have [simp]: "restrictA (edom ae ∪ edom (Aheap Δ e⋅a)) Γ = restrictA (edom ae) Γ"
by (auto intro: restrictA_cong dest!: subsetD[OF edom_Aheap])
have "set r ⊆ domA Γ ∪ upds S" using let⇩1 by auto
have [simp]: "restrictA (- set r) Δ = Δ"
apply (rule restrictA_noop)
apply auto
by (metis IntI UnE ‹set r ⊆ domA Γ ∪ upds S› ‹domA Δ ∩ domA Γ = {}› ‹domA Δ ∩ upds S = {}› contra_subsetD empty_iff)
{
have "edom (?ae ⊔ ae) = edom (?ce ⊔ ce)"
using let⇩1(4) by (auto simp add: edom_cHeap)
moreover
{ fix x e'
assume "x ∈ thunks Γ"
hence "x ∉ edom ?ce" using fresh_distinct[OF let⇩1(1)]
by (auto simp add: edom_cHeap dest: subsetD[OF edom_Aheap] subsetD[OF thunks_domA])
hence [simp]: "?ce x = ⊥" unfolding edomIff by auto
assume "many ⊑ (?ce ⊔ ce) x"
with let⇩1 ‹x ∈ thunks Γ›
have "(?ae ⊔ ae) x = up ⋅0" by auto
}
moreover
{ fix x e'
assume "x ∈ thunks Δ"
hence "x ∉ domA Γ" and "x ∉ upds S"
using fresh_distinct[OF let⇩1(1)] fresh_distinct_fv[OF let⇩1(2)]
by (auto dest!: subsetD[OF thunks_domA] subsetD[OF ups_fv_subset])
hence "x ∉ edom ce" using ‹edom ae ⊆ domA Γ ∪ upds S› ‹edom ce = edom ae› by auto
hence [simp]: "ce x = ⊥" by (auto simp add: edomIff)
assume "many ⊑ (?ce ⊔ ce) x" with ‹x ∈ thunks Δ›
have "(?ae ⊔ ae) x = up⋅0" by (auto simp add: Aheap_heap3)
}
moreover
{
from let⇩1(1,2) ‹edom ae ⊆ domA Γ ∪ upds S›
have "prognosis (?ae ⊔ ae) as a (Δ @ Γ, e, S) ⊑ ?ce ⊔ prognosis ae as a (Γ, Let Δ e, S)" by (rule prognosis_Let)
also have "prognosis ae as a (Γ, Let Δ e, S) ⊑ ce" using let⇩1 by auto
finally have "prognosis (?ae ⊔ ae) as a (Δ @ Γ, e, S) ⊑ ?ce ⊔ ce" by this simp
}
moreover
have "a_consistent (ae, a, as) (restrictA (- set r) Γ, Let Δ e, restr_stack (- set r) S)"
using let⇩1 by auto
hence "a_consistent (?ae ⊔ ae, a, as) (Δ @ restrictA (- set r) Γ, e, restr_stack (- set r) S)"
using let⇩1(1,2) ‹edom ae ∩ domA Δ = {}›
by (auto intro!: a_consistent_let simp del: join_comm)
hence "a_consistent (?ae ⊔ ae, a, as) (restrictA (- set r) (Δ @ Γ), e, restr_stack (- set r) S)"
by (simp add: restrictA_append)
moreover
have "set r ⊆ (domA Γ ∪ upds S) - edom ce" using let⇩1 by auto
hence "set r ⊆ (domA Γ ∪ upds S) - edom (?ce ⊔ ce)"
apply (rule order_trans)
using ‹domA Δ ∩ domA Γ = {}› ‹domA Δ ∩ upds S = {}›
apply (auto simp add: edom_cHeap dest!: subsetD[OF edom_Aheap])
done
ultimately
have "consistent (?ae ⊔ ae, ?ce ⊔ ce, a, as, r) (Δ @ Γ, e, S)" by auto
}
moreover
{
have "⋀ x. x ∈ domA Γ ⟹ x ∉ edom ?ae" "⋀ x. x ∈ domA Γ ⟹ x ∉ edom ?ce"
using fresh_distinct[OF let⇩1(1)]
by (auto simp add: edom_cHeap dest!: subsetD[OF edom_Aheap])
hence "map_transform Aeta_expand (?ae ⊔ ae) (map_transform transform (?ae ⊔ ae) (restrictA (-set r) Γ))
= map_transform Aeta_expand ae (map_transform transform ae (restrictA (-set r) Γ))"
by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
moreover
from ‹edom ae ⊆ domA Γ ∪ upds S› ‹edom ce = edom ae›
have "⋀ x. x ∈ domA Δ ⟹ x ∉ edom ce" and "⋀ x. x ∈ domA Δ ⟹ x ∉ edom ae"
using fresh_distinct[OF let⇩1(1)] fresh_distinct_ups[OF let⇩1(2)] by auto
hence "map_transform Aeta_expand (?ae ⊔ ae) (map_transform transform (?ae ⊔ ae) (restrictA (- set r) Δ))
= map_transform Aeta_expand ?ae (map_transform transform ?ae (restrictA (- set r) Δ))"
by (auto intro!: map_transform_cong restrictA_cong simp add: edomIff)
moreover
from ‹domA Δ ∩ domA Γ = {}› ‹domA Δ ∩ upds S = {}›
have "atom ` domA Δ ♯* set r"
by (auto simp add: fresh_star_def fresh_at_base fresh_finite_set_at_base dest!: subsetD[OF ‹set r ⊆ domA Γ ∪ upds S›])
hence "atom ` domA Δ ♯* map Dummy (rev r)"
apply -
apply (rule eqvt_fresh_star_cong1[where f = "map Dummy"], perm_simp, rule)
apply (rule eqvt_fresh_star_cong1[where f = "rev"], perm_simp, rule)
apply (auto simp add: fresh_star_def fresh_set)
done
ultimately
have "conf_transform (ae, ce, a, as, r) (Γ, Let Δ e, S) ⇒⇩G conf_transform (?ae ⊔ ae, ?ce ⊔ ce, a, as, r) (Δ @ Γ, e, S)"
using restr_stack_simp2 let⇩1(1,2) ‹edom ce = edom ae›
apply (auto simp add: map_transform_append restrictA_append edom_cHeap restr_stack_simp2[simplified] )
apply (rule normal)
apply (rule step.let⇩1)
apply (auto intro: normal step.let⇩1 dest: subsetD[OF edom_Aheap] simp add: fresh_star_list)
done
}
ultimately
show ?case by (blast del: consistentI consistentE)
next
case (if⇩1 Γ scrut e1 e2 S)
have "prognosis ae as a (Γ, scrut ? e1 : e2, S) ⊑ ce" using if⇩1 by auto
hence "prognosis ae (a#as) 0 (Γ, scrut, Alts e1 e2 # S) ⊑ ce"
by (rule below_trans[OF prognosis_IfThenElse])
hence "consistent (ae, ce, 0, a#as, r) (Γ, scrut, Alts e1 e2 # S)"
using if⇩1 by (auto dest: a_consistent_if⇩1)
moreover
have "conf_transform (ae, ce, a, as, r) (Γ, scrut ? e1 : e2, S) ⇒⇩G conf_transform (ae, ce, 0, a#as, r) (Γ, scrut, Alts e1 e2 # S)"
by (auto intro: normal step.intros)
ultimately
show ?case by (blast del: consistentI consistentE)
next
case (if⇩2 Γ b e1 e2 S)
hence "a_consistent (ae, a, as) (restrictA (- set r) Γ, Bool b, Alts e1 e2 # restr_stack (-set r) S)" by auto
then obtain a' as' where [simp]: "as = a' # as'" "a = 0"
by (rule a_consistent_alts_on_stack)
{
have "prognosis ae (a'#as') 0 (Γ, Bool b, Alts e1 e2 # S) ⊑ ce" using if⇩2 by auto
hence "prognosis ae as' a' (Γ, if b then e1 else e2, S) ⊑ ce" by (rule below_trans[OF prognosis_Alts])
then
have "consistent (ae, ce, a', as', r) (Γ, if b then e1 else e2, S)"
using if⇩2 by (auto dest!: a_consistent_if⇩2)
}
moreover
have "conf_transform (ae, ce, a, as, r) (Γ, Bool b, Alts e1 e2 # S) ⇒⇩G conf_transform (ae, ce, a', as', r) (Γ, if b then e1 else e2, S)"
by (auto intro: normal step.if⇩2[where b = True, simplified] step.if⇩2[where b = False, simplified])
ultimately
show ?case by (blast del: consistentI consistentE)
next
case refl thus ?case by force
next
case (trans c c' c'')
from trans(3)[OF trans(5)]
obtain ae' ce' a' as' r'
where "consistent (ae', ce', a', as', r') c'" and *: "conf_transform (ae, ce, a, as, r) c ⇒⇩G⇧* conf_transform (ae', ce', a', as', r') c'" by blast
from trans(4)[OF this(1)]
obtain ae'' ce'' a'' as'' r''
where "consistent (ae'', ce'', a'', as'', r'') c''" and **: "conf_transform (ae', ce', a', as', r') c' ⇒⇩G⇧* conf_transform (ae'', ce'', a'', as'', r'') c''" by blast
from this(1) rtranclp_trans[OF * **]
show ?case by blast
qed
end
end