--- /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
+
+
+

--- a/Nominal/Ex/TestMorePerm.thy	Thu Apr 08 10:25:38 2010 +0200
+++ b/Nominal/Ex/TestMorePerm.thy	Thu Apr 08 11:40:13 2010 +0200
@@ -2,34 +2,6 @@
 imports "../Parser"
 begin
 
-(* Since there are more permutations, we do not know how to prove equivalence
-   (it is probably not true with the way alpha is defined now) so *)
-ML {* val _ = cheat_equivp := true *}
-
-
-atom_decl name
-
-(* example from my PHD *)
-
-atom_decl coname
-
-nominal_datatype phd =
-   Ax "name" "coname"
-|  Cut n::"coname" t1::"phd" c::"coname" t2::"phd"              bind n in t1, bind c in t2
-|  AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname"  bind c1 in t1, bind c2 in t2
-|  AndL1 n::"name" t::"phd" "name"                              bind n in t
-|  AndL2 n::"name" t::"phd" "name"                              bind n in t
-|  ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name"        bind c in t1, bind n in t2
-|  ImpR c::"coname" n::"name" t::"phd" "coname"                 bind n in t, bind c in t
-
-thm phd.fv
-thm phd.eq_iff
-thm phd.bn
-thm phd.perm
-thm phd.induct
-thm phd.distinct
-thm phd.fv[simplified phd.supp]
-
 text {* weirdo example from Peter Sewell's bestiary *}
 
 nominal_datatype weird =

--- a/TODO	Thu Apr 08 10:25:38 2010 +0200
+++ b/TODO	Thu Apr 08 11:40:13 2010 +0200
@@ -35,6 +35,13 @@
   (both are equivalent, but the second seems to be closer to
    the fv-function)
 
+- when there are more than one shallow binder, then alpha
+  equivalence creates more than one permutation. According
+  to the paper, this is incorrect.
+
+  Example in TestMorePerm.
+
+
 - nested recursion, like types "trm list" in a constructor
 
 - define permute_bn automatically and prove properties of it