
diff -r 5335c0ea743a -r 313e6f2cdd89 Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/Classical.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -83,21 +83,28 @@
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   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(simp add: eqvt_at_def)
+  apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(clarify)
+  apply(simp add: eqvt_at_def)
+  apply(simp add: 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: 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(simp add: eqvt_at_def)
+  apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
+  apply(simp add: atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
   apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -105,7 +112,9 @@
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(rule conjI)
   apply(elim conjE)
@@ -114,7 +123,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -124,7 +135,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -132,13 +145,17 @@
   apply(erule_tac c="(da,ea)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   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: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
@@ -146,7 +163,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -156,7 +175,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -167,7 +188,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -177,7 +200,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -189,7 +214,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)  
@@ -197,8 +224,11 @@
   apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
+  apply(simp add: eqvt_at_def)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -210,7 +240,9 @@
   apply(simp add: Abs_fresh_star)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -254,19 +286,25 @@
   apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(subgoal_tac "eqvt_at nrename_sumC (M, ua, va)")
@@ -274,7 +312,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -285,7 +325,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -294,7 +336,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -304,7 +348,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -314,7 +360,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -322,13 +370,17 @@
   apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(erule_tac c="(ua,va)" in Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(elim conjE)
   apply(rule conjI)
@@ -337,7 +389,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -346,7 +400,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -355,7 +411,9 @@
   apply(simp add: Abs_fresh_star)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(erule conjE)+
   apply(rule conjI)
@@ -364,7 +422,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)
@@ -373,7 +433,9 @@
   apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_at_base fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def)
   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
   apply(blast)
   apply(blast)




