author | traytel |
Sun, 03 Apr 2016 10:25:17 +0200 | |
changeset 62827 | 609f97d79bc2 |
parent 62722 | f5ee068b96a6 |
child 62863 | e0b894bba6ff |
permissions | -rw-r--r-- |
55061 | 1 |
(* Title: HOL/Tools/BNF/bnf_fp_util.ML |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
57668 | 4 |
Author: Martin Desharnais, TU Muenchen |
58256
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
5 |
Author: Stefan Berghofer, TU Muenchen |
57668 | 6 |
Copyright 2012, 2013, 2014 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
|
49389 | 8 |
Shared library for the datatype and codatatype constructions. |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
|
51850
106afdf5806c
renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
blanchet
parents:
51839
diff
changeset
|
11 |
signature BNF_FP_UTIL = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
sig |
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
13 |
type fp_result = |
51859 | 14 |
{Ts: typ list, |
15 |
bnfs: BNF_Def.bnf list, |
|
62684
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62621
diff
changeset
|
16 |
pre_bnfs: BNF_Def.bnf list, |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62621
diff
changeset
|
17 |
absT_infos: BNF_Comp.absT_info list, |
51839 | 18 |
ctors: term list, |
51819 | 19 |
dtors: term list, |
62721 | 20 |
xtor_un_folds_legacy: term list, |
55868 | 21 |
xtor_co_recs: term list, |
53106 | 22 |
xtor_co_induct: thm, |
51819 | 23 |
dtor_ctors: thm list, |
24 |
ctor_dtors: thm list, |
|
25 |
ctor_injects: thm list, |
|
53203
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53202
diff
changeset
|
26 |
dtor_injects: thm list, |
58583 | 27 |
xtor_maps: thm list, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
28 |
xtor_map_uniques: thm list, |
58584 | 29 |
xtor_setss: thm list list, |
58585 | 30 |
xtor_rels: thm list, |
62721 | 31 |
xtor_un_fold_thms_legacy: thm list, |
55868 | 32 |
xtor_co_rec_thms: thm list, |
62721 | 33 |
xtor_un_fold_uniques_legacy: thm list, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
34 |
xtor_co_rec_uniques: thm list, |
62721 | 35 |
xtor_un_fold_o_maps_legacy: thm list, |
58578
9ff8ca957c02
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
desharna
parents:
58448
diff
changeset
|
36 |
xtor_co_rec_o_maps: thm list, |
62721 | 37 |
xtor_un_fold_transfers_legacy: thm list, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
38 |
xtor_co_rec_transfers: thm list, |
58579
b7bc5ba2f3fb
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
desharna
parents:
58578
diff
changeset
|
39 |
xtor_rel_co_induct: thm, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
40 |
dtor_set_inducts: thm list} |
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
41 |
|
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
42 |
val morph_fp_result: morphism -> fp_result -> fp_result |
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
43 |
|
53143
ba80154a1118
configuration option to control timing output for (co)datatypes
traytel
parents:
53138
diff
changeset
|
44 |
val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
45 |
|
55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
46 |
val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list |
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
47 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
val IITN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
49 |
val LevN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
50 |
val algN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
51 |
val behN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
val bisN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
53 |
val carTN: string |
49338 | 54 |
val caseN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
val coN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
val coinductN: string |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57700
diff
changeset
|
57 |
val coinduct_strongN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
58 |
val corecN: string |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57700
diff
changeset
|
59 |
val corec_discN: string |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57700
diff
changeset
|
60 |
val corec_disc_iffN: string |
49501 | 61 |
val ctorN: string |
62 |
val ctor_dtorN: string |
|
63 |
val ctor_exhaustN: string |
|
64 |
val ctor_induct2N: string |
|
65 |
val ctor_inductN: string |
|
66 |
val ctor_injectN: string |
|
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
67 |
val ctor_foldN: string |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
68 |
val ctor_fold_o_mapN: string |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
69 |
val ctor_fold_transferN: string |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
70 |
val ctor_fold_uniqueN: string |
49541 | 71 |
val ctor_mapN: string |
49543
53b3c532a082
renamed low-level "map_unique" to have "ctor" or "dtor" in the name
blanchet
parents:
49542
diff
changeset
|
72 |
val ctor_map_uniqueN: string |
49501 | 73 |
val ctor_recN: string |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
74 |
val ctor_rec_o_mapN: string |
58444 | 75 |
val ctor_rec_transferN: string |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
76 |
val ctor_rec_uniqueN: string |
49518
b377da40244b
renamed LFP low-level rel property to have ctor not dtor in its name
blanchet
parents:
49516
diff
changeset
|
77 |
val ctor_relN: string |
55901
8c6d49dd8ae1
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
blanchet
parents:
55899
diff
changeset
|
78 |
val ctor_rel_inductN: string |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
79 |
val ctor_set_inclN: string |
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
80 |
val ctor_set_set_inclN: string |
49501 | 81 |
val dtorN: string |
49582
557302525778
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
blanchet
parents:
49581
diff
changeset
|
82 |
val dtor_coinductN: string |
49501 | 83 |
val dtor_corecN: string |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
84 |
val dtor_corec_o_mapN: string |
58445 | 85 |
val dtor_corec_transferN: string |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
86 |
val dtor_corec_uniqueN: string |
49518
b377da40244b
renamed LFP low-level rel property to have ctor not dtor in its name
blanchet
parents:
49516
diff
changeset
|
87 |
val dtor_ctorN: string |
49501 | 88 |
val dtor_exhaustN: string |
89 |
val dtor_injectN: string |
|
49545
8bb6e2d7346b
renamed coinduction principles to have "dtor" in the name
blanchet
parents:
49544
diff
changeset
|
90 |
val dtor_mapN: string |
49581
4e5bd3883429
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
blanchet
parents:
49545
diff
changeset
|
91 |
val dtor_map_coinductN: string |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57700
diff
changeset
|
92 |
val dtor_map_coinduct_strongN: string |
49543
53b3c532a082
renamed low-level "map_unique" to have "ctor" or "dtor" in the name
blanchet
parents:
49542
diff
changeset
|
93 |
val dtor_map_uniqueN: string |
49545
8bb6e2d7346b
renamed coinduction principles to have "dtor" in the name
blanchet
parents:
49544
diff
changeset
|
94 |
val dtor_relN: string |
55901
8c6d49dd8ae1
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
blanchet
parents:
55899
diff
changeset
|
95 |
val dtor_rel_coinductN: string |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
96 |
val dtor_set_inclN: string |
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
97 |
val dtor_set_set_inclN: string |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57700
diff
changeset
|
98 |
val dtor_coinduct_strongN: string |
49516
d4859efc1096
renamed "rel_simp" to "dtor_rel" and similarly for "srel"
blanchet
parents:
49510
diff
changeset
|
99 |
val dtor_unfoldN: string |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
100 |
val dtor_unfold_o_mapN: string |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
101 |
val dtor_unfold_transferN: string |
49516
d4859efc1096
renamed "rel_simp" to "dtor_rel" and similarly for "srel"
blanchet
parents:
49510
diff
changeset
|
102 |
val dtor_unfold_uniqueN: string |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
103 |
val exhaustN: string |
56113 | 104 |
val colN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
105 |
val inductN: string |
49019 | 106 |
val injectN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
107 |
val isNodeN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
108 |
val lsbisN: string |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
109 |
val mapN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
110 |
val map_uniqueN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
111 |
val min_algN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
112 |
val morN: string |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
113 |
val nchotomyN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
114 |
val recN: string |
57525 | 115 |
val rel_casesN: string |
51918 | 116 |
val rel_coinductN: string |
117 |
val rel_inductN: string |
|
49592
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
118 |
val rel_injectN: string |
57493 | 119 |
val rel_introsN: string |
49592
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
120 |
val rel_distinctN: string |
57563 | 121 |
val rel_selN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
122 |
val rvN: string |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57700
diff
changeset
|
123 |
val corec_selN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
124 |
val set_inclN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
125 |
val set_set_inclN: string |
53694 | 126 |
val setN: string |
49438 | 127 |
val simpsN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
128 |
val strTN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
129 |
val str_initN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
130 |
val sum_bdN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
131 |
val sum_bdTN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
132 |
val uniqueN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
133 |
|
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
134 |
(* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *) |
49584
4339aa335355
use singular since there is always only one theorem
blanchet
parents:
49582
diff
changeset
|
135 |
val mk_ctor_setN: int -> string |
4339aa335355
use singular since there is always only one theorem
blanchet
parents:
49582
diff
changeset
|
136 |
val mk_dtor_setN: int -> string |
49542
b39354db8629
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset
|
137 |
val mk_dtor_set_inductN: int -> string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
138 |
val mk_set_inductN: int -> string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
139 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55570
diff
changeset
|
140 |
val co_prefix: BNF_Util.fp_kind -> string |
51863 | 141 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
142 |
val split_conj_thm: thm -> thm list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
143 |
val split_conj_prems: int -> thm -> thm |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
144 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
145 |
val mk_sumTN: typ list -> typ |
58159 | 146 |
val mk_sumTN_balanced: typ list -> typ |
55969 | 147 |
val mk_tupleT_balanced: typ list -> typ |
55966 | 148 |
val mk_sumprodT_balanced: typ list list -> typ |
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
149 |
|
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
150 |
val mk_proj: typ -> int -> int -> term |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
151 |
|
53032 | 152 |
val mk_convol: term * term -> term |
58443 | 153 |
val mk_rel_prod: term -> term -> term |
154 |
val mk_rel_sum: term -> term -> term |
|
49368 | 155 |
|
49121 | 156 |
val Inl_const: typ -> typ -> term |
157 |
val Inr_const: typ -> typ -> term |
|
55969 | 158 |
val mk_tuple_balanced: term list -> term |
159 |
val mk_tuple1_balanced: typ list -> term list -> term |
|
59873 | 160 |
val abs_curried_balanced: typ list -> term -> term |
62124 | 161 |
val mk_tupled_fun: term -> term -> term list -> term |
49121 | 162 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
163 |
val mk_case_sum: term * term -> term |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
164 |
val mk_case_sumN: term list -> term |
55968 | 165 |
val mk_case_absumprod: typ -> term -> term list -> term list list -> term list list -> term |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
166 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
167 |
val mk_Inl: typ -> term -> term |
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
168 |
val mk_Inr: typ -> term -> term |
59673 | 169 |
val mk_sumprod_balanced: typ -> int -> int -> term list -> term |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
170 |
val mk_absumprod: typ -> term -> int -> int -> term list -> term |
49121 | 171 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
172 |
val dest_sumT: typ -> typ * typ |
58159 | 173 |
val dest_sumTN_balanced: int -> typ -> typ list |
174 |
val dest_tupleT_balanced: int -> typ -> typ list |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
175 |
val dest_absumprodT: typ -> typ -> int -> int list -> typ -> typ list list |
49176 | 176 |
|
53202
2333fae25719
export one more ML function, needed for primcorec
blanchet
parents:
53143
diff
changeset
|
177 |
val If_const: typ -> term |
2333fae25719
export one more ML function, needed for primcorec
blanchet
parents:
53143
diff
changeset
|
178 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
179 |
val mk_Field: term -> term |
49275 | 180 |
val mk_If: term -> term -> term -> term |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
181 |
val mk_union: term * term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
182 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
183 |
val mk_absumprodE: thm -> int list -> thm |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
184 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
185 |
val mk_sum_caseN: int -> int -> thm |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
186 |
val mk_sum_caseN_balanced: int -> int -> thm |
49125 | 187 |
|
55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
188 |
val mk_sum_Cinfinite: thm list -> thm |
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
189 |
val mk_sum_card_order: thm list -> thm |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
190 |
|
58579
b7bc5ba2f3fb
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
desharna
parents:
58578
diff
changeset
|
191 |
val mk_xtor_rel_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list -> |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55570
diff
changeset
|
192 |
term list -> term list -> term list -> term list -> term list -> |
52505
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
193 |
({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm |
62827 | 194 |
val mk_xtor_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list -> |
58443 | 195 |
term list -> term list -> term list -> term list -> |
196 |
({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list |
|
62827 | 197 |
val mk_xtor_co_iter_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list -> |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
198 |
thm list -> thm list -> thm list |
52505
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
199 |
|
62722 | 200 |
val fixpoint_bnf: (binding -> binding) -> |
201 |
(binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> |
|
202 |
BNF_Comp.absT_info list -> local_theory -> 'a) -> |
|
55701 | 203 |
binding list -> (string * sort) list -> (string * sort) list -> ((string * sort) * typ) list -> |
62720 | 204 |
BNF_Comp.comp_cache -> local_theory -> |
205 |
((BNF_Def.bnf list * BNF_Comp.absT_info list) * BNF_Comp.comp_cache) * 'a |
|
58256
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
206 |
val fp_antiquote_setup: binding -> theory -> theory |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
207 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
208 |
|
51850
106afdf5806c
renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries
blanchet
parents:
51839
diff
changeset
|
209 |
structure BNF_FP_Util : BNF_FP_UTIL = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
210 |
struct |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
211 |
|
56650
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
212 |
open Ctr_Sugar |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
213 |
open BNF_Comp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
214 |
open BNF_Def |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
215 |
open BNF_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
216 |
|
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
217 |
type fp_result = |
51859 | 218 |
{Ts: typ list, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
219 |
bnfs: bnf list, |
62684
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62621
diff
changeset
|
220 |
pre_bnfs: BNF_Def.bnf list, |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62621
diff
changeset
|
221 |
absT_infos: BNF_Comp.absT_info list, |
51839 | 222 |
ctors: term list, |
51819 | 223 |
dtors: term list, |
62721 | 224 |
xtor_un_folds_legacy: term list, |
55868 | 225 |
xtor_co_recs: term list, |
53106 | 226 |
xtor_co_induct: thm, |
51819 | 227 |
dtor_ctors: thm list, |
228 |
ctor_dtors: thm list, |
|
229 |
ctor_injects: thm list, |
|
53203
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53202
diff
changeset
|
230 |
dtor_injects: thm list, |
58583 | 231 |
xtor_maps: thm list, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
232 |
xtor_map_uniques: thm list, |
58584 | 233 |
xtor_setss: thm list list, |
58585 | 234 |
xtor_rels: thm list, |
62721 | 235 |
xtor_un_fold_thms_legacy: thm list, |
55868 | 236 |
xtor_co_rec_thms: thm list, |
62721 | 237 |
xtor_un_fold_uniques_legacy: thm list, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
238 |
xtor_co_rec_uniques: thm list, |
62721 | 239 |
xtor_un_fold_o_maps_legacy: thm list, |
58578
9ff8ca957c02
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
desharna
parents:
58448
diff
changeset
|
240 |
xtor_co_rec_o_maps: thm list, |
62721 | 241 |
xtor_un_fold_transfers_legacy: thm list, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
242 |
xtor_co_rec_transfers: thm list, |
58579
b7bc5ba2f3fb
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
desharna
parents:
58578
diff
changeset
|
243 |
xtor_rel_co_induct: thm, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
244 |
dtor_set_inducts: thm list}; |
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
245 |
|
62721 | 246 |
fun morph_fp_result phi {Ts, bnfs, pre_bnfs, absT_infos, ctors, dtors, xtor_un_folds_legacy, |
247 |
xtor_co_recs, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, |
|
248 |
xtor_map_uniques, xtor_setss, xtor_rels, xtor_un_fold_thms_legacy, xtor_co_rec_thms, |
|
249 |
xtor_un_fold_uniques_legacy, xtor_co_rec_uniques, xtor_un_fold_o_maps_legacy, |
|
250 |
xtor_co_rec_o_maps, xtor_un_fold_transfers_legacy, xtor_co_rec_transfers, xtor_rel_co_induct, |
|
251 |
dtor_set_inducts} = |
|
51859 | 252 |
{Ts = map (Morphism.typ phi) Ts, |
253 |
bnfs = map (morph_bnf phi) bnfs, |
|
62684
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62621
diff
changeset
|
254 |
pre_bnfs = map (morph_bnf phi) pre_bnfs, |
cb20e8828196
document that n2m does not depend on most things in fp_sugar in its type
traytel
parents:
62621
diff
changeset
|
255 |
absT_infos = map (morph_absT_info phi) absT_infos, |
51839 | 256 |
ctors = map (Morphism.term phi) ctors, |
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
257 |
dtors = map (Morphism.term phi) dtors, |
62721 | 258 |
xtor_un_folds_legacy = map (Morphism.term phi) xtor_un_folds_legacy, |
55868 | 259 |
xtor_co_recs = map (Morphism.term phi) xtor_co_recs, |
53106 | 260 |
xtor_co_induct = Morphism.thm phi xtor_co_induct, |
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
261 |
dtor_ctors = map (Morphism.thm phi) dtor_ctors, |
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
262 |
ctor_dtors = map (Morphism.thm phi) ctor_dtors, |
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
263 |
ctor_injects = map (Morphism.thm phi) ctor_injects, |
53203
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53202
diff
changeset
|
264 |
dtor_injects = map (Morphism.thm phi) dtor_injects, |
58583 | 265 |
xtor_maps = map (Morphism.thm phi) xtor_maps, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
266 |
xtor_map_uniques = map (Morphism.thm phi) xtor_map_uniques, |
58584 | 267 |
xtor_setss = map (map (Morphism.thm phi)) xtor_setss, |
58585 | 268 |
xtor_rels = map (Morphism.thm phi) xtor_rels, |
62721 | 269 |
xtor_un_fold_thms_legacy = map (Morphism.thm phi) xtor_un_fold_thms_legacy, |
55868 | 270 |
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms, |
62721 | 271 |
xtor_un_fold_uniques_legacy = map (Morphism.thm phi) xtor_un_fold_uniques_legacy, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
272 |
xtor_co_rec_uniques = map (Morphism.thm phi) xtor_co_rec_uniques, |
62721 | 273 |
xtor_un_fold_o_maps_legacy = map (Morphism.thm phi) xtor_un_fold_o_maps_legacy, |
58578
9ff8ca957c02
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
desharna
parents:
58448
diff
changeset
|
274 |
xtor_co_rec_o_maps = map (Morphism.thm phi) xtor_co_rec_o_maps, |
62721 | 275 |
xtor_un_fold_transfers_legacy = map (Morphism.thm phi) xtor_un_fold_transfers_legacy, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
276 |
xtor_co_rec_transfers = map (Morphism.thm phi) xtor_co_rec_transfers, |
58579
b7bc5ba2f3fb
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
desharna
parents:
58578
diff
changeset
|
277 |
xtor_rel_co_induct = Morphism.thm phi xtor_rel_co_induct, |
59856
ed0ca9029021
export more low-level theorems in data structure (partly for 'corec')
blanchet
parents:
59819
diff
changeset
|
278 |
dtor_set_inducts = map (Morphism.thm phi) dtor_set_inducts}; |
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
279 |
|
53143
ba80154a1118
configuration option to control timing output for (co)datatypes
traytel
parents:
53138
diff
changeset
|
280 |
fun time ctxt timer msg = (if Config.get ctxt bnf_timing |
55811 | 281 |
then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ |
62685 | 282 |
" ms") |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
283 |
else (); Timer.startRealTimer ()); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
284 |
|
49223 | 285 |
val preN = "pre_" |
286 |
val rawN = "raw_" |
|
49218 | 287 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
288 |
val coN = "co" |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
289 |
val unN = "un" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
290 |
val algN = "alg" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
291 |
val IITN = "IITN" |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
292 |
val foldN = "fold" |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
293 |
val unfoldN = unN ^ foldN |
62125 | 294 |
val uniqueN = "unique" |
295 |
val transferN = "transfer" |
|
49438 | 296 |
val simpsN = "simps" |
49501 | 297 |
val ctorN = "ctor" |
298 |
val dtorN = "dtor" |
|
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
299 |
val ctor_foldN = ctorN ^ "_" ^ foldN |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
300 |
val dtor_unfoldN = dtorN ^ "_" ^ unfoldN |
62125 | 301 |
val ctor_fold_uniqueN = ctor_foldN ^ "_" ^ uniqueN |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
302 |
val ctor_fold_o_mapN = ctor_foldN ^ "_o_" ^ mapN |
62125 | 303 |
val dtor_unfold_uniqueN = dtor_unfoldN ^ "_" ^ uniqueN |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
304 |
val dtor_unfold_o_mapN = dtor_unfoldN ^ "_o_" ^ mapN |
62125 | 305 |
val ctor_fold_transferN = ctor_foldN ^ "_" ^ transferN |
306 |
val dtor_unfold_transferN = dtor_unfoldN ^ "_" ^ transferN |
|
49541 | 307 |
val ctor_mapN = ctorN ^ "_" ^ mapN |
308 |
val dtor_mapN = dtorN ^ "_" ^ mapN |
|
62125 | 309 |
val map_uniqueN = mapN ^ "_" ^ uniqueN |
49543
53b3c532a082
renamed low-level "map_unique" to have "ctor" or "dtor" in the name
blanchet
parents:
49542
diff
changeset
|
310 |
val ctor_map_uniqueN = ctorN ^ "_" ^ map_uniqueN |
53b3c532a082
renamed low-level "map_unique" to have "ctor" or "dtor" in the name
blanchet
parents:
49542
diff
changeset
|
311 |
val dtor_map_uniqueN = dtorN ^ "_" ^ map_uniqueN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
312 |
val min_algN = "min_alg" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
313 |
val morN = "mor" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
314 |
val bisN = "bis" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
315 |
val lsbisN = "lsbis" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
316 |
val sum_bdTN = "sbdT" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
317 |
val sum_bdN = "sbd" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
318 |
val carTN = "carT" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
319 |
val strTN = "strT" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
320 |
val isNodeN = "isNode" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
321 |
val LevN = "Lev" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
322 |
val rvN = "recover" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
323 |
val behN = "beh" |
53694 | 324 |
val setN = "set" |
49584
4339aa335355
use singular since there is always only one theorem
blanchet
parents:
49582
diff
changeset
|
325 |
val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN |
4339aa335355
use singular since there is always only one theorem
blanchet
parents:
49582
diff
changeset
|
326 |
val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
327 |
fun mk_set_inductN i = mk_setN i ^ "_induct" |
49542
b39354db8629
renamed low-level "set_simps" and "set_induct" to have "ctor" or "dtor" in the name
blanchet
parents:
49541
diff
changeset
|
328 |
val mk_dtor_set_inductN = prefix (dtorN ^ "_") o mk_set_inductN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
329 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
330 |
val str_initN = "str_init" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
331 |
val recN = "rec" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
332 |
val corecN = coN ^ recN |
49501 | 333 |
val ctor_recN = ctorN ^ "_" ^ recN |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
334 |
val ctor_rec_o_mapN = ctor_recN ^ "_o_" ^ mapN |
62125 | 335 |
val ctor_rec_transferN = ctor_recN ^ "_" ^ transferN |
336 |
val ctor_rec_uniqueN = ctor_recN ^ "_" ^ uniqueN |
|
49501 | 337 |
val dtor_corecN = dtorN ^ "_" ^ corecN |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
338 |
val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN |
62125 | 339 |
val dtor_corec_transferN = dtor_corecN ^ "_" ^ transferN |
340 |
val dtor_corec_uniqueN = dtor_corecN ^ "_" ^ uniqueN |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
341 |
|
49501 | 342 |
val ctor_dtorN = ctorN ^ "_" ^ dtorN |
343 |
val dtor_ctorN = dtorN ^ "_" ^ ctorN |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
344 |
val nchotomyN = "nchotomy" |
49019 | 345 |
val injectN = "inject" |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
346 |
val exhaustN = "exhaust" |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
347 |
val ctor_injectN = ctorN ^ "_" ^ injectN |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
348 |
val ctor_exhaustN = ctorN ^ "_" ^ exhaustN |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
349 |
val dtor_injectN = dtorN ^ "_" ^ injectN |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
350 |
val dtor_exhaustN = dtorN ^ "_" ^ exhaustN |
49545
8bb6e2d7346b
renamed coinduction principles to have "dtor" in the name
blanchet
parents:
49544
diff
changeset
|
351 |
val ctor_relN = ctorN ^ "_" ^ relN |
8bb6e2d7346b
renamed coinduction principles to have "dtor" in the name
blanchet
parents:
49544
diff
changeset
|
352 |
val dtor_relN = dtorN ^ "_" ^ relN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
353 |
val inductN = "induct" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
354 |
val coinductN = coN ^ inductN |
49501 | 355 |
val ctor_inductN = ctorN ^ "_" ^ inductN |
356 |
val ctor_induct2N = ctor_inductN ^ "2" |
|
49581
4e5bd3883429
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
blanchet
parents:
49545
diff
changeset
|
357 |
val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN |
49582
557302525778
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
blanchet
parents:
49581
diff
changeset
|
358 |
val dtor_coinductN = dtorN ^ "_" ^ coinductN |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57700
diff
changeset
|
359 |
val coinduct_strongN = coinductN ^ "_strong" |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57700
diff
changeset
|
360 |
val dtor_map_coinduct_strongN = dtor_mapN ^ "_" ^ coinduct_strongN |
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57700
diff
changeset
|
361 |
val dtor_coinduct_strongN = dtorN ^ "_" ^ coinduct_strongN |
56113 | 362 |
val colN = "col" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
363 |
val set_inclN = "set_incl" |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
364 |
val ctor_set_inclN = ctorN ^ "_" ^ set_inclN |
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
365 |
val dtor_set_inclN = dtorN ^ "_" ^ set_inclN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
366 |
val set_set_inclN = "set_set_incl" |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
367 |
val ctor_set_set_inclN = ctorN ^ "_" ^ set_set_inclN |
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
368 |
val dtor_set_set_inclN = dtorN ^ "_" ^ set_set_inclN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
369 |
|
49338 | 370 |
val caseN = "case" |
49342 | 371 |
val discN = "disc" |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57700
diff
changeset
|
372 |
val corec_discN = corecN ^ "_" ^ discN |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
373 |
val iffN = "_iff" |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57700
diff
changeset
|
374 |
val corec_disc_iffN = corec_discN ^ iffN |
49592
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
375 |
val distinctN = "distinct" |
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
376 |
val rel_distinctN = relN ^ "_" ^ distinctN |
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
377 |
val injectN = "inject" |
57525 | 378 |
val rel_casesN = relN ^ "_cases" |
49592
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
379 |
val rel_injectN = relN ^ "_" ^ injectN |
57493 | 380 |
val rel_introsN = relN ^ "_intros" |
51918 | 381 |
val rel_coinductN = relN ^ "_" ^ coinductN |
57563 | 382 |
val rel_selN = relN ^ "_sel" |
55901
8c6d49dd8ae1
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
blanchet
parents:
55899
diff
changeset
|
383 |
val dtor_rel_coinductN = dtorN ^ "_" ^ rel_coinductN |
51918 | 384 |
val rel_inductN = relN ^ "_" ^ inductN |
55901
8c6d49dd8ae1
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
blanchet
parents:
55899
diff
changeset
|
385 |
val ctor_rel_inductN = ctorN ^ "_" ^ rel_inductN |
49342 | 386 |
val selN = "sel" |
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
57700
diff
changeset
|
387 |
val corec_selN = corecN ^ "_" ^ selN |
49338 | 388 |
|
55966 | 389 |
fun co_prefix fp = case_fp fp "" "co"; |
51863 | 390 |
|
49264 | 391 |
fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T'); |
392 |
||
393 |
val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT; |
|
394 |
||
55966 | 395 |
fun dest_tupleT_balanced 0 @{typ unit} = [] |
396 |
| dest_tupleT_balanced n T = Balanced_Tree.dest HOLogic.dest_prodT n T; |
|
49264 | 397 |
|
55966 | 398 |
fun dest_absumprodT absT repT n ms = |
399 |
map2 dest_tupleT_balanced ms o dest_sumTN_balanced n o mk_repT absT repT; |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
400 |
|
49264 | 401 |
val mk_sumTN = Library.foldr1 mk_sumT; |
402 |
val mk_sumTN_balanced = Balanced_Tree.make mk_sumT; |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
403 |
|
55966 | 404 |
fun mk_tupleT_balanced [] = HOLogic.unitT |
405 |
| mk_tupleT_balanced Ts = Balanced_Tree.make HOLogic.mk_prodT Ts; |
|
406 |
||
407 |
val mk_sumprodT_balanced = mk_sumTN_balanced o map mk_tupleT_balanced; |
|
408 |
||
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
409 |
fun mk_proj T n k = |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
410 |
let val (binders, _) = strip_typeN n T in |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
411 |
fold_rev (fn T => fn t => Abs (Name.uu, T, t)) binders (Bound (n - k - 1)) |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
412 |
end; |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
413 |
|
53032 | 414 |
fun mk_convol (f, g) = |
415 |
let |
|
416 |
val (fU, fTU) = `range_type (fastype_of f); |
|
417 |
val ((gT, gU), gTU) = `dest_funT (fastype_of g); |
|
418 |
val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU); |
|
419 |
in Const (@{const_name convol}, convolT) $ f $ g end; |
|
49368 | 420 |
|
58443 | 421 |
fun mk_rel_prod R S = |
422 |
let |
|
423 |
val ((A1, A2), RT) = `dest_pred2T (fastype_of R); |
|
424 |
val ((B1, B2), ST) = `dest_pred2T (fastype_of S); |
|
425 |
val rel_prodT = RT --> ST --> mk_pred2T (HOLogic.mk_prodT (A1, B1)) (HOLogic.mk_prodT (A2, B2)); |
|
426 |
in Const (@{const_name rel_prod}, rel_prodT) $ R $ S end; |
|
427 |
||
428 |
fun mk_rel_sum R S = |
|
429 |
let |
|
430 |
val ((A1, A2), RT) = `dest_pred2T (fastype_of R); |
|
431 |
val ((B1, B2), ST) = `dest_pred2T (fastype_of S); |
|
432 |
val rel_sumT = RT --> ST --> mk_pred2T (mk_sumT (A1, B1)) (mk_sumT (A2, B2)); |
|
433 |
in Const (@{const_name rel_sum}, rel_sumT) $ R $ S end; |
|
434 |
||
49121 | 435 |
fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT)); |
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
436 |
fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t; |
49121 | 437 |
|
438 |
fun Inr_const LT RT = Const (@{const_name Inr}, RT --> mk_sumT (LT, RT)); |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
439 |
fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t; |
49121 | 440 |
|
55969 | 441 |
fun mk_prod1 bound_Ts (t, u) = |
442 |
HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u; |
|
443 |
||
444 |
fun mk_tuple1_balanced _ [] = HOLogic.unit |
|
445 |
| mk_tuple1_balanced bound_Ts ts = Balanced_Tree.make (mk_prod1 bound_Ts) ts; |
|
446 |
||
447 |
val mk_tuple_balanced = mk_tuple1_balanced []; |
|
55966 | 448 |
|
59873 | 449 |
fun abs_curried_balanced Ts t = |
450 |
t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0)) |
|
451 |
|> fold_rev (Term.abs o pair Name.uu) Ts; |
|
452 |
||
59673 | 453 |
fun mk_sumprod_balanced T n k ts = Sum_Tree.mk_inj T n k (mk_tuple_balanced ts); |
454 |
||
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
455 |
fun mk_absumprod absT abs0 n k ts = |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
456 |
let val abs = mk_abs absT abs0; |
59673 | 457 |
in abs $ mk_sumprod_balanced (domain_type (fastype_of abs)) n k ts end; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
458 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
459 |
fun mk_case_sum (f, g) = |
49129 | 460 |
let |
55968 | 461 |
val (fT, T') = dest_funT (fastype_of f); |
462 |
val (gT, _) = dest_funT (fastype_of g); |
|
49129 | 463 |
in |
55968 | 464 |
Sum_Tree.mk_sumcase fT gT T' f g |
49129 | 465 |
end; |
466 |
||
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
467 |
val mk_case_sumN = Library.foldr1 mk_case_sum; |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
468 |
val mk_case_sumN_balanced = Balanced_Tree.make mk_case_sum; |
49176 | 469 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
470 |
fun mk_tupled_fun f x xs = |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
471 |
if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs)); |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
472 |
|
55968 | 473 |
fun mk_case_absumprod absT rep fs xss xss' = |
62124 | 474 |
HOLogic.mk_comp (mk_case_sumN_balanced |
475 |
(@{map 3} mk_tupled_fun fs (map mk_tuple_balanced xss) xss'), mk_rep absT rep); |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
476 |
|
53202
2333fae25719
export one more ML function, needed for primcorec
blanchet
parents:
53143
diff
changeset
|
477 |
fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T); |
2333fae25719
export one more ML function, needed for primcorec
blanchet
parents:
53143
diff
changeset
|
478 |
fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end; |
49275 | 479 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
480 |
fun mk_Field r = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
481 |
let val T = fst (dest_relT (fastype_of r)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
482 |
in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
483 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
484 |
val mk_union = HOLogic.mk_binop @{const_name sup}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
485 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
486 |
(*dangerous; use with monotonic, converging functions only!*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
487 |
fun fixpoint eq f X = if subset eq (f X, X) then X else fixpoint eq f (f X); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
488 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
489 |
(* stolen from "~~/src/HOL/Tools/Datatype/datatype_aux.ML" *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
490 |
fun split_conj_thm th = |
49119 | 491 |
((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th]; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
492 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
493 |
fun split_conj_prems limit th = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
494 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
495 |
fun split n i th = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
496 |
if i = n then th else split n (i + 1) (conjI RSN (i, th)) handle THM _ => th; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
497 |
in split limit 1 th end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
498 |
|
49335 | 499 |
fun mk_obj_sumEN_balanced n = |
500 |
Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f}))) |
|
501 |
(replicate n asm_rl); |
|
502 |
||
55966 | 503 |
fun mk_tupled_allIN_balanced 0 = @{thm unit_all_impI} |
504 |
| mk_tupled_allIN_balanced n = |
|
505 |
let |
|
506 |
val (tfrees, _) = BNF_Util.mk_TFrees n @{context}; |
|
507 |
val T = mk_tupleT_balanced tfrees; |
|
508 |
in |
|
509 |
@{thm asm_rl[of "ALL x. P x --> Q x" for P Q]} |
|
60801 | 510 |
|> Thm.instantiate' [SOME (Thm.ctyp_of @{context} T)] [] |
55966 | 511 |
|> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]} |
512 |
|> (fn thm => impI RS funpow n (fn th => allI RS th) thm) |
|
513 |
|> Thm.varifyT_global |
|
514 |
end; |
|
49335 | 515 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
516 |
fun mk_absumprodE type_definition ms = |
49335 | 517 |
let val n = length ms in |
55966 | 518 |
mk_obj_sumEN_balanced n OF map mk_tupled_allIN_balanced ms RS |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
519 |
(type_definition RS @{thm type_copy_obj_one_point_absE}) |
49335 | 520 |
end; |
49264 | 521 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
522 |
fun mk_sum_caseN 1 1 = refl |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
523 |
| mk_sum_caseN _ 1 = @{thm sum.case(1)} |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
524 |
| mk_sum_caseN 2 2 = @{thm sum.case(2)} |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
525 |
| mk_sum_caseN n k = trans OF [@{thm case_sum_step(2)}, mk_sum_caseN (n - 1) (k - 1)]; |
49264 | 526 |
|
527 |
fun mk_sum_step base step thm = |
|
528 |
if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm]; |
|
529 |
||
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
530 |
fun mk_sum_caseN_balanced 1 1 = refl |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
531 |
| mk_sum_caseN_balanced n k = |
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55575
diff
changeset
|
532 |
Balanced_Tree.access {left = mk_sum_step @{thm sum.case(1)} @{thm case_sum_step(1)}, |
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55575
diff
changeset
|
533 |
right = mk_sum_step @{thm sum.case(2)} @{thm case_sum_step(2)}, init = refl} n k; |
49130
3c26e17b2849
implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset
|
534 |
|
55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
535 |
fun mk_sum_Cinfinite [thm] = thm |
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
536 |
| mk_sum_Cinfinite (thm :: thms) = @{thm Cinfinite_csum_weak} OF [thm, mk_sum_Cinfinite thms]; |
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
537 |
|
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
538 |
fun mk_sum_card_order [thm] = thm |
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
539 |
| mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms]; |
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
540 |
|
58579
b7bc5ba2f3fb
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
desharna
parents:
58578
diff
changeset
|
541 |
fun mk_xtor_rel_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy = |
52505
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
542 |
let |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
543 |
val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels; |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
544 |
val relphis = map (fn rel => Term.list_comb (rel, phis)) rels; |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
545 |
fun mk_xtor fp' xtor x = if fp = fp' then xtor $ x else x; |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
546 |
val dtor = mk_xtor Greatest_FP; |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
547 |
val ctor = mk_xtor Least_FP; |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
548 |
fun flip f x y = if fp = Greatest_FP then f y x else f x y; |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
549 |
|
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
550 |
fun mk_prem pre_relphi phi x y xtor xtor' = |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
551 |
HOLogic.mk_Trueprop (list_all_free [x, y] (flip (curry HOLogic.mk_imp) |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
552 |
(pre_relphi $ (dtor xtor x) $ (dtor xtor' y)) (phi $ (ctor xtor x) $ (ctor xtor' y)))); |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58585
diff
changeset
|
553 |
val prems = @{map 6} mk_prem pre_relphis pre_phis xs ys xtors xtor's; |
52505
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
554 |
|
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
555 |
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
556 |
(map2 (flip mk_leq) relphis pre_phis)); |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
557 |
in |
52506 | 558 |
Goal.prove_sorry lthy (map (fst o dest_Free) (phis @ pre_phis)) prems concl tac |
52505
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
559 |
|> Thm.close_derivation |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
560 |
|> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]})) |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
561 |
end; |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
562 |
|
62827 | 563 |
fun mk_xtor_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy = |
52731 | 564 |
let |
58443 | 565 |
val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_iphis)) pre_rels; |
52731 | 566 |
val relphis = map (fn rel => Term.list_comb (rel, phis)) rels; |
567 |
fun flip f x y = if fp = Greatest_FP then f y x else f x y; |
|
568 |
||
58443 | 569 |
val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_ophis; |
52731 | 570 |
fun mk_transfer relphi pre_phi un_fold un_fold' = |
55945 | 571 |
fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold'; |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58585
diff
changeset
|
572 |
val transfers = @{map 4} mk_transfer relphis pre_ophis un_folds un_folds'; |
52731 | 573 |
|
58443 | 574 |
val goal = fold_rev Logic.all (phis @ pre_ophis) |
52731 | 575 |
(HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers)); |
576 |
in |
|
577 |
Goal.prove_sorry lthy [] [] goal tac |
|
578 |
|> Thm.close_derivation |
|
579 |
|> split_conj_thm |
|
580 |
end; |
|
581 |
||
62827 | 582 |
fun mk_xtor_co_iter_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
583 |
map_cong0s = |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
584 |
let |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
585 |
val n = length sym_map_comps; |
55966 | 586 |
val rewrite_comp_comp2 = case_fp fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2}; |
587 |
val rewrite_comp_comp = case_fp fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp}; |
|
588 |
val map_cong_passive_args1 = replicate m (case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong); |
|
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
589 |
val map_cong_active_args1 = replicate n (if is_rec |
55966 | 590 |
then case_fp fp @{thm convol_o} @{thm o_case_sum} RS fun_cong |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
591 |
else refl); |
55966 | 592 |
val map_cong_passive_args2 = replicate m (case_fp fp @{thm comp_id} @{thm id_comp} RS fun_cong); |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
593 |
val map_cong_active_args2 = replicate n (if is_rec |
55966 | 594 |
then case_fp fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id} |
595 |
else case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong); |
|
55990 | 596 |
fun mk_map_congs passive active = |
597 |
map (fn thm => thm OF (passive @ active) RS @{thm ext}) map_cong0s; |
|
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
598 |
val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1; |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
599 |
val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2; |
57489 | 600 |
|
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
601 |
fun mk_rewrites map_congs = map2 (fn sym_map_comp => fn map_cong => |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
602 |
mk_trans sym_map_comp map_cong RS rewrite_comp_comp) sym_map_comps map_congs; |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
603 |
val rewrite1s = mk_rewrites map_cong1s; |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
604 |
val rewrite2s = mk_rewrites map_cong2s; |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
605 |
val unique_prems = |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58585
diff
changeset
|
606 |
@{map 4} (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 => |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
607 |
mk_trans (rewrite_comp_comp2 OF [xtor_map, un_fold]) |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
608 |
(mk_trans rewrite1 (mk_sym rewrite2))) |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
609 |
xtor_maps xtor_un_folds rewrite1s rewrite2s; |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
610 |
in |
55966 | 611 |
split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems) |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
612 |
end; |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
613 |
|
62722 | 614 |
fun fixpoint_bnf extra_qualify construct_fp bs resBs Ds0 fp_eqs comp_cache0 lthy = |
51868 | 615 |
let |
53143
ba80154a1118
configuration option to control timing output for (co)datatypes
traytel
parents:
53138
diff
changeset
|
616 |
val time = time lthy; |
51868 | 617 |
val timer = time (Timer.startRealTimer ()); |
58332 | 618 |
|
619 |
val nn = length fp_eqs; |
|
53222 | 620 |
val (Xs, rhsXs) = split_list fp_eqs; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
621 |
|
58332 | 622 |
fun flatten_tyargs Ass = |
53222 | 623 |
subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs; |
51868 | 624 |
|
53263 | 625 |
fun raw_qualify base_b = |
59858 | 626 |
let |
627 |
val qs = Binding.path_of base_b; |
|
628 |
val n = Binding.name_of base_b; |
|
53264 | 629 |
in |
630 |
Binding.prefix_name rawN |
|
631 |
#> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)]) |
|
62722 | 632 |
#> extra_qualify #> Binding.concealed |
53264 | 633 |
end; |
51868 | 634 |
|
62720 | 635 |
val ((bnfs, (deadss, livess)), (comp_cache, unfold_set)) = |
55706 | 636 |
apfst (apsnd split_list o split_list) |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58585
diff
changeset
|
637 |
(@{fold_map 2} |
62621 | 638 |
(fn b => bnf_of_typ true Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs |
62720 | 639 |
((comp_cache0, empty_unfolds), lthy)); |
51868 | 640 |
|
62722 | 641 |
fun norm_qualify i = |
642 |
Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1)))) |
|
643 |
#> extra_qualify #> Binding.concealed; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
644 |
|
49132 | 645 |
val Ass = map (map dest_TFree) livess; |
58332 | 646 |
val Ds' = fold (fold Term.add_tfreesT) deadss []; |
647 |
val Ds = union (op =) Ds' Ds0; |
|
648 |
val missing = resBs |> fold (subtract (op =)) (Ds' :: Ass); |
|
649 |
val (dead_phantoms, live_phantoms) = List.partition (member (op =) Ds0) missing; |
|
650 |
val resBs' = resBs |> fold (subtract (op =)) [dead_phantoms, Ds]; |
|
49132 | 651 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
652 |
val timer = time (timer "Construction of BNFs"); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
653 |
|
62720 | 654 |
val ((kill_poss, _), (bnfs', ((comp_cache', unfold_set'), lthy'))) = |
655 |
normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs (comp_cache, unfold_set); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
656 |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58585
diff
changeset
|
657 |
val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
658 |
|
62722 | 659 |
fun pre_qualify b = |
660 |
Binding.qualify false (Binding.name_of b) |
|
661 |
#> extra_qualify |
|
62093 | 662 |
#> not (Config.get lthy' bnf_internals) ? Binding.concealed; |
53264 | 663 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
664 |
val ((pre_bnfs, (deadss, absT_infos)), lthy'') = |
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
58585
diff
changeset
|
665 |
@{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) |
58332 | 666 |
bs (not (null live_phantoms) :: replicate (nn - 1) false) Dss bnfs' lthy' |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
667 |
|>> split_list |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
668 |
|>> apsnd split_list; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
669 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
670 |
val timer = time (timer "Normalization & sealing of BNFs"); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
671 |
|
58332 | 672 |
val res = construct_fp bs resBs (map TFree dead_phantoms, deadss) pre_bnfs absT_infos lthy''; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
673 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
674 |
val timer = time (timer "FP construction in total"); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
675 |
in |
62720 | 676 |
(((pre_bnfs, absT_infos), comp_cache'), res) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
677 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
678 |
|
58256
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
679 |
fun fp_antiquote_setup binding = |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
680 |
Thy_Output.antiquotation binding (Args.type_name {proper = true, strict = true}) |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
681 |
(fn {source = src, context = ctxt, ...} => fn fcT_name => |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
682 |
(case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
683 |
NONE => error ("Not a known freely generated type name: " ^ quote fcT_name) |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
684 |
| SOME {T = T0, ctrs = ctrs0, ...} => |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
685 |
let |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
686 |
val freezeT = Term.map_atyps (fn TVar ((s, _), S) => TFree (s, S) | T => T); |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
687 |
|
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
688 |
val T = freezeT T0; |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
689 |
val ctrs = map (Term.map_types freezeT) ctrs0; |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
690 |
|
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
691 |
val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt); |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
692 |
fun pretty_ctr ctr = |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
693 |
Pretty.block (Pretty.breaks (Syntax.pretty_term ctxt ctr :: |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
694 |
map pretty_typ_bracket (binder_types (fastype_of ctr)))); |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
695 |
val pretty_co_datatype = |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
696 |
Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 :: |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
697 |
Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 :: |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
698 |
flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs))); |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
699 |
in |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
700 |
Thy_Output.output ctxt |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
701 |
(Thy_Output.maybe_pretty_source (K (K pretty_co_datatype)) ctxt src [()]) |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
702 |
end)); |
08c0f0d4b9f4
generalized 'datatype' LaTeX antiquotation and added 'codatatype'
blanchet
parents:
58208
diff
changeset
|
703 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
704 |
end; |