theory DeadCodeRemoval2Correct
imports Launchbury LaunchburyAbstractTransformation DeadCodeRemoval2
begin
definition rdcH :: "var set \ heap \ heap"
where "rdcH S \ = restrictA (-S) (clearjunk (map_ran (\ _ e . remove_dead_code e) \))"
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 delete_map_ran[simp]: "delete x (map_ran f \) = map_ran f (delete x \)"
by (induction \) auto
lemma map_of_rdcH: "map_of (rdcH S \) x = (if x \ S then None else map_option remove_dead_code (map_of \ x))"
apply (induction \ rule: clearjunk.induct)
apply (auto simp add: rdcH_def map_of_clearjunk split: if_splits)
by (metis delete_map_ran map_of_delete)
lemma delete_rdcH[simp]: "delete x (rdcH S \) = rdcH S (delete x \)"
by (induction \ rule:clearjunk.induct)
(auto simp add: rdcH_def delete_twist split: if_splits)
lemma restrictA_UNIV[simp]: "restrictA UNIV \ = \"
by (induction \) auto
lemma restrictA_delete[simp]: "restrictA S (delete x \) = restrictA (S - {x}) \"
by (induction \) auto
lemma clearjunk_append: "clearjunk (\1 @ \2) = clearjunk \1 @ clearjunk (restrictA (-domA \1) \2)"
by (induction \1 arbitrary: \2 rule:clearjunk.induct) (auto simp add: Compl_insert)
lemma restrictA_clearjunk: "restrictA S (clearjunk \) = clearjunk (restrictA S \)"
by (induction \ rule:clearjunk.induct) (auto simp add: Compl_insert)
lemma rdcH_append[simp]: "domA as \ domA \ = {} \ rdcH S (as @ \) = rdcH S as @ rdcH S \"
unfolding rdcH_def apply (simp add: clearjunk_append restrictA_clearjunk map_ran_append restrictA_append)
apply (rule arg_cong) back
apply (rule restrictA_cong)
apply auto
done
lemma restrict_is_nil[simp]: "restrictA S \ = [] \ S \ domA \ = {}"
by (induction \) auto
lemma rdcH_nil[simp]: "rdcH S [] = []"
by (auto simp add: rdcH_def)
lemma rdcH_is_nil: "domA \ \ S \ rdcH S \ = []"
by (auto simp add: rdcH_def)
lemma rdcH_cong_set: "S \ domA \ = S' \ domA \ \ rdcH S \ = rdcH S' \"
unfolding rdcH_def by (rule restrictA_cong) auto
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 \ rule: clearjunk.induct)
(auto simp add: rdcH_def fresh_Nil fresh_Pair fresh_Cons eqvt_fresh_cong1[OF remove_dead_code.eqvt] fresh_delete)
lemma rdch_fv_subset: "fv (rdcH S \) \ fv \"
using rdch_fresh unfolding fresh_def fv_def by auto
lemma rdch_Cons[simp]:
"x \ S \ rdcH S ((x, z) # \) = (x, remove_dead_code z) # rdcH S (delete x \)"
unfolding rdcH_def
by (auto simp add: clearjunk_restrict[symmetric] delete_map_ran[symmetric] simp del: delete_map_ran)
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
moreover
assume "x \ domA \"
ultimately
have [simp]: "rdcH S ((x, z) # \) = (x,remove_dead_code z) # rdcH S \" by simp
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 "Terms.Let as e = Terms.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
lemma disjoint_mono: "A \ B = {} \ A' \ A \ B' \ B \ A' \ B' = {}" by auto
lemma disjoint_Un1: "(A \ B) \ C = {} \ A \ C = {} \ B \ C = {} " by auto
lemma disjoint_Un2: "C \ (A \ B) = {} \ C \ A = {} \ C \ B = {} " by auto
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')
let "Terms.Let ?as' ?body'" = "Terms.Let (restrict_reachable (map_ran (\_. remove_dead_code) as) (remove_dead_code body)) (remove_dead_code body)"
from `(\, Terms.Let as body) \\<^bsub>L\<^esub> (\', let')`
obtain S where "\' = rdcH S \" and "let' = SmartLet ?as' ?body'"
and "S \ domA \ \ set L" and S: "S \ fv (rdcH S \, SmartLet ?as' ?body', L) = {}" by (auto elim!: dc_rel.cases)
let "?S'" = "domA as - reachable (map_ran (\_. remove_dead_code) as) ?body'"
from `S \ _` and fresh_distinct[OF Let(1)] and fresh_distinct_list[OF Let(2)]
have "S \ domA as = {}" by auto
hence [simp]: "(rdcH (?S' \ S) as) = ?as'"
unfolding restrict_reachable_def rdcH_def
by -(rule restrictA_cong, auto)
have [simp]: "(rdcH (?S' \ 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 (?S' \ S) (as @ \), ?body')"
proof (rule dc_rel.intros)
show "(?S' \ S) \ domA (as @ \) \ set L" using `S \ domA \ \ set L` by auto
have "?S' \ fv ?as' = {}"
using fv_heap_reachable by auto
moreover
have "?S' \ fv \ = {}"
using Let(1) by (auto simp add: fresh_star_def fresh_def fv_def)
hence "?S' \ fv (rdcH S \) = {}"
by (rule disjoint_mono[OF _ subset_refl rdch_fv_subset])
moreover
have "?S' \ fv (?body') = {}"
using fv_e_reachable by auto
moreover
have "?S' \ fv L = {}"
using fresh_distinct_list[OF Let(2)] by auto
moreover
have "S \ fv ?as' = {}"
using S `S \ domA as = {}` by auto
moreover
have "S \ fv (rdcH S \) = {}"
using S by auto
moreover
have "S \ fv (?body') = {}"
using S `S \