theory DeadCodeRemovalCorrect
imports Launchbury LaunchburyAbstractTransformation DeadCodeRemoval
begin
definition rdcH :: "var set \ heap \ heap"
where "rdcH S \ = [ (x, remove_dead_code e) . (x,e) \ \, x \ S]"
inductive dc_rel :: "(heap \ exp) \ var list \ (heap \ exp) \ bool" ("_ \\<^bsub>_\<^esub> _" [50,50,50] 50 )
where "S \ domA \ \ set L \ S \ fv (rdcH S \, remove_dead_code e, L) = {} \ (\, e) \\<^bsub>L\<^esub> (rdcH S \, remove_dead_code e)"
lemma map_of_rdcH: "map_of (rdcH S \) x = (if x \ S then None else map_option remove_dead_code (map_of \ x))"
by (induction \) (auto simp add: rdcH_def split: if_splits)
lemma delete_rdcH[simp]: "delete x (rdcH S \) = rdcH S (delete x \)"
by (induction \) (auto simp add: rdcH_def split: if_splits)
lemma rdcH_append[simp]: "rdcH S (as @ \) = rdcH S as @ rdcH S \"
unfolding rdcH_def by simp
lemma rdcH_nil[simp]: "rdcH S [] = []"
unfolding rdcH_def by simp
lemma rdcH_is_nil: "domA \ \ S \ rdcH S \ = []"
by (induction \) (auto simp add: rdcH_def split: if_splits)
lemma rdcH_cong_set: "S \ domA \ = S' \ domA \ \ rdcH S \ = rdcH S' \"
by(induction \ rule: heapToAssn.induct)(auto simp add: rdcH_def split: if_splits )
interpretation rel_lambda_cong dc_rel
by default (auto elim!: dc_rel.cases simp del: exp_assn.eq_iff(4))
interpretation rel_app_cong dc_rel
by default (auto elim: dc_rel.cases)
interpretation rel_var_cong dc_rel
by default (auto elim: dc_rel.cases)
lemma rdcH_eqvt[eqvt]: "\ \ (rdcH S \) = rdcH (\ \ S) (\ \ \)"
unfolding rdcH_def by perm_simp rule
lemma rdch_fresh[intro]: "a \ \ \ a \ rdcH S \"
by (induction \)
(auto simp add: rdcH_def fresh_Nil fresh_Pair fresh_Cons eqvt_fresh_cong1[OF remove_dead_code.eqvt] )
lemma rdch_fv_subset: "fv (rdcH S \) \ fv \"
using rdch_fresh unfolding fresh_def fv_def by auto
interpretation reds_rel_fresh dc_rel
by default (auto elim!: dc_rel.cases intro: eqvt_fresh_cong1[OF remove_dead_code.eqvt])
interpretation rel_lambda_case dc_rel by default
lemma Lam_eq_same_var[simp]: "Lam [y]. e = Lam [y]. e' \ e = e'"
by auto (metis fresh_PairD(2) obtain_fresh)
interpretation rel_app_case dc_rel
proof
fix \ e x L \' e''
assume "(\, App e x) \\<^bsub>L\<^esub> (\', App e'' x)"
thus "(\, e) \\<^bsub>x # L\<^esub> (\', e'')"
by (fastforce elim!: dc_rel.cases intro!: dc_rel.intros)
next
fix \ y body x L \' body'
assume "(\, Lam [y]. body) \\<^bsub>x # L\<^esub> (\', Lam [y]. body')"
thus "(\, body[y::=x]) \\<^bsub>L\<^esub> (\', body'[y::=x])"
apply (auto elim!: dc_rel.cases intro!: dc_rel.intros dest: set_mp simp del: exp_assn.eq_iff(4) simp add: subst_remove_dead_code disjoint_iff_not_equal fv_subst_eq split: if_splits)
apply (auto simp add: subst_remove_dead_code[symmetric] fv_subst_eq split: if_splits)
done
qed
interpretation rel_var_case dc_rel
proof
case (goal1 \ x L \' e thesis)
show thesis
proof (rule goal1)
from goal1(1)
obtain S where "\' = rdcH S \"
and "S \ domA \ \ set L" and "S \ fv (rdcH S \, Var x, L) = {}" by (auto elim!: dc_rel.cases)
hence "x \ S" by auto
from `map_of \ x = Some e` and `\' = _` and `x \ S`
show "map_of \' x = Some (remove_dead_code e)" by (auto simp add: map_of_rdcH)
have *: "\ S . fv (rdcH S (delete x \)) \ fv (rdcH S \)" by (metis delete_rdcH fv_delete_subset)
from `map_of \' x = Some (remove_dead_code e)`
have **: "fv (remove_dead_code e) \ fv \'" by (metis domA_from_set map_of_fv_subset map_of_is_SomeD option.sel)
from goal1(1)
show "(delete x \, e) \\<^bsub>x # L\<^esub> (delete x \', remove_dead_code e)"
by (fastforce elim!: dc_rel.cases intro!: dc_rel.intros dest: set_mp[OF *] set_mp[OF **] simp add: disjoint_iff_not_equal)
qed
next
fix \ z x L \' z'
assume "(\, z) \\<^bsub>x # L\<^esub> (\', z')"
then obtain S where "\' = rdcH S \" and "z' = remove_dead_code z"
and "S \ insert x (domA \ \ set L)" and "S \ fv (rdcH S \, remove_dead_code z, x # L) = {}" by (auto elim!: dc_rel.cases)
from this(4)
have "x \ S" by auto
hence [simp]: "rdcH S ((x, z) # \) = (x,remove_dead_code z) # rdcH S \"
unfolding rdcH_def by auto
have "((x, z) # \, z) \\<^bsub>L\<^esub> (rdcH S ((x, z) # \), remove_dead_code z)"
apply (rule dc_rel.intros) using `S \ _` `S \ _ = _` by auto
thus "((x, z) # \, z) \\<^bsub>L\<^esub> ((x, z') # \', z')"
unfolding `\' = _` `z' = _` by auto
qed
locale let_removed =
fixes \ as body
assumes "domA as \ fv body = {} "
lemma map_fst_map_ran[simp]: "map fst (map_ran f l) = map fst l" by (induction l) auto
lemma permute_list_id: "supp p \ set xs \ p \ xs = xs \ p = 0"
proof (induction xs)
case Nil
hence "supp p = {}" by auto
thus "p = 0" by (metis empty_subsetI supp_perm_singleton)
next
case (Cons x xs)
hence "p \ x = x" by auto
hence "x \ supp p" by (metis fresh_def fresh_perm)
with Cons show "p = 0" by auto
qed
lemma Abs_lst_same[simp]: "[xs]lst. (y::'a::fs) = [xs]lst. y' \ y = y'"
apply rule
prefer 2
apply simp
unfolding Abs_eq_iff2
apply (erule exE)
apply auto
unfolding alpha_lst.simps
apply (subgoal_tac "p = 0")
apply auto[1]
apply (auto simp add: permute_list_id)
done
lemma Let_eq_same_var[simp]:
assumes "map fst as = map fst as'"
shows "Let as e = Let as' e' \ (as = as' \ e = e')"
proof-
from assms have "map (\x. atom (fst x)) as = map (\x. atom (fst x)) as'"
by (induction as as' rule: list_induct2') auto
thus ?thesis by auto
qed
locale let_not_removed =
fixes as :: heap and body :: exp
assumes let_not_removed: " domA as \ fv body \ {} "
begin
sublocale rel_let_cong dc_rel \ as body for \
by default (auto elim!: dc_rel.cases simp add: if_not_P[OF let_not_removed] simp del: Let_eq_iff)
sublocale rel_let_case dc_rel \ as body for \
proof
fix L \' as' body'
assume "(\, Let as body) \\<^bsub>L\<^esub> (\', Let as' body')" and "map fst as = map fst as'"
then obtain S where "\' = rdcH S \" and "body' = remove_dead_code body" and "as' = map_ran (\_. remove_dead_code) as"
and "S \ domA \ \ set L" and "S \ fv (rdcH S \, remove_dead_code (Let as body), L) = {}"
by (fastforce elim!: dc_rel.cases simp add: if_not_P[OF let_not_removed] simp del: Let_eq_iff)
assume fresh: "atom ` domA as \* \"
hence "domA as \ domA \ = {}" by (metis fresh_distinct)
moreover
assume "atom ` domA as \* L"
hence "domA as \ set L = {}" by (induction L) (auto simp add: fresh_star_Cons fresh_star_at_base)
ultimately
have * : "domA as \ S = {}" using `S \ domA \ \ set L` by auto
hence [simp]: "rdcH S as = map_ran (\_. remove_dead_code) as"
unfolding rdcH_def by (induction as) auto
have "(as @ \, body) \\<^bsub>L\<^esub> (rdcH S (as @ \), remove_dead_code body)"
proof
show "S \ domA (as @ \) \ set L" using * `S \ _` by auto
show "S \ fv (rdcH S (as @ \), remove_dead_code body, L) = {}" using `S \ _ = _` *
apply (simp add: if_not_P[OF let_not_removed])
apply (auto simp add: disjoint_iff_not_equal)
done
qed
thus "(as @ \, body) \\<^bsub>L\<^esub> (as' @ \', body')" unfolding `as' = _` `\' = _` `body' = _` by simp
qed
end
theorem DeadCodeRemovalCorrect:
assumes "\ : e \\<^bsub>L\<^esub> \ : z"
assumes "(\, e) \\<^bsub>L\<^esub> (\', e')"
shows "\ \' z'. (\, z) \\<^bsub>L\<^esub> (\', z') \ \' : e' \\<^bsub>L\<^esub> \' : z'"
using assms
proof(nominal_induct arbitrary: \' e' rule:reds.strong_induct)
case (Lambda \ x e L) thus ?case by (rule lambda_case)
next
case (Application y \ e x L \ \ z body) thus ?case by (rule app_case)
next
case (Variable \ x e L \ z \' var) thus ?case by (rule var_case)
next
case (Let as \ L body \ z \' let')
show ?case
proof (cases "domA as \ fv body = {}")
case True
with `(\, Let as body) \\<^bsub>L\<^esub> (\', let')`
obtain S where "\' = rdcH S \" and "let' = remove_dead_code body"
and "S \ domA \ \ set L" and "S \ fv (rdcH S \, remove_dead_code body, L) = {}" by (auto elim!: dc_rel.cases)
have [simp]: "(rdcH (domA as \ S) as) = []" by (rule rdcH_is_nil) auto
have [simp]: "(rdcH (domA as \ S) \) = (rdcH S \)"
using fresh_distinct[OF Let(1)]
by (auto intro: rdcH_cong_set simp add: fresh_star_at_base)
have "(as @ \, body) \\<^bsub>L\<^esub> (rdcH (domA as \ S) (as @ \), remove_dead_code body)"
proof (rule dc_rel.intros)
show "(domA as \ S) \ domA (as @ \) \ set L" using `S \ domA \ \ set L` by auto
from True
have "atom ` domA as \* body" by (auto simp add: fresh_star_def fv_def fresh_def)
from Let(1,2) True this
have "atom ` domA as \* (rdcH S \, remove_dead_code body, L)"
by (auto simp add: fresh_star_def fresh_Pair intro!: eqvt_fresh_cong1[OF remove_dead_code.eqvt])
find_theorems supp remove_dead_code
hence "domA as \ fv (rdcH S \, remove_dead_code body, L) = {}"
by (auto simp add: fresh_star_def fv_def fresh_def)
moreover
have "S \ fv (rdcH S \, remove_dead_code body, L) = {}" using `S \ _ = {}` by auto
ultimately
show "(domA as \ S) \ fv (rdcH (domA as \ S) (as @ \), remove_dead_code body, L) = {}" by auto
qed
hence "(as @ \, body) \\<^bsub>L\<^esub> (\', remove_dead_code body)" unfolding `\'=_` by simp
from Let(4)[OF this]
show ?thesis unfolding `let' = _`.
next
case False
interpret let_not_removed as body apply default using False.
show ?thesis using Let by (rule let_case)
qed
qed
corollary
assumes "[] : e \\<^bsub>L\<^esub> \ : z"
shows "\ \' z'. [] : remove_dead_code e \\<^bsub>L\<^esub> \