author | traytel |
Tue, 05 Apr 2016 09:54:17 +0200 | |
changeset 62863 | e0b894bba6ff |
parent 62721 | f3248e77c960 |
child 62907 | 9ad0bac25a84 |
permissions | -rw-r--r-- |
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/BNF/bnf_lfp_basic_sugar.ML |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
3 |
Copyright 2014 |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
4 |
|
58353 | 5 |
Registration of basic types as BNF least fixpoints (datatypes). |
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
6 |
*) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
7 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
8 |
structure BNF_LFP_Basic_Sugar : sig end = |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
9 |
struct |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
10 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
11 |
open Ctr_Sugar |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
12 |
open BNF_Util |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
13 |
open BNF_Def |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
14 |
open BNF_Comp |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
15 |
open BNF_FP_Rec_Sugar_Util |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
16 |
open BNF_FP_Util |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
17 |
open BNF_FP_Def_Sugar |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
18 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
19 |
fun trivial_absT_info_of fpT = |
59819 | 20 |
{absT = fpT, repT = fpT, abs = Const (@{const_name id_bnf}, fpT --> fpT), |
58353 | 21 |
rep = Const (@{const_name id_bnf}, fpT --> fpT), |
22 |
abs_inject = @{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV UNIV_I UNIV_I]}, |
|
23 |
abs_inverse = @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV UNIV_I]}, |
|
24 |
type_definition = @{thm type_definition_id_bnf_UNIV}}; |
|
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
25 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
26 |
fun the_frozen_ctr_sugar_of ctxt fpT_name = |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
27 |
the (ctr_sugar_of ctxt fpT_name) |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
28 |
|> morph_ctr_sugar (Morphism.typ_morphism "BNF" Logic.unvarifyT_global |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
29 |
$> Morphism.term_morphism "BNF" (Term.map_types Logic.unvarifyT_global)); |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
30 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
31 |
fun trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct = |
59819 | 32 |
let |
33 |
val xtors = [Const (@{const_name xtor}, fpT --> fpT)]; |
|
34 |
val co_recs = [Const (@{const_name ctor_rec}, (fpT --> C) --> (fpT --> C))]; |
|
35 |
val co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}]; |
|
62863
e0b894bba6ff
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
traytel
parents:
62721
diff
changeset
|
36 |
val co_rec_unique_thm = map_id0_of_bnf fp_bnf RS @{thm ctor_rec_unique}; |
59819 | 37 |
in |
62684
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62335
diff
changeset
|
38 |
{Ts = [fpT], bnfs = [fp_bnf], pre_bnfs = [ID_bnf], absT_infos = [trivial_absT_info_of fpT], |
62721 | 39 |
ctors = xtors, dtors = xtors, xtor_un_folds_legacy = co_recs, |
59819 | 40 |
xtor_co_recs = co_recs, xtor_co_induct = @{thm xtor_induct}, dtor_ctors = @{thms xtor_xtor}, |
41 |
ctor_dtors = @{thms xtor_xtor}, ctor_injects = @{thms xtor_inject}, |
|
62863
e0b894bba6ff
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
traytel
parents:
62721
diff
changeset
|
42 |
dtor_injects = @{thms xtor_inject}, xtor_maps = [xtor_map], |
e0b894bba6ff
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
traytel
parents:
62721
diff
changeset
|
43 |
xtor_map_unique = @{thm xtor_map_unique}, xtor_setss = [xtor_sets], xtor_rels = [xtor_rel], |
e0b894bba6ff
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
traytel
parents:
62721
diff
changeset
|
44 |
xtor_un_fold_thms_legacy = co_rec_thms, xtor_co_rec_thms = co_rec_thms, |
e0b894bba6ff
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
traytel
parents:
62721
diff
changeset
|
45 |
xtor_un_fold_unique_legacy = co_rec_unique_thm, xtor_co_rec_unique = co_rec_unique_thm, |
62721 | 46 |
xtor_un_fold_o_maps_legacy = [ctor_rec_o_map], xtor_co_rec_o_maps = [ctor_rec_o_map], |
47 |
xtor_un_fold_transfers_legacy = [], xtor_co_rec_transfers = [], |
|
48 |
xtor_rel_co_induct = xtor_rel_induct, dtor_set_inducts = []} |
|
59819 | 49 |
end; |
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
50 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
51 |
fun fp_sugar_of_sum ctxt = |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
52 |
let |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
53 |
val fpT as Type (fpT_name, As) = @{typ "'a + 'b"}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
54 |
val fpBT = @{typ "'c + 'd"}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
55 |
val C = @{typ 'e}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
56 |
val X = @{typ 'sum}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
57 |
val ctr_Tss = map single As; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
58 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
59 |
val fp_bnf = the (bnf_of ctxt fpT_name); |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
60 |
val xtor_map = @{thm xtor_map[of "map_sum f1 f2" for f1 f2]}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
61 |
val xtor_sets = @{thms xtor_set[of setl] xtor_set[of setr]}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
62 |
val xtor_rel = @{thm xtor_rel[of "rel_sum R1 R2" for R1 R2]}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
63 |
val ctor_rec_o_map = @{thm ctor_rec_o_map[of _ "map_sum g1 g2" for g1 g2]}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
64 |
val xtor_rel_induct = @{thm xtor_rel_induct[of "rel_sum R1 R2" for R1 R2]}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
65 |
in |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
66 |
{T = fpT, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
67 |
BT = fpBT, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
68 |
X = X, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
69 |
fp = Least_FP, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
70 |
fp_res_index = 0, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
71 |
fp_res = |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
72 |
trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
73 |
pre_bnf = ID_bnf (*wrong*), |
58674 | 74 |
fp_bnf = fp_bnf, |
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
75 |
absT_info = trivial_absT_info_of fpT, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
76 |
fp_nesting_bnfs = [], |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
77 |
live_nesting_bnfs = [], |
58460 | 78 |
fp_ctr_sugar = |
79 |
{ctrXs_Tss = ctr_Tss, |
|
62321
1abe81758619
keep 'ctor_iff_dtor' theorem around in BNF FP database
blanchet
parents:
61424
diff
changeset
|
80 |
ctor_iff_dtor = @{thm xtor_iff_xtor}, |
58460 | 81 |
ctr_defs = @{thms Inl_def_alt Inr_def_alt}, |
58569 | 82 |
ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name, |
58916 | 83 |
ctr_transfers = @{thms Inl_transfer Inr_transfer}, |
84 |
case_transfers = @{thms case_sum_transfer}, |
|
85 |
disc_transfers = @{thms isl_transfer}, |
|
58676 | 86 |
sel_transfers = []}, |
58459 | 87 |
fp_bnf_sugar = |
58462 | 88 |
{map_thms = @{thms map_sum.simps}, |
58916 | 89 |
map_disc_iffs = @{thms isl_map_sum}, |
90 |
map_selss = map single @{thms map_sum_sel}, |
|
58462 | 91 |
rel_injects = @{thms rel_sum_simps(1,4)}, |
58562 | 92 |
rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}, |
58916 | 93 |
rel_sels = @{thms rel_sum_sel}, |
94 |
rel_intros = @{thms rel_sum.intros}, |
|
95 |
rel_cases = @{thms rel_sum.cases}, |
|
62335 | 96 |
pred_injects = @{thms pred_sum_inject}, |
58916 | 97 |
set_thms = @{thms sum_set_simps}, |
98 |
set_selssss = [[[@{thms set_sum_sel(1)}], [[]]], [[[]], [@{thms set_sum_sel(2)}]]], |
|
99 |
set_introssss = [[[@{thms setl.intros[OF refl]}], [[]]], |
|
100 |
[[[]], [@{thms setr.intros[OF refl]}]]], |
|
101 |
set_cases = @{thms setl.cases[unfolded hypsubst_in_prems] |
|
102 |
setr.cases[unfolded hypsubst_in_prems]}}, |
|
58459 | 103 |
fp_co_induct_sugar = |
58461 | 104 |
{co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), |
105 |
common_co_inducts = @{thms sum.induct}, |
|
106 |
co_inducts = @{thms sum.induct}, |
|
107 |
co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]}, |
|
58459 | 108 |
co_rec_thms = @{thms sum.case}, |
109 |
co_rec_discs = [], |
|
58572 | 110 |
co_rec_disc_iffs = [], |
58573 | 111 |
co_rec_selss = [], |
112 |
co_rec_codes = [], |
|
58916 | 113 |
co_rec_transfers = @{thms case_sum_transfer}, |
58734 | 114 |
co_rec_o_maps = @{thms case_sum_o_map_sum}, |
58916 | 115 |
common_rel_co_inducts = @{thms rel_sum.inducts}, |
116 |
rel_co_inducts = @{thms rel_sum.induct}, |
|
58577 | 117 |
common_set_inducts = [], |
118 |
set_inducts = []}} |
|
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
119 |
end; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
120 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
121 |
fun fp_sugar_of_prod ctxt = |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
122 |
let |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
123 |
val fpT as Type (fpT_name, As) = @{typ "'a * 'b"}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
124 |
val fpBT = @{typ "'c * 'd"}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
125 |
val C = @{typ 'e}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
126 |
val X = @{typ 'prod}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
127 |
val ctr_Ts = As; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
128 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
129 |
val fp_bnf = the (bnf_of ctxt fpT_name); |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
130 |
val xtor_map = @{thm xtor_map[of "map_prod f1 f2" for f1 f2]}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
131 |
val xtor_sets = @{thms xtor_set[of fsts] xtor_set[of snds]}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
132 |
val xtor_rel = @{thm xtor_rel[of "rel_prod R1 R2" for R1 R2]}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
133 |
val ctor_rec_o_map = @{thm ctor_rec_o_map[of _ "map_prod g1 g2" for g1 g2]}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
134 |
val xtor_rel_induct = @{thm xtor_rel_induct[of "rel_prod R1 R2" for R1 R2]}; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
135 |
in |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
136 |
{T = fpT, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
137 |
BT = fpBT, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
138 |
X = X, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
139 |
fp = Least_FP, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
140 |
fp_res_index = 0, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
141 |
fp_res = |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
142 |
trivial_fp_result_of fp_bnf fpT C xtor_map xtor_sets xtor_rel ctor_rec_o_map xtor_rel_induct, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
143 |
pre_bnf = ID_bnf (*wrong*), |
58674 | 144 |
fp_bnf = fp_bnf, |
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
145 |
absT_info = trivial_absT_info_of fpT, |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
146 |
fp_nesting_bnfs = [], |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
147 |
live_nesting_bnfs = [], |
58460 | 148 |
fp_ctr_sugar = |
149 |
{ctrXs_Tss = [ctr_Ts], |
|
62321
1abe81758619
keep 'ctor_iff_dtor' theorem around in BNF FP database
blanchet
parents:
61424
diff
changeset
|
150 |
ctor_iff_dtor = @{thm xtor_iff_xtor}, |
58460 | 151 |
ctr_defs = @{thms Pair_def_alt}, |
58569 | 152 |
ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name, |
58916 | 153 |
ctr_transfers = @{thms Pair_transfer}, |
154 |
case_transfers = @{thms case_prod_transfer}, |
|
58676 | 155 |
disc_transfers = [], |
58916 | 156 |
sel_transfers = @{thms fst_transfer snd_transfer}}, |
58459 | 157 |
fp_bnf_sugar = |
58462 | 158 |
{map_thms = @{thms map_prod_simp}, |
58560 | 159 |
map_disc_iffs = [], |
58916 | 160 |
map_selss = [@{thms fst_map_prod snd_map_prod}], |
62335 | 161 |
rel_injects = @{thms rel_prod_inject}, |
58562 | 162 |
rel_distincts = [], |
58916 | 163 |
rel_sels = @{thms rel_prod_sel}, |
164 |
rel_intros = @{thms rel_prod.intros}, |
|
165 |
rel_cases = @{thms rel_prod.cases}, |
|
62335 | 166 |
pred_injects = @{thms pred_prod_inject}, |
58916 | 167 |
set_thms = @{thms prod_set_simps}, |
168 |
set_selssss = [[[@{thms fsts.intros}, []]], [[[], @{thms snds.intros}]]], |
|
169 |
set_introssss = [[[@{thms fsts.intros[of "(a, b)" for a b, unfolded fst_conv]}, []]], |
|
170 |
[[[], @{thms snds.intros[of "(a, b)" for a b, unfolded snd_conv]}]]], |
|
171 |
set_cases = @{thms fsts.cases[unfolded eq_fst_iff ex_neg_all_pos] |
|
172 |
snds.cases[unfolded eq_snd_iff ex_neg_all_pos]}}, |
|
58459 | 173 |
fp_co_induct_sugar = |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61125
diff
changeset
|
174 |
{co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), |
58461 | 175 |
common_co_inducts = @{thms prod.induct}, |
176 |
co_inducts = @{thms prod.induct}, |
|
177 |
co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]}, |
|
58459 | 178 |
co_rec_thms = @{thms prod.case}, |
179 |
co_rec_discs = [], |
|
58572 | 180 |
co_rec_disc_iffs = [], |
58573 | 181 |
co_rec_selss = [], |
182 |
co_rec_codes = [], |
|
58916 | 183 |
co_rec_transfers = @{thms case_prod_transfer}, |
58734 | 184 |
co_rec_o_maps = @{thms case_prod_o_map_prod}, |
58916 | 185 |
common_rel_co_inducts = @{thms rel_prod.inducts}, |
186 |
rel_co_inducts = @{thms rel_prod.induct}, |
|
58577 | 187 |
common_set_inducts = [], |
188 |
set_inducts = []}} |
|
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
189 |
end; |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
190 |
|
58665 | 191 |
val _ = Theory.setup (Named_Target.theory_map (fn lthy => |
58377
c6f93b8d2d8e
moved old 'size' generator together with 'old_datatype'
blanchet
parents:
58353
diff
changeset
|
192 |
fold (BNF_FP_Def_Sugar.register_fp_sugars (K true) o single o (fn f => f lthy)) |
58352
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
193 |
[fp_sugar_of_sum, fp_sugar_of_prod] lthy)); |
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
194 |
|
37745650a3f4
register 'prod' and 'sum' as datatypes, to allow N2M through them
blanchet
parents:
diff
changeset
|
195 |
end; |