--- a/Nominal/NewParser.thy	Sat May 01 09:15:46 2010 +0100
+++ b/Nominal/NewParser.thy	Sun May 02 14:06:26 2010 +0100
@@ -258,9 +258,78 @@
 end
 *}
 
+
+text {* 
+  nominal_datatype2 does the following things in order:
+
+Parser.thy/raw_nominal_decls
+  1) define the raw datatype
+  2) define the raw binding functions 
+
+Perm.thy/define_raw_perms
+  3) define permutations of the raw datatype and show that the raw type is 
+     in the pt typeclass
+      
+Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha
+  4) define fv and fv_bn
+  5) define alpha and alpha_bn
+
+Perm.thy/distinct_rel
+  6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...)             (Proof by cases; simp)
+
+Tacs.thy/build_rel_inj
+  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)
+Equivp.thy/prove_eqvt
+  7) prove bn_eqvt (common induction on the raw datatype)
+  8) prove fv_eqvt (common induction on the raw datatype with help of above)
+Rsp.thy/build_alpha_eqvts
+  9) prove alpha_eqvt and alpha_bn_eqvt
+     (common alpha-induction, unfolding alpha_gen, permute of #* and =)
+Equivp.thy/build_alpha_refl & Equivp.thy/build_equivps
+ 10) prove that alpha and alpha_bn are equivalence relations
+     (common induction and application of 'compose' lemmas)
+Lift.thy/define_quotient_types
+ 11) define quotient types
+Rsp.thy/build_fvbv_rsps
+ 12) prove bn respects     (common induction and simp with alpha_gen)
+Rsp.thy/prove_const_rsp
+ 13) prove fv respects     (common induction and simp with alpha_gen)
+ 14) prove permute respects    (unfolds to alpha_eqvt)
+Rsp.thy/prove_alpha_bn_rsp
+ 15) prove alpha_bn respects
+     (alpha_induct then cases then sym and trans of the relations)
+Rsp.thy/prove_alpha_alphabn
+ 16) show that alpha implies alpha_bn (by unduction, needed in following step)
+Rsp.thy/prove_const_rsp
+ 17) prove respects for all datatype constructors
+     (unfold eq_iff and alpha_gen; introduce zero permutations; simp)
+Perm.thy/quotient_lift_consts_export
+ 18) define lifted constructors, fv, bn, alpha_bn, permutations
+Perm.thy/define_lifted_perms
+ 19) lift permutation zero and add properties to show that quotient type is in the pt typeclass
+Lift.thy/lift_thm
+ 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
+Equivp.thy/prove_supports
+ 27) prove that union of arguments supports constructors
+Equivp.thy/prove_fs
+ 28) show that the lifted type is in fs typeclass     (* by q_induct, supports *)
+Equivp.thy/supp_eq
+ 29) prove supp = fv
+*}
+
+
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
+
+  (* definition of the raw datatype and raw bn-functions *)
   val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) =
     raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
 
@@ -279,6 +348,7 @@
   val induct = #induct dtinfo;
   val exhausts = map #exhaust dtinfos;
 
+  (* definitions of raw permutations *)
   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
 
@@ -579,6 +649,8 @@
   (main_parser >> nominal_datatype2_cmd)
 *}
 
+
+(*
 atom_decl name
 
 nominal_datatype lam =
@@ -658,21 +730,24 @@
 
 thm ty_tys.fv[simplified ty_tys.supp]
 thm ty_tys.eq_iff
+*)
+
 
 (* some further tests *)
 
-nominal_datatype ty =
-  Vr "name"
-| Fn "ty" "ty"
+(*
+nominal_datatype ty2 =
+  Vr2 "name"
+| Fn2 "ty2" "ty2"
 
-nominal_datatype tys =
-  All xs::"name fset" ty::"ty_raw" bind_res xs in ty
+nominal_datatype tys2 =
+  All2 xs::"name fset" ty::"ty2" bind_res xs in ty
 
 nominal_datatype lam2 =
   Var2 "name"
 | App2 "lam2" "lam2 list"
 | Lam2 x::"name" t::"lam2" bind x in t
-
+*)