--- a/Nominal/Ex/Lambda.thy	Wed Apr 13 13:44:25 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Fri Apr 15 15:20:56 2011 +0900
@@ -20,6 +20,26 @@
 apply(auto simp add: fresh_star_def)
 done 
 
+lemma Abs1_eq_fdest:
+  fixes x y :: "'a :: at_base"
+    and S T :: "'b :: fs"
+  assumes "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"
+  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom x \<sharp> f x T"
+  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> atom y \<sharp> f x T"
+  and "x \<noteq> y \<Longrightarrow> atom y \<sharp> T \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> T = S \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S"
+  and "sort_of (atom x) = sort_of (atom y)"
+  shows "f x T = f y S"
+using assms apply -
+apply (subst (asm) Abs1_eq_iff')
+apply simp_all
+apply (elim conjE disjE)
+apply simp
+apply(rule trans)
+apply (rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])
+apply(rule fresh_star_supp_conv)
+apply(simp add: supp_swap fresh_star_def)
+apply(simp add: swap_commute)
+done
 
 text {* height function *}
 
@@ -32,11 +52,8 @@
 defer
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto simp add: lam.distinct lam.eq_iff)
-apply(simp add: Abs_eq_iff alphas)
-apply(clarify)
-apply(subst (4) supp_perm_eq[where p="p", symmetric])
-apply(simp add: pure_supp fresh_star_def)
-apply(simp add: eqvt_at_def)
+apply (erule Abs1_eq_fdest)
+apply(simp_all add: fresh_def pure_supp eqvt_at_def)
 apply(subgoal_tac "\<And>p x r. height_graph x r \<Longrightarrow> height_graph (p \<bullet> x) (p \<bullet> r)") 
 unfolding eqvt_def
 apply(rule allI)
@@ -82,23 +99,12 @@
 defer
 apply(rule_tac y="x" in lam.exhaust)
 apply(simp_all)[3]
-apply(simp_all only: lam.distinct)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: Abs_eq_iff)
-apply(erule exE)
-apply(simp add: alphas)
-apply(simp add: atom_eqvt)
-apply(clarify)
-apply(rule trans)
-apply(rule_tac p="p" in supp_perm_eq[symmetric])
-apply(simp (no_asm) add: supp_removeAll)
+apply(simp_all add: lam.distinct lam.eq_iff)
+apply (erule Abs1_eq_fdest)
+apply(simp add: supp_removeAll fresh_def)
 apply(drule supp_eqvt_at)
 apply(simp add: finite_supp)
-apply(auto simp add: fresh_star_def)[1]
-unfolding eqvt_at_def
-apply(simp only: removeAll_eqvt atom_eqvt)
+apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def)
 apply(subgoal_tac "\<And>p x r. frees_lst_graph x r \<Longrightarrow> frees_lst_graph (p \<bullet> x) (p \<bullet> r)") 
 unfolding eqvt_def
 apply(rule allI)
@@ -151,36 +157,15 @@
 apply(auto simp add: lam.distinct lam.eq_iff)
 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
 apply(blast)+
-apply(simp add: fresh_star_def)
-apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t")
-apply(subst (asm) Abs_eq_iff2)
-apply(simp add: alphas atom_eqvt)
-apply(clarify)
-apply(rule trans)
-apply(rule_tac p="p" in supp_perm_eq[symmetric])
-apply(rule fresh_star_supp_conv)
-apply(drule fresh_star_perm_set_conv)
-apply(simp add: finite_supp)
-apply(subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* ([[atom x]]lst. subst_sumC (t, ya, sa))")
-apply(auto simp add: fresh_star_def)[1]
-apply(simp (no_asm) add: fresh_star_def)
-apply(rule conjI)
-apply(simp (no_asm) add: Abs_fresh_iff)
-apply(clarify)
-apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
-apply(simp add: finite_supp)
-apply(simp (no_asm_use) add: fresh_Pair)
-apply(simp add: Abs_fresh_iff)
-apply(simp)
-apply(simp add: Abs_fresh_iff)
-apply(subgoal_tac "p \<bullet> ya = ya")
-apply(subgoal_tac "p \<bullet> sa = sa")
-apply(simp add: atom_eqvt eqvt_at_def)
-apply(rule perm_supp_eq)
-apply(auto simp add: fresh_star_def fresh_Pair)[1]
-apply(rule perm_supp_eq)
-apply(auto simp add: fresh_star_def fresh_Pair)[1]
-apply(simp add: Abs_fresh_iff)
+apply(simp_all add: fresh_star_def fresh_Pair_elim)
+apply (erule Abs1_eq_fdest)
+apply(simp_all add: Abs_fresh_iff)
+apply(drule_tac a="atom (xa)" in fresh_eqvt_at)
+apply(simp_all add: finite_supp fresh_Pair)
+apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa")
+apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya")
+apply(simp add: eqvt_at_def)
+apply(rule perm_supp_eq,simp add: fresh_star_def fresh_Pair supp_swap)+
 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") 
 unfolding eqvt_def
 apply(rule allI)
@@ -256,6 +241,28 @@
 apply (auto simp add: lam.fresh fresh_at_base)
 done
 
+lemma height_ge_one:
+  shows "1 \<le> (height e)"
+by (induct e rule: lam.induct) (simp_all)
+
+theorem height_subst:
+  shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')"
+proof (nominal_induct e avoiding: x e' rule: lam.strong_induct)
+  case (Var y)
+  have "1 \<le> height e'" by (rule height_ge_one)
+  then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp
+next
+  case (Lam y e1)
+  hence ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by simp
+  moreover
+  have vc: "atom y\<sharp>x" "atom y\<sharp>e'" by fact+ (* usual variable convention *)
+  ultimately show "height ((Lam [y]. e1)[x::=e']) \<le> height (Lam [y]. e1) - 1 + height e'" by simp
+next
+  case (App e1 e2)
+  hence ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')"
+    and ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by simp_all
+  then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'"  by simp
+qed
 
 subsection {* single-step beta-reduction *}
 
@@ -332,9 +339,7 @@
 
 lemma [eqvt]:
   shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
-  apply(induct xs arbitrary: n)
-  apply(simp_all add: permute_pure)
-  done
+  by (induct xs arbitrary: n) (simp_all add: permute_pure)
 
 nominal_primrec
   trans :: "lam \<Rightarrow> name list \<Rightarrow> ln"
@@ -349,50 +354,18 @@
 apply(simp_all add: fresh_star_def)[3]
 apply(blast)
 apply(blast)
-apply(simp_all add: lam.distinct)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(simp add: lam.eq_iff)
-apply(erule conjE)
-apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t")
+apply(simp_all add: lam.distinct lam.eq_iff)
+apply(elim conjE)
+apply clarify
+apply (erule Abs1_eq_fdest)
+apply (simp_all add: ln.fresh)
 prefer 2
-apply(simp add: Abs_fresh_iff)
-apply(subst (asm) Abs_eq_iff2)
-apply(auto)
-apply(simp add: alphas)
-apply(simp add: atom_eqvt)
-apply(clarify)
-apply(rule trans)
-apply(rule_tac p="p" in supp_perm_eq[symmetric])
+apply(drule supp_eqvt_at)
+apply (auto simp add: finite_supp supp_Pair fresh_def supp_Cons supp_at_base)[2]
 prefer 2
-apply (subgoal_tac "p \<bullet> xsa = xsa")
+apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")
 apply (simp add: eqvt_at_def)
-apply (rule supp_perm_eq)
-apply (rule fresh_star_supp_conv)
-apply (subgoal_tac "{atom (p \<bullet> x), atom x} \<sharp>* xsa")
-apply (simp add: fresh_star_def fresh_def)
-apply blast
-apply (simp add: fresh_star_def fresh_def)
-apply (simp add:  ln.supp)
-apply(rule fresh_star_supp_conv)
-apply (subst (asm) supp_perm_pair)
-apply (elim disjE)
-apply (simp add: fresh_star_def supp_zero_perm)
-apply (simp add: flip_def[symmetric])
-apply(subgoal_tac "supp (x \<leftrightarrow> p \<bullet> x) \<sharp>* trans_sumC (t, x # xsa)")
-apply simp
-apply (subst flip_def)
-apply (simp add: supp_swap)
-apply (simp add: fresh_star_def)
-apply (rule)
-apply rule
-prefer 2
-apply(drule_tac a="atom (p \<bullet> x)" in fresh_eqvt_at)
-apply(simp add: finite_supp)
-apply(simp (no_asm_use) add: fresh_Pair)
-apply(simp add: Abs_fresh_iff fresh_Cons)[1]
-apply (metis Rep_name_inverse atom_name_def fresh_at_base)
-apply assumption
+apply (metis atom_name_def swap_fresh_fresh)
 oops
 
 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)"