--- a/Nominal/Ex/Classical.thy	Thu Jun 23 13:09:17 2011 +0100
+++ b/Nominal/Ex/Classical.thy	Thu Jun 23 22:21:43 2011 +0100
@@ -9,7 +9,7 @@
 
 nominal_datatype trm =
   Ax "name" "coname"
-| Cut n::"coname" t1::"trm" c::"coname" t2::"trm"             bind n in t1, bind c in t2  
+| Cut c::"coname" t1::"trm" n::"name" t2::"trm"             bind n in t1, bind c in t2  
      ("Cut <_>._ '(_')._" [100,100,100,100] 100)
 | NotR n::"name" t::"trm" "coname"                            bind n in t
      ("NotR '(_')._ _" [100,100,100] 100)
@@ -46,7 +46,7 @@
 thm trm.supp
 thm trm.supp[simplified]
 
-nominal_primrec 
+nominal_primrec (* (invariant "\<lambda>(_, e, d) y. atom e \<sharp> y \<and> atom d \<sharp> y") *)
   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)" 
@@ -68,6 +68,8 @@
   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)
@@ -96,8 +98,21 @@
   apply(metis)  
   apply(simp add: fresh_star_def)
   apply(metis)
-  -- "clashes"
+  -- "compatibility"
   apply(simp_all)
+  apply(rule conjI)
+  apply(erule 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(drule sym)
+  apply(drule sym)
+  apply(drule sym)
+  apply(drule sym)
+  apply(simp add: eqvt_at_def swap_fresh_fresh)
   oops
 
 end