--- a/Nominal/Ex/Lambda.thy	Sat Jun 25 22:51:43 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Sun Jun 26 17:55:22 2011 +0100
@@ -3,6 +3,93 @@
 begin
 
 
+lemma Abs_lst1_fcb2:
+  fixes a b :: "'a :: at"
+    and S T :: "'b :: fs"
+    and c::"'c::fs"
+  assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)"
+  and fcb1: "atom a \<sharp> f a T c"
+  and fcb2: "atom b \<sharp> f b S c"
+  and fresh: "{atom a, atom b} \<sharp>* c"
+  and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c"
+  and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c"
+  shows "f a T c = f b S c"
+proof -
+  have fin1: "finite (supp (f a T c))"
+    apply(rule_tac S="supp (a, T, c)" in supports_finite)
+    apply(simp add: supports_def)
+    apply(simp add: fresh_def[symmetric])
+    apply(clarify)
+    apply(subst perm1)
+    apply(simp add: supp_swap fresh_star_def)
+    apply(simp add: swap_fresh_fresh fresh_Pair)
+    apply(simp add: finite_supp)
+    done
+  have fin2: "finite (supp (f b S c))"
+    apply(rule_tac S="supp (b, S, c)" in supports_finite)
+    apply(simp add: supports_def)
+    apply(simp add: fresh_def[symmetric])
+    apply(clarify)
+    apply(subst perm2)
+    apply(simp add: supp_swap fresh_star_def)
+    apply(simp add: swap_fresh_fresh fresh_Pair)
+    apply(simp add: finite_supp)
+    done
+  obtain d::"'a::at" where fr: "atom d \<sharp> (a, b, S, T, c, f a T c, f b S c)" 
+    using obtain_fresh'[where x="(a, b, S, T, c, f a T c, f b S c)"]
+    apply(auto simp add: finite_supp supp_Pair fin1 fin2)
+    done
+  have "(a \<leftrightarrow> d) \<bullet> (Abs_lst [atom a] T) = (b \<leftrightarrow> d) \<bullet> (Abs_lst [atom b] S)" 
+    apply(simp (no_asm_use) only: flip_def)
+    apply(subst swap_fresh_fresh)
+    apply(simp add: Abs_fresh_iff)
+    using fr
+    apply(simp add: Abs_fresh_iff)
+    apply(subst swap_fresh_fresh)
+    apply(simp add: Abs_fresh_iff)
+    using fr
+    apply(simp add: Abs_fresh_iff)
+    apply(rule e)
+    done
+  then have "Abs_lst [atom d] ((a \<leftrightarrow> d) \<bullet> T) = Abs_lst [atom d] ((b \<leftrightarrow> d) \<bullet> S)"
+    apply (simp add: swap_atom flip_def)
+    done
+  then have eq: "(a \<leftrightarrow> d) \<bullet> T = (b \<leftrightarrow> d) \<bullet> S"
+    by (simp add: Abs1_eq_iff)
+  have "f a T c = (a \<leftrightarrow> d) \<bullet> f a T c"
+    unfolding flip_def
+    apply(rule sym)
+    apply(rule swap_fresh_fresh)
+    using fcb1 
+    apply(simp)
+    using fr
+    apply(simp add: fresh_Pair)
+    done
+  also have "... = f d ((a \<leftrightarrow> d) \<bullet> T) c"
+    unfolding flip_def
+    apply(subst perm1)
+    using fresh fr
+    apply(simp add: supp_swap fresh_star_def fresh_Pair)
+    apply(simp)
+    done
+  also have "... = f d ((b \<leftrightarrow> d) \<bullet> S) c" using eq by simp
+  also have "... = (b \<leftrightarrow> d) \<bullet> f b S c"
+    unfolding flip_def
+    apply(subst perm2)
+    using fresh fr
+    apply(simp add: supp_swap fresh_star_def fresh_Pair)
+    apply(simp)
+    done
+  also have "... = f b S c"   
+    apply(rule flip_fresh_fresh)
+    using fcb2
+    apply(simp)
+    using fr
+    apply(simp add: fresh_Pair)
+    done
+  finally show ?thesis by simp
+qed
+
 
 atom_decl name
 
@@ -44,11 +131,12 @@
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)
-apply (erule Abs_lst1_fcb)
+apply (erule_tac c="()" in Abs_lst1_fcb2)
+apply(simp add: supp_removeAll fresh_def)
 apply(simp add: supp_removeAll fresh_def)
-apply(drule supp_eqvt_at)
-apply(simp add: finite_supp)
-apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def)
+apply(simp add: fresh_star_def fresh_Unit)
+apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt)
+apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt)
 done
 
 termination
@@ -73,10 +161,12 @@
   apply(rule_tac y="x" in lam.exhaust)
   apply(auto)[3]
   apply(simp)
-  apply(erule Abs_lst1_fcb)
-  apply(simp_all add: fresh_minus_atom_set)
-  apply(erule fresh_eqvt_at)
-  apply(simp_all add: finite_supp eqvt_at_def eqvts)
+  apply(erule_tac c="()" in Abs_lst1_fcb2)
+  apply(simp add: fresh_minus_atom_set)
+  apply(simp add: fresh_minus_atom_set)
+  apply(simp add: fresh_star_def fresh_Unit)
+  apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl)
+  apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl)
   done
 
 termination 
@@ -155,14 +245,14 @@
   "height (Var x) = 1"
 | "height (App t1 t2) = max (height t1) (height t2) + 1"
 | "height (Lam [x].t) = height t + 1"
-  unfolding eqvt_def height_graph_def
+  apply(simp add: eqvt_def height_graph_def)
   apply (rule, perm_simp, rule)
-apply(rule TrueI)
-apply(rule_tac y="x" in lam.exhaust)
-apply(auto simp add: lam.distinct lam.eq_iff)
-apply (erule Abs_lst1_fcb)
-apply(simp_all add: fresh_def pure_supp eqvt_at_def)
-done
+  apply(rule TrueI)
+  apply(rule_tac y="x" in lam.exhaust)
+  apply(auto)
+  apply (erule_tac c="()" in Abs_lst1_fcb2)
+  apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
+  done
 
 termination
   by lexicographic_order
@@ -180,19 +270,16 @@
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
   unfolding eqvt_def subst_graph_def
   apply (rule, perm_simp, rule)
-apply(rule TrueI)
-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_all add: fresh_star_def fresh_Pair_elim)
-apply (erule Abs_lst1_fcb)
-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(simp_all add: swap_fresh_fresh)
+  apply(rule TrueI)
+  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_all add: fresh_star_def fresh_Pair_elim)
+  apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
+  apply(simp_all add: Abs_fresh_iff)
+  apply(simp add: fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
 done
 
 termination
@@ -365,18 +452,21 @@
   apply (simp add: eqvt_def trans_graph_def)
   apply (rule, perm_simp, rule)
   apply (erule trans_graph.induct)
-  apply (auto simp add: ln.fresh)
+  apply (auto simp add: ln.fresh)[3]
   apply (simp add: supp_lookup_fresh)
   apply (simp add: fresh_star_def ln.fresh)
   apply (simp add: ln.fresh fresh_star_def)
+  apply(auto)[1]
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply (auto simp add: fresh_star_def)[3]
-  apply (erule Abs_lst1_fcb)
-  apply (simp_all add: fresh_star_def)
-  apply (drule supp_eqvt_at)
-  apply (rule finite_supp)
-  apply (auto simp add: supp_Pair fresh_def supp_Cons supp_at_base)[1]
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
+  apply(simp_all)
+  apply(erule conjE)+
+  apply (erule Abs_lst1_fcb2)
+  apply (simp add: fresh_star_def)
+  apply (simp add: fresh_star_def)
+  apply (simp add: fresh_star_def)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   done
 
 termination
@@ -395,10 +485,14 @@
   apply(simp_all)
   apply(case_tac x)
   apply(rule_tac y="a" and c="b" in lam.strong_exhaust)
-  apply(auto simp add: fresh_star_def)
-  apply(erule Abs_lst1_fcb)
-  apply(simp_all add: pure_fresh)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
+  apply(auto simp add: fresh_star_def)[3]
+  apply(erule conjE)
+  apply(erule Abs_lst1_fcb2)
+  apply(simp add: pure_fresh fresh_star_def)
+  apply(simp add: pure_fresh fresh_star_def)
+  apply(simp add: pure_fresh fresh_star_def)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   done
 
 termination
@@ -460,13 +554,15 @@
   apply(rule TrueI)
   apply (case_tac x)
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
-  apply (auto simp add: fresh_star_def fresh_at_list)
-  apply (rule_tac f="dblam_in" in arg_cong)
-  apply (erule Abs_lst1_fcb)
-  apply (simp_all add: pure_fresh)
-  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa")
-  apply (simp add: eqvt_at_def)
-  apply (metis atom_name_def swap_fresh_fresh fresh_at_list)
+  apply (auto simp add: fresh_star_def fresh_at_list)[3]
+  apply(simp_all)
+  apply(erule conjE)
+  apply (erule_tac c="xsa" in Abs_lst1_fcb2)
+  apply (simp add: pure_fresh)
+  apply (simp add: pure_fresh)
+  apply(simp add: fresh_star_def fresh_at_list)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq db_in_eqvt)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq db_in_eqvt)
   done
 
 termination
@@ -549,43 +645,37 @@
 | "apply_subst (Var x) t2 = App (Var x) t2"
 | "apply_subst (App t0 t1) t2 = App (App t0 t1) t2"
 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"
-apply(simp add: eval_apply_subst_graph_def eqvt_def)
-apply(rule, perm_simp, rule)
-apply(rule TrueI)
-apply (case_tac x)
-apply (case_tac a rule: lam.exhaust)
-apply simp_all[3]
-apply blast
-apply (case_tac b)
-apply (rule_tac y="a" and c="ba" in lam.strong_exhaust)
-apply simp_all[3]
-apply blast
-apply blast
-apply (simp add: Abs1_eq_iff fresh_star_def)
-apply(simp_all)
-apply(erule Abs_lst1_fcb)
-apply (simp add: Abs_fresh_iff)
-apply (simp add: Abs_fresh_iff)
-apply (erule fresh_eqvt_at)
-apply (simp add: finite_supp)
-apply (simp add: fresh_Inl)
-apply (simp add: eqvt_at_def)
-apply simp
-apply clarify
-apply(erule Abs_lst1_fcb)
-apply (erule fresh_eqvt_at)
-apply (simp add: finite_supp)
-apply (simp add: fresh_Inl var_fresh_subst)
-apply (erule fresh_eqvt_at)
-apply (simp add: finite_supp)
-apply (simp add: fresh_Inl)
-apply (simp add: fresh_def)
-using supp_subst apply blast
-apply (simp add: eqvt_at_def subst_eqvt)
-apply (subst (2) swap_fresh_fresh)
-apply assumption+
-apply rule
-apply simp
+  apply(simp add: eval_apply_subst_graph_def eqvt_def)
+  apply(rule, perm_simp, rule)
+  apply(rule TrueI)
+  apply (case_tac x)
+  apply (case_tac a rule: lam.exhaust)
+  apply simp_all[3]
+  apply blast
+  apply (case_tac b)
+  apply (rule_tac y="a" and c="ba" in lam.strong_exhaust)
+  apply simp_all[3]
+  apply blast
+  apply blast
+  apply (simp add: Abs1_eq_iff fresh_star_def)
+  apply(simp_all)
+  apply(erule_tac c="()" in Abs_lst1_fcb2)
+  apply (simp add: Abs_fresh_iff)
+  apply (simp add: Abs_fresh_iff)
+  apply(simp add: fresh_star_def fresh_Unit)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(erule conjE)
+  apply(erule_tac c="t2a" in Abs_lst1_fcb2)
+  apply (erule fresh_eqvt_at)
+  apply (simp add: finite_supp)
+  apply (simp add: fresh_Inl var_fresh_subst)
+  apply (erule fresh_eqvt_at)
+  apply (simp add: finite_supp)
+  apply (simp add: fresh_Inl var_fresh_subst)
+  apply(simp add: fresh_star_def fresh_Unit)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt)
 done