author | blanchet |
Wed, 23 Apr 2014 10:23:27 +0200 | |
changeset 56650 | 1f9ab71d43a5 |
parent 56113 | e3b8f8319d73 |
child 57397 | 5004aca20821 |
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 |
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
4 |
Copyright 2012, 2013 |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
|
49389 | 6 |
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
|
7 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
|
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
|
9 |
signature BNF_FP_UTIL = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
sig |
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
11 |
type fp_result = |
51859 | 12 |
{Ts: typ list, |
13 |
bnfs: BNF_Def.bnf list, |
|
51839 | 14 |
ctors: term list, |
51819 | 15 |
dtors: term list, |
55868 | 16 |
xtor_co_recs: term list, |
53106 | 17 |
xtor_co_induct: thm, |
51819 | 18 |
dtor_ctors: thm list, |
19 |
ctor_dtors: thm list, |
|
20 |
ctor_injects: thm list, |
|
53203
222ea6acbdd6
moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
traytel
parents:
53202
diff
changeset
|
21 |
dtor_injects: thm list, |
52314 | 22 |
xtor_map_thms: thm list, |
23 |
xtor_set_thmss: thm list list, |
|
24 |
xtor_rel_thms: thm list, |
|
55868 | 25 |
xtor_co_rec_thms: thm list, |
26 |
xtor_co_rec_o_map_thms: thm list, |
|
53258
775b43e72d82
renamed an ML filed for consistency (low-level => ctor/dtor/xtor in name)
blanchet
parents:
53223
diff
changeset
|
27 |
rel_xtor_co_induct_thm: thm} |
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
28 |
|
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
29 |
val morph_fp_result: morphism -> fp_result -> fp_result |
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
30 |
|
56650
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
31 |
type fp_sugar = |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
32 |
{T: typ, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
33 |
BT: typ, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
34 |
X: typ, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
35 |
fp: BNF_Util.fp_kind, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
36 |
fp_res_index: int, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
37 |
fp_res: fp_result, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
38 |
pre_bnf: BNF_Def.bnf, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
39 |
absT_info: BNF_Comp.absT_info, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
40 |
nested_bnfs: BNF_Def.bnf list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
41 |
nesting_bnfs: BNF_Def.bnf list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
42 |
ctrXs_Tss: typ list list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
43 |
ctr_defs: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
44 |
ctr_sugar: Ctr_Sugar.ctr_sugar, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
45 |
co_rec: term, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
46 |
co_rec_def: thm, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
47 |
maps: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
48 |
common_co_inducts: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
49 |
co_inducts: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
50 |
co_rec_thms: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
51 |
disc_co_recs: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
52 |
sel_co_recss: thm list list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
53 |
rel_injects: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
54 |
rel_distincts: thm list}; |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
55 |
|
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
56 |
val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
57 |
val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
58 |
|
53143
ba80154a1118
configuration option to control timing output for (co)datatypes
traytel
parents:
53138
diff
changeset
|
59 |
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
|
60 |
|
55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
61 |
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
|
62 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
63 |
val IITN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
val LevN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
65 |
val algN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
66 |
val behN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
67 |
val bisN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
val carTN: string |
49338 | 69 |
val caseN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
70 |
val coN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
val coinductN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
72 |
val corecN: string |
49501 | 73 |
val ctorN: string |
74 |
val ctor_dtorN: string |
|
75 |
val ctor_exhaustN: string |
|
76 |
val ctor_induct2N: string |
|
77 |
val ctor_inductN: string |
|
78 |
val ctor_injectN: string |
|
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
79 |
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
|
80 |
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
|
81 |
val ctor_fold_transferN: string |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
82 |
val ctor_fold_uniqueN: string |
49541 | 83 |
val ctor_mapN: string |
49543
53b3c532a082
renamed low-level "map_unique" to have "ctor" or "dtor" in the name
blanchet
parents:
49542
diff
changeset
|
84 |
val ctor_map_uniqueN: string |
49501 | 85 |
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
|
86 |
val ctor_rec_o_mapN: string |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
87 |
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
|
88 |
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
|
89 |
val ctor_rel_inductN: string |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
90 |
val ctor_set_inclN: string |
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
91 |
val ctor_set_set_inclN: string |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
92 |
val disc_corecN: string |
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
93 |
val disc_corec_iffN: string |
49501 | 94 |
val dtorN: string |
49582
557302525778
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
blanchet
parents:
49581
diff
changeset
|
95 |
val dtor_coinductN: string |
49501 | 96 |
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
|
97 |
val dtor_corec_o_mapN: string |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
98 |
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
|
99 |
val dtor_ctorN: string |
49501 | 100 |
val dtor_exhaustN: string |
101 |
val dtor_injectN: string |
|
49545
8bb6e2d7346b
renamed coinduction principles to have "dtor" in the name
blanchet
parents:
49544
diff
changeset
|
102 |
val dtor_mapN: string |
49581
4e5bd3883429
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
blanchet
parents:
49545
diff
changeset
|
103 |
val dtor_map_coinductN: string |
4e5bd3883429
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
blanchet
parents:
49545
diff
changeset
|
104 |
val dtor_map_strong_coinductN: string |
49543
53b3c532a082
renamed low-level "map_unique" to have "ctor" or "dtor" in the name
blanchet
parents:
49542
diff
changeset
|
105 |
val dtor_map_uniqueN: string |
49545
8bb6e2d7346b
renamed coinduction principles to have "dtor" in the name
blanchet
parents:
49544
diff
changeset
|
106 |
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
|
107 |
val dtor_rel_coinductN: string |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
108 |
val dtor_set_inclN: string |
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
109 |
val dtor_set_set_inclN: string |
49582
557302525778
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
blanchet
parents:
49581
diff
changeset
|
110 |
val dtor_strong_coinductN: string |
49516
d4859efc1096
renamed "rel_simp" to "dtor_rel" and similarly for "srel"
blanchet
parents:
49510
diff
changeset
|
111 |
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
|
112 |
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
|
113 |
val dtor_unfold_transferN: string |
49516
d4859efc1096
renamed "rel_simp" to "dtor_rel" and similarly for "srel"
blanchet
parents:
49510
diff
changeset
|
114 |
val dtor_unfold_uniqueN: string |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
115 |
val exhaustN: string |
56113 | 116 |
val colN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
117 |
val inductN: string |
49019 | 118 |
val injectN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
119 |
val isNodeN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
120 |
val lsbisN: string |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
121 |
val mapN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
122 |
val map_uniqueN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
123 |
val min_algN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
124 |
val morN: string |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
125 |
val nchotomyN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
126 |
val recN: string |
51918 | 127 |
val rel_coinductN: string |
128 |
val rel_inductN: string |
|
49592
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
129 |
val rel_injectN: string |
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
130 |
val rel_distinctN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
131 |
val rvN: string |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
132 |
val sel_corecN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
133 |
val set_inclN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
134 |
val set_set_inclN: string |
53694 | 135 |
val setN: string |
49438 | 136 |
val simpsN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
137 |
val strTN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
138 |
val str_initN: string |
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
139 |
val strong_coinductN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
140 |
val sum_bdN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
141 |
val sum_bdTN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
142 |
val uniqueN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
143 |
|
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
144 |
(* 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
|
145 |
val mk_ctor_setN: int -> string |
4339aa335355
use singular since there is always only one theorem
blanchet
parents:
49582
diff
changeset
|
146 |
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
|
147 |
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
|
148 |
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
|
149 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55570
diff
changeset
|
150 |
val co_prefix: BNF_Util.fp_kind -> string |
51863 | 151 |
|
52963
96754402c851
reverted ill-advised naming scheme of 5a77edcdbe54
blanchet
parents:
52958
diff
changeset
|
152 |
val base_name_of_typ: typ -> string |
49327
541d818d2ff3
put an underscore between names, for compatibility with old package (and also because it makes sense)
blanchet
parents:
49308
diff
changeset
|
153 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
154 |
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
|
155 |
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
|
156 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
157 |
val mk_sumTN: typ list -> typ |
55969 | 158 |
val mk_tupleT_balanced: typ list -> typ |
55966 | 159 |
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
|
160 |
|
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
161 |
val mk_proj: typ -> int -> int -> term |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
162 |
|
53032 | 163 |
val mk_convol: term * term -> term |
49368 | 164 |
|
49121 | 165 |
val Inl_const: typ -> typ -> term |
166 |
val Inr_const: typ -> typ -> term |
|
55969 | 167 |
val mk_tuple_balanced: term list -> term |
168 |
val mk_tuple1_balanced: typ list -> term list -> term |
|
49121 | 169 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
170 |
val mk_case_sum: term * term -> term |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
171 |
val mk_case_sumN: term list -> term |
55968 | 172 |
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
|
173 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
174 |
val mk_Inl: typ -> term -> term |
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
175 |
val mk_Inr: typ -> term -> term |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
176 |
val mk_absumprod: typ -> term -> int -> int -> term list -> term |
49121 | 177 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
178 |
val dest_sumT: typ -> typ * typ |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
179 |
val dest_absumprodT: typ -> typ -> int -> int list -> typ -> typ list list |
49176 | 180 |
|
53202
2333fae25719
export one more ML function, needed for primcorec
blanchet
parents:
53143
diff
changeset
|
181 |
val If_const: typ -> term |
2333fae25719
export one more ML function, needed for primcorec
blanchet
parents:
53143
diff
changeset
|
182 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
183 |
val mk_Field: term -> term |
49275 | 184 |
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
|
185 |
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
|
186 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
187 |
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
|
188 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
189 |
val mk_sum_caseN: int -> int -> thm |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
190 |
val mk_sum_caseN_balanced: int -> int -> thm |
49125 | 191 |
|
55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
192 |
val mk_sum_Cinfinite: thm list -> thm |
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
193 |
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
|
194 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55570
diff
changeset
|
195 |
val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list -> |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55570
diff
changeset
|
196 |
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
|
197 |
({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55570
diff
changeset
|
198 |
val mk_un_fold_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list -> |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55570
diff
changeset
|
199 |
term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> |
52731 | 200 |
Proof.context -> thm list |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55570
diff
changeset
|
201 |
val mk_xtor_un_fold_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
|
202 |
thm list -> thm list -> thm list |
52505
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
203 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
204 |
val mk_strong_coinduct_thm: thm -> thm list -> thm list -> (thm -> thm) -> Proof.context -> thm |
53105
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
205 |
|
51867 | 206 |
val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list -> |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
207 |
BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) -> |
55701 | 208 |
binding list -> (string * sort) list -> (string * sort) list -> ((string * sort) * typ) list -> |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
209 |
local_theory -> (BNF_Def.bnf list * BNF_Comp.absT_info list) * 'a |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
210 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
211 |
|
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
|
212 |
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
|
213 |
struct |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
214 |
|
56650
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
215 |
open Ctr_Sugar |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
216 |
open BNF_Comp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
217 |
open BNF_Def |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
218 |
open BNF_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
219 |
|
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
220 |
type fp_result = |
51859 | 221 |
{Ts: typ list, |
222 |
bnfs: BNF_Def.bnf list, |
|
51839 | 223 |
ctors: term list, |
51819 | 224 |
dtors: 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, |
52314 | 231 |
xtor_map_thms: thm list, |
232 |
xtor_set_thmss: thm list list, |
|
233 |
xtor_rel_thms: thm list, |
|
55868 | 234 |
xtor_co_rec_thms: thm list, |
235 |
xtor_co_rec_o_map_thms: thm list, |
|
53258
775b43e72d82
renamed an ML filed for consistency (low-level => ctor/dtor/xtor in name)
blanchet
parents:
53223
diff
changeset
|
236 |
rel_xtor_co_induct_thm: thm}; |
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
237 |
|
55899
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55869
diff
changeset
|
238 |
fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct, |
55868 | 239 |
dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, |
55899
8c0a13e84963
N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
traytel
parents:
55869
diff
changeset
|
240 |
xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} = |
51859 | 241 |
{Ts = map (Morphism.typ phi) Ts, |
242 |
bnfs = map (morph_bnf phi) bnfs, |
|
51839 | 243 |
ctors = map (Morphism.term phi) ctors, |
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
244 |
dtors = map (Morphism.term phi) dtors, |
55868 | 245 |
xtor_co_recs = map (Morphism.term phi) xtor_co_recs, |
53106 | 246 |
xtor_co_induct = Morphism.thm phi xtor_co_induct, |
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
247 |
dtor_ctors = map (Morphism.thm phi) dtor_ctors, |
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
248 |
ctor_dtors = map (Morphism.thm phi) ctor_dtors, |
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
249 |
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
|
250 |
dtor_injects = map (Morphism.thm phi) dtor_injects, |
52314 | 251 |
xtor_map_thms = map (Morphism.thm phi) xtor_map_thms, |
252 |
xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss, |
|
253 |
xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms, |
|
55868 | 254 |
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms, |
255 |
xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms, |
|
53258
775b43e72d82
renamed an ML filed for consistency (low-level => ctor/dtor/xtor in name)
blanchet
parents:
53223
diff
changeset
|
256 |
rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm}; |
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
257 |
|
56650
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
258 |
type fp_sugar = |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
259 |
{T: typ, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
260 |
BT: typ, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
261 |
X: typ, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
262 |
fp: fp_kind, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
263 |
fp_res_index: int, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
264 |
fp_res: fp_result, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
265 |
pre_bnf: bnf, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
266 |
absT_info: absT_info, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
267 |
nested_bnfs: bnf list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
268 |
nesting_bnfs: bnf list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
269 |
ctrXs_Tss: typ list list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
270 |
ctr_defs: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
271 |
ctr_sugar: Ctr_Sugar.ctr_sugar, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
272 |
co_rec: term, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
273 |
co_rec_def: thm, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
274 |
maps: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
275 |
common_co_inducts: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
276 |
co_inducts: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
277 |
co_rec_thms: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
278 |
disc_co_recs: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
279 |
sel_co_recss: thm list list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
280 |
rel_injects: thm list, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
281 |
rel_distincts: thm list}; |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
282 |
|
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
283 |
fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
284 |
nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
285 |
co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, rel_injects, rel_distincts} : fp_sugar) = |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
286 |
{T = Morphism.typ phi T, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
287 |
BT = Morphism.typ phi BT, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
288 |
X = Morphism.typ phi X, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
289 |
fp = fp, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
290 |
fp_res = morph_fp_result phi fp_res, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
291 |
fp_res_index = fp_res_index, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
292 |
pre_bnf = morph_bnf phi pre_bnf, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
293 |
absT_info = morph_absT_info phi absT_info, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
294 |
nested_bnfs = map (morph_bnf phi) nested_bnfs, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
295 |
nesting_bnfs = map (morph_bnf phi) nesting_bnfs, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
296 |
ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
297 |
ctr_defs = map (Morphism.thm phi) ctr_defs, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
298 |
ctr_sugar = morph_ctr_sugar phi ctr_sugar, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
299 |
co_rec = Morphism.term phi co_rec, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
300 |
co_rec_def = Morphism.thm phi co_rec_def, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
301 |
maps = map (Morphism.thm phi) maps, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
302 |
common_co_inducts = map (Morphism.thm phi) common_co_inducts, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
303 |
co_inducts = map (Morphism.thm phi) co_inducts, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
304 |
co_rec_thms = map (Morphism.thm phi) co_rec_thms, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
305 |
disc_co_recs = map (Morphism.thm phi) disc_co_recs, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
306 |
sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
307 |
rel_injects = map (Morphism.thm phi) rel_injects, |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
308 |
rel_distincts = map (Morphism.thm phi) rel_distincts}; |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
309 |
|
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
310 |
val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of; |
1f9ab71d43a5
no need to make 'size' generation an interpretation -- overkill
blanchet
parents:
56113
diff
changeset
|
311 |
|
53143
ba80154a1118
configuration option to control timing output for (co)datatypes
traytel
parents:
53138
diff
changeset
|
312 |
fun time ctxt timer msg = (if Config.get ctxt bnf_timing |
55811 | 313 |
then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^ |
314 |
"ms") |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
315 |
else (); Timer.startRealTimer ()); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
316 |
|
49223 | 317 |
val preN = "pre_" |
318 |
val rawN = "raw_" |
|
49218 | 319 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
320 |
val coN = "co" |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
321 |
val unN = "un" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
322 |
val algN = "alg" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
323 |
val IITN = "IITN" |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
324 |
val foldN = "fold" |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
325 |
val unfoldN = unN ^ foldN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
326 |
val uniqueN = "_unique" |
52731 | 327 |
val transferN = "_transfer" |
49438 | 328 |
val simpsN = "simps" |
49501 | 329 |
val ctorN = "ctor" |
330 |
val dtorN = "dtor" |
|
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
331 |
val ctor_foldN = ctorN ^ "_" ^ foldN |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
332 |
val dtor_unfoldN = dtorN ^ "_" ^ unfoldN |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
333 |
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
|
334 |
val ctor_fold_o_mapN = ctor_foldN ^ "_o_" ^ mapN |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
335 |
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
|
336 |
val dtor_unfold_o_mapN = dtor_unfoldN ^ "_o_" ^ mapN |
52731 | 337 |
val ctor_fold_transferN = ctor_foldN ^ transferN |
338 |
val dtor_unfold_transferN = dtor_unfoldN ^ transferN |
|
49541 | 339 |
val ctor_mapN = ctorN ^ "_" ^ mapN |
340 |
val dtor_mapN = dtorN ^ "_" ^ mapN |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
341 |
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
|
342 |
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
|
343 |
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
|
344 |
val min_algN = "min_alg" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
345 |
val morN = "mor" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
346 |
val bisN = "bis" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
347 |
val lsbisN = "lsbis" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
348 |
val sum_bdTN = "sbdT" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
349 |
val sum_bdN = "sbd" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
350 |
val carTN = "carT" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
351 |
val strTN = "strT" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
352 |
val isNodeN = "isNode" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
353 |
val LevN = "Lev" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
354 |
val rvN = "recover" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
355 |
val behN = "beh" |
53694 | 356 |
val setN = "set" |
49584
4339aa335355
use singular since there is always only one theorem
blanchet
parents:
49582
diff
changeset
|
357 |
val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN |
4339aa335355
use singular since there is always only one theorem
blanchet
parents:
49582
diff
changeset
|
358 |
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
|
359 |
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
|
360 |
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
|
361 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
362 |
val str_initN = "str_init" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
363 |
val recN = "rec" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
364 |
val corecN = coN ^ recN |
49501 | 365 |
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
|
366 |
val ctor_rec_o_mapN = ctor_recN ^ "_o_" ^ mapN |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
367 |
val ctor_rec_uniqueN = ctor_recN ^ uniqueN |
49501 | 368 |
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
|
369 |
val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
370 |
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
|
371 |
|
49501 | 372 |
val ctor_dtorN = ctorN ^ "_" ^ dtorN |
373 |
val dtor_ctorN = dtorN ^ "_" ^ ctorN |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
374 |
val nchotomyN = "nchotomy" |
49019 | 375 |
val injectN = "inject" |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
376 |
val exhaustN = "exhaust" |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
377 |
val ctor_injectN = ctorN ^ "_" ^ injectN |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
378 |
val ctor_exhaustN = ctorN ^ "_" ^ exhaustN |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
379 |
val dtor_injectN = dtorN ^ "_" ^ injectN |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
380 |
val dtor_exhaustN = dtorN ^ "_" ^ exhaustN |
49545
8bb6e2d7346b
renamed coinduction principles to have "dtor" in the name
blanchet
parents:
49544
diff
changeset
|
381 |
val ctor_relN = ctorN ^ "_" ^ relN |
8bb6e2d7346b
renamed coinduction principles to have "dtor" in the name
blanchet
parents:
49544
diff
changeset
|
382 |
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
|
383 |
val inductN = "induct" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
384 |
val coinductN = coN ^ inductN |
49501 | 385 |
val ctor_inductN = ctorN ^ "_" ^ inductN |
386 |
val ctor_induct2N = ctor_inductN ^ "2" |
|
49581
4e5bd3883429
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
blanchet
parents:
49545
diff
changeset
|
387 |
val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN |
49582
557302525778
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
blanchet
parents:
49581
diff
changeset
|
388 |
val dtor_coinductN = dtorN ^ "_" ^ coinductN |
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
389 |
val strong_coinductN = "strong_" ^ coinductN |
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
390 |
val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN |
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
391 |
val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN |
56113 | 392 |
val colN = "col" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
393 |
val set_inclN = "set_incl" |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
394 |
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
|
395 |
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
|
396 |
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
|
397 |
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
|
398 |
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
|
399 |
|
49338 | 400 |
val caseN = "case" |
49342 | 401 |
val discN = "disc" |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
402 |
val disc_corecN = discN ^ "_" ^ corecN |
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
403 |
val iffN = "_iff" |
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
404 |
val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN |
49592
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
405 |
val distinctN = "distinct" |
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
406 |
val rel_distinctN = relN ^ "_" ^ distinctN |
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
407 |
val injectN = "inject" |
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
408 |
val rel_injectN = relN ^ "_" ^ injectN |
51918 | 409 |
val rel_coinductN = relN ^ "_" ^ coinductN |
55901
8c6d49dd8ae1
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
blanchet
parents:
55899
diff
changeset
|
410 |
val dtor_rel_coinductN = dtorN ^ "_" ^ rel_coinductN |
51918 | 411 |
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
|
412 |
val ctor_rel_inductN = ctorN ^ "_" ^ rel_inductN |
49342 | 413 |
val selN = "sel" |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
414 |
val sel_corecN = selN ^ "_" ^ corecN |
49338 | 415 |
|
55966 | 416 |
fun co_prefix fp = case_fp fp "" "co"; |
51863 | 417 |
|
52963
96754402c851
reverted ill-advised naming scheme of 5a77edcdbe54
blanchet
parents:
52958
diff
changeset
|
418 |
fun add_components_of_typ (Type (s, Ts)) = |
53223 | 419 |
cons (Long_Name.base_name s) #> fold_rev add_components_of_typ Ts |
52963
96754402c851
reverted ill-advised naming scheme of 5a77edcdbe54
blanchet
parents:
52958
diff
changeset
|
420 |
| add_components_of_typ _ = I; |
96754402c851
reverted ill-advised naming scheme of 5a77edcdbe54
blanchet
parents:
52958
diff
changeset
|
421 |
|
96754402c851
reverted ill-advised naming scheme of 5a77edcdbe54
blanchet
parents:
52958
diff
changeset
|
422 |
fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []); |
96754402c851
reverted ill-advised naming scheme of 5a77edcdbe54
blanchet
parents:
52958
diff
changeset
|
423 |
|
49264 | 424 |
fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T'); |
425 |
||
426 |
val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT; |
|
427 |
||
55966 | 428 |
fun dest_tupleT_balanced 0 @{typ unit} = [] |
429 |
| dest_tupleT_balanced n T = Balanced_Tree.dest HOLogic.dest_prodT n T; |
|
49264 | 430 |
|
55966 | 431 |
fun dest_absumprodT absT repT n ms = |
432 |
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
|
433 |
|
49264 | 434 |
val mk_sumTN = Library.foldr1 mk_sumT; |
435 |
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
|
436 |
|
55966 | 437 |
fun mk_tupleT_balanced [] = HOLogic.unitT |
438 |
| mk_tupleT_balanced Ts = Balanced_Tree.make HOLogic.mk_prodT Ts; |
|
439 |
||
440 |
val mk_sumprodT_balanced = mk_sumTN_balanced o map mk_tupleT_balanced; |
|
441 |
||
54923
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
442 |
fun mk_proj T n k = |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
443 |
let val (binders, _) = strip_typeN n T in |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
444 |
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
|
445 |
end; |
ffed2452f5f6
instantiate schematics as projections to avoid HOU trouble
blanchet
parents:
54171
diff
changeset
|
446 |
|
53032 | 447 |
fun mk_convol (f, g) = |
448 |
let |
|
449 |
val (fU, fTU) = `range_type (fastype_of f); |
|
450 |
val ((gT, gU), gTU) = `dest_funT (fastype_of g); |
|
451 |
val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU); |
|
452 |
in Const (@{const_name convol}, convolT) $ f $ g end; |
|
49368 | 453 |
|
49121 | 454 |
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
|
455 |
fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t; |
49121 | 456 |
|
457 |
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
|
458 |
fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t; |
49121 | 459 |
|
55969 | 460 |
fun mk_prod1 bound_Ts (t, u) = |
461 |
HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u; |
|
462 |
||
463 |
fun mk_tuple1_balanced _ [] = HOLogic.unit |
|
464 |
| mk_tuple1_balanced bound_Ts ts = Balanced_Tree.make (mk_prod1 bound_Ts) ts; |
|
465 |
||
466 |
val mk_tuple_balanced = mk_tuple1_balanced []; |
|
55966 | 467 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
468 |
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
|
469 |
let val abs = mk_abs absT abs0; |
55968 | 470 |
in abs $ Sum_Tree.mk_inj (domain_type (fastype_of abs)) n k (mk_tuple_balanced ts) end; |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
471 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
472 |
fun mk_case_sum (f, g) = |
49129 | 473 |
let |
55968 | 474 |
val (fT, T') = dest_funT (fastype_of f); |
475 |
val (gT, _) = dest_funT (fastype_of g); |
|
49129 | 476 |
in |
55968 | 477 |
Sum_Tree.mk_sumcase fT gT T' f g |
49129 | 478 |
end; |
479 |
||
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
480 |
val mk_case_sumN = Library.foldr1 mk_case_sum; |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
481 |
val mk_case_sumN_balanced = Balanced_Tree.make mk_case_sum; |
49176 | 482 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
483 |
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
|
484 |
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
|
485 |
|
55968 | 486 |
fun mk_case_absumprod absT rep fs xss xss' = |
487 |
HOLogic.mk_comp (mk_case_sumN_balanced (map3 mk_tupled_fun fs (map mk_tuple_balanced xss) xss'), |
|
488 |
mk_rep absT rep); |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
489 |
|
53202
2333fae25719
export one more ML function, needed for primcorec
blanchet
parents:
53143
diff
changeset
|
490 |
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
|
491 |
fun mk_If p t f = let val T = fastype_of t in If_const T $ p $ t $ f end; |
49275 | 492 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
493 |
fun mk_Field r = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
494 |
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
|
495 |
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
|
496 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
497 |
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
|
498 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
499 |
(*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
|
500 |
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
|
501 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
502 |
(* 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
|
503 |
fun split_conj_thm th = |
49119 | 504 |
((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
|
505 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
506 |
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
|
507 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
508 |
fun split n i th = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
509 |
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
|
510 |
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
|
511 |
|
49335 | 512 |
fun mk_obj_sumEN_balanced n = |
513 |
Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f}))) |
|
514 |
(replicate n asm_rl); |
|
515 |
||
55966 | 516 |
fun mk_tupled_allIN_balanced 0 = @{thm unit_all_impI} |
517 |
| mk_tupled_allIN_balanced n = |
|
518 |
let |
|
519 |
val (tfrees, _) = BNF_Util.mk_TFrees n @{context}; |
|
520 |
val T = mk_tupleT_balanced tfrees; |
|
521 |
in |
|
522 |
@{thm asm_rl[of "ALL x. P x --> Q x" for P Q]} |
|
523 |
|> Drule.instantiate' [SOME (ctyp_of @{theory} T)] [] |
|
524 |
|> Raw_Simplifier.rewrite_goals_rule @{context} @{thms split_paired_All[THEN eq_reflection]} |
|
525 |
|> (fn thm => impI RS funpow n (fn th => allI RS th) thm) |
|
526 |
|> Thm.varifyT_global |
|
527 |
end; |
|
49335 | 528 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
529 |
fun mk_absumprodE type_definition ms = |
49335 | 530 |
let val n = length ms in |
55966 | 531 |
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
|
532 |
(type_definition RS @{thm type_copy_obj_one_point_absE}) |
49335 | 533 |
end; |
49264 | 534 |
|
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
535 |
fun mk_sum_caseN 1 1 = refl |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
536 |
| mk_sum_caseN _ 1 = @{thm sum.case(1)} |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
537 |
| mk_sum_caseN 2 2 = @{thm sum.case(2)} |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
538 |
| mk_sum_caseN n k = trans OF [@{thm case_sum_step(2)}, mk_sum_caseN (n - 1) (k - 1)]; |
49264 | 539 |
|
540 |
fun mk_sum_step base step thm = |
|
541 |
if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm]; |
|
542 |
||
55414
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
543 |
fun mk_sum_caseN_balanced 1 1 = refl |
eab03e9cee8a
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents:
55394
diff
changeset
|
544 |
| 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
|
545 |
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
|
546 |
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
|
547 |
|
55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
548 |
fun mk_sum_Cinfinite [thm] = thm |
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
549 |
| 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
|
550 |
|
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
551 |
fun mk_sum_card_order [thm] = thm |
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset
|
552 |
| 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
|
553 |
|
53258
775b43e72d82
renamed an ML filed for consistency (low-level => ctor/dtor/xtor in name)
blanchet
parents:
53223
diff
changeset
|
554 |
fun mk_rel_xtor_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
|
555 |
let |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
556 |
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
|
557 |
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
|
558 |
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
|
559 |
val dtor = mk_xtor Greatest_FP; |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
560 |
val ctor = mk_xtor Least_FP; |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
561 |
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
|
562 |
|
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
563 |
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
|
564 |
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
|
565 |
(pre_relphi $ (dtor xtor x) $ (dtor xtor' y)) (phi $ (ctor xtor x) $ (ctor xtor' y)))); |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
566 |
val prems = map6 mk_prem pre_relphis pre_phis xs ys xtors xtor's; |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
567 |
|
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
568 |
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
|
569 |
(map2 (flip mk_leq) relphis pre_phis)); |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
570 |
in |
52506 | 571 |
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
|
572 |
|> Thm.close_derivation |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
573 |
|> (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
|
574 |
end; |
e62f3fd2035e
share some code between codatatypes, datatypes and eventually prim(co)rec
traytel
parents:
52344
diff
changeset
|
575 |
|
52731 | 576 |
fun mk_un_fold_transfer_thms fp pre_rels pre_phis rels phis un_folds un_folds' tac lthy = |
577 |
let |
|
578 |
val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels; |
|
579 |
val relphis = map (fn rel => Term.list_comb (rel, phis)) rels; |
|
580 |
fun flip f x y = if fp = Greatest_FP then f y x else f x y; |
|
581 |
||
55945 | 582 |
val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_phis; |
52731 | 583 |
fun mk_transfer relphi pre_phi un_fold un_fold' = |
55945 | 584 |
fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold'; |
52731 | 585 |
val transfers = map4 mk_transfer relphis pre_phis un_folds un_folds'; |
586 |
||
587 |
val goal = fold_rev Logic.all (phis @ pre_phis) |
|
588 |
(HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers)); |
|
589 |
in |
|
590 |
Goal.prove_sorry lthy [] [] goal tac |
|
591 |
|> Thm.close_derivation |
|
592 |
|> split_conj_thm |
|
593 |
end; |
|
594 |
||
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
595 |
fun mk_xtor_un_fold_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
596 |
map_cong0s = |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
597 |
let |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
598 |
val n = length sym_map_comps; |
55966 | 599 |
val rewrite_comp_comp2 = case_fp fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2}; |
600 |
val rewrite_comp_comp = case_fp fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp}; |
|
601 |
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
|
602 |
val map_cong_active_args1 = replicate n (if is_rec |
55966 | 603 |
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
|
604 |
else refl); |
55966 | 605 |
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
|
606 |
val map_cong_active_args2 = replicate n (if is_rec |
55966 | 607 |
then case_fp fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id} |
608 |
else case_fp fp @{thm id_comp} @{thm comp_id} RS fun_cong); |
|
55990 | 609 |
fun mk_map_congs passive active = |
610 |
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
|
611 |
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
|
612 |
val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2; |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
613 |
|
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
614 |
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
|
615 |
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
|
616 |
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
|
617 |
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
|
618 |
val unique_prems = |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
619 |
map4 (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 => |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
620 |
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
|
621 |
(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
|
622 |
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
|
623 |
in |
55966 | 624 |
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
|
625 |
end; |
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52899
diff
changeset
|
626 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
627 |
fun mk_strong_coinduct_thm coind rel_eqs rel_monos mk_vimage2p ctxt = |
53105
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
628 |
let |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
629 |
val n = Thm.nprems_of coind; |
53106 | 630 |
val m = Thm.nprems_of (hd rel_monos) - n; |
53105
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
631 |
fun mk_inst phi = (phi, mk_union (phi, HOLogic.eq_const (fst (dest_pred2T (fastype_of phi))))) |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
632 |
|> pairself (certify ctxt); |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
633 |
val insts = Term.add_vars (Thm.prop_of coind) [] |> rev |> take n |> map (mk_inst o Var); |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
634 |
fun mk_unfold rel_eq rel_mono = |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
635 |
let |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
636 |
val eq = iffD2 OF [rel_eq RS @{thm predicate2_eqD}, refl]; |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
637 |
val mono = rel_mono OF (replicate m @{thm order_refl} @ replicate n @{thm eq_subset}); |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
638 |
in mk_vimage2p (eq RS (mono RS @{thm predicate2D})) RS @{thm eqTrueI} end; |
53105
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
639 |
val unfolds = map2 mk_unfold rel_eqs rel_monos @ @{thms sup_fun_def sup_bool_def |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
640 |
imp_disjL all_conj_distrib subst_eq_imp simp_thms(18,21,35)}; |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
641 |
in |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
642 |
Thm.instantiate ([], insts) coind |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
643 |
|> unfold_thms ctxt unfolds |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
644 |
end; |
ec38e9f4352f
simpler (forward) derivation of strong (up-to equality) coinduction properties
traytel
parents:
53037
diff
changeset
|
645 |
|
55701 | 646 |
fun fp_bnf construct_fp bs resBs Ds0 fp_eqs lthy = |
51868 | 647 |
let |
53143
ba80154a1118
configuration option to control timing output for (co)datatypes
traytel
parents:
53138
diff
changeset
|
648 |
val time = time lthy; |
51868 | 649 |
val timer = time (Timer.startRealTimer ()); |
53222 | 650 |
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
|
651 |
|
53222 | 652 |
(* FIXME: because of "@ Xs", the output could contain type variables that are not in the |
51868 | 653 |
input; also, "fp_sort" should put the "resBs" first and in the order in which they appear *) |
654 |
fun fp_sort Ass = |
|
53222 | 655 |
subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs; |
51868 | 656 |
|
53263 | 657 |
fun raw_qualify base_b = |
53264 | 658 |
let val (_, qs, n) = Binding.dest base_b; |
659 |
in |
|
660 |
Binding.prefix_name rawN |
|
661 |
#> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)]) |
|
53566 | 662 |
#> Binding.conceal |
53264 | 663 |
end; |
51868 | 664 |
|
55904 | 665 |
val ((bnfs, (deadss, livess)), accum) = |
55706 | 666 |
apfst (apsnd split_list o split_list) |
667 |
(fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs Ds0) bs rhsXs |
|
668 |
((empty_comp_cache, empty_unfolds), lthy)); |
|
51868 | 669 |
|
53566 | 670 |
fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1)))) |
671 |
#> Binding.conceal; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
672 |
|
49132 | 673 |
val Ass = map (map dest_TFree) livess; |
51866 | 674 |
val resDs = fold (subtract (op =)) Ass resBs; |
55701 | 675 |
val Ds = fold (fold Term.add_tfreesT) deadss Ds0; |
49132 | 676 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
677 |
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
|
678 |
|
55904 | 679 |
val ((kill_poss, _), (bnfs', ((_, unfold_set'), lthy'))) = |
680 |
normalize_bnfs norm_qualify Ass Ds fp_sort bnfs accum; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
681 |
|
49132 | 682 |
val Dss = map3 (append 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
|
683 |
|
53566 | 684 |
fun pre_qualify b = Binding.qualify false (Binding.name_of b) |
685 |
#> Config.get lthy' bnf_note_all = false ? Binding.conceal; |
|
53264 | 686 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
687 |
val ((pre_bnfs, (deadss, absT_infos)), lthy'') = |
53264 | 688 |
fold_map3 (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b)) |
689 |
bs Dss bnfs' lthy' |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
690 |
|>> split_list |
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
691 |
|>> apsnd split_list; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
692 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
693 |
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
|
694 |
|
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
695 |
val res = construct_fp bs resBs (map TFree resDs, 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
|
696 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
697 |
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
|
698 |
in |
55803
74d3fe9031d8
joint work with blanchet: intermediate typedef for the input to fp-operations
traytel
parents:
55706
diff
changeset
|
699 |
timer; ((pre_bnfs, absT_infos), res) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
700 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
701 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
702 |
end; |