Theory SestoftGC
theory SestoftGC
imports Sestoft
begin
inductive gc_step :: "conf ⇒ conf ⇒ bool" (infix "⇒⇩G" 50) where
normal: "c ⇒ c' ⟹ c ⇒⇩G c'"
| dropUpd: "(Γ, e, Upd x # S) ⇒⇩G (Γ, e, S @ [Dummy x])"
lemmas gc_step_intros[intro] =
normal[OF step.intros(1)] normal[OF step.intros(2)] normal[OF step.intros(3)]
normal[OF step.intros(4)] normal[OF step.intros(5)] dropUpd
abbreviation gc_steps (infix "⇒⇩G⇧*" 50) where "gc_steps ≡ gc_step⇧*⇧*"
lemmas converse_rtranclp_into_rtranclp[of gc_step, OF _ r_into_rtranclp, trans]
lemma var_onceI:
assumes "map_of Γ x = Some e"
shows "(Γ, Var x, S) ⇒⇩G⇧* (delete x Γ, e , S@[Dummy x])"
proof-
from assms
have "(Γ, Var x, S) ⇒⇩G (delete x Γ, e , Upd x # S)"..
moreover
have "… ⇒⇩G (delete x Γ, e, S@[Dummy x])"..
ultimately
show ?thesis by (rule converse_rtranclp_into_rtranclp[OF _ r_into_rtranclp])
qed
lemma normal_trans: "c ⇒⇧* c' ⟹ c ⇒⇩G⇧* c'"
by (induction rule:rtranclp_induct)
(simp, metis normal rtranclp.rtrancl_into_rtrancl)
fun to_gc_conf :: "var list ⇒ conf ⇒ conf"
where "to_gc_conf r (Γ, e, S) = (restrictA (- set r) Γ, e, restr_stack (- set r) S @ (map Dummy (rev r)))"
lemma restr_stack_map_Dummy[simp]: "restr_stack V (map Dummy l) = map Dummy l"
by (induction l) auto
lemma restr_stack_append[simp]: "restr_stack V (l@l') = restr_stack V l @ restr_stack V l'"
by (induction l rule: restr_stack.induct) auto
lemma to_gc_conf_append[simp]:
"to_gc_conf (r@r') c = to_gc_conf r (to_gc_conf r' c)"
by (cases c) auto
lemma to_gc_conf_eqE[elim!]:
assumes "to_gc_conf r c = (Γ, e, S)"
obtains Γ' S' where "c = (Γ', e, S')" and "Γ = restrictA (- set r) Γ'" and "S = restr_stack (- set r) S' @ map Dummy (rev r)"
using assms by (cases c) auto
fun safe_hd :: "'a list ⇒ 'a option"
where "safe_hd (x#_) = Some x"
| "safe_hd [] = None"
lemma safe_hd_None[simp]: "safe_hd xs = None ⟷ xs = []"
by (cases xs) auto
abbreviation r_ok :: "var list ⇒ conf ⇒ bool"
where "r_ok r c ≡ set r ⊆ domA (fst c) ∪ upds (snd (snd c))"
lemma subset_bound_invariant:
"invariant step (r_ok r)"
proof
fix x y
assume "x ⇒ y" and "r_ok r x" thus "r_ok r y"
by (induction) auto
qed
lemma safe_hd_restr_stack[simp]:
"Some a = safe_hd (restr_stack V (a # S)) ⟷ restr_stack V (a # S) = a # restr_stack V S"
apply (cases a)
apply (auto split: if_splits)
apply (thin_tac "P a" for P)
apply (induction S rule: restr_stack.induct)
apply (auto split: if_splits)
done
lemma sestoftUnGCStack:
assumes "heap_upds_ok (Γ, S)"
obtains Γ' S' where
"(Γ, e, S) ⇒⇧* (Γ', e, S')"
"to_gc_conf r (Γ, e, S) = to_gc_conf r (Γ', e, S')"
"¬ isVal e ∨ safe_hd S' = safe_hd (restr_stack (- set r) S')"
proof-
show ?thesis
proof(cases "isVal e")
case False
thus ?thesis using assms by -(rule that, auto)
next
case True
from that assms
show ?thesis
apply (atomize_elim)
proof(induction S arbitrary: Γ)
case Nil thus ?case by (fastforce)
next
case (Cons s S)
show ?case
proof(cases "Some s = safe_hd (restr_stack (- set r) (s#S))")
case True
thus ?thesis
using ‹isVal e› ‹heap_upds_ok (Γ, s # S)›
apply auto
apply (intro exI conjI)
apply (rule rtranclp.intros(1))
apply auto
done
next
case False
then obtain x where [simp]: "s = Upd x" and [simp]: "x ∈ set r"
by(cases s) (auto split: if_splits)
from ‹heap_upds_ok (Γ, s # S)› ‹s = Upd x›
have [simp]: "x ∉ domA Γ" and "heap_upds_ok ((x,e) # Γ, S)"
by (auto dest: heap_upds_okE)
have "(Γ, e, s # S) ⇒⇧* (Γ, e, Upd x # S)" unfolding ‹s = _› ..
also have "… ⇒ ((x,e) # Γ, e, S)" by (rule step.var⇩2[OF ‹x ∉ domA Γ› ‹isVal e›])
also
from Cons.IH[OF ‹heap_upds_ok ((x,e) # Γ, S)› ]
obtain Γ' S' where "((x,e) # Γ, e, S) ⇒⇧* (Γ', e, S')"
and res: "to_gc_conf r ((x,e) # Γ, e, S) = to_gc_conf r (Γ', e, S')"
"(¬ isVal e ∨ safe_hd S' = safe_hd (restr_stack (- set r) S'))"
by blast
note this(1)
finally
have "(Γ, e, s # S) ⇒⇧* (Γ', e, S')".
thus ?thesis using res by auto
qed
qed
qed
qed
lemma perm_exI_trivial:
"P x x ⟹ ∃ π. P (π ∙ x) x"
by (rule exI[where x = "0::perm"]) auto
lemma upds_list_restr_stack[simp]:
"upds_list (restr_stack V S) = filter (λ x. x∈V) (upds_list S)"
by (induction S rule: restr_stack.induct) auto
lemma heap_upd_ok_to_gc_conf:
"heap_upds_ok (Γ, S) ⟹ to_gc_conf r (Γ, e, S) = (Γ'', e'', S'') ⟹ heap_upds_ok (Γ'', S'')"
by (auto simp add: heap_upds_ok.simps)
lemma delete_restrictA_conv:
"delete x Γ = restrictA (-{x}) Γ"
by (induction Γ) auto
lemma sestoftUnGCstep:
assumes "to_gc_conf r c ⇒⇩G d"
assumes "heap_upds_ok_conf c"
assumes "closed c"
and "r_ok r c"
shows "∃ r' c'. c ⇒⇧* c' ∧ d = to_gc_conf r' c' ∧ r_ok r' c'"
proof-
obtain Γ e S where "c = (Γ, e, S)" by (cases c) auto
with assms
have "heap_upds_ok (Γ,S)" and "closed (Γ, e, S)" and "r_ok r (Γ, e, S)" by auto
from sestoftUnGCStack[OF this(1)]
obtain Γ' S' where
"(Γ, e, S) ⇒⇧* (Γ', e, S')"
and *: "to_gc_conf r (Γ, e, S) = to_gc_conf r (Γ', e, S')"
and disj: "¬ isVal e ∨ safe_hd S' = safe_hd (restr_stack (- set r) S')"
by metis
from invariant_starE[OF ‹_ ⇒⇧* _› heap_upds_ok_invariant] ‹heap_upds_ok (Γ,S)›
have "heap_upds_ok (Γ', S')" by auto
from invariant_starE[OF ‹_ ⇒⇧* _› closed_invariant ‹closed (Γ, e, S)› ]
have "closed (Γ', e, S')" by auto
from invariant_starE[OF ‹_ ⇒⇧* _› subset_bound_invariant ‹r_ok r (Γ, e, S)› ]
have "r_ok r (Γ', e, S')" by auto
from assms(1)[unfolded ‹c =_ › *]
have "∃ r' Γ'' e'' S''. (Γ', e, S') ⇒⇧* (Γ'', e'', S'') ∧ d = to_gc_conf r' (Γ'', e'', S'') ∧ r_ok r' (Γ'', e'', S'')"
proof(cases rule: gc_step.cases)
case normal
hence "∃ Γ'' e'' S''. (Γ', e, S') ⇒ (Γ'', e'', S'') ∧ d = to_gc_conf r (Γ'', e'', S'')"
proof(cases rule: step.cases)
case app⇩1
thus ?thesis
apply auto
apply (intro exI conjI)
apply (rule step.intros)
apply auto
done
next
case (app⇩2 Γ y ea x S)
thus ?thesis
using disj
apply (cases S')
apply auto
apply (intro exI conjI)
apply (rule step.intros)
apply auto
done
next
case var⇩1
thus ?thesis
apply auto
apply (intro exI conjI)
apply (rule step.intros)
apply (auto simp add: restr_delete_twist)
done
next
case var⇩2
thus ?thesis
using disj
apply (cases S')
apply auto
apply (intro exI conjI)
apply (rule step.intros)
apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
done
next
case (let⇩1 Δ'' Γ'' S'' e')
from ‹closed (Γ', e, S')› let⇩1
have "closed (Γ', Let Δ'' e', S')" by simp
from fresh_distinct[OF let⇩1(3)] fresh_distinct_fv[OF let⇩1(4)]
have "domA Δ'' ∩ domA Γ'' = {}" and "domA Δ'' ∩ upds S'' = {}" and "domA Δ'' ∩ dummies S'' = {}"
by (auto dest: subsetD[OF ups_fv_subset] subsetD[OF dummies_fv_subset])
moreover
from let⇩1(1)
have "domA Γ' ∪ upds S' ⊆ domA Γ'' ∪ upds S'' ∪ dummies S''"
by auto
ultimately
have disj: "domA Δ'' ∩ domA Γ' = {}" "domA Δ'' ∩ upds S' = {}"
by auto
from ‹domA Δ'' ∩ dummies S'' = {}› let⇩1(1)
have "domA Δ'' ∩ set r = {}" by auto
hence [simp]: "restrictA (- set r) Δ'' = Δ''"
by (auto intro: restrictA_noop)
from let⇩1(1-3)
show ?thesis
apply auto
apply (intro exI[where x = "r"] exI[where x = "Δ'' @ Γ'"] exI[where x = "S'"] conjI)
apply (rule let⇩1_closed[OF ‹closed (Γ', Let Δ'' e', S')› disj])
apply (auto simp add: restrictA_append)
done
next
case if⇩1
thus ?thesis
apply auto
apply (intro exI[where x = "0::perm"] exI conjI)
unfolding permute_zero
apply (rule step.intros)
apply (auto)
done
next
case if⇩2
thus ?thesis
using disj
apply (cases S')
apply auto
apply (intro exI exI conjI)
apply (rule step.if⇩2[where b = True, simplified] step.if⇩2[where b = False, simplified])
apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
apply (intro exI conjI)
apply (rule step.if⇩2[where b = True, simplified] step.if⇩2[where b = False, simplified])
apply (auto split: if_splits dest: Upd_eq_restr_stackD2)
done
qed
with invariantE[OF subset_bound_invariant _ ‹r_ok r (Γ', e, S')›]
show ?thesis by blast
next
case (dropUpd Γ'' e'' x S'')
from ‹to_gc_conf r (Γ', e, S') = (Γ'', e'', Upd x # S'')›
have "x ∉ set r" by (auto dest!: arg_cong[where f = upds])
from ‹heap_upds_ok (Γ', S')› and ‹to_gc_conf r (Γ', e, S') = (Γ'', e'', Upd x # S'')›
have "heap_upds_ok (Γ'', Upd x # S'')" by (rule heap_upd_ok_to_gc_conf)
hence [simp]: "x ∉ domA Γ''" "x ∉ upds S''" by (auto dest: heap_upds_ok_upd)
have "to_gc_conf (x # r) (Γ', e, S') = to_gc_conf ([x]@ r) (Γ', e, S')" by simp
also have "… = to_gc_conf [x] (to_gc_conf r (Γ', e, S'))" by (rule to_gc_conf_append)
also have "… = to_gc_conf [x] (Γ'', e'', Upd x # S'')" unfolding ‹to_gc_conf r (Γ', e, S') = _›..
also have "… = (Γ'', e'', S''@[Dummy x])" by (auto intro: restrictA_noop)
also have "… = d" using ‹ d= _› by simp
finally have "to_gc_conf (x # r) (Γ', e, S') = d".
moreover
from ‹to_gc_conf r (Γ', e, S') = (Γ'', e'', Upd x # S'')›
have "x ∈ upds S'" by (auto dest!: arg_cong[where f = upds])
with ‹r_ok r (Γ', e, S')›
have "r_ok (x # r) (Γ', e, S')" by auto
moreover
note ‹to_gc_conf r (Γ', e, S') = (Γ'', e'', Upd x # S'')›
ultimately
show ?thesis by fastforce
qed
then obtain r' Γ'' e'' S''
where "(Γ', e, S') ⇒⇧* (Γ'', e'', S'')"
and "d = to_gc_conf r' (Γ'', e'', S'')"
and "r_ok r' (Γ'', e'', S'')"
by metis
from ‹(Γ, e, S) ⇒⇧* (Γ', e, S')› and ‹(Γ', e, S') ⇒⇧* (Γ'', e'', S'')›
have "(Γ, e, S) ⇒⇧* (Γ'', e'', S'')" by (rule rtranclp_trans)
with ‹d = _› ‹r_ok r' _›
show ?thesis unfolding ‹c = _› by auto
qed
lemma sestoftUnGC:
assumes "(to_gc_conf r c) ⇒⇩G⇧* d" and "heap_upds_ok_conf c" and "closed c" and "r_ok r c"
shows "∃ r' c'. c ⇒⇧* c' ∧ d = to_gc_conf r' c' ∧ r_ok r' c'"
using assms
proof(induction rule: rtranclp_induct)
case base
thus ?case by blast
next
case (step d' d'')
then obtain r' c' where "c ⇒⇧* c'" and "d' = to_gc_conf r' c'" and "r_ok r' c'" by auto
from invariant_starE[OF ‹_ ⇒⇧* _› heap_upds_ok_invariant] ‹heap_upds_ok _›
have "heap_upds_ok_conf c'".
from invariant_starE[OF ‹_ ⇒⇧* _› closed_invariant] ‹closed _›
have "closed c'".
from step ‹d' = to_gc_conf r' c'›
have "to_gc_conf r' c' ⇒⇩G d''" by simp
from this ‹heap_upds_ok_conf c'› ‹closed c'› ‹r_ok r' c'›
have "∃ r'' c''. c' ⇒⇧* c'' ∧ d'' = to_gc_conf r'' c'' ∧ r_ok r'' c''"
by (rule sestoftUnGCstep)
then obtain r'' c'' where "c' ⇒⇧* c''" and "d'' = to_gc_conf r'' c''" and "r_ok r'' c''" by auto
from ‹c' ⇒⇧* c''› ‹c ⇒⇧* c'›
have "c ⇒⇧* c''" by auto
with ‹d'' = _› ‹r_ok r'' c''›
show ?case by blast
qed
lemma dummies_unchanged_invariant:
"invariant step (λ (Γ, e, S) . dummies S = V)" (is "invariant _ ?I")
proof
fix c c'
assume "c ⇒ c'" and "?I c"
thus "?I c'" by (induction) auto
qed
lemma sestoftUnGC':
assumes "([], e, []) ⇒⇩G⇧* (Γ, e', map Dummy r)"
assumes "isVal e'"
assumes "fv e = ({}::var set)"
shows "∃ Γ''. ([], e, []) ⇒⇧* (Γ'', e', []) ∧ Γ = restrictA (- set r) Γ'' ∧ set r ⊆ domA Γ''"
proof-
from sestoftUnGC[where r = "[]" and c = "([], e, [])", simplified, OF assms(1,3)]
obtain r' Γ' S'
where "([], e, []) ⇒⇧* (Γ', e', S')"
and "Γ = restrictA (- set r') Γ'"
and "map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')"
and "r_ok r' (Γ', e', S')"
by auto
from invariant_starE[OF ‹([], e, []) ⇒⇧* (Γ', e', S')› dummies_unchanged_invariant]
have "dummies S' = {}" by auto
with ‹map Dummy r = restr_stack (- set r') S' @ map Dummy (rev r')›
have "restr_stack (- set r') S' = []" and [simp]: "r = rev r'"
by (induction S' rule: restr_stack.induct) (auto split: if_splits)
from invariant_starE[OF ‹_ ⇒⇧* _› heap_upds_ok_invariant]
have "heap_upds_ok (Γ', S')" by auto
from ‹isVal e'› sestoftUnGCStack[where e = e', OF ‹heap_upds_ok (Γ', S')› ]
obtain Γ'' S''
where "(Γ', e', S') ⇒⇧* (Γ'', e', S'')"
and "to_gc_conf r (Γ', e', S') = to_gc_conf r (Γ'', e', S'')"
and "safe_hd S'' = safe_hd (restr_stack (- set r) S'')"
by metis
from this (2,3) ‹restr_stack (- set r') S' = []›
have "S'' = []" by auto
from ‹([], e, []) ⇒⇧* (Γ', e', S')› and ‹(Γ', e', S') ⇒⇧* (Γ'', e', S'')› and ‹S'' = []›
have "([], e, []) ⇒⇧* (Γ'', e', [])" by auto
moreover
have "Γ = restrictA (- set r) Γ''" using ‹to_gc_conf r _ = _› ‹Γ = _› by auto
moreover
from invariant_starE[OF ‹(Γ', e', S') ⇒⇧* (Γ'', e', S'')› subset_bound_invariant ‹r_ok r' (Γ', e', S')›]
have "set r ⊆ domA Γ''" using ‹S'' = []› by auto
ultimately
show ?thesis by blast
qed
end