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