theory LaunchburyUnBH
imports LaunchburyStacked LaunchburyNoBH
begin
lemma delete_append[simp]: "delete x (al1@al2) = delete x al1 @ delete x al2"
by (simp add: AList.delete_eq)
lemma forgetBH:
assumes "\ : \' \ \ : \'"
assumes "distinctVars (\' @ \)"
shows "\' @ \ [\] \' @ \"
using assms
proof (induct rule: reds_distinct_ind)
case (Lambda \ x y e \')
show ?case
unfolding append_Cons
apply (rule LaunchburyNoBH.Lambda)
done
next
case (Application n \ \' \ \' x e y \ \' z e')
show ?case
unfolding append_Cons
proof(rule LaunchburyNoBH.Application)
show "atom n \ (\' @ \, delete x ((x, App (Var n) y) # \' @ \), x, e, y, \' @ \, z)"
and "atom z \ (\' @ \, delete x ((x, App (Var n) y) # \' @ \), x, e, y, \' @ \)"
using Application
by (auto simp add: fresh_Pair fresh_Cons fresh_append eqvt_fresh_cong2[where f = delete, OF delete_eqvt])
show "(n, e) # (x, App (Var n) y) # \' @ \ [\] (n, Lam [z]. e') # (x, App (Var n) y) # \' @ \"
by (rule Application(9)[unfolded append_Cons])
have "x \ heapVars (\' @ \)"
using Application(6)
by (simp add: distinctVars_Cons)
hence [simp]:"delete x \' = \'" "delete x \ = \"
by (auto intro: delete_no_there)
show "(x, e'[z::=y]) # delete x ((x, App (Var n) y) # \' @ \) [\] \' @ \"
using Application(11)
by simp
qed
next
case (Variable y e \ x \' z \' \)
have [simp]:"x \ y"
using Variable(3)
by (auto simp add: distinctVars_Cons)
note this[symmetric,simp]
have "y \ heapVars \'"
using Variable(3)
by (auto simp add: distinctVars_Cons)
hence [simp]: "delete y \' = \'"
by (rule delete_no_there)
have "x \ heapVars \'"
using Variable(4)
by (auto simp add: distinctVars_Cons)
hence [simp]: "delete x \' = \'"
by (rule delete_no_there)
have "x \ heapVars \"
using Variable(4)
by (auto simp add: distinctVars_Cons)
hence [simp]: "delete x \ = \"
by (rule delete_no_there)
have "((x, Var y) # \') @ \ [\] (x, z) # delete x (((x, Var y) # \') @ (y, z) # \)"
unfolding append_Cons
proof (rule LaunchburyNoBH.Variable)
show "(y, e) \ set ((x, Var y) # \' @ \)"
using Variable(1) by simp
show "(y, e) # delete y ((x, Var y) # \' @ \) [\] (y, z) # (((x, Var y) # \') @ \)"
using Variable(7) by simp
show "set ((x, Var y) # \' @ (y, z) # \) = set ((y, z) # ((x, Var y) # \') @ \)"
by auto
qed
thus ?case
unfolding append_Cons
by simp
next
case (Let as \ x body \' \' \)
show ?case
unfolding append_Cons
proof (rule LaunchburyNoBH.Let)
show "set (bn as) \* (\' @ \, x, Terms.Let as body)"
using Let(1) by (simp add: fresh_star_Pair fresh_star_append)
show "distinctVars (asToHeap as)" by fact
show " (x, body) # \' @ asToHeap as @ \ [\] \' @ \"
using Let(7) by simp
show "set (\' @ asToHeap as @ \) = set (asToHeap as @ \' @ \)"
by auto
qed
qed