[STATEMENT]
lemma root_info:
  assumes irr: "irreducible p" and deg: "degree p > 0"
  shows "root_info_cond (root_info p) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root_info_cond (root_info p) p
[PROOF STEP]
proof (cases "degree p = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. degree p = 1 \<Longrightarrow> root_info_cond (root_info p) p
 2. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
case deg: True
[PROOF STATE]
proof (state)
this:
degree p = 1

goal (2 subgoals):
 1. degree p = 1 \<Longrightarrow> root_info_cond (root_info p) p
 2. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
from degree1_coeffs[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b. p = [:b, a:] \<and> a \<noteq> 0
[PROOF STEP]
obtain a b where p: "p = [:b,a:]" and "a \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b. p = [:b, a:] \<and> a \<noteq> 0

goal (1 subgoal):
 1. (\<And>b a. \<lbrakk>p = [:b, a:]; a \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = [:b, a:]
a \<noteq> 0

goal (2 subgoals):
 1. degree p = 1 \<Longrightarrow> root_info_cond (root_info p) p
 2. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
from deg
[PROOF STATE]
proof (chain)
picking this:
degree p = 1
[PROOF STEP]
have "degree (real_of_int_poly p) = 1"
[PROOF STATE]
proof (prove)
using this:
degree p = 1

goal (1 subgoal):
 1. degree (real_of_int_poly p) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
degree (real_of_int_poly p) = 1

goal (2 subgoals):
 1. degree p = 1 \<Longrightarrow> root_info_cond (root_info p) p
 2. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
from roots1[OF this, unfolded roots1_def] p
[PROOF STATE]
proof (chain)
picking this:
{x. poly (real_of_int_poly p) x = 0} = {- coeff (real_of_int_poly p) 0 / coeff (real_of_int_poly p) 1}
p = [:b, a:]
[PROOF STEP]
have id: "(ipoly p x = 0) = ((x :: real) = - b / a)" for x
[PROOF STATE]
proof (prove)
using this:
{x. poly (real_of_int_poly p) x = 0} = {- coeff (real_of_int_poly p) 0 / coeff (real_of_int_poly p) 1}
p = [:b, a:]

goal (1 subgoal):
 1. (poly (real_of_int_poly p) x = 0) = (x = real_of_int (- b) / real_of_int a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(poly (real_of_int_poly p) ?x = 0) = (?x = real_of_int (- b) / real_of_int a)

goal (2 subgoals):
 1. degree p = 1 \<Longrightarrow> root_info_cond (root_info p) p
 2. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
have idd: "{x. real_of_rat aa \<le> x \<and>
                 x \<le> real_of_rat ba \<and> x = real_of_int (- b) / real_of_int a}
   = (if real_of_rat aa \<le> real_of_int (- b) / real_of_int a \<and>
                 real_of_int (- b) / real_of_int a \<le> real_of_rat ba then {real_of_int (- b) / real_of_int a} else {})"
    for aa ba
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. real_of_rat aa \<le> x \<and> x \<le> real_of_rat ba \<and> x = real_of_int (- b) / real_of_int a} = (if real_of_rat aa \<le> real_of_int (- b) / real_of_int a \<and> real_of_int (- b) / real_of_int a \<le> real_of_rat ba then {real_of_int (- b) / real_of_int a} else {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. real_of_rat ?aa \<le> x \<and> x \<le> real_of_rat ?ba \<and> x = real_of_int (- b) / real_of_int a} = (if real_of_rat ?aa \<le> real_of_int (- b) / real_of_int a \<and> real_of_int (- b) / real_of_int a \<le> real_of_rat ?ba then {real_of_int (- b) / real_of_int a} else {})

goal (2 subgoals):
 1. degree p = 1 \<Longrightarrow> root_info_cond (root_info p) p
 2. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
have iddd: "{x. x \<le> real_of_rat aa \<and> x = real_of_int (- b) / real_of_int a}
    = (if real_of_int (- b) / real_of_int a \<le> real_of_rat aa then {real_of_int (- b) / real_of_int a} else {})" for aa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. x \<le> real_of_rat aa \<and> x = real_of_int (- b) / real_of_int a} = (if real_of_int (- b) / real_of_int a \<le> real_of_rat aa then {real_of_int (- b) / real_of_int a} else {})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. x \<le> real_of_rat ?aa \<and> x = real_of_int (- b) / real_of_int a} = (if real_of_int (- b) / real_of_int a \<le> real_of_rat ?aa then {real_of_int (- b) / real_of_int a} else {})

goal (2 subgoals):
 1. degree p = 1 \<Longrightarrow> root_info_cond (root_info p) p
 2. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
have id4: "real_of_int x = real_of_rat (rat_of_int x)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int x = real_of_rat (rat_of_int x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real_of_int ?x = real_of_rat (rat_of_int ?x)

goal (2 subgoals):
 1. degree p = 1 \<Longrightarrow> root_info_cond (root_info p) p
 2. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root_info_cond (root_info p) p
[PROOF STEP]
unfolding root_info_def deg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root_info_cond (if 1 = 1 then let x = Rat.Fract (- coeff p 0) (coeff p 1) in Root_Info (\<lambda>l r. if l \<le> x \<and> x \<le> r then 1 else 0) (\<lambda>b. if x \<le> b then 1 else 0) else let rp = of_int_poly p; ps = sturm_rat rp in Root_Info (\<lambda>a b. sign_changes_rat ps a - sign_changes_rat ps b) (\<lambda>a. sign_changes_neg_number_rootat ps - sign_changes_rat ps a)) p
[PROOF STEP]
unfolding root_info_cond_def id root_cond_def split
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>aa ba. aa \<le> ba \<longrightarrow> root_info.l_r (if 1 = 1 then let x = Rat.Fract (- coeff p 0) (coeff p 1) in Root_Info (\<lambda>l r. if l \<le> x \<and> x \<le> r then 1 else 0) (\<lambda>b. if x \<le> b then 1 else 0) else let rp = of_int_poly p; ps = sturm_rat rp in Root_Info (\<lambda>a b. sign_changes_rat ps a - sign_changes_rat ps b) (\<lambda>a. sign_changes_neg_number_rootat ps - sign_changes_rat ps a)) aa ba = card {x. real_of_rat aa \<le> x \<and> x \<le> real_of_rat ba \<and> x = real_of_int (- b) / real_of_int a}) \<and> (\<forall>aa. root_info.number_root (if 1 = 1 then let x = Rat.Fract (- coeff p 0) (coeff p 1) in Root_Info (\<lambda>l r. if l \<le> x \<and> x \<le> r then 1 else 0) (\<lambda>b. if x \<le> b then 1 else 0) else let rp = of_int_poly p; ps = sturm_rat rp in Root_Info (\<lambda>a b. sign_changes_rat ps a - sign_changes_rat ps b) (\<lambda>a. sign_changes_neg_number_rootat ps - sign_changes_rat ps a)) aa = card {x. x \<le> real_of_rat aa \<and> x = real_of_int (- b) / real_of_int a})
[PROOF STEP]
unfolding p Fract_of_int_quotient Let_def idd iddd
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>aa ba. aa \<le> ba \<longrightarrow> root_info.l_r (if 1 = 1 then Root_Info (\<lambda>l r. if l \<le> rat_of_int (- coeff [:b, a:] 0) / rat_of_int (coeff [:b, a:] 1) \<and> rat_of_int (- coeff [:b, a:] 0) / rat_of_int (coeff [:b, a:] 1) \<le> r then 1 else 0) (\<lambda>ba. if rat_of_int (- coeff [:b, a:] 0) / rat_of_int (coeff [:b, a:] 1) \<le> ba then 1 else 0) else Root_Info (\<lambda>aa ba. sign_changes_rat (sturm_rat (of_int_poly [:b, a:])) aa - sign_changes_rat (sturm_rat (of_int_poly [:b, a:])) ba) (\<lambda>aa. sign_changes_neg_number_rootat (sturm_rat (of_int_poly [:b, a:])) - sign_changes_rat (sturm_rat (of_int_poly [:b, a:])) aa)) aa ba = card (if real_of_rat aa \<le> real_of_int (- b) / real_of_int a \<and> real_of_int (- b) / real_of_int a \<le> real_of_rat ba then {real_of_int (- b) / real_of_int a} else {})) \<and> (\<forall>aa. root_info.number_root (if 1 = 1 then Root_Info (\<lambda>l r. if l \<le> rat_of_int (- coeff [:b, a:] 0) / rat_of_int (coeff [:b, a:] 1) \<and> rat_of_int (- coeff [:b, a:] 0) / rat_of_int (coeff [:b, a:] 1) \<le> r then 1 else 0) (\<lambda>ba. if rat_of_int (- coeff [:b, a:] 0) / rat_of_int (coeff [:b, a:] 1) \<le> ba then 1 else 0) else Root_Info (\<lambda>aa ba. sign_changes_rat (sturm_rat (of_int_poly [:b, a:])) aa - sign_changes_rat (sturm_rat (of_int_poly [:b, a:])) ba) (\<lambda>aa. sign_changes_neg_number_rootat (sturm_rat (of_int_poly [:b, a:])) - sign_changes_rat (sturm_rat (of_int_poly [:b, a:])) aa)) aa = card (if real_of_int (- b) / real_of_int a \<le> real_of_rat aa then {real_of_int (- b) / real_of_int a} else {}))
[PROOF STEP]
unfolding id4 of_rat_divide[symmetric] of_rat_less_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>aa ba. aa \<le> ba \<longrightarrow> root_info.l_r (if 1 = 1 then Root_Info (\<lambda>l r. if l \<le> rat_of_int (- coeff [:b, a:] 0) / rat_of_int (coeff [:b, a:] 1) \<and> rat_of_int (- coeff [:b, a:] 0) / rat_of_int (coeff [:b, a:] 1) \<le> r then 1 else 0) (\<lambda>ba. if rat_of_int (- coeff [:b, a:] 0) / rat_of_int (coeff [:b, a:] 1) \<le> ba then 1 else 0) else Root_Info (\<lambda>aa ba. sign_changes_rat (sturm_rat (of_int_poly [:b, a:])) aa - sign_changes_rat (sturm_rat (of_int_poly [:b, a:])) ba) (\<lambda>aa. sign_changes_neg_number_rootat (sturm_rat (of_int_poly [:b, a:])) - sign_changes_rat (sturm_rat (of_int_poly [:b, a:])) aa)) aa ba = card (if aa \<le> rat_of_int (- b) / rat_of_int a \<and> rat_of_int (- b) / rat_of_int a \<le> ba then {real_of_rat (rat_of_int (- b) / rat_of_int a)} else {})) \<and> (\<forall>aa. root_info.number_root (if 1 = 1 then Root_Info (\<lambda>l r. if l \<le> rat_of_int (- coeff [:b, a:] 0) / rat_of_int (coeff [:b, a:] 1) \<and> rat_of_int (- coeff [:b, a:] 0) / rat_of_int (coeff [:b, a:] 1) \<le> r then 1 else 0) (\<lambda>ba. if rat_of_int (- coeff [:b, a:] 0) / rat_of_int (coeff [:b, a:] 1) \<le> ba then 1 else 0) else Root_Info (\<lambda>aa ba. sign_changes_rat (sturm_rat (of_int_poly [:b, a:])) aa - sign_changes_rat (sturm_rat (of_int_poly [:b, a:])) ba) (\<lambda>aa. sign_changes_neg_number_rootat (sturm_rat (of_int_poly [:b, a:])) - sign_changes_rat (sturm_rat (of_int_poly [:b, a:])) aa)) aa = card (if rat_of_int (- b) / rat_of_int a \<le> aa then {real_of_rat (rat_of_int (- b) / rat_of_int a)} else {}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
root_info_cond (root_info p) p

goal (1 subgoal):
 1. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
degree p \<noteq> 1

goal (1 subgoal):
 1. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
have irr_d: "irreducible\<^sub>d p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irreducible\<^sub>d p
[PROOF STEP]
by (simp add: deg irr irreducible_connect_rev)
[PROOF STATE]
proof (state)
this:
irreducible\<^sub>d p

goal (1 subgoal):
 1. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
from irreducible\<^sub>d_int_rat[OF this]
[PROOF STATE]
proof (chain)
picking this:
irreducible\<^sub>d (of_int_poly p)
[PROOF STEP]
have "irreducible (of_int_poly p :: rat poly)"
[PROOF STATE]
proof (prove)
using this:
irreducible\<^sub>d (of_int_poly p)

goal (1 subgoal):
 1. irreducible (of_int_poly p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
irreducible (of_int_poly p)

goal (1 subgoal):
 1. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
from irreducible_root_free[OF this]
[PROOF STATE]
proof (chain)
picking this:
root_free (of_int_poly p)
[PROOF STEP]
have idd: "(poly (of_int_poly p) a = 0) = False" for a :: rat
[PROOF STATE]
proof (prove)
using this:
root_free (of_int_poly p)

goal (1 subgoal):
 1. (ipoly p a = 0) = False
[PROOF STEP]
unfolding root_free_def
[PROOF STATE]
proof (prove)
using this:
degree (of_int_poly p) = 1 \<or> (\<forall>x. ipoly p x \<noteq> 0)

goal (1 subgoal):
 1. (ipoly p a = 0) = False
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
degree (of_int_poly p) = 1 \<or> (\<forall>x. ipoly p x \<noteq> 0)
degree p \<noteq> 1

goal (1 subgoal):
 1. (ipoly p a = 0) = False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(ipoly p ?a = 0) = False

goal (1 subgoal):
 1. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
have id: "root_info p = count_roots_interval_rat p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root_info p = count_roots_interval_rat p
[PROOF STEP]
unfolding root_info_def if_False count_roots_interval_rat_code Let_def idd
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if degree p = 1 then Root_Info (\<lambda>l r. if l \<le> Rat.Fract (- coeff p 0) (coeff p 1) \<and> Rat.Fract (- coeff p 0) (coeff p 1) \<le> r then 1 else 0) (\<lambda>b. if Rat.Fract (- coeff p 0) (coeff p 1) \<le> b then 1 else 0) else Root_Info (\<lambda>a b. sign_changes_rat (sturm_rat (of_int_poly p)) a - sign_changes_rat (sturm_rat (of_int_poly p)) b) (\<lambda>a. sign_changes_neg_number_rootat (sturm_rat (of_int_poly p)) - sign_changes_rat (sturm_rat (of_int_poly p)) a)) = Root_Info (\<lambda>a b. sign_changes_rat (sturm_rat (of_int_poly p)) a - sign_changes_rat (sturm_rat (of_int_poly p)) b + 0) (\<lambda>a. sign_changes_neg_number_rootat (sturm_rat (of_int_poly p)) - sign_changes_rat (sturm_rat (of_int_poly p)) a)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
degree p \<noteq> 1

goal (1 subgoal):
 1. (if degree p = 1 then Root_Info (\<lambda>l r. if l \<le> Rat.Fract (- coeff p 0) (coeff p 1) \<and> Rat.Fract (- coeff p 0) (coeff p 1) \<le> r then 1 else 0) (\<lambda>b. if Rat.Fract (- coeff p 0) (coeff p 1) \<le> b then 1 else 0) else Root_Info (\<lambda>a b. sign_changes_rat (sturm_rat (of_int_poly p)) a - sign_changes_rat (sturm_rat (of_int_poly p)) b) (\<lambda>a. sign_changes_neg_number_rootat (sturm_rat (of_int_poly p)) - sign_changes_rat (sturm_rat (of_int_poly p)) a)) = Root_Info (\<lambda>a b. sign_changes_rat (sturm_rat (of_int_poly p)) a - sign_changes_rat (sturm_rat (of_int_poly p)) b + 0) (\<lambda>a. sign_changes_neg_number_rootat (sturm_rat (of_int_poly p)) - sign_changes_rat (sturm_rat (of_int_poly p)) a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
root_info p = count_roots_interval_rat p

goal (1 subgoal):
 1. degree p \<noteq> 1 \<Longrightarrow> root_info_cond (root_info p) p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root_info_cond (root_info p) p
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root_info_cond (count_roots_interval_rat p) p
[PROOF STEP]
by (rule count_roots_interval_rat[OF irreducible\<^sub>d_square_free[OF irr_d]])
[PROOF STATE]
proof (state)
this:
root_info_cond (root_info p) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_test:
  "[] : (Let [(x, Lam [y]. Var y)] (Var x)) \<Down>\<^bsub>[]\<^esub> [(x, Lam [y]. Var y)] : (Lam [y]. Var y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] : let x be Lam [y]. Var y in Var x  \<Down>\<^bsub>[]\<^esub> [(x, Lam [y]. Var y)] : Lam [y]. Var y
[PROOF STEP]
apply(auto intro!: Lambda Application Variable Let
 simp add: fresh_Pair fresh_Cons fresh_Nil fresh_star_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma eval_test2:
  "y \<noteq> x \<Longrightarrow> n \<noteq> y \<Longrightarrow> n \<noteq> x \<Longrightarrow>[] : (Let [(x, Lam [y]. Var y)] (App (Var x) x)) \<Down>\<^bsub>[]\<^esub> [(x, Lam [y]. Var y)] : (Lam [y]. Var y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<noteq> x; n \<noteq> y; n \<noteq> x\<rbrakk> \<Longrightarrow> [] : let x be Lam [y]. Var y in App (Var x) x  \<Down>\<^bsub>[]\<^esub> [(x, Lam [y]. Var y)] : Lam [y]. Var y
[PROOF STEP]
by (auto intro!: Lambda Application Variable Let simp add: fresh_Pair fresh_at_base fresh_Cons fresh_Nil fresh_star_def pure_fresh)


[STATEMENT]
lemma reds_ApplicationI:
  assumes "\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'"
  assumes "\<Delta> : e'[y::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z"
  shows "\<Gamma> : App e x \<Down>\<^bsub>L\<^esub> \<Theta> : z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> : App e x \<Down>\<^bsub>L\<^esub> \<Theta> : z
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma> : App e x \<Down>\<^bsub>L\<^esub> \<Theta> : z
[PROOF STEP]
obtain y' :: var where "atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z, e')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y'. atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z, e') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z, e')

goal (1 subgoal):
 1. \<Gamma> : App e x \<Down>\<^bsub>L\<^esub> \<Theta> : z
[PROOF STEP]
have a: "Lam [y']. ((y' \<leftrightarrow> y) \<bullet> e') = Lam [y]. e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Lam [y']. ((y' \<leftrightarrow> y) \<bullet> e') = Lam [y]. e'
[PROOF STEP]
using \<open>atom y' \<sharp> _\<close>
[PROOF STATE]
proof (prove)
using this:
atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z, e')

goal (1 subgoal):
 1. Lam [y']. ((y' \<leftrightarrow> y) \<bullet> e') = Lam [y]. e'
[PROOF STEP]
by (auto simp add: Abs1_eq_iff fresh_Pair fresh_at_base)
[PROOF STATE]
proof (state)
this:
Lam [y']. ((y' \<leftrightarrow> y) \<bullet> e') = Lam [y]. e'

goal (1 subgoal):
 1. \<Gamma> : App e x \<Down>\<^bsub>L\<^esub> \<Theta> : z
[PROOF STEP]
have b: "((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
proof(cases "x = y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
 2. x \<noteq> y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
 2. x \<noteq> y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
have "atom y' \<sharp> e'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom y' \<sharp> e'
[PROOF STEP]
using \<open>atom y' \<sharp> _\<close>
[PROOF STATE]
proof (prove)
using this:
atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z, e')

goal (1 subgoal):
 1. atom y' \<sharp> e'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atom y' \<sharp> e'

goal (2 subgoals):
 1. x = y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
 2. x \<noteq> y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom y' \<sharp> e'

goal (1 subgoal):
 1. ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
by (simp add: True subst_swap_same  subst_subst_back)
[PROOF STATE]
proof (state)
this:
((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
hence "atom y \<sharp> x"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y

goal (1 subgoal):
 1. atom y \<sharp> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atom y \<sharp> x

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
have [simp]: "(y' \<leftrightarrow> y) \<bullet> x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y' \<leftrightarrow> y) \<bullet> x = x
[PROOF STEP]
using \<open>atom y \<sharp> _\<close>  \<open>atom y' \<sharp> _\<close>
[PROOF STATE]
proof (prove)
using this:
atom y \<sharp> x
atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z, e')

goal (1 subgoal):
 1. (y' \<leftrightarrow> y) \<bullet> x = x
[PROOF STEP]
by (simp add: flip_fresh_fresh fresh_Pair fresh_at_base)
[PROOF STATE]
proof (state)
this:
(y' \<leftrightarrow> y) \<bullet> x = x

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
have "((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = (y' \<leftrightarrow> y) \<bullet> (e'[y::=x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = (y' \<leftrightarrow> y) \<bullet> e'[y::=x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = (y' \<leftrightarrow> y) \<bullet> e'[y::=x]

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = (y' \<leftrightarrow> y) \<bullet> e'[y::=x]

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
have "\<dots> = e'[y::=x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y' \<leftrightarrow> y) \<bullet> e'[y::=x] = e'[y::=x]
[PROOF STEP]
using \<open>atom y \<sharp> _\<close>  \<open>atom y' \<sharp> _\<close>
[PROOF STATE]
proof (prove)
using this:
atom y \<sharp> x
atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z, e')

goal (1 subgoal):
 1. (y' \<leftrightarrow> y) \<bullet> e'[y::=x] = e'[y::=x]
[PROOF STEP]
by (simp add: flip_fresh_fresh fresh_Pair fresh_at_base subst_pres_fresh)
[PROOF STATE]
proof (state)
this:
(y' \<leftrightarrow> y) \<bullet> e'[y::=x] = e'[y::=x]

goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]

goal (1 subgoal):
 1. ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] = e'[y::=x]

goal (1 subgoal):
 1. \<Gamma> : App e x \<Down>\<^bsub>L\<^esub> \<Theta> : z
[PROOF STEP]
have "atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z)
[PROOF STEP]
using  \<open>atom y' \<sharp> _\<close>
[PROOF STATE]
proof (prove)
using this:
atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z, e')

goal (1 subgoal):
 1. atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z)
[PROOF STEP]
by (simp add: fresh_Pair)
[PROOF STATE]
proof (state)
this:
atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z)

goal (1 subgoal):
 1. \<Gamma> : App e x \<Down>\<^bsub>L\<^esub> \<Theta> : z
[PROOF STEP]
from this assms[folded a b]
[PROOF STATE]
proof (chain)
picking this:
atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z)
\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y']. ((y' \<leftrightarrow> y) \<bullet> e')
\<Delta> : ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
atom y' \<sharp> (\<Gamma>, e, x, L, \<Delta>, \<Theta>, z)
\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y']. ((y' \<leftrightarrow> y) \<bullet> e')
\<Delta> : ((y' \<leftrightarrow> y) \<bullet> e')[y'::=x] \<Down>\<^bsub>L\<^esub> \<Theta> : z

goal (1 subgoal):
 1. \<Gamma> : App e x \<Down>\<^bsub>L\<^esub> \<Theta> : z
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<Gamma> : App e x \<Down>\<^bsub>L\<^esub> \<Theta> : z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reds_SmartLet: "\<lbrakk>
    atom ` domA \<Delta> \<sharp>* (\<Gamma>, L);
    \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z
  \<rbrakk> \<Longrightarrow>
    \<Gamma> : SmartLet \<Delta> body \<Down>\<^bsub>L\<^esub> \<Theta> : z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z\<rbrakk> \<Longrightarrow> \<Gamma> : SmartLet \<Delta> body \<Down>\<^bsub>L\<^esub> \<Theta> : z
[PROOF STEP]
unfolding SmartLet_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z\<rbrakk> \<Longrightarrow> \<Gamma> : (if \<Delta> = [] then body else Let \<Delta> body) \<Down>\<^bsub>L\<^esub> \<Theta> : z
[PROOF STEP]
by (auto intro: reds.Let)


[STATEMENT]
lemma reds_isValI:
  "isVal z \<Longrightarrow> \<Gamma> : z \<Down>\<^bsub>L\<^esub> \<Gamma> : z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isVal z \<Longrightarrow> \<Gamma> : z \<Down>\<^bsub>L\<^esub> \<Gamma> : z
[PROOF STEP]
by (cases z rule:isVal.cases) (auto intro: reds.intros)


[STATEMENT]
lemma reds_doesnt_forget:
  "\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z \<Longrightarrow> domA \<Gamma> \<subseteq> domA \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z \<Longrightarrow> domA \<Gamma> \<subseteq> domA \<Delta>
[PROOF STEP]
by(induct rule: reds.induct) auto


[STATEMENT]
lemma reds_avoids_live':
 assumes "\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z"
 shows "(domA \<Delta> - domA \<Gamma>) \<inter> set L = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (domA \<Delta> - domA \<Gamma>) \<inter> set L = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z

goal (1 subgoal):
 1. (domA \<Delta> - domA \<Gamma>) \<inter> set L = {}
[PROOF STEP]
by(induct rule:reds.induct)
  (auto dest: map_of_domAD fresh_distinct_list simp add: fresh_star_Pair)


[STATEMENT]
lemma reds_avoids_live:
  "\<lbrakk> \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z;
   x \<in> set L;
   x \<notin> domA \<Gamma>
  \<rbrakk> \<Longrightarrow> x \<notin> domA \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z; x \<in> set L; x \<notin> domA \<Gamma>\<rbrakk> \<Longrightarrow> x \<notin> domA \<Delta>
[PROOF STEP]
using reds_avoids_live'
[PROOF STATE]
proof (prove)
using this:
?\<Gamma> : ?e \<Down>\<^bsub>?L\<^esub> ?\<Delta> : ?z \<Longrightarrow> (domA ?\<Delta> - domA ?\<Gamma>) \<inter> set ?L = {}

goal (1 subgoal):
 1. \<lbrakk>\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z; x \<in> set L; x \<notin> domA \<Gamma>\<rbrakk> \<Longrightarrow> x \<notin> domA \<Delta>
[PROOF STEP]
by blast


[STATEMENT]
lemma reds_fresh:" \<lbrakk> \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z;
   atom (x::var) \<sharp> (\<Gamma>, e)
  \<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> (domA \<Delta> - set L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z; atom x \<sharp> (\<Gamma>, e)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set L
[PROOF STEP]
proof(induct rule: reds.induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>\<Gamma> xa e L. atom x \<sharp> (\<Gamma>, Lam [xa]. e) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Lam [xa]. e) \<or> x \<in> domA \<Gamma> - set L
 2. \<And>y \<Gamma> e xa L \<Delta> \<Theta> z e'. \<lbrakk>atom y \<sharp> (\<Gamma>, e, xa, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; atom x \<sharp> (\<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, Lam [y]. e') \<or> x \<in> domA \<Delta> - set L; \<Delta> : e'[y::=xa] \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, e'[y::=xa]) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, App e xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 3. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 4. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 5. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 6. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
case (Lambda \<Gamma> x e)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Gamma>, Lam [x]. e)

goal (6 subgoals):
 1. \<And>\<Gamma> xa e L. atom x \<sharp> (\<Gamma>, Lam [xa]. e) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Lam [xa]. e) \<or> x \<in> domA \<Gamma> - set L
 2. \<And>y \<Gamma> e xa L \<Delta> \<Theta> z e'. \<lbrakk>atom y \<sharp> (\<Gamma>, e, xa, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; atom x \<sharp> (\<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, Lam [y]. e') \<or> x \<in> domA \<Delta> - set L; \<Delta> : e'[y::=xa] \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, e'[y::=xa]) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, App e xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 3. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 4. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 5. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 6. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (\<Gamma>, Lam [x]. e)

goal (1 subgoal):
 1. atom x \<sharp> (\<Gamma>, Lam [x]. e) \<or> x \<in> domA \<Gamma> - set L_
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Gamma>, Lam [x]. e) \<or> x \<in> domA \<Gamma> - set L_

goal (5 subgoals):
 1. \<And>y \<Gamma> e xa L \<Delta> \<Theta> z e'. \<lbrakk>atom y \<sharp> (\<Gamma>, e, xa, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; atom x \<sharp> (\<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, Lam [y]. e') \<or> x \<in> domA \<Delta> - set L; \<Delta> : e'[y::=xa] \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, e'[y::=xa]) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, App e xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 4. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>y \<Gamma> e xa L \<Delta> \<Theta> z e'. \<lbrakk>atom y \<sharp> (\<Gamma>, e, xa, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; atom x \<sharp> (\<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, Lam [y]. e') \<or> x \<in> domA \<Delta> - set L; \<Delta> : e'[y::=xa] \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, e'[y::=xa]) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, App e xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 4. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
case (Application y \<Gamma> e x' L \<Delta> \<Theta> z e')
[PROOF STATE]
proof (state)
this:
atom y \<sharp> (\<Gamma>, e, x', L, \<Delta>, \<Theta>, z)
\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'
atom x \<sharp> (\<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, Lam [y]. e') \<or> x \<in> domA \<Delta> - set L
\<Delta> : e'[y::=x'] \<Down>\<^bsub>L\<^esub> \<Theta> : z
atom x \<sharp> (\<Delta>, e'[y::=x']) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
atom x \<sharp> (\<Gamma>, App e x')

goal (5 subgoals):
 1. \<And>y \<Gamma> e xa L \<Delta> \<Theta> z e'. \<lbrakk>atom y \<sharp> (\<Gamma>, e, xa, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; atom x \<sharp> (\<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, Lam [y]. e') \<or> x \<in> domA \<Delta> - set L; \<Delta> : e'[y::=xa] \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, e'[y::=xa]) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, App e xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 4. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
hence "atom x \<sharp> (\<Delta>, Lam [y]. e') \<or> x \<in> domA \<Delta> - set (x' # L)"
[PROOF STATE]
proof (prove)
using this:
atom y \<sharp> (\<Gamma>, e, x', L, \<Delta>, \<Theta>, z)
\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'
atom x \<sharp> (\<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, Lam [y]. e') \<or> x \<in> domA \<Delta> - set L
\<Delta> : e'[y::=x'] \<Down>\<^bsub>L\<^esub> \<Theta> : z
atom x \<sharp> (\<Delta>, e'[y::=x']) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
atom x \<sharp> (\<Gamma>, App e x')

goal (1 subgoal):
 1. atom x \<sharp> (\<Delta>, Lam [y]. e') \<or> x \<in> domA \<Delta> - set (x' # L)
[PROOF STEP]
by (auto simp add: fresh_Pair)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Delta>, Lam [y]. e') \<or> x \<in> domA \<Delta> - set (x' # L)

goal (5 subgoals):
 1. \<And>y \<Gamma> e xa L \<Delta> \<Theta> z e'. \<lbrakk>atom y \<sharp> (\<Gamma>, e, xa, L, \<Delta>, \<Theta>, z); \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : Lam [y]. e'; atom x \<sharp> (\<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, Lam [y]. e') \<or> x \<in> domA \<Delta> - set L; \<Delta> : e'[y::=xa] \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, e'[y::=xa]) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, App e xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 3. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 4. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 5. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (\<Delta>, Lam [y]. e') \<or> x \<in> domA \<Delta> - set (x' # L)

goal (1 subgoal):
 1. atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. atom x \<sharp> (\<Delta>, Lam [y]. e') \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. x \<in> domA \<Delta> - set (x' # L) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
assume  "atom x \<sharp> (\<Delta>, Lam [y]. e')"
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Delta>, Lam [y]. e')

goal (2 subgoals):
 1. atom x \<sharp> (\<Delta>, Lam [y]. e') \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. x \<in> domA \<Delta> - set (x' # L) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
hence "atom x \<sharp> e'[y ::= x']"
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (\<Delta>, Lam [y]. e')

goal (1 subgoal):
 1. atom x \<sharp> e'[y::=x']
[PROOF STEP]
using Application.prems
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (\<Delta>, Lam [y]. e')
atom x \<sharp> (\<Gamma>, App e x')

goal (1 subgoal):
 1. atom x \<sharp> e'[y::=x']
[PROOF STEP]
by (auto intro: subst_pres_fresh simp add: fresh_Pair)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> e'[y::=x']

goal (2 subgoals):
 1. atom x \<sharp> (\<Delta>, Lam [y]. e') \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. x \<in> domA \<Delta> - set (x' # L) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> e'[y::=x']

goal (1 subgoal):
 1. atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
using Application.hyps(5) \<open>atom x \<sharp> (\<Delta>, Lam [y]. e')\<close>
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> e'[y::=x']
atom x \<sharp> (\<Delta>, e'[y::=x']) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
atom x \<sharp> (\<Delta>, Lam [y]. e')

goal (1 subgoal):
 1. atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L

goal (1 subgoal):
 1. x \<in> domA \<Delta> - set (x' # L) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> domA \<Delta> - set (x' # L) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
assume "x \<in> domA \<Delta> - set (x' # L)"
[PROOF STATE]
proof (state)
this:
x \<in> domA \<Delta> - set (x' # L)

goal (1 subgoal):
 1. x \<in> domA \<Delta> - set (x' # L) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> domA \<Delta> - set (x' # L)

goal (1 subgoal):
 1. atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
using reds_doesnt_forget[OF Application.hyps(4)]
[PROOF STATE]
proof (prove)
using this:
x \<in> domA \<Delta> - set (x' # L)
domA \<Delta> \<subseteq> domA \<Theta>

goal (1 subgoal):
 1. atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L

goal (4 subgoals):
 1. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 3. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 3. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
case(Variable \<Gamma> v e L \<Delta> z)
[PROOF STATE]
proof (state)
this:
map_of \<Gamma> v = Some e
delete v \<Gamma> : e \<Down>\<^bsub>v # L\<^esub> \<Delta> : z
atom x \<sharp> (delete v \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (v # L)
atom x \<sharp> (\<Gamma>, Var v)

goal (4 subgoals):
 1. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 3. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
have "atom x \<sharp> \<Gamma>" and "atom x \<sharp> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<sharp> \<Gamma> &&& atom x \<sharp> v
[PROOF STEP]
using Variable.prems(1)
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (\<Gamma>, Var v)

goal (1 subgoal):
 1. atom x \<sharp> \<Gamma> &&& atom x \<sharp> v
[PROOF STEP]
by (auto simp add: fresh_Pair)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> \<Gamma>
atom x \<sharp> v

goal (4 subgoals):
 1. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 3. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
from fresh_delete[OF this(1)]
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> delete ?v \<Gamma>
[PROOF STEP]
have "atom x \<sharp> delete v \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> delete ?v \<Gamma>

goal (1 subgoal):
 1. atom x \<sharp> delete v \<Gamma>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
atom x \<sharp> delete v \<Gamma>

goal (4 subgoals):
 1. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 3. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
atom x \<sharp> delete v \<Gamma>

goal (4 subgoals):
 1. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 3. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
have "v \<in> domA \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> domA \<Gamma>
[PROOF STEP]
using Variable.hyps(1)
[PROOF STATE]
proof (prove)
using this:
map_of \<Gamma> v = Some e

goal (1 subgoal):
 1. v \<in> domA \<Gamma>
[PROOF STEP]
by (metis domA_from_set map_of_SomeD)
[PROOF STATE]
proof (state)
this:
v \<in> domA \<Gamma>

goal (4 subgoals):
 1. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 3. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
from fresh_map_of[OF this  \<open>atom x \<sharp> \<Gamma>\<close>]
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> the (map_of \<Gamma> v)
[PROOF STEP]
have "atom x \<sharp> the (map_of \<Gamma> v)"
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> the (map_of \<Gamma> v)

goal (1 subgoal):
 1. atom x \<sharp> the (map_of \<Gamma> v)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
atom x \<sharp> the (map_of \<Gamma> v)

goal (4 subgoals):
 1. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 3. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
hence "atom x \<sharp> e"
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> the (map_of \<Gamma> v)

goal (1 subgoal):
 1. atom x \<sharp> e
[PROOF STEP]
using \<open>map_of \<Gamma> v = Some e\<close>
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> the (map_of \<Gamma> v)
map_of \<Gamma> v = Some e

goal (1 subgoal):
 1. atom x \<sharp> e
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atom x \<sharp> e

goal (4 subgoals):
 1. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 3. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> delete v \<Gamma>
atom x \<sharp> e
[PROOF STEP]
have "atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (v # L)"
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> delete v \<Gamma>
atom x \<sharp> e

goal (1 subgoal):
 1. atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (v # L)
[PROOF STEP]
using Variable.hyps(3)
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> delete v \<Gamma>
atom x \<sharp> e
atom x \<sharp> (delete v \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (v # L)

goal (1 subgoal):
 1. atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (v # L)
[PROOF STEP]
by (auto simp add: fresh_Pair)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (v # L)

goal (4 subgoals):
 1. \<And>\<Gamma> xa e L \<Delta> z. \<lbrakk>map_of \<Gamma> xa = Some e; delete xa \<Gamma> : e \<Down>\<^bsub>xa # L\<^esub> \<Delta> : z; atom x \<sharp> (delete xa \<Gamma>, e) \<Longrightarrow> atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (xa # L); atom x \<sharp> (\<Gamma>, Var xa)\<rbrakk> \<Longrightarrow> atom x \<sharp> ((xa, z) # \<Delta>, z) \<or> x \<in> domA ((xa, z) # \<Delta>) - set L
 2. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 3. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 4. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (v # L)

goal (1 subgoal):
 1. atom x \<sharp> ((v, z) # \<Delta>, z) \<or> x \<in> domA ((v, z) # \<Delta>) - set L
[PROOF STEP]
using \<open>atom x \<sharp> v\<close>
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (\<Delta>, z) \<or> x \<in> domA \<Delta> - set (v # L)
atom x \<sharp> v

goal (1 subgoal):
 1. atom x \<sharp> ((v, z) # \<Delta>, z) \<or> x \<in> domA ((v, z) # \<Delta>) - set L
[PROOF STEP]
by (auto simp add: fresh_Pair fresh_Cons fresh_at_base)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> ((v, z) # \<Delta>, z) \<or> x \<in> domA ((v, z) # \<Delta>) - set L

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 3. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 3. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
case (Bool \<Gamma> b L)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Gamma>, Bool b)

goal (3 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. \<And>\<Gamma> b L. atom x \<sharp> (\<Gamma>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
 3. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (\<Gamma>, Bool b)

goal (1 subgoal):
 1. atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Gamma>, Bool b) \<or> x \<in> domA \<Gamma> - set L

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
case (IfThenElse \<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z)
[PROOF STATE]
proof (state)
this:
\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b
atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L
\<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z
atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
from \<open>atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<close>
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)
[PROOF STEP]
have "atom x \<sharp> (\<Gamma>, scrut)" and "atom x \<sharp> (e\<^sub>1, e\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)

goal (1 subgoal):
 1. atom x \<sharp> (\<Gamma>, scrut) &&& atom x \<sharp> (e\<^sub>1, e\<^sub>2)
[PROOF STEP]
by (auto simp add: fresh_Pair)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Gamma>, scrut)
atom x \<sharp> (e\<^sub>1, e\<^sub>2)

goal (2 subgoals):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. \<And>\<Gamma> scrut L \<Delta> b e\<^sub>1 e\<^sub>2 \<Theta> z. \<lbrakk>\<Gamma> : scrut \<Down>\<^bsub>L\<^esub> \<Delta> : Bool b; atom x \<sharp> (\<Gamma>, scrut) \<Longrightarrow> atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L; \<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, scrut ? e\<^sub>1 : e\<^sub>2)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
from IfThenElse.hyps(2)[OF this(1)]
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (\<Delta>, Bool b) \<or> x \<in> domA \<Delta> - set L

goal (1 subgoal):
 1. atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. atom x \<sharp> (\<Delta>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. x \<in> domA \<Delta> - set L \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
assume "atom x \<sharp> (\<Delta>, Bool b)"
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Delta>, Bool b)

goal (2 subgoals):
 1. atom x \<sharp> (\<Delta>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. x \<in> domA \<Delta> - set L \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
with \<open>atom x \<sharp> (e\<^sub>1, e\<^sub>2)\<close>
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> (e\<^sub>1, e\<^sub>2)
atom x \<sharp> (\<Delta>, Bool b)
[PROOF STEP]
have "atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (e\<^sub>1, e\<^sub>2)
atom x \<sharp> (\<Delta>, Bool b)

goal (1 subgoal):
 1. atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Delta>, if b then e\<^sub>1 else e\<^sub>2)

goal (2 subgoals):
 1. atom x \<sharp> (\<Delta>, Bool b) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. x \<in> domA \<Delta> - set L \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
from IfThenElse.hyps(4)[OF this]
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L

goal (1 subgoal):
 1. atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L

goal (1 subgoal):
 1. x \<in> domA \<Delta> - set L \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> domA \<Delta> - set L \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
assume "x \<in> domA \<Delta> - set L"
[PROOF STATE]
proof (state)
this:
x \<in> domA \<Delta> - set L

goal (1 subgoal):
 1. x \<in> domA \<Delta> - set L \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
with reds_doesnt_forget[OF \<open>\<Delta> : (if b then e\<^sub>1 else e\<^sub>2) \<Down>\<^bsub>L\<^esub> \<Theta> : z\<close>]
[PROOF STATE]
proof (chain)
picking this:
domA \<Delta> \<subseteq> domA \<Theta>
x \<in> domA \<Delta> - set L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
domA \<Delta> \<subseteq> domA \<Theta>
x \<in> domA \<Delta> - set L

goal (1 subgoal):
 1. atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
case (Let \<Delta> \<Gamma> L body \<Theta> z)
[PROOF STATE]
proof (state)
this:
atom ` domA \<Delta> \<sharp>* (\<Gamma>, L)
\<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z
atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
atom x \<sharp> (\<Gamma>, Let \<Delta> body)

goal (1 subgoal):
 1. \<And>\<Delta> \<Gamma> L body \<Theta> z. \<lbrakk>atom ` domA \<Delta> \<sharp>* (\<Gamma>, L); \<Delta> @ \<Gamma> : body \<Down>\<^bsub>L\<^esub> \<Theta> : z; atom x \<sharp> (\<Delta> @ \<Gamma>, body) \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L; atom x \<sharp> (\<Gamma>, Let \<Delta> body)\<rbrakk> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
proof (cases "x \<in> domA \<Delta>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> domA \<Delta> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. x \<notin> domA \<Delta> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> domA \<Delta>

goal (2 subgoals):
 1. x \<in> domA \<Delta> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. x \<notin> domA \<Delta> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
hence "atom x \<sharp> \<Delta>"
[PROOF STATE]
proof (prove)
using this:
x \<notin> domA \<Delta>

goal (1 subgoal):
 1. atom x \<sharp> \<Delta>
[PROOF STEP]
using Let.prems
[PROOF STATE]
proof (prove)
using this:
x \<notin> domA \<Delta>
atom x \<sharp> (\<Gamma>, Let \<Delta> body)

goal (1 subgoal):
 1. atom x \<sharp> \<Delta>
[PROOF STEP]
by(auto simp add: fresh_Pair)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> \<Delta>

goal (2 subgoals):
 1. x \<in> domA \<Delta> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
 2. x \<notin> domA \<Delta> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
apply(rule Let.hyps(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom x \<sharp> (\<Delta> @ \<Gamma>, body)
[PROOF STEP]
using Let.prems \<open>atom x \<sharp> \<Delta>\<close> False
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (\<Gamma>, Let \<Delta> body)
atom x \<sharp> \<Delta>
x \<notin> domA \<Delta>

goal (1 subgoal):
 1. atom x \<sharp> (\<Delta> @ \<Gamma>, body)
[PROOF STEP]
by (auto simp add: fresh_Pair fresh_append)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L

goal (1 subgoal):
 1. x \<in> domA \<Delta> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> domA \<Delta> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> domA \<Delta>

goal (1 subgoal):
 1. x \<in> domA \<Delta> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
hence "x \<notin> set L"
[PROOF STATE]
proof (prove)
using this:
x \<in> domA \<Delta>

goal (1 subgoal):
 1. x \<notin> set L
[PROOF STEP]
using Let(1)
[PROOF STATE]
proof (prove)
using this:
x \<in> domA \<Delta>
atom ` domA \<Delta> \<sharp>* (\<Gamma>, L)

goal (1 subgoal):
 1. x \<notin> set L
[PROOF STEP]
by (metis fresh_PairD(2) fresh_star_def image_eqI set_not_fresh)
[PROOF STATE]
proof (state)
this:
x \<notin> set L

goal (1 subgoal):
 1. x \<in> domA \<Delta> \<Longrightarrow> atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
x \<in> domA \<Delta>
x \<notin> set L
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> domA \<Delta>
x \<notin> set L

goal (1 subgoal):
 1. atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
using reds_doesnt_forget[OF Let.hyps(2)]
[PROOF STATE]
proof (prove)
using this:
x \<in> domA \<Delta>
x \<notin> set L
domA (\<Delta> @ \<Gamma>) \<subseteq> domA \<Theta>

goal (1 subgoal):
 1. atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (\<Theta>, z) \<or> x \<in> domA \<Theta> - set L

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reds_fresh_fv: "\<lbrakk> \<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z;
   x \<in> fv (\<Delta>, z) \<and> (x \<notin> domA \<Delta> \<or>  x \<in> set L)
  \<rbrakk> \<Longrightarrow> x \<in> fv (\<Gamma>, e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z; x \<in> fv (\<Delta>, z) \<and> (x \<notin> domA \<Delta> \<or> x \<in> set L)\<rbrakk> \<Longrightarrow> x \<in> fv (\<Gamma>, e)
[PROOF STEP]
using reds_fresh
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<Gamma> : ?e \<Down>\<^bsub>?L\<^esub> ?\<Delta> : ?z; atom ?x \<sharp> (?\<Gamma>, ?e)\<rbrakk> \<Longrightarrow> atom ?x \<sharp> (?\<Delta>, ?z) \<or> ?x \<in> domA ?\<Delta> - set ?L

goal (1 subgoal):
 1. \<lbrakk>\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z; x \<in> fv (\<Delta>, z) \<and> (x \<notin> domA \<Delta> \<or> x \<in> set L)\<rbrakk> \<Longrightarrow> x \<in> fv (\<Gamma>, e)
[PROOF STEP]
unfolding fv_def fresh_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<Gamma> : ?e \<Down>\<^bsub>?L\<^esub> ?\<Delta> : ?z; atom ?x \<notin> supp (?\<Gamma>, ?e)\<rbrakk> \<Longrightarrow> atom ?x \<notin> supp (?\<Delta>, ?z) \<or> ?x \<in> domA ?\<Delta> - set ?L

goal (1 subgoal):
 1. \<lbrakk>\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z; x \<in> {v. atom v \<in> supp (\<Delta>, z)} \<and> (x \<notin> domA \<Delta> \<or> x \<in> set L)\<rbrakk> \<Longrightarrow> x \<in> {v. atom v \<in> supp (\<Gamma>, e)}
[PROOF STEP]
by blast


[STATEMENT]
lemma new_free_vars_on_heap:
  assumes "\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z"
  shows "fv (\<Delta>, z) - domA \<Delta> \<subseteq> fv (\<Gamma>, e) - domA \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (\<Delta>, z) - domA \<Delta> \<subseteq> fv (\<Gamma>, e) - domA \<Gamma>
[PROOF STEP]
using reds_fresh_fv[OF assms(1)] reds_doesnt_forget[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
?x \<in> fv (\<Delta>, z) \<and> (?x \<notin> domA \<Delta> \<or> ?x \<in> set L) \<Longrightarrow> ?x \<in> fv (\<Gamma>, e)
domA \<Gamma> \<subseteq> domA \<Delta>

goal (1 subgoal):
 1. fv (\<Delta>, z) - domA \<Delta> \<subseteq> fv (\<Gamma>, e) - domA \<Gamma>
[PROOF STEP]
by auto


[STATEMENT]
lemma reds_pres_closed:
  assumes "\<Gamma> : e \<Down>\<^bsub>L\<^esub> \<Delta> : z"
  and     "fv (\<Gamma>, e) \<subseteq> set L \<union> domA \<Gamma>"
  shows   "fv (\<Delta>, z) \<subseteq> set L \<union> domA \<Delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (\<Delta>, z) \<subseteq> set L \<union> domA \<Delta>
[PROOF STEP]
using new_free_vars_on_heap[OF assms(1)] assms(2)
[PROOF STATE]
proof (prove)
using this:
fv (\<Delta>, z) - domA \<Delta> \<subseteq> fv (\<Gamma>, e) - domA \<Gamma>
fv (\<Gamma>, e) \<subseteq> set L \<union> domA \<Gamma>

goal (1 subgoal):
 1. fv (\<Delta>, z) \<subseteq> set L \<union> domA \<Delta>
[PROOF STEP]
by auto