--- a/Nominal/Ex/Classical.thy	Fri Jun 24 11:18:18 2011 +0900
+++ b/Nominal/Ex/Classical.thy	Fri Jun 24 09:42:44 2011 +0100
@@ -46,10 +46,12 @@
 thm trm.supp
 thm trm.supp[simplified]
 
-lemma swap_at_base_sort: "sort_of (atom a) \<noteq> sort_of (atom x) \<Longrightarrow> sort_of (atom b) \<noteq> sort_of (atom x) \<Longrightarrow> (atom a \<rightleftharpoons> atom b) \<bullet> x = x"
+lemma swap_at_base_sort: 
+  "sort_of (atom a) \<noteq> sort_of (atom x) \<Longrightarrow> sort_of (atom b) \<noteq> sort_of (atom x) 
+  \<Longrightarrow> (atom a \<rightleftharpoons> atom b) \<bullet> x = x"
   by (rule swap_fresh_fresh) (simp_all add: fresh_at_base(1))
 
-nominal_primrec (* (invariant "\<lambda>(_, e, d) y. atom e \<sharp> y \<and> atom d \<sharp> y") *)
+nominal_primrec 
   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
 where
   "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" 
@@ -71,8 +73,6 @@
   apply(simp only: eqvt_def)
   apply(simp only: crename_graph_def)
   apply (rule, perm_simp, rule)
-  (*apply(erule crename_graph.induct)
-  apply(simp add: trm.fresh)*)
   apply(rule TrueI)
   -- "covered all cases"
   apply(case_tac x)
@@ -91,6 +91,142 @@
   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(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(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(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(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(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(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(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
   oops
 
 end