theory CardinalityEtaExpandCorrect
imports ArityEtaExpand CardinalityAnalysisSpec AbstractTransform Sestoft SestoftGC ArityEtaExpansionSestoft ArityAnalysisStack ArityConsistent
begin
context CardinalityPrognosisCorrect
begin
sublocale AbstractTransformBoundSubst
"\ a . inc\a"
"\ a . pred\a"
"\ \ e a . (a, Aheap \ e\a)"
"fst"
"snd"
"\ _. 0"
"Aeta_expand"
"snd"
apply default
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!: set_mp[OF supp_map_transform] set_mp[OF supp_map_transform_step] )
interpretation supp_bounded_transform transform
by default (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
\ upds S - edom ce \ set r
\ 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!: set_mp[OF edom_prognosis])
thus ?thesis
by (auto simp add: edom_empty_iff_bot closed_a_consistent[OF assms])
qed
lemma foo:
fixes c c'
assumes "c \\<^sup>* 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 \\<^sub>G\<^sup>* 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\<^sub>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\<^sub>1 have "consistent (ae, ce, inc\a, as, r) (\, e, Arg x # S)"
by (auto intro: a_consistent_app\<^sub>1 elim: below_trans)
moreover
have "conf_transform (ae, ce, a, as, r) (\, App e x, S) \\<^sub>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\<^sub>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\<^sub>2
by (auto 4 3 intro: a_consistent_app\<^sub>2 elim: below_trans)
moreover
have "conf_transform (ae, ce, a, as, r) (\, Lam [y]. e, Arg x # S) \\<^sub>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 set_mp[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) \\<^sub>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 "\ \\<^sub>G\<^sup>* 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 "\ \\<^sub>G\<^sup>* 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_correct **)
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) \\<^sub>G\<^sup>* 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) \\<^sub>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) \\<^sub>G\<^sup>*
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 "\ \\<^sub>G\<^sup>* 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_correct[OF ** ]])
finally(rtranclp_trans)
have "conf_transform (ae, ce, a, as, r) (\, Var x, S) \\<^sub>G\<^sup>* conf_transform (ae, ce, u, as, r) ((x, e) # delete x \, e, S)".
}
ultimately show ?case by (blast del: consistentI consistentE)
next
case (var\<^sub>2 \ x e S)
show ?case
proof(cases "x \ edom ce")
case True[simp]
hence [simp]: "x \ set r" using var\<^sub>2 by auto
from var\<^sub>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\<^sub>2 by (auto intro!: a_consistent_var\<^sub>2)
ultimately
have "consistent (ae, ce, 0, as, r) ((x, e) # \, e, S)"
using var\<^sub>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) \\<^sub>G conf_transform (ae, ce, 0, as, r) ((x, e) # \, e, S)"
using `ae x = up\0` `a = 0` var\<^sub>2
by (auto intro: gc_step.intros simp add: map_transform_Cons)
ultimately show ?thesis by (blast del: consistentI consistentE)
next
case False[simp]
hence "ce x = \" using var\<^sub>2 by (auto simp add: edom_def)
from False have "x \ edom ae" using var\<^sub>2 by auto
hence [simp]: "ae x = \" by (auto simp add: edom_def)
from False have [simp]: "x \ set r" using var\<^sub>2 by auto
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 (\