--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Classical.thy	Thu Apr 08 11:40:13 2010 +0200
@@ -0,0 +1,70 @@
+theory Classical
+imports "../Parser"
+begin
+
+(* 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
+*)
+ML {* val _ = cheat_equivp := true *}
+
+atom_decl name
+atom_decl coname
+
+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 in t, bind c in t
+
+
+thm trm.fv
+thm trm.eq_iff
+thm trm.bn
+thm trm.perm
+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)"
+
+
+end
+
+
+