diff -r c9d3dda79fe3 -r 758904445fb2 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Fri Mar 26 16:20:39 2010 +0100
+++ b/Nominal/Parser.thy	Fri Mar 26 17:22:02 2010 +0100
@@ -294,6 +294,43 @@
 ML {* fun map_option _ NONE = NONE
         | map_option f (SOME x) = SOME (f x) *}
 
+(* nominal_datatype2 does the following things in order:
+  1) define the raw datatype
+  2) define the raw binding functions
+  3) define permutations of the raw datatype and show that raw type is in the pt typeclass
+  4) define fv and fb_bn
+  5) define alpha and alpha_bn
+  6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...)             (Proof by cases; simp)
+  6) prove alpha_eq_iff    (C1 x = C2 y \<leftrightarrow> P x y ...)
+     (left-to-right by intro rule, right-to-left by cases; simp)
+  7) prove bn_eqvt (common induction on the raw datatype)
+  8) prove fv_eqvt (common induction on the raw datatype with help of above)
+  9) prove alpha_eqvt and alpha_bn_eqvt
+     (common alpha-induction, unfolding alpha_gen, permute of #* and =)
+ 10) prove that alpha and alpha_bn are equivalence relations
+     (common induction and application of 'compose' lemmas)
+ 11) define quotient types
+ 12) prove bn respects     (common induction and simp with alpha_gen)
+ 13) prove fv respects     (common induction and simp with alpha_gen)
+ 14) prove permute respects    (unfolds to alpha_eqvt)
+ 15) prove alpha_bn respects
+     (alpha_induct then cases then sym and trans of the relations)
+ 16) show that alpha implies alpha_bn (by unduction, needed in following step)
+ 17) prove respects for all datatype constructors
+     (unfold eq_iff and alpha_gen; introduce zero permutations; simp)
+ 18) define lifted constructors, fv, bn, alpha_bn, permutations
+ 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass
+ 20) lift permutation simplifications
+ 21) lift induction
+ 22) lift fv
+ 23) lift bn
+ 24) lift eq_iff
+ 25) lift alpha_distincts
+ 26) lift fv and bn eqvts
+ 27) prove that union of arguments supports constructors
+ 28) show that the lifted type is in fs typeclass     (* by q_induct, supports *)
+ 29) prove supp = fv
+*)
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let