--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Sep 07 13:53:16 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Sep 07 13:53:16 2016 +0200
@@ -594,10 +594,10 @@
b_names Ts thmss)
#> filter_out (null o fst o hd o snd);
-fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs'
- fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps
- live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor
- dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
+fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs fp_nesting_set_maps
+ fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs
+ live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor dtor_ctor pre_map_def
+ pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
({casex, case_thms, discs, selss, sel_defs, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss,
injects, distincts, distinct_discsss, ...} : ctr_sugar)
lthy =
@@ -627,6 +627,8 @@
val ctrAs = map (mk_ctr As) ctrs;
val ctrBs = map (mk_ctr Bs) ctrs;
+ val ctr_defs' = map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs;
+
fun derive_rel_case relAsBs rel_inject_thms rel_distinct_thms =
let
val rel_Rs_a_b = list_comb (relAsBs, Rs) $ ta $ tb;
@@ -1705,8 +1707,8 @@
mk_coinduct_attrs fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss)
end;
-fun derive_set_induct_thms_for_types lthy nn fpTs ctrss setss dtor_set_inducts exhausts
- set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses =
+fun derive_set_induct_thms_for_types lthy nn fpTs ctrss setss dtor_set_inducts exhausts set_pre_defs
+ ctor_defs dtor_ctors Abs_pre_inverses =
let
fun mk_prems A Ps ctr_args t ctxt =
(case fastype_of t of
@@ -2248,7 +2250,8 @@
val fpTs = map (domain_type o fastype_of) dtors;
val fpBTs = map B_ify_T fpTs;
- val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
+ val code_attrs =
+ if plugins code_plugin then [Code.add_default_eqn_attrib Code.Equation] else [];
val ctr_Tsss = map (map (map (Term.typ_subst_atomic (Xs ~~ fpTs)))) ctrXs_Tsss;
val ns = map length ctr_Tsss;
@@ -2259,10 +2262,8 @@
mk_co_recs_prelims lthy fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0;
val lthy' = lthy;
- fun define_ctrs_dtrs_for_type fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor
- ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms
- abs abs_inject type_definition ctr_bindings ctr_mixfixes ctr_Tss disc_bindings sel_bindingss
- raw_sel_default_eqs no_defs_lthy =
+ fun define_ctrs_dtrs_for_type fp_b fpT ctor dtor ctor_dtor dtor_ctor n ks abs ctr_bindings
+ ctr_mixfixes ctr_Tss no_defs_lthy =
let
val fp_b_name = Binding.name_of fp_b;
@@ -2292,21 +2293,33 @@
map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_absumprod ctr_absT abs n k xs))
ks xss;
- val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
+ val ((raw_ctrs, raw_ctr_defs), (lthy, lthy_old)) = no_defs_lthy
|> Local_Theory.open_target |> snd
|> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs =>
- Local_Theory.define
- ((b, mx), ((Thm.make_def_binding (Config.get no_defs_lthy bnf_internals) b, []), rhs))
- #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss
+ Local_Theory.define ((b, mx),
+ ((Thm.make_def_binding (Config.get no_defs_lthy bnf_internals) b, []), rhs))
+ #>> apsnd snd) ctr_bindings ctr_mixfixes ctr_rhss
||> `Local_Theory.close_target;
- val phi = Proof_Context.export_morphism lthy lthy';
+ val phi = Proof_Context.export_morphism lthy_old lthy;
val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
- val ctr_defs' =
- map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs;
-
val ctrs0 = map (Morphism.term phi) raw_ctrs;
+ in
+ ((xss, ctrs0, ctor_iff_dtor_thm, ctr_defs), lthy)
+ end;
+
+ fun define_ctrs_dtrs_for_type_etc fp_bnf fp_b fpT C E ctor dtor xtor_co_rec ctor_dtor dtor_ctor
+ ctor_inject pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm n ks ms
+ abs abs_inject type_definition ctr_bindings ctr_mixfixes ctr_Tss disc_bindings sel_bindingss
+ raw_sel_default_eqs no_defs_lthy =
+ let
+ val ((xss, ctrs0, ctor_iff_dtor_thm, ctr_defs), lthy) =
+ define_ctrs_dtrs_for_type fp_b fpT ctor dtor ctor_dtor dtor_ctor n ks abs ctr_bindings
+ ctr_mixfixes ctr_Tss no_defs_lthy;
+
+ val fp_b_name = Binding.name_of fp_b;
+
val ctrs = map (mk_ctr As) ctrs0;
fun wrap_ctrs lthy =
@@ -2340,7 +2353,7 @@
fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
val ctr_specs = @{map 3} ctr_spec_of disc_bindings ctrs0 sel_bindingss;
- val (ctr_sugar as {case_cong, ...}, lthy') =
+ val (ctr_sugar as {case_cong, ...}, lthy) =
free_constructors (ctr_sugar_kind_of_fp_kind fp) tacss
((((plugins, discs_sels), standard_binding), ctr_specs), sel_default_eqs) lthy
@@ -2349,13 +2362,13 @@
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
val notes =
- if Config.get lthy' bnf_internals then
+ if Config.get lthy bnf_internals then
[(ctor_iff_dtorN, [ctor_iff_dtor_thm], K [])]
|> massage_simple_notes fp_b_name
else
[];
in
- (ctr_sugar, lthy' |> Local_Theory.notes (anonymous_notes @ notes) |> snd)
+ (ctr_sugar, lthy |> Local_Theory.notes (anonymous_notes @ notes) |> snd)
end;
fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
@@ -2366,7 +2379,7 @@
in
(wrap_ctrs
#> (fn (ctr_sugar, lthy) =>
- derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs'
+ derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs
fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps
live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor
ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms
@@ -2375,7 +2388,7 @@
##>>
(if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps
else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec
- #> massage_res, lthy')
+ #> massage_res, lthy)
end;
fun wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
@@ -2738,7 +2751,7 @@
val lthy'' = lthy'
|> live > 0 ? fold2 (fn Type (s, _) => fn bnf => register_bnf_raw s bnf) fpTs fp_bnfs
- |> @{fold_map 29} define_ctrs_dtrs_for_type fp_bnfs fp_bs fpTs Cs Es ctors dtors
+ |> @{fold_map 29} define_ctrs_dtrs_for_type_etc fp_bnfs fp_bs fpTs Cs Es ctors dtors
xtor_co_recs ctor_dtors dtor_ctors ctor_injects pre_map_defs pre_set_defss pre_rel_defs
xtor_maps xtor_setss xtor_rels ns kss mss abss abs_injects type_definitions ctr_bindingss
ctr_mixfixess ctr_Tsss disc_bindingss sel_bindingsss raw_sel_default_eqss