# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272812547 -3600
# Node ID 12ce87b55f974b0b69e5b1355b37de63080a22ae
# Parent  19fe16dd36c208fdae5ac6401b0a2c273d8cc99c
tried to add some comments in the huge(!) nominal2_cmd function

diff -r 19fe16dd36c2 -r 12ce87b55f97 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sun May 02 16:01:45 2010 +0100
+++ b/Nominal/NewParser.thy	Sun May 02 16:02:27 2010 +0100
@@ -328,15 +328,13 @@
 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
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
   val {descr, sorts, ...} = dtinfo;
-  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
-  val raw_tys = map (fn (i, _) => nth_dtyp i) descr;
+  val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
   val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
 
   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
@@ -359,13 +357,18 @@
   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
   val thy = Local_Theory.exit_global lthy2;
   val thy_name = Context.theory_name thy
+
   val lthy3 = Theory_Target.init NONE thy;
   val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
+  (* definition of raw fv_functions *)
   val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  
+  (* definition of raw alphas *)
   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
     define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a;
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
+  
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
@@ -374,12 +377,18 @@
     (rel_distinct ~~ alpha_ts_nobn));
   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
+  
+  (* definition of raw_alpha_eq_iff  lemmas *)
   val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
+  
+  (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
   val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
   val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
   fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy
   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
+
+  (* provind alpha equivalence *)
   val _ = warning "Proving equivalence";
   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
   val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
@@ -425,7 +434,8 @@
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a;
   val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
-  val (qalpha_ts_bn, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
+  val (qalpha_ts_bn, qalphabn_defs, lthy12c) = 
+    quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
   val _ = warning "Lifting permutations";
   val thy = Local_Theory.exit_global lthy12c;
   val perm_names = map (fn x => "permute_" ^ x) qty_names
@@ -441,7 +451,8 @@
   fun note_simp_suffix s th ctxt =
     snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
   val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
-    [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13;
+    [Attrib.internal (K (Rule_Cases.case_names constr_names))]), 
+    [Rule_Cases.name constr_names q_induct]) lthy13;
   val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct
   val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
   val q_perm = map (lift_thm qtys lthy14) raw_perm_def;
@@ -649,8 +660,6 @@
   (main_parser >> nominal_datatype2_cmd)
 *}
 
-
-(*
 atom_decl name
 
 nominal_datatype lam =
@@ -730,7 +739,7 @@
 
 thm ty_tys.fv[simplified ty_tys.supp]
 thm ty_tys.eq_iff
-*)
+
 
 
 (* some further tests *)