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