author | blanchet |
Fri, 07 Jun 2013 09:28:59 +0200 | |
changeset 52330 | 8ce7fba90bb3 |
parent 52328 | 2f286a2b7f98 |
child 52343 | a83404aca047 |
permissions | -rw-r--r-- |
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
|
1 |
(* Title: HOL/BNF/Tools/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 |
52207
21026c312cc3
tuning -- avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52031
diff
changeset
|
11 |
datatype fp_kind = Least_FP | Greatest_FP |
21026c312cc3
tuning -- avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52031
diff
changeset
|
12 |
|
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, |
|
51839 | 16 |
ctors: term list, |
51819 | 17 |
dtors: term list, |
52328 | 18 |
xtor_co_iterss: term list list, |
52312
f461dca57c66
tuned record field names to avoid confusion between low-level and high-level constants/theorems
blanchet
parents:
52207
diff
changeset
|
19 |
xtor_co_induct: thm, |
f461dca57c66
tuned record field names to avoid confusion between low-level and high-level constants/theorems
blanchet
parents:
52207
diff
changeset
|
20 |
xtor_strong_co_induct: thm, |
51819 | 21 |
dtor_ctors: thm list, |
22 |
ctor_dtors: thm list, |
|
23 |
ctor_injects: thm list, |
|
52314 | 24 |
xtor_map_thms: thm list, |
25 |
xtor_set_thmss: thm list list, |
|
26 |
xtor_rel_thms: thm list, |
|
52328 | 27 |
xtor_co_iter_thmss: thm list list} |
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 |
val eq_fp_result: fp_result * fp_result -> bool |
52330 | 31 |
val un_fold_of: 'a list -> 'a |
32 |
val co_rec_of: 'a list -> 'a |
|
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
33 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
34 |
val time: Timer.real_timer -> string -> Timer.real_timer |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
35 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
36 |
val IITN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
37 |
val LevN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
38 |
val algN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
39 |
val behN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
40 |
val bisN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
41 |
val carTN: string |
49338 | 42 |
val caseN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
val coN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
44 |
val coinductN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
45 |
val corecN: string |
49501 | 46 |
val ctorN: string |
47 |
val ctor_dtorN: string |
|
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
48 |
val ctor_dtor_corecN: string |
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
49 |
val ctor_dtor_unfoldN: string |
49501 | 50 |
val ctor_exhaustN: string |
51 |
val ctor_induct2N: string |
|
52 |
val ctor_inductN: string |
|
53 |
val ctor_injectN: string |
|
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
54 |
val ctor_foldN: string |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
55 |
val ctor_fold_uniqueN: string |
49541 | 56 |
val ctor_mapN: string |
49543
53b3c532a082
renamed low-level "map_unique" to have "ctor" or "dtor" in the name
blanchet
parents:
49542
diff
changeset
|
57 |
val ctor_map_uniqueN: string |
49501 | 58 |
val ctor_recN: string |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
59 |
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
|
60 |
val ctor_relN: string |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
61 |
val ctor_set_inclN: string |
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
62 |
val ctor_set_set_inclN: string |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
63 |
val disc_unfoldN: string |
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
64 |
val disc_unfold_iffN: string |
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
65 |
val disc_corecN: string |
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
66 |
val disc_corec_iffN: string |
49501 | 67 |
val dtorN: string |
49582
557302525778
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
blanchet
parents:
49581
diff
changeset
|
68 |
val dtor_coinductN: string |
49501 | 69 |
val dtor_corecN: string |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
70 |
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
|
71 |
val dtor_ctorN: string |
49501 | 72 |
val dtor_exhaustN: string |
73 |
val dtor_injectN: string |
|
49545
8bb6e2d7346b
renamed coinduction principles to have "dtor" in the name
blanchet
parents:
49544
diff
changeset
|
74 |
val dtor_mapN: string |
49581
4e5bd3883429
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
blanchet
parents:
49545
diff
changeset
|
75 |
val dtor_map_coinductN: string |
4e5bd3883429
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
blanchet
parents:
49545
diff
changeset
|
76 |
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
|
77 |
val dtor_map_uniqueN: string |
49545
8bb6e2d7346b
renamed coinduction principles to have "dtor" in the name
blanchet
parents:
49544
diff
changeset
|
78 |
val dtor_relN: string |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
79 |
val dtor_set_inclN: string |
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
80 |
val dtor_set_set_inclN: string |
49582
557302525778
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
blanchet
parents:
49581
diff
changeset
|
81 |
val dtor_strong_coinductN: string |
49516
d4859efc1096
renamed "rel_simp" to "dtor_rel" and similarly for "srel"
blanchet
parents:
49510
diff
changeset
|
82 |
val dtor_unfoldN: string |
d4859efc1096
renamed "rel_simp" to "dtor_rel" and similarly for "srel"
blanchet
parents:
49510
diff
changeset
|
83 |
val dtor_unfold_uniqueN: string |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
84 |
val exhaustN: string |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
85 |
val foldN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
val hsetN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
val hset_recN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
88 |
val inductN: string |
49019 | 89 |
val injectN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
val isNodeN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
91 |
val lsbisN: string |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
92 |
val mapN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
93 |
val map_uniqueN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
94 |
val min_algN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
95 |
val morN: string |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
96 |
val nchotomyN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
97 |
val recN: string |
51918 | 98 |
val rel_coinductN: string |
99 |
val rel_inductN: string |
|
49592
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
100 |
val rel_injectN: string |
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
101 |
val rel_distinctN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
102 |
val rvN: string |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
103 |
val sel_corecN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
104 |
val set_inclN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
105 |
val set_set_inclN: string |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
106 |
val sel_unfoldN: string |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
107 |
val setsN: string |
49438 | 108 |
val simpsN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
109 |
val strTN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
110 |
val str_initN: string |
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
111 |
val strong_coinductN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
112 |
val sum_bdN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
113 |
val sum_bdTN: string |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
114 |
val unfoldN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
115 |
val uniqueN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
116 |
|
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
117 |
(* 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
|
118 |
val mk_ctor_setN: int -> string |
4339aa335355
use singular since there is always only one theorem
blanchet
parents:
49582
diff
changeset
|
119 |
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
|
120 |
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
|
121 |
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
|
122 |
|
52207
21026c312cc3
tuning -- avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52031
diff
changeset
|
123 |
val datatype_word: fp_kind -> string |
51863 | 124 |
|
51858
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
125 |
val base_name_of_typ: typ -> string |
49498 | 126 |
val mk_common_name: string list -> string |
49327
541d818d2ff3
put an underscore between names, for compatibility with old package (and also because it makes sense)
blanchet
parents:
49308
diff
changeset
|
127 |
|
51858
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
128 |
val variant_types: string list -> sort list -> Proof.context -> |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
129 |
(string * sort) list * Proof.context |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
130 |
val variant_tfrees: string list -> Proof.context -> typ list * Proof.context |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
131 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
132 |
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
|
133 |
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
|
134 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
135 |
val mk_sumTN: typ list -> typ |
49264 | 136 |
val mk_sumTN_balanced: typ list -> typ |
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
137 |
|
49368 | 138 |
val id_const: typ -> term |
139 |
||
49121 | 140 |
val Inl_const: typ -> typ -> term |
141 |
val Inr_const: typ -> typ -> term |
|
142 |
||
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
143 |
val mk_Inl: typ -> term -> term |
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
144 |
val mk_Inr: typ -> term -> term |
49121 | 145 |
val mk_InN: typ list -> term -> int -> term |
49264 | 146 |
val mk_InN_balanced: typ -> int -> term -> int -> term |
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
147 |
val mk_sum_case: term * term -> term |
49129 | 148 |
val mk_sum_caseN: term list -> term |
49264 | 149 |
val mk_sum_caseN_balanced: term list -> term |
49121 | 150 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
151 |
val dest_sumT: typ -> typ * typ |
49176 | 152 |
val dest_sumTN: int -> typ -> typ list |
49264 | 153 |
val dest_sumTN_balanced: int -> typ -> typ list |
49176 | 154 |
val dest_tupleT: int -> typ -> typ list |
155 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
156 |
val mk_Field: term -> term |
49275 | 157 |
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
|
158 |
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
|
159 |
|
49125 | 160 |
val mk_sumEN: int -> thm |
49264 | 161 |
val mk_sumEN_balanced: int -> thm |
49335 | 162 |
val mk_sumEN_tupled_balanced: int list -> thm |
49130
3c26e17b2849
implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset
|
163 |
val mk_sum_casesN: int -> int -> thm |
49264 | 164 |
val mk_sum_casesN_balanced: int -> int -> thm |
49125 | 165 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
166 |
val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
167 |
|
51867 | 168 |
val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list -> |
51868 | 169 |
BNF_Def.bnf list -> local_theory -> 'a) -> |
170 |
binding list -> (string * sort) list -> ((string * sort) * typ) list -> local_theory -> |
|
171 |
BNF_Def.bnf list * 'a |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
172 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
173 |
|
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
|
174 |
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
|
175 |
struct |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
176 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
177 |
open BNF_Comp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
178 |
open BNF_Def |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
179 |
open BNF_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
180 |
|
52207
21026c312cc3
tuning -- avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52031
diff
changeset
|
181 |
datatype fp_kind = Least_FP | Greatest_FP; |
21026c312cc3
tuning -- avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52031
diff
changeset
|
182 |
|
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
183 |
type fp_result = |
51859 | 184 |
{Ts: typ list, |
185 |
bnfs: BNF_Def.bnf list, |
|
51839 | 186 |
ctors: term list, |
51819 | 187 |
dtors: term list, |
52328 | 188 |
xtor_co_iterss: term list list, |
52312
f461dca57c66
tuned record field names to avoid confusion between low-level and high-level constants/theorems
blanchet
parents:
52207
diff
changeset
|
189 |
xtor_co_induct: thm, |
f461dca57c66
tuned record field names to avoid confusion between low-level and high-level constants/theorems
blanchet
parents:
52207
diff
changeset
|
190 |
xtor_strong_co_induct: thm, |
51819 | 191 |
dtor_ctors: thm list, |
192 |
ctor_dtors: thm list, |
|
193 |
ctor_injects: thm list, |
|
52314 | 194 |
xtor_map_thms: thm list, |
195 |
xtor_set_thmss: thm list list, |
|
196 |
xtor_rel_thms: thm list, |
|
52328 | 197 |
xtor_co_iter_thmss: thm list list}; |
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
198 |
|
52328 | 199 |
fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct, |
52314 | 200 |
xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, |
52328 | 201 |
xtor_rel_thms, xtor_co_iter_thmss} = |
51859 | 202 |
{Ts = map (Morphism.typ phi) Ts, |
203 |
bnfs = map (morph_bnf phi) bnfs, |
|
51839 | 204 |
ctors = map (Morphism.term phi) ctors, |
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
205 |
dtors = map (Morphism.term phi) dtors, |
52328 | 206 |
xtor_co_iterss = map (map (Morphism.term phi)) xtor_co_iterss, |
52312
f461dca57c66
tuned record field names to avoid confusion between low-level and high-level constants/theorems
blanchet
parents:
52207
diff
changeset
|
207 |
xtor_co_induct = Morphism.thm phi xtor_co_induct, |
f461dca57c66
tuned record field names to avoid confusion between low-level and high-level constants/theorems
blanchet
parents:
52207
diff
changeset
|
208 |
xtor_strong_co_induct = Morphism.thm phi xtor_strong_co_induct, |
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
209 |
dtor_ctors = map (Morphism.thm phi) dtor_ctors, |
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
210 |
ctor_dtors = map (Morphism.thm phi) ctor_dtors, |
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
211 |
ctor_injects = map (Morphism.thm phi) ctor_injects, |
52314 | 212 |
xtor_map_thms = map (Morphism.thm phi) xtor_map_thms, |
213 |
xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss, |
|
214 |
xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms, |
|
52328 | 215 |
xtor_co_iter_thmss = map (map (Morphism.thm phi)) xtor_co_iter_thmss}; |
51823
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
216 |
|
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
217 |
fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) = |
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
218 |
eq_list eq_bnf (bnfs1, bnfs2); |
38996458bc5c
create data structure for storing (co)datatype information
blanchet
parents:
51819
diff
changeset
|
219 |
|
52330 | 220 |
fun un_fold_of [f, _] = f; |
221 |
fun co_rec_of [_, r] = r; |
|
222 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
223 |
val timing = true; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
224 |
fun time timer msg = (if timing |
52031
9a9238342963
tuning -- renamed '_from_' to '_of_' in Sledgehammer
blanchet
parents:
51918
diff
changeset
|
225 |
then warning (msg ^ ": " ^ ATP_Util.string_of_time (Timer.checkRealTimer timer)) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
226 |
else (); Timer.startRealTimer ()); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
227 |
|
49223 | 228 |
val preN = "pre_" |
229 |
val rawN = "raw_" |
|
49218 | 230 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
231 |
val coN = "co" |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
232 |
val unN = "un" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
233 |
val algN = "alg" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
234 |
val IITN = "IITN" |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
235 |
val foldN = "fold" |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
236 |
val unfoldN = unN ^ foldN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
237 |
val uniqueN = "_unique" |
49438 | 238 |
val simpsN = "simps" |
49501 | 239 |
val ctorN = "ctor" |
240 |
val dtorN = "dtor" |
|
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
241 |
val ctor_foldN = ctorN ^ "_" ^ foldN |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
242 |
val dtor_unfoldN = dtorN ^ "_" ^ unfoldN |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
243 |
val ctor_fold_uniqueN = ctor_foldN ^ uniqueN |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49502
diff
changeset
|
244 |
val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
245 |
val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN |
49541 | 246 |
val ctor_mapN = ctorN ^ "_" ^ mapN |
247 |
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
|
248 |
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
|
249 |
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
|
250 |
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
|
251 |
val min_algN = "min_alg" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
252 |
val morN = "mor" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
253 |
val bisN = "bis" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
254 |
val lsbisN = "lsbis" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
255 |
val sum_bdTN = "sbdT" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
256 |
val sum_bdN = "sbd" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
257 |
val carTN = "carT" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
258 |
val strTN = "strT" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
259 |
val isNodeN = "isNode" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
260 |
val LevN = "Lev" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
261 |
val rvN = "recover" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
262 |
val behN = "beh" |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
263 |
val setsN = "sets" |
49584
4339aa335355
use singular since there is always only one theorem
blanchet
parents:
49582
diff
changeset
|
264 |
val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN |
4339aa335355
use singular since there is always only one theorem
blanchet
parents:
49582
diff
changeset
|
265 |
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
|
266 |
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
|
267 |
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
|
268 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
269 |
val str_initN = "str_init" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
270 |
val recN = "rec" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
271 |
val corecN = coN ^ recN |
49501 | 272 |
val ctor_recN = ctorN ^ "_" ^ recN |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
273 |
val ctor_rec_uniqueN = ctor_recN ^ uniqueN |
49501 | 274 |
val dtor_corecN = dtorN ^ "_" ^ corecN |
51739
3514b90d0a8b
(co)rec is (just as the (un)fold) the unique morphism;
traytel
parents:
49635
diff
changeset
|
275 |
val dtor_corec_uniqueN = dtor_corecN ^ uniqueN |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
276 |
val ctor_dtor_corecN = ctorN ^ "_" ^ dtor_corecN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
277 |
|
49501 | 278 |
val ctor_dtorN = ctorN ^ "_" ^ dtorN |
279 |
val dtor_ctorN = dtorN ^ "_" ^ ctorN |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
280 |
val nchotomyN = "nchotomy" |
49019 | 281 |
val injectN = "inject" |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
282 |
val exhaustN = "exhaust" |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
283 |
val ctor_injectN = ctorN ^ "_" ^ injectN |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
284 |
val ctor_exhaustN = ctorN ^ "_" ^ exhaustN |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
285 |
val dtor_injectN = dtorN ^ "_" ^ injectN |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49584
diff
changeset
|
286 |
val dtor_exhaustN = dtorN ^ "_" ^ exhaustN |
49545
8bb6e2d7346b
renamed coinduction principles to have "dtor" in the name
blanchet
parents:
49544
diff
changeset
|
287 |
val ctor_relN = ctorN ^ "_" ^ relN |
8bb6e2d7346b
renamed coinduction principles to have "dtor" in the name
blanchet
parents:
49544
diff
changeset
|
288 |
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
|
289 |
val inductN = "induct" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
290 |
val coinductN = coN ^ inductN |
49501 | 291 |
val ctor_inductN = ctorN ^ "_" ^ inductN |
292 |
val ctor_induct2N = ctor_inductN ^ "2" |
|
49581
4e5bd3883429
renamed "dtor_coinduct" etc. to "dtor_map_coinduct"
blanchet
parents:
49545
diff
changeset
|
293 |
val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN |
49582
557302525778
renamed "dtor_rel_coinduct" etc. to "dtor_coinduct"
blanchet
parents:
49581
diff
changeset
|
294 |
val dtor_coinductN = dtorN ^ "_" ^ coinductN |
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
295 |
val strong_coinductN = "strong_" ^ coinductN |
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
296 |
val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN |
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
297 |
val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
298 |
val hsetN = "Hset" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
299 |
val hset_recN = hsetN ^ "_rec" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
300 |
val set_inclN = "set_incl" |
49544
24094fa47e0d
renamed "set_incl" etc. to have "ctor" or "dtor" in the name
blanchet
parents:
49543
diff
changeset
|
301 |
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
|
302 |
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
|
303 |
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
|
304 |
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
|
305 |
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
|
306 |
|
49338 | 307 |
val caseN = "case" |
49342 | 308 |
val discN = "disc" |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
309 |
val disc_unfoldN = discN ^ "_" ^ unfoldN |
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
310 |
val disc_corecN = discN ^ "_" ^ corecN |
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
311 |
val iffN = "_iff" |
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
312 |
val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN |
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
313 |
val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN |
49592
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
314 |
val distinctN = "distinct" |
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
315 |
val rel_distinctN = relN ^ "_" ^ distinctN |
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
316 |
val injectN = "inject" |
b859a02c1150
fixed "rels" + split them into injectivity and distinctness
blanchet
parents:
49591
diff
changeset
|
317 |
val rel_injectN = relN ^ "_" ^ injectN |
51918 | 318 |
val rel_coinductN = relN ^ "_" ^ coinductN |
319 |
val rel_inductN = relN ^ "_" ^ inductN |
|
49342 | 320 |
val selN = "sel" |
49594
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
321 |
val sel_unfoldN = selN ^ "_" ^ unfoldN |
55e798614c45
tweaked theorem names (in particular, dropped s's)
blanchet
parents:
49592
diff
changeset
|
322 |
val sel_corecN = selN ^ "_" ^ corecN |
49338 | 323 |
|
52207
21026c312cc3
tuning -- avoided unreadable true/false all over the place for LFP/GFP
blanchet
parents:
52031
diff
changeset
|
324 |
fun datatype_word fp = (if fp = Greatest_FP then "co" else "") ^ "datatype"; |
51863 | 325 |
|
51858
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
326 |
fun add_components_of_typ (Type (s, Ts)) = |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
327 |
fold add_components_of_typ Ts #> cons (Long_Name.base_name s) |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
328 |
| add_components_of_typ _ = I; |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
329 |
|
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
330 |
fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []); |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
331 |
|
49498 | 332 |
val mk_common_name = space_implode "_"; |
49327
541d818d2ff3
put an underscore between names, for compatibility with old package (and also because it makes sense)
blanchet
parents:
49308
diff
changeset
|
333 |
|
49264 | 334 |
fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T'); |
335 |
||
336 |
fun dest_sumTN 1 T = [T] |
|
337 |
| dest_sumTN n (Type (@{type_name sum}, [T, T'])) = T :: dest_sumTN (n - 1) T'; |
|
338 |
||
339 |
val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT; |
|
340 |
||
341 |
(* TODO: move something like this to "HOLogic"? *) |
|
342 |
fun dest_tupleT 0 @{typ unit} = [] |
|
343 |
| dest_tupleT 1 T = [T] |
|
344 |
| dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T'; |
|
345 |
||
346 |
val mk_sumTN = Library.foldr1 mk_sumT; |
|
347 |
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
|
348 |
|
49368 | 349 |
fun id_const T = Const (@{const_name id}, T --> T); |
350 |
||
49121 | 351 |
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
|
352 |
fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t; |
49121 | 353 |
|
354 |
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
|
355 |
fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t; |
49121 | 356 |
|
357 |
fun mk_InN [_] t 1 = t |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
358 |
| mk_InN (_ :: Ts) t 1 = mk_Inl (mk_sumTN Ts) t |
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
359 |
| mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1)) |
49121 | 360 |
| mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t])); |
361 |
||
49264 | 362 |
fun mk_InN_balanced sum_T n t k = |
363 |
let |
|
364 |
fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t |
|
365 |
| repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t |
|
366 |
| repair_types _ t = t |
|
367 |
and repair_inj_types T s get t = |
|
368 |
let val T' = get (dest_sumT T) in |
|
369 |
Const (s, T' --> T) $ repair_types T' t |
|
370 |
end; |
|
371 |
in |
|
372 |
Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k |
|
373 |
|> repair_types sum_T |
|
374 |
end; |
|
375 |
||
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
376 |
fun mk_sum_case (f, g) = |
49129 | 377 |
let |
378 |
val fT = fastype_of f; |
|
379 |
val gT = fastype_of g; |
|
380 |
in |
|
381 |
Const (@{const_name sum_case}, |
|
382 |
fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g |
|
383 |
end; |
|
384 |
||
49264 | 385 |
val mk_sum_caseN = Library.foldr1 mk_sum_case; |
386 |
val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case; |
|
49176 | 387 |
|
49275 | 388 |
fun mk_If p t f = |
389 |
let val T = fastype_of t; |
|
390 |
in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end; |
|
391 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
392 |
fun mk_Field r = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
393 |
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
|
394 |
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
|
395 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
396 |
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
|
397 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
398 |
(*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
|
399 |
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
|
400 |
|
51858
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
401 |
fun variant_types ss Ss ctxt = |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
402 |
let |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
403 |
val (tfrees, _) = |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
404 |
fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt); |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
405 |
val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt; |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
406 |
in (tfrees, ctxt') end; |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
407 |
|
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
408 |
fun variant_tfrees ss = |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
409 |
apfst (map TFree) o variant_types (map (prefix "'") ss) (replicate (length ss) HOLogic.typeS); |
7a08fe1e19b1
added and moved library functions (used in primrec code)
blanchet
parents:
51850
diff
changeset
|
410 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
411 |
(* 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
|
412 |
fun split_conj_thm th = |
49119 | 413 |
((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
|
414 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
415 |
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
|
416 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
417 |
fun split n i th = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
418 |
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
|
419 |
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
|
420 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
421 |
fun mk_sumEN 1 = @{thm one_pointE} |
49240 | 422 |
| mk_sumEN 2 = @{thm sumE} |
423 |
| mk_sumEN n = |
|
424 |
(fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF |
|
425 |
replicate n (impI RS allI); |
|
49125 | 426 |
|
49335 | 427 |
fun mk_obj_sumEN_balanced n = |
428 |
Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f}))) |
|
429 |
(replicate n asm_rl); |
|
430 |
||
431 |
fun mk_sumEN_balanced' n all_impIs = mk_obj_sumEN_balanced n OF all_impIs RS @{thm obj_one_pointE}; |
|
432 |
||
433 |
fun mk_sumEN_balanced 1 = @{thm one_pointE} (*optimization*) |
|
49264 | 434 |
| mk_sumEN_balanced 2 = @{thm sumE} (*optimization*) |
49335 | 435 |
| mk_sumEN_balanced n = mk_sumEN_balanced' n (replicate n (impI RS allI)); |
436 |
||
437 |
fun mk_tupled_allIN 0 = @{thm unit_all_impI} |
|
438 |
| mk_tupled_allIN 1 = @{thm impI[THEN allI]} |
|
439 |
| mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*) |
|
440 |
| mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step}; |
|
441 |
||
442 |
fun mk_sumEN_tupled_balanced ms = |
|
443 |
let val n = length ms in |
|
444 |
if forall (curry (op =) 1) ms then mk_sumEN_balanced n |
|
445 |
else mk_sumEN_balanced' n (map mk_tupled_allIN ms) |
|
446 |
end; |
|
49264 | 447 |
|
448 |
fun mk_sum_casesN 1 1 = refl |
|
49130
3c26e17b2849
implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset
|
449 |
| mk_sum_casesN _ 1 = @{thm sum.cases(1)} |
3c26e17b2849
implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset
|
450 |
| mk_sum_casesN 2 2 = @{thm sum.cases(2)} |
49264 | 451 |
| mk_sum_casesN n k = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (k - 1)]; |
452 |
||
453 |
fun mk_sum_step base step thm = |
|
454 |
if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm]; |
|
455 |
||
456 |
fun mk_sum_casesN_balanced 1 1 = refl |
|
457 |
| mk_sum_casesN_balanced n k = |
|
458 |
Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)}, |
|
459 |
right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k; |
|
49130
3c26e17b2849
implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset
|
460 |
|
51868 | 461 |
fun fp_bnf construct_fp bs resBs eqs lthy = |
462 |
let |
|
463 |
val timer = time (Timer.startRealTimer ()); |
|
464 |
val (lhss, rhss) = split_list eqs; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
465 |
|
51868 | 466 |
(* FIXME: because of "@ lhss", the output could contain type variables that are not in the |
467 |
input; also, "fp_sort" should put the "resBs" first and in the order in which they appear *) |
|
468 |
fun fp_sort Ass = |
|
469 |
subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ lhss; |
|
470 |
||
471 |
fun raw_qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b)); |
|
472 |
||
473 |
val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list) |
|
474 |
(fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort) bs rhss |
|
475 |
(empty_unfolds, lthy)); |
|
476 |
||
49498 | 477 |
val name = mk_common_name (map Binding.name_of bs); |
49425 | 478 |
fun qualify i = |
479 |
let val namei = name ^ nonzero_string_of_int i; |
|
480 |
in Binding.qualify true namei end; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
481 |
|
49132 | 482 |
val Ass = map (map dest_TFree) livess; |
51866 | 483 |
val resDs = fold (subtract (op =)) Ass resBs; |
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
484 |
val Ds = fold (fold Term.add_tfreesT) deadss []; |
49132 | 485 |
|
49156 | 486 |
val _ = (case Library.inter (op =) Ds lhss of [] => () |
49591
91b228e26348
generate high-level "coinduct" and "strong_coinduct" properties
blanchet
parents:
49589
diff
changeset
|
487 |
| A :: _ => error ("Inadmissible type recursion (cannot take fixed point of dead type \ |
49132 | 488 |
\variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")")); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
489 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
490 |
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
|
491 |
|
49502 | 492 |
val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) = |
51868 | 493 |
normalize_bnfs qualify Ass Ds fp_sort bnfs unfold_set lthy; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
494 |
|
49132 | 495 |
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
|
496 |
|
51865 | 497 |
val ((pre_bnfs, deadss), lthy'') = |
49502 | 498 |
fold_map3 (seal_bnf unfold_set') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy' |
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
499 |
|>> split_list; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
500 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
501 |
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
|
502 |
|
51867 | 503 |
val res = construct_fp bs resBs (map TFree resDs, deadss) pre_bnfs lthy''; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
504 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
505 |
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
|
506 |
in |
51865 | 507 |
timer; (pre_bnfs, res) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
508 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
509 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
510 |
end; |