diff -r 9c3f6a4d95d4 -r e26c6c728b9e Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Sun Jun 26 17:55:22 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Sun Jun 26 21:42:07 2011 +0100
@@ -52,12 +52,24 @@
     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 fcb2: "atom b \<sharp> f b S c"
+    using e[symmetric]
+    apply(simp add: Abs_eq_iff2)
+    apply(erule exE)
+    apply(simp add: alphas)
+    apply(rule_tac p="p" in permute_boolE)
+    apply(simp add: fresh_eqvt)
+    apply(subst perm2)
+    using fresh
+    apply(auto simp add: fresh_star_def)[1]
+    apply(simp add: atom_eqvt)
+    apply(rule fcb1)
+    done
   have fin1: "finite (supp (f a T c))"
     apply(rule_tac S="supp (a, T, c)" in supports_finite)
     apply(simp add: supports_def)
@@ -133,7 +145,20 @@
   finally show ?thesis by simp
 qed
 
-
+(*
+lemma Abs_lst_fcb2:
+  fixes as bs :: "atom list"
+    and x y :: "'b :: fs"
+    and c::"'c::fs"
+  assumes e: "(Abs_lst as x) = (Abs_lst bs y)"
+  and fcb1: "(set as) \<sharp>* f as x c"
+  and fcb2: "(set bs) \<sharp>* f bs y c"
+  and fresh1: "set as \<sharp>* c"
+  and fresh2: "set bs \<sharp>* c"
+  and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
+  and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
+  shows "f as x c = f bs y c"
+*)
 
 nominal_primrec 
   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
@@ -169,14 +194,12 @@
   apply(elim conjE)
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
   apply(elim conjE)
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
@@ -185,7 +208,6 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
@@ -194,7 +216,6 @@
   apply(elim conjE)
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
@@ -204,7 +225,6 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
@@ -215,7 +235,6 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
@@ -224,14 +243,12 @@
   apply(elim conjE)
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
   apply(elim conjE)
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
@@ -240,7 +257,6 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
@@ -251,7 +267,6 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
@@ -263,7 +278,6 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
@@ -274,7 +288,6 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
@@ -287,7 +300,6 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)
@@ -297,7 +309,6 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base 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)