# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1309038703 -3600
# Node ID 754aa24006c816f0e55b7ca50fc5d2bcd1f233f1
# Parent  d66430c7c4f1c5dbe754861b268c7dfc54095c6a
did all cases, except the multiple binder case

diff -r d66430c7c4f1 -r 754aa24006c8 Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Sat Jun 25 21:28:24 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Sat Jun 25 22:51:43 2011 +0100
@@ -53,8 +53,8 @@
   assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)"
   and fcb: "\<And>a T. atom a \<sharp> f a T c"
   and fresh: "{atom a, atom b} \<sharp>* c"
-  and p1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c"
-  and p2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) 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))"
@@ -62,7 +62,7 @@
     apply(simp add: supports_def)
     apply(simp add: fresh_def[symmetric])
     apply(clarify)
-    apply(subst p1)
+    apply(subst perm1)
     apply(simp add: supp_swap fresh_star_def)
     apply(simp add: swap_fresh_fresh fresh_Pair)
     apply(simp add: finite_supp)
@@ -72,7 +72,7 @@
     apply(simp add: supports_def)
     apply(simp add: fresh_def[symmetric])
     apply(clarify)
-    apply(subst p2)
+    apply(subst perm2)
     apply(simp add: supp_swap fresh_star_def)
     apply(simp add: swap_fresh_fresh fresh_Pair)
     apply(simp add: finite_supp)
@@ -109,7 +109,7 @@
     done
   also have "... = f d ((a \<leftrightarrow> d) \<bullet> T) c"
     unfolding flip_def
-    apply(subst p1)
+    apply(subst perm1)
     using fresh fr
     apply(simp add: supp_swap fresh_star_def fresh_Pair)
     apply(simp)
@@ -117,7 +117,7 @@
   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 p2)
+    apply(subst perm2)
     using fresh fr
     apply(simp add: supp_swap fresh_star_def fresh_Pair)
     apply(simp)
@@ -181,133 +181,117 @@
   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)
-  -- "old fcb"
+  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 atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(blast)
+  apply(blast)
+  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(rule conjI)
   apply(elim conjE)
   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
-  apply(erule Abs_lst1_fcb)
-  apply(simp add: Abs_fresh_iff)
+  apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
+  apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(erule fresh_eqvt_at)
-  apply(simp add: finite_supp)
-  apply(simp add: fresh_Pair fresh_at_base(1))
-  apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh)
-  apply simp
+  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(blast)
+  apply(blast)
+  apply(erule conjE)+
+  apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
+  apply(subgoal_tac "eqvt_at crename_sumC (Na, 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 atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(blast)
   apply(blast)
   apply(elim conjE)
-  apply(erule Abs_lst1_fcb)
+  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(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(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 atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(blast)
+  apply(blast)
+  apply(erule 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(erule fresh_eqvt_at)
-  apply(simp add: finite_supp)
-  apply(simp add: fresh_Pair fresh_at_base(1))
-  apply(simp add: fresh_Pair)
-  apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh)
-  apply simp
+  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(blast)
+  apply(blast)
+  apply(rule conjI)
+  apply(erule 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 atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(blast)
+  apply(blast)
+  apply(erule conjE)+
+  apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
+  apply(subgoal_tac "eqvt_at crename_sumC (Na, 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 atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  apply(blast)
+  apply(blast)
+  defer
   apply(erule conjE)+
   apply(rule conjI)
   apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
-  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_Pair fresh_at_base(1))
-  apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh)
-  apply simp
-  apply(blast)
-  apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
-  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_Pair fresh_at_base(1))
-  apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh)
-  apply simp
-  apply(blast)
-  apply(elim conjE)
-  apply(erule Abs_lst1_fcb)
-  apply(simp add: Abs_fresh_iff)
+  apply(subgoal_tac "eqvt_at crename_sumC (Ma, da, ea)")
+  apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(erule fresh_eqvt_at)
-  apply(simp add: finite_supp)
-  apply(simp add: fresh_Pair fresh_at_base(1))
-  apply(simp add: fresh_Pair)
-  apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh)
-  apply simp
-  apply(elim conjE)
-  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_Pair fresh_at_base(1))
-  apply(simp add: fresh_Pair)
-  apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh)
-  apply simp
-  apply(erule conjE)+
-  apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
-  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_Pair fresh_at_base(1))
-  apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh)
-  apply simp
+  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(blast)
-  apply(erule conjE)+
-  apply(subgoal_tac "eqvt_at crename_sumC (M, da, ea)")
-  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_Pair fresh_at_base(1))
-  apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh)
-  apply simp
-  apply(blast)
-  apply(rule conjI)
-  apply(elim conjE)
-  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_Pair fresh_at_base(1))
-  apply(simp add: eqvt_at_def swap_at_base_sort)
-  apply simp
-  apply(elim conjE)
-  apply(erule Abs_lst1_fcb)
-  apply(simp add: Abs_fresh_iff)
+  apply(blast)  
+  apply(subgoal_tac "eqvt_at crename_sumC (N, da, ea)")
+  apply(subgoal_tac "eqvt_at crename_sumC (Na, da, ea)")
+  apply(erule Abs_lst1_fcb2)
   apply(simp add: Abs_fresh_iff)
-  apply(erule fresh_eqvt_at)
-  apply(simp add: finite_supp)
-  apply(simp add: fresh_Pair fresh_at_base(1))
-  apply(simp add: fresh_Pair)
-  apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh)
-  apply simp
-  apply(erule conjE)+
-  defer
-  apply(elim conjE)
-  apply(rule conjI)
-  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_Pair fresh_at_base(1))
-  apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh)
-  apply simp
-  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_Pair fresh_at_base(1))
-  apply(simp add: fresh_Pair)
-  apply(simp add: eqvt_at_def swap_at_base_sort swap_fresh_fresh)
-  apply simp
+  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(blast)
+  apply(blast)
   oops
 
 end