--- 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);