--- a/Nominal/Ex/Classical.thy	Tue Jun 01 15:46:07 2010 +0200
+++ b/Nominal/Ex/Classical.thy	Wed Jun 02 11:37:51 2010 +0200
@@ -4,26 +4,23 @@
 
 (* example from my Urban's PhD *)
 
-(* 
-  alpha_trm_raw is incorrectly defined, therefore the equivalence proof
-  does not go through; below the correct definition is given
-*)
-
 atom_decl name
 atom_decl coname
 
-ML {* val _ = cheat_equivp := true *}
+declare [[STEPS = 9]]
 
 nominal_datatype trm =
    Ax "name" "coname"
-|  Cut n::"coname" t1::"trm" c::"coname" t2::"trm"              bind n in t1, bind c in t2
-|  AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname"  bind c1 in t1, bind c2 in t2
-|  AndL1 n::"name" t::"trm" "name"                              bind n in t
-|  AndL2 n::"name" t::"trm" "name"                              bind n in t
-|  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"        bind c in t1, bind n in t2
-|  ImpR c::"coname" n::"name" t::"trm" "coname"                 bind n c in t
+|  Cut n::"coname" t1::"trm" c::"coname" t2::"trm"              bind_set n in t1, bind_set c in t2
+|  AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname"  bind_set c1 in t1, bind_set c2 in t2
+|  AndL1 n::"name" t::"trm" "name"                              bind_set n in t
+|  AndL2 n::"name" t::"trm" "name"                              bind_set n in t
+|  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"        bind_set c in t1, bind_set n in t2
+|  ImpR c::"coname" n::"name" t::"trm" "coname"                 bind_set n c in t
 
+thm alpha_trm_raw.intros[no_vars]
 
+(*
 thm trm.fv
 thm trm.eq_iff
 thm trm.bn
@@ -31,44 +28,7 @@
 thm trm.induct
 thm trm.distinct
 thm trm.fv[simplified trm.supp]
-
-(* correct alpha definition *)
-
-inductive
-  alpha
-where
-  "\<lbrakk>name = namea; coname = conamea\<rbrakk> \<Longrightarrow> 
-  alpha (Ax_raw name coname) (Ax_raw namea conamea)"
-| "\<lbrakk>\<exists>pi. ({atom coname1}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a); 
-    \<exists>pia. ({atom coname2}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a)\<rbrakk> \<Longrightarrow>
-   alpha (Cut_raw coname1 trm_raw1 coname2 trm_raw2)
-         (Cut_raw coname1a trm_raw1a coname2a trm_raw2a)"
-| "\<lbrakk>\<exists>pi. ({atom coname1}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a);
-    \<exists>pia. ({atom coname2}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a);
-    coname3 = coname3a\<rbrakk> \<Longrightarrow>
-   alpha (AndR_raw coname1 trm_raw1 coname2 trm_raw2 coname3)
-         (AndR_raw coname1a trm_raw1a coname2a trm_raw2a coname3a)"
-| "\<lbrakk>\<exists>pi. ({atom name1}, trm_raw) \<approx>gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa);
-    name2 = name2a\<rbrakk> \<Longrightarrow>
-   alpha (AndL1_raw name1 trm_raw name2) (AndL1_raw name1a trm_rawa name2a)"
-| "\<lbrakk>\<exists>pi. ({atom name1}, trm_raw) \<approx>gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa);
-     name2 = name2a\<rbrakk> \<Longrightarrow>
-   alpha (AndL2_raw name1 trm_raw name2) (AndL2_raw name1a trm_rawa name2a)"
-| "\<lbrakk>\<exists>pi. ({atom coname}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom conamea}, trm_raw1a);
-    \<exists>pia. ({atom name1}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom name1a}, trm_raw2a);
-    name2 = name2a\<rbrakk> \<Longrightarrow>
-   alpha (ImpL_raw coname trm_raw1 name1 trm_raw2 name2)
-         (ImpL_raw conamea trm_raw1a name1a trm_raw2a name2a)"
-| "\<lbrakk>\<exists>pi.({atom name} \<union> {atom coname1}, trm_raw) \<approx>gen alpha fv_trm_raw pi  
-        ({atom namea} \<union> {atom coname1a}, trm_rawa); coname2 = coname2a\<rbrakk> \<Longrightarrow>
-   alpha (ImpR_raw coname1 name trm_raw coname2)
-         (ImpR_raw coname1a namea trm_rawa coname2a)"
-
-thm alpha.intros
-
-equivariance alpha
-
-thm eqvts_raw
+*)
 
 
 end