
diff -r 107c06267f33 -r c6d30d5f5ba1 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sun Aug 15 11:03:13 2010 +0800
+++ b/Nominal/NewParser.thy	Sun Aug 15 14:00:28 2010 +0800
@@ -312,20 +312,19 @@
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
-  val all_raw_constrs = 
+  val raw_constrs = 
     flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts))
-  val all_raw_tys = all_dtyps descr sorts
-  val all_raw_ty_names = map (fst o dest_Type) all_raw_tys
+  val raw_tys = all_dtyps descr sorts
+  val raw_full_ty_names = map (fst o dest_Type) raw_tys
   
-  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_ty_names  
-  val inject_thms = flat (map #inject dtinfos)
-  val distinct_thms = flat (map #distinct dtinfos)
-  val constr_thms = inject_thms @ distinct_thms 
-  
-  val raw_induct_thm = #induct dtinfo;
-  val raw_induct_thms = #inducts dtinfo;
-  val exhaust_thms = map #exhaust dtinfos;
-  val raw_size_trms = map size_const all_raw_tys
+  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names  
+ 
+  val raw_inject_thms = flat (map #inject dtinfos)
+  val raw_distinct_thms = flat (map #distinct dtinfos)
+  val raw_induct_thm = #induct dtinfo
+  val raw_induct_thms = #inducts dtinfo
+  val raw_exhaust_thms = map #exhaust dtinfos
+  val raw_size_trms = map size_const raw_tys
   val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)
     |> `(fn thms => (length thms) div 2)
     |> uncurry drop
@@ -335,7 +334,7 @@
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) =
     if get_STEPS lthy0 > 1 
     then Local_Theory.theory_result 
-      (define_raw_perms all_raw_ty_names all_raw_tys all_raw_constrs raw_induct_thm) lthy0
+      (define_raw_perms raw_full_ty_names raw_tys raw_constrs raw_induct_thm) lthy0
     else raise TEST lthy0
   val lthy2a = Named_Target.reinit lthy2 lthy2
  
@@ -346,12 +345,13 @@
   val _ = warning "Definition of raw fv-functions";
   val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
     if get_STEPS lthy3 > 2 
-    then raw_bn_decls all_raw_ty_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
+    then raw_bn_decls raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs 
+      (raw_inject_thms @ raw_distinct_thms) lthy3
     else raise TEST lthy3
 
   val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = 
     if get_STEPS lthy3a > 3 
-    then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a
+    then define_raw_fvs descr sorts raw_bn_info raw_bclauses (raw_inject_thms @ raw_distinct_thms) lthy3a
     else raise TEST lthy3a
 
   (* definition of raw alphas *)
@@ -365,14 +365,14 @@
   (* definition of alpha-distinct lemmas *)
   val _ = warning "Distinct theorems";
   val alpha_distincts = 
-    mk_alpha_distincts lthy4 alpha_cases distinct_thms alpha_trms all_raw_tys
+    mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys
 
   (* definition of alpha_eq_iff  lemmas *)
   (* they have a funny shape for the simplifier *)
   val _ = warning "Eq-iff theorems";
   val (alpha_eq_iff_simps, alpha_eq_iff) = 
     if get_STEPS lthy > 5
-    then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases
+    then mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases
     else raise TEST lthy4
 
   (* proving equivariance lemmas for bns, fvs, size and alpha *)
@@ -421,7 +421,7 @@
 
   val alpha_trans_thms = 
     if get_STEPS lthy > 12
-    then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) 
+    then raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) 
            alpha_intros alpha_induct alpha_cases lthy6
     else raise TEST lthy6
 
@@ -447,7 +447,7 @@
     (raw_size_thms @ raw_size_eqvt) lthy6
     |> map mk_funs_rsp
 
-  val raw_constrs_rsp = raw_constrs_rsp all_raw_constrs alpha_trms alpha_intros
+  val raw_constrs_rsp = raw_constrs_rsp raw_constrs alpha_trms alpha_intros
     (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 
 
   val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
@@ -462,21 +462,22 @@
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
   val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
-  val qty_binds = map (fn (_, bind, _, _) => bind) dts        
-  val qty_names = map Name.of_binding qty_binds;              
-  
+     
   val (qty_infos, lthy7) = 
     if get_STEPS lthy > 16
-    then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a
+    then define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a
     else raise TEST lthy6a
 
   val qtys = map #qtyp qty_infos
-  
+  val qty_full_names = map (fst o dest_Type) qtys
+  val qty_names = map Long_Name.base_name qty_full_names             
+
+
   (* defining of quotient term-constructors, binding functions, free vars functions *)
   val _ = warning "Defining the quotient constants"
   val qconstrs_descr = 
     flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts)
-    |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs
+    |> map2 (fn t => fn (b, mx) => (b, t, mx)) raw_constrs
 
   val qbns_descr =
     map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns
@@ -493,20 +494,34 @@
   val qperm_descr =
     map2 (fn n => fn t => ("permute_" ^ n, t, NoSyn)) qty_names raw_perm_funs
 
+  val qsize_descr =
+    map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
+
   val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = 
     if get_STEPS lthy > 17
     then 
       lthy7
-      |> qconst_defs qtys qconstrs_descr 
-      ||>> qconst_defs qtys qbns_descr 
-      ||>> qconst_defs qtys qfvs_descr
-      ||>> qconst_defs qtys qfv_bns_descr
-      ||>> qconst_defs qtys qalpha_bns_descr
+      |> define_qconsts qtys qconstrs_descr 
+      ||>> define_qconsts qtys qbns_descr 
+      ||>> define_qconsts qtys qfvs_descr
+      ||>> define_qconsts qtys qfv_bns_descr
+      ||>> define_qconsts qtys qalpha_bns_descr
     else raise TEST lthy7
 
-  (*val _ = Local_Theory.theory_result 
-    (qperm_defs qtys qty_full_names qperm_descr raw_perm_laws) lthy8*) 
+  (* definition of the quotient permfunctions and pt-class *)
+  val lthy9 = 
+    if get_STEPS lthy > 18
+    then Local_Theory.theory 
+      (define_qperms qtys qty_full_names qperm_descr raw_perm_laws) lthy8 
+    else raise TEST lthy8
+  
+  val lthy9' = 
+    if get_STEPS lthy > 19
+    then Local_Theory.theory 
+      (define_qsizes qtys qty_full_names qsize_descr) lthy9
+    else raise TEST lthy9
 
+  val lthy9a = Named_Target.reinit lthy9' lthy9'
 
   val qconstrs = map #qconst qconstrs_info
   val qbns = map #qconst qbns_info
@@ -517,7 +532,7 @@
   
   (* temporary theorem bindings *)
 
-  val (_, lthy8') = lthy8
+  val (_, lthy9') = lthy9a
      |> Local_Theory.note ((@{binding "distinct"}, []), alpha_distincts) 
      ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff)
      ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) 
@@ -527,12 +542,12 @@
      ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
 
   val _ = 
-    if get_STEPS lthy > 18
-    then true else raise TEST lthy8'
+    if get_STEPS lthy > 20
+    then true else raise TEST lthy9'
   
   (* old stuff *)
 
-  val thy = ProofContext.theory_of lthy8'
+  val thy = ProofContext.theory_of lthy9'
   val thy_name = Context.theory_name thy  
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names 
 
@@ -561,28 +576,28 @@
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
     else
-      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
+      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_trms alpha_induct (alpha_eq_iff @ alpha_distincts) alpha_equivp_thms raw_exhaust_thms alpha_bn_trms lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     alpha_bn_rsp_tac) alpha_bn_trms lthy11
   fun const_rsp_tac _ =
     let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a
       in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
-    const_rsp_tac) all_raw_constrs lthy11a
+    const_rsp_tac) raw_constrs lthy11a
   val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns)
-  val (qfv_info, lthy12a) = qconst_defs qtys dd lthy12;
+  val (qfv_info, lthy12a) = define_qconsts qtys dd lthy12;
   val qfv_ts = map #qconst qfv_info
   val qfv_defs = map #def qfv_info
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bns
-  val (qbn_info, lthy12b) = qconst_defs qtys dd lthy12a;
+  val (qbn_info, lthy12b) = define_qconsts qtys dd lthy12a;
   val qbn_ts = map #qconst qbn_info
   val qbn_defs = map #def qbn_info
   val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms
-  val (qalpha_info, lthy12c) = qconst_defs qtys dd lthy12b;
+  val (qalpha_info, lthy12c) = define_qconsts qtys dd lthy12b;
   val qalpha_bn_trms = map #qconst qalpha_info
   val qalphabn_defs = map #def qalpha_info
   
@@ -591,7 +606,7 @@
   val perm_names = map (fn x => "permute_" ^ x) qty_names
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
   (* use Local_Theory.theory_result *)
-  val thy' = qperm_defs qtys qty_full_names dd raw_perm_laws thy;
+  val thy' = define_qperms qtys qty_full_names dd raw_perm_laws thy;
   val lthy13 = Named_Target.init "" thy';
   
   val q_name = space_implode "_" qty_names;




