62 fun get_bn_fun_strs bn_funs = |
62 fun get_bn_fun_strs bn_funs = |
63 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
63 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
64 *} |
64 *} |
65 |
65 |
66 |
66 |
67 text {* Infrastructure for adding "_raw" to types and terms *} |
67 text {* Infrastructure for adding @{text "_raw"} to types and terms *} |
68 |
68 |
69 ML {* |
69 ML {* |
70 fun add_raw s = s ^ "_raw" |
70 fun add_raw s = s ^ "_raw" |
71 fun add_raws ss = map add_raw ss |
71 fun add_raws ss = map add_raw ss |
72 fun raw_bind bn = Binding.suffix_name "_raw" bn |
72 fun raw_bind bn = Binding.suffix_name "_raw" bn |
107 let |
107 let |
108 val bn_funs' = map (fn (bn, ty, _) => |
108 val bn_funs' = map (fn (bn, ty, _) => |
109 (raw_bind bn, SOME (replace_typ dts_env ty), NoSyn)) bn_funs |
109 (raw_bind bn, SOME (replace_typ dts_env ty), NoSyn)) bn_funs |
110 |
110 |
111 val bn_eqs' = map (fn (attr, trm) => |
111 val bn_eqs' = map (fn (attr, trm) => |
112 (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs |
112 ((attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm), [], [])) bn_eqs |
113 in |
113 in |
114 (bn_funs', bn_eqs') |
114 (bn_funs', bn_eqs') |
115 end |
115 end |
116 *} |
116 *} |
117 |
117 |
258 (* noting the raw_bn_eqvt lemmas in a temprorary theory *) |
258 (* noting the raw_bn_eqvt lemmas in a temprorary theory *) |
259 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4) |
259 val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4) |
260 |
260 |
261 val raw_fv_eqvt = |
261 val raw_fv_eqvt = |
262 raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) |
262 raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) |
263 (Local_Theory.restore lthy_tmp) |
263 (Local_Theory.reset lthy_tmp) |
264 |
264 |
265 val raw_size_eqvt = |
265 val raw_size_eqvt = |
266 let |
266 let |
267 val RawDtInfo {raw_size_trms, raw_size_thms, raw_induct_thms, ...} = raw_dt_info |
267 val RawDtInfo {raw_size_trms, raw_size_thms, raw_induct_thms, ...} = raw_dt_info |
268 in |
268 in |
269 raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) |
269 raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) |
270 (Local_Theory.restore lthy_tmp) |
270 (Local_Theory.reset lthy_tmp) |
271 |> map (rewrite_rule (Local_Theory.restore lthy_tmp) |
271 |> map (rewrite_rule (Local_Theory.reset lthy_tmp) |
272 @{thms permute_nat_def[THEN eq_reflection]}) |
272 @{thms permute_nat_def[THEN eq_reflection]}) |
273 |> map (fn thm => thm RS @{thm sym}) |
273 |> map (fn thm => thm RS @{thm sym}) |
274 end |
274 end |
275 |
275 |
276 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) |
276 val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp) |
487 (* noting the theorems *) |
487 (* noting the theorems *) |
488 |
488 |
489 (* generating the prefix for the theorem names *) |
489 (* generating the prefix for the theorem names *) |
490 val thms_name = |
490 val thms_name = |
491 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
491 the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name |
492 fun thms_suffix s = Binding.qualified true s thms_name |
492 fun thms_suffix s = Binding.qualify_name true thms_name s |
493 val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names)) |
493 val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names)) |
494 |
494 |
495 val infos = mk_infos qty_full_names qeq_iffs' qdistincts qstrong_exhaust_thms qstrong_induct_thms |
495 val infos = mk_infos qty_full_names qeq_iffs' qdistincts qstrong_exhaust_thms qstrong_induct_thms |
496 |
496 |
497 val (_, lthy9') = lthyC |
497 val (_, lthy9') = lthyC |
580 fun prepare_bn_funs bn_fun_strs bn_eq_strs thy = |
580 fun prepare_bn_funs bn_fun_strs bn_eq_strs thy = |
581 let |
581 let |
582 val lthy = Named_Target.theory_init thy |
582 val lthy = Named_Target.theory_init thy |
583 |
583 |
584 val ((bn_funs, bn_eqs), lthy') = |
584 val ((bn_funs, bn_eqs), lthy') = |
585 Specification.read_spec bn_fun_strs bn_eq_strs lthy |
585 Specification.read_multi_specs bn_fun_strs bn_eq_strs lthy |
586 |
586 |
587 fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) |
587 fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) |
588 |
588 |
589 val bn_funs' = map prep_bn_fun bn_funs |
589 val bn_funs' = map prep_bn_fun bn_funs |
590 |
590 |
725 (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix >> triple2) -- |
725 (Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix >> triple2) -- |
726 (@{keyword "="} |-- Parse.enum1 "|" cnstr_parser) |
726 (@{keyword "="} |-- Parse.enum1 "|" cnstr_parser) |
727 |
727 |
728 (* binding function parser *) |
728 (* binding function parser *) |
729 val bnfun_parser = |
729 val bnfun_parser = |
730 Scan.optional (@{keyword "binder"} |-- Parse.fixes -- Parse_Spec.where_alt_specs) ([], []) |
730 Scan.optional (@{keyword "binder"} |-- Parse_Spec.specification) ([], []) |
731 |
731 |
732 (* main parser *) |
732 (* main parser *) |
733 val main_parser = |
733 val main_parser = |
734 opt_name -- Parse.and_list1 dt_parser -- bnfun_parser >> tuple3 |
734 opt_name -- Parse.and_list1 dt_parser -- bnfun_parser >> tuple3 |
735 |
735 |