Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/Classical.thy
changeset 3183 313e6f2cdd89
parent 2975 c62e26830420
child 3192 14c7d7e29c44 
--- 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)
nominal2