
diff -r c670a849af65 -r 1e6160690546 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sat Aug 14 16:54:41 2010 +0800
+++ b/Nominal/NewParser.thy	Sat Aug 14 23:33:23 2010 +0800
@@ -13,6 +13,13 @@
 
 section{* Interface for nominal_datatype *}
 
+ML {*
+(* attributes *)
+val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+val rsp_attrib = Attrib.internal (K Quotient_Info.rsp_rules_add)
+
+*}
+
 
 ML {* 
 (* nominal datatype parser *)
@@ -305,11 +312,11 @@
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
-  val all_raw_tys = all_dtyps descr sorts
-  val all_raw_ty_names = map (fn (_, (n, _, _)) => n) descr
   val all_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 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);
@@ -329,20 +336,16 @@
   val _ = warning "Definition of raw permutations";
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2) =
     if get_STEPS lthy0 > 1 
-    then Local_Theory.theory_result (define_raw_perms descr sorts raw_induct_thm (length dts)) lthy0
+    then Local_Theory.theory_result 
+      (define_raw_perms all_raw_ty_names all_raw_tys all_raw_constrs raw_induct_thm) lthy0
     else raise TEST lthy0
+  val lthy2a = Named_Target.reinit lthy2 lthy2
  
   (* noting the raw permutations as eqvt theorems *)
-  val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
-  val (_, lthy2a) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2
-
-  val thy = Local_Theory.exit_global lthy2a;
-  val thy_name = Context.theory_name thy
+  val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_perm_simps) lthy2a
 
   (* definition of raw fv_functions *)
   val _ = warning "Definition of raw fv-functions";
-  val lthy3 = Named_Target.init NONE thy;
-
   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
@@ -382,8 +385,7 @@
     else raise TEST lthy4
 
   (* noting the bn_eqvt lemmas in a temprorary theory *)
-  val add_eqvt = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
-  val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), bn_eqvt) lthy4)
+  val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), bn_eqvt) lthy4)
 
   val fv_eqvt = 
     if get_STEPS lthy > 7
@@ -399,7 +401,7 @@
       |> map (fn thm => thm RS @{thm sym})
     else raise TEST lthy4
  
-  val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
+  val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), fv_eqvt) lthy_tmp)
 
   val (alpha_eqvt, lthy6) =
     if get_STEPS lthy > 9
@@ -452,17 +454,23 @@
 
   val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
 
+  (* noting the quot_respects lemmas *)
+  val (_, lthy6a) = 
+    if get_STEPS lthy > 15
+    then Local_Theory.note ((Binding.empty, [rsp_attrib]),
+      raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp) lthy6
+    else raise TEST lthy6
+
   (* 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_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *)
   
   val (qty_infos, lthy7) = 
-    if get_STEPS lthy > 15
-    then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
-    else raise TEST lthy6
+    if get_STEPS lthy > 16
+    then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a
+    else raise TEST lthy6a
 
   val qtys = map #qtyp qty_infos
   
@@ -479,13 +487,16 @@
     map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs
 
   val qfv_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs  raw_fv_bns
+    map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_fv_bns
 
   val qalpha_bns_descr = 
     map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
 
+  val qperm_descr =
+    map2 (fn n => fn t => ("permute_" ^ n, t, NoSyn)) qty_names raw_perm_funs
+
   val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = 
-    if get_STEPS lthy > 16
+    if get_STEPS lthy > 17
     then 
       lthy7
       |> qconst_defs qtys qconstrs_descr 
@@ -495,12 +506,17 @@
       ||>> qconst_defs 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*) 
+
+
   val qconstrs = map #qconst qconstrs_info
   val qbns = map #qconst qbns_info
   val qfvs = map #qconst qfvs_info
   val qfv_bns = map #qconst qfv_bns_info
   val qalpha_bns = map #qconst qalpha_bns_info
 
+  
   (* temporary theorem bindings *)
 
   val (_, lthy8') = lthy8
@@ -511,17 +527,17 @@
      ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) 
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
      ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
-     ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp)
-     ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp)
-     ||>> Local_Theory.note ((@{binding "constrs_rsp"}, []), raw_constrs_rsp)
-     ||>> Local_Theory.note ((@{binding "permute_rsp"}, []), alpha_permute_rsp)
 
   val _ = 
-    if get_STEPS lthy > 17
+    if get_STEPS lthy > 18
     then true else raise TEST lthy8'
   
   (* old stuff *)
 
+  val thy = ProofContext.theory_of lthy8'
+  val thy_name = Context.theory_name thy  
+  val qty_full_names = map (Long_Name.qualify thy_name) qty_names 
+
   val _ = warning "Proving respects";
 
   val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
@@ -578,7 +594,7 @@
   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 lthy13 = Named_Target.init NONE thy';
+  val lthy13 = Named_Target.init "" thy';
   
   val q_name = space_implode "_" qty_names;
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);




