author | blanchet |
Tue, 18 Sep 2012 11:42:22 +0200 | |
changeset 49438 | 5bc80d96241e |
parent 49425 | f27f83f71e94 |
child 49456 | fa8302c8dea1 |
permissions | -rw-r--r-- |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Codatatype/Tools/bnf_fp_util.ML |
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 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
|
49389 | 5 |
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
|
6 |
*) |
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 |
signature BNF_FP_UTIL = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
sig |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
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
|
11 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
val IITN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
val LevN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
val algN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
15 |
val behN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
val bisN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
17 |
val carTN: string |
49338 | 18 |
val caseN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
19 |
val coN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
20 |
val coinductN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
21 |
val coiterN: string |
49338 | 22 |
val coitersN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
23 |
val corecN: string |
49338 | 24 |
val corecsN: string |
25 |
val disc_coitersN: string |
|
26 |
val disc_corecsN: string |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
27 |
val exhaustN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
val fldN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
29 |
val fld_exhaustN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
val fld_induct2N: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
val fld_inductN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
val fld_injectN: string |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
33 |
val fld_iterN: string |
49338 | 34 |
val fld_iter_uniqueN: string |
49222
cbe8c859817c
for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
blanchet
parents:
49218
diff
changeset
|
35 |
val fld_itersN: string |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
36 |
val fld_recN: string |
49222
cbe8c859817c
for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
blanchet
parents:
49218
diff
changeset
|
37 |
val fld_recsN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
38 |
val fld_unfN: string |
49231 | 39 |
val fld_unf_coitersN: string |
40 |
val fld_unf_corecsN: string |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
41 |
val hsetN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
42 |
val hset_recN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
val inductN: string |
49019 | 44 |
val injectN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
45 |
val isNodeN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
val iterN: string |
49338 | 47 |
val itersN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
val lsbisN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
49 |
val map_simpsN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
50 |
val map_uniqueN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
51 |
val min_algN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
val morN: string |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
53 |
val nchotomyN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
54 |
val pred_coinductN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
val pred_coinduct_uptoN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
val recN: string |
49338 | 57 |
val recsN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
58 |
val rel_coinductN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
59 |
val rel_coinduct_uptoN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
60 |
val rvN: string |
49338 | 61 |
val sel_coitersN: string |
62 |
val sel_corecsN: string |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
63 |
val set_inclN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
val set_set_inclN: string |
49438 | 65 |
val simpsN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
66 |
val strTN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
67 |
val str_initN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
val sum_bdN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
69 |
val sum_bdTN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
70 |
val unfN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
val unf_coinductN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
72 |
val unf_coinduct_uptoN: string |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
73 |
val unf_coiterN: string |
49338 | 74 |
val unf_coiter_uniqueN: string |
49222
cbe8c859817c
for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
blanchet
parents:
49218
diff
changeset
|
75 |
val unf_coitersN: string |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
76 |
val unf_corecN: string |
49222
cbe8c859817c
for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
blanchet
parents:
49218
diff
changeset
|
77 |
val unf_corecsN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
78 |
val unf_exhaustN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
val unf_fldN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
80 |
val unf_injectN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
81 |
val uniqueN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
val uptoN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
83 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
84 |
val mk_exhaustN: string -> string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
85 |
val mk_injectN: string -> string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
val mk_nchotomyN: string -> string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
val mk_set_simpsN: int -> string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
88 |
val mk_set_minimalN: int -> string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
89 |
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
|
90 |
|
49337 | 91 |
val mk_common_name: binding 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
|
92 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
93 |
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
|
94 |
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
|
95 |
|
49330
276ff43ee0b1
reuse generated names (they look better + slightly more efficient)
blanchet
parents:
49327
diff
changeset
|
96 |
val retype_free: typ -> term -> term |
276ff43ee0b1
reuse generated names (they look better + slightly more efficient)
blanchet
parents:
49327
diff
changeset
|
97 |
|
276ff43ee0b1
reuse generated names (they look better + slightly more efficient)
blanchet
parents:
49327
diff
changeset
|
98 |
val mk_predT: typ -> typ; |
276ff43ee0b1
reuse generated names (they look better + slightly more efficient)
blanchet
parents:
49327
diff
changeset
|
99 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
100 |
val mk_sumTN: typ list -> typ |
49264 | 101 |
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
|
102 |
|
49368 | 103 |
val id_const: typ -> term |
104 |
val id_abs: typ -> term |
|
105 |
||
49121 | 106 |
val Inl_const: typ -> typ -> term |
107 |
val Inr_const: typ -> typ -> term |
|
108 |
||
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
109 |
val mk_Inl: typ -> term -> term |
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
110 |
val mk_Inr: typ -> term -> term |
49121 | 111 |
val mk_InN: typ list -> term -> int -> term |
49264 | 112 |
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
|
113 |
val mk_sum_case: term * term -> term |
49129 | 114 |
val mk_sum_caseN: term list -> term |
49264 | 115 |
val mk_sum_caseN_balanced: term list -> term |
49121 | 116 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
117 |
val dest_sumT: typ -> typ * typ |
49176 | 118 |
val dest_sumTN: int -> typ -> typ list |
49264 | 119 |
val dest_sumTN_balanced: int -> typ -> typ list |
49176 | 120 |
val dest_tupleT: int -> typ -> typ list |
121 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
122 |
val mk_Field: term -> term |
49275 | 123 |
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
|
124 |
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
|
125 |
|
49125 | 126 |
val mk_sumEN: int -> thm |
49264 | 127 |
val mk_sumEN_balanced: int -> thm |
49335 | 128 |
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
|
129 |
val mk_sum_casesN: int -> int -> thm |
49264 | 130 |
val mk_sum_casesN_balanced: int -> int -> thm |
49125 | 131 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
132 |
val mk_tactics: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
133 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
134 |
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
|
135 |
|
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
136 |
val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> |
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
137 |
typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) -> |
49169 | 138 |
binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list -> |
49226 | 139 |
local_theory -> BNF_Def.BNF list * 'a |
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
140 |
val fp_bnf_cmd: (mixfix list -> (string * sort) list option -> binding list -> |
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
141 |
typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) -> |
49134
846264f80f16
optionally provide extra dead variables to the FP constructions
blanchet
parents:
49132
diff
changeset
|
142 |
binding list * (string list * string list) -> local_theory -> 'a |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
143 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
144 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
145 |
structure BNF_FP_Util : BNF_FP_UTIL = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
146 |
struct |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
147 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
148 |
open BNF_Comp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
149 |
open BNF_Def |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
150 |
open BNF_Util |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
151 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
152 |
val timing = true; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
153 |
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
|
154 |
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
|
155 |
else (); Timer.startRealTimer ()); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
156 |
|
49223 | 157 |
val preN = "pre_" |
158 |
val rawN = "raw_" |
|
49218 | 159 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
160 |
val coN = "co" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
161 |
val algN = "alg" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
162 |
val IITN = "IITN" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
163 |
val iterN = "iter" |
49342 | 164 |
val itersN = iterN ^ "s" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
165 |
val coiterN = coN ^ iterN |
49342 | 166 |
val coitersN = coiterN ^ "s" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
167 |
val uniqueN = "_unique" |
49438 | 168 |
val simpsN = "simps" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
169 |
val fldN = "fld" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
170 |
val unfN = "unf" |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
171 |
val fld_iterN = fldN ^ "_" ^ iterN |
49222
cbe8c859817c
for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
blanchet
parents:
49218
diff
changeset
|
172 |
val fld_itersN = fld_iterN ^ "s" |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
173 |
val unf_coiterN = unfN ^ "_" ^ coiterN |
49222
cbe8c859817c
for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
blanchet
parents:
49218
diff
changeset
|
174 |
val unf_coitersN = unf_coiterN ^ "s" |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
175 |
val fld_iter_uniqueN = fld_iterN ^ uniqueN |
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
176 |
val unf_coiter_uniqueN = unf_coiterN ^ uniqueN |
49225 | 177 |
val fld_unf_coitersN = fldN ^ "_" ^ unf_coiterN ^ "s" |
49438 | 178 |
val map_simpsN = mapN ^ "_" ^ simpsN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
179 |
val map_uniqueN = mapN ^ uniqueN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
180 |
val min_algN = "min_alg" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
181 |
val morN = "mor" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
182 |
val bisN = "bis" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
183 |
val lsbisN = "lsbis" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
184 |
val sum_bdTN = "sbdT" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
185 |
val sum_bdN = "sbd" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
186 |
val carTN = "carT" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
187 |
val strTN = "strT" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
188 |
val isNodeN = "isNode" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
189 |
val LevN = "Lev" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
190 |
val rvN = "recover" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
191 |
val behN = "beh" |
49438 | 192 |
fun mk_set_simpsN i = mk_setN i ^ "_" ^ simpsN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
193 |
fun mk_set_minimalN i = mk_setN i ^ "_minimal" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
194 |
fun mk_set_inductN i = mk_setN i ^ "_induct" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
195 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
196 |
val str_initN = "str_init" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
197 |
val recN = "rec" |
49342 | 198 |
val recsN = recN ^ "s" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
199 |
val corecN = coN ^ recN |
49342 | 200 |
val corecsN = corecN ^ "s" |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
201 |
val fld_recN = fldN ^ "_" ^ recN |
49222
cbe8c859817c
for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
blanchet
parents:
49218
diff
changeset
|
202 |
val fld_recsN = fld_recN ^ "s" |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
203 |
val unf_corecN = unfN ^ "_" ^ corecN |
49222
cbe8c859817c
for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
blanchet
parents:
49218
diff
changeset
|
204 |
val unf_corecsN = unf_corecN ^ "s" |
49231 | 205 |
val fld_unf_corecsN = fldN ^ "_" ^ unf_corecN ^ "s" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
206 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
207 |
val fld_unfN = fldN ^ "_" ^ unfN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
208 |
val unf_fldN = unfN ^ "_" ^ fldN |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
209 |
val nchotomyN = "nchotomy" |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
210 |
fun mk_nchotomyN s = s ^ "_" ^ nchotomyN |
49019 | 211 |
val injectN = "inject" |
212 |
fun mk_injectN s = s ^ "_" ^ injectN |
|
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
213 |
val exhaustN = "exhaust" |
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
214 |
fun mk_exhaustN s = s ^ "_" ^ exhaustN |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
215 |
val fld_injectN = mk_injectN fldN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
216 |
val fld_exhaustN = mk_exhaustN fldN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
217 |
val unf_injectN = mk_injectN unfN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
218 |
val unf_exhaustN = mk_exhaustN unfN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
219 |
val inductN = "induct" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
220 |
val coinductN = coN ^ inductN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
221 |
val fld_inductN = fldN ^ "_" ^ inductN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
222 |
val fld_induct2N = fld_inductN ^ "2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
223 |
val unf_coinductN = unfN ^ "_" ^ coinductN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
224 |
val rel_coinductN = relN ^ "_" ^ coinductN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
225 |
val pred_coinductN = predN ^ "_" ^ coinductN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
226 |
val uptoN = "upto" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
227 |
val unf_coinduct_uptoN = unf_coinductN ^ "_" ^ uptoN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
228 |
val rel_coinduct_uptoN = rel_coinductN ^ "_" ^ uptoN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
229 |
val pred_coinduct_uptoN = pred_coinductN ^ "_" ^ uptoN |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
230 |
val hsetN = "Hset" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
231 |
val hset_recN = hsetN ^ "_rec" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
232 |
val set_inclN = "set_incl" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
233 |
val set_set_inclN = "set_set_incl" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
234 |
|
49338 | 235 |
val caseN = "case" |
49342 | 236 |
val discN = "disc" |
237 |
val disc_coitersN = discN ^ "_" ^ coitersN |
|
238 |
val disc_corecsN = discN ^ "_" ^ corecsN |
|
239 |
val selN = "sel" |
|
240 |
val sel_coitersN = selN ^ "_" ^ coitersN |
|
241 |
val sel_corecsN = selN ^ "_" ^ corecsN |
|
49338 | 242 |
|
49337 | 243 |
val mk_common_name = space_implode "_" o map Binding.name_of; |
49327
541d818d2ff3
put an underscore between names, for compatibility with old package (and also because it makes sense)
blanchet
parents:
49308
diff
changeset
|
244 |
|
49330
276ff43ee0b1
reuse generated names (they look better + slightly more efficient)
blanchet
parents:
49327
diff
changeset
|
245 |
fun mk_predT T = T --> HOLogic.boolT; |
276ff43ee0b1
reuse generated names (they look better + slightly more efficient)
blanchet
parents:
49327
diff
changeset
|
246 |
|
276ff43ee0b1
reuse generated names (they look better + slightly more efficient)
blanchet
parents:
49327
diff
changeset
|
247 |
fun retype_free T (Free (s, _)) = Free (s, T); |
276ff43ee0b1
reuse generated names (they look better + slightly more efficient)
blanchet
parents:
49327
diff
changeset
|
248 |
|
49264 | 249 |
fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T'); |
250 |
||
251 |
fun dest_sumTN 1 T = [T] |
|
252 |
| dest_sumTN n (Type (@{type_name sum}, [T, T'])) = T :: dest_sumTN (n - 1) T'; |
|
253 |
||
254 |
val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT; |
|
255 |
||
256 |
(* TODO: move something like this to "HOLogic"? *) |
|
257 |
fun dest_tupleT 0 @{typ unit} = [] |
|
258 |
| dest_tupleT 1 T = [T] |
|
259 |
| dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T'; |
|
260 |
||
261 |
val mk_sumTN = Library.foldr1 mk_sumT; |
|
262 |
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
|
263 |
|
49368 | 264 |
fun id_const T = Const (@{const_name id}, T --> T); |
265 |
fun id_abs T = Abs (Name.uu, T, Bound 0); |
|
266 |
||
49121 | 267 |
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
|
268 |
fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t; |
49121 | 269 |
|
270 |
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
|
271 |
fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t; |
49121 | 272 |
|
273 |
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
|
274 |
| 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
|
275 |
| mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1)) |
49121 | 276 |
| mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t])); |
277 |
||
49264 | 278 |
fun mk_InN_balanced sum_T n t k = |
279 |
let |
|
280 |
fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t |
|
281 |
| repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t |
|
282 |
| repair_types _ t = t |
|
283 |
and repair_inj_types T s get t = |
|
284 |
let val T' = get (dest_sumT T) in |
|
285 |
Const (s, T' --> T) $ repair_types T' t |
|
286 |
end; |
|
287 |
in |
|
288 |
Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k |
|
289 |
|> repair_types sum_T |
|
290 |
end; |
|
291 |
||
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
292 |
fun mk_sum_case (f, g) = |
49129 | 293 |
let |
294 |
val fT = fastype_of f; |
|
295 |
val gT = fastype_of g; |
|
296 |
in |
|
297 |
Const (@{const_name sum_case}, |
|
298 |
fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g |
|
299 |
end; |
|
300 |
||
49264 | 301 |
val mk_sum_caseN = Library.foldr1 mk_sum_case; |
302 |
val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case; |
|
49176 | 303 |
|
49275 | 304 |
fun mk_If p t f = |
305 |
let val T = fastype_of t; |
|
306 |
in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end; |
|
307 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
308 |
fun mk_Field r = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
309 |
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
|
310 |
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
|
311 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
312 |
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
|
313 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
314 |
(*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
|
315 |
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
|
316 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
317 |
(* 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
|
318 |
fun split_conj_thm th = |
49119 | 319 |
((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
|
320 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
321 |
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
|
322 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
323 |
fun split n i th = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
324 |
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
|
325 |
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
|
326 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
327 |
fun mk_sumEN 1 = @{thm one_pointE} |
49240 | 328 |
| mk_sumEN 2 = @{thm sumE} |
329 |
| mk_sumEN n = |
|
330 |
(fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF |
|
331 |
replicate n (impI RS allI); |
|
49125 | 332 |
|
49335 | 333 |
fun mk_obj_sumEN_balanced n = |
334 |
Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f}))) |
|
335 |
(replicate n asm_rl); |
|
336 |
||
337 |
fun mk_sumEN_balanced' n all_impIs = mk_obj_sumEN_balanced n OF all_impIs RS @{thm obj_one_pointE}; |
|
338 |
||
339 |
fun mk_sumEN_balanced 1 = @{thm one_pointE} (*optimization*) |
|
49264 | 340 |
| mk_sumEN_balanced 2 = @{thm sumE} (*optimization*) |
49335 | 341 |
| mk_sumEN_balanced n = mk_sumEN_balanced' n (replicate n (impI RS allI)); |
342 |
||
343 |
fun mk_tupled_allIN 0 = @{thm unit_all_impI} |
|
344 |
| mk_tupled_allIN 1 = @{thm impI[THEN allI]} |
|
345 |
| mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*) |
|
346 |
| mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step}; |
|
347 |
||
348 |
fun mk_sumEN_tupled_balanced ms = |
|
349 |
let val n = length ms in |
|
350 |
if forall (curry (op =) 1) ms then mk_sumEN_balanced n |
|
351 |
else mk_sumEN_balanced' n (map mk_tupled_allIN ms) |
|
352 |
end; |
|
49264 | 353 |
|
354 |
fun mk_sum_casesN 1 1 = refl |
|
49130
3c26e17b2849
implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset
|
355 |
| mk_sum_casesN _ 1 = @{thm sum.cases(1)} |
3c26e17b2849
implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset
|
356 |
| mk_sum_casesN 2 2 = @{thm sum.cases(2)} |
49264 | 357 |
| mk_sum_casesN n k = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (k - 1)]; |
358 |
||
359 |
fun mk_sum_step base step thm = |
|
360 |
if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm]; |
|
361 |
||
362 |
fun mk_sum_casesN_balanced 1 1 = refl |
|
363 |
| mk_sum_casesN_balanced n k = |
|
364 |
Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)}, |
|
365 |
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
|
366 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
367 |
fun mk_tactics mid mcomp mcong snat bdco bdinf sbd inbd wpull = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
368 |
[mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
369 |
|
49141 | 370 |
(* FIXME: because of "@ lhss", the output could contain type variables that are not in the input; |
371 |
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
|
372 |
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
|
373 |
(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
|
374 |
| 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
|
375 |
(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
|
376 |
|
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
377 |
fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
378 |
let |
49337 | 379 |
val name = mk_common_name bs; |
49425 | 380 |
fun qualify i = |
381 |
let val namei = name ^ nonzero_string_of_int i; |
|
382 |
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
|
383 |
|
49132 | 384 |
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
|
385 |
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
|
386 |
val Ds = fold (fold Term.add_tfreesT) deadss []; |
49132 | 387 |
|
49156 | 388 |
val _ = (case Library.inter (op =) Ds lhss of [] => () |
49132 | 389 |
| A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \ |
390 |
\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
|
391 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
392 |
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
|
393 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
394 |
val ((kill_poss, _), (bnfs', (unfold', lthy'))) = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
395 |
normalize_bnfs qualify Ass Ds sort bnfs unfold lthy; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
396 |
|
49132 | 397 |
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
|
398 |
|
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
399 |
val ((bnfs'', deadss), lthy'') = |
49223 | 400 |
fold_map3 (seal_bnf unfold') (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
|
401 |
|>> split_list; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
402 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
403 |
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
|
404 |
|
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
405 |
val res = construct resBs bs (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
|
406 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
407 |
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
|
408 |
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
|
409 |
timer; (bnfs'', res) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
410 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
411 |
|
49169 | 412 |
fun fp_bnf construct bs mixfixes resBs eqs lthy = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
413 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
414 |
val timer = time (Timer.startRealTimer ()); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
415 |
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
|
416 |
val sort = fp_sort lhss (SOME resBs); |
49425 | 417 |
fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b)); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
418 |
val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list) |
49425 | 419 |
(fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
420 |
(empty_unfold, lthy)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
421 |
in |
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
422 |
mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy' |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
423 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
424 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
425 |
fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
426 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
427 |
val timer = time (Timer.startRealTimer ()); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
428 |
val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss; |
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
429 |
val sort = fp_sort lhss NONE; |
49425 | 430 |
fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b)); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
431 |
val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
432 |
(fold_map2 (fn b => fn rawT => |
49425 | 433 |
(bnf_of_typ Smart_Inline (qualify b) sort (Syntax.read_typ lthy rawT))) |
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
434 |
bs raw_bnfs (empty_unfold, lthy)); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
435 |
in |
49207 | 436 |
snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy') |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
437 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
438 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
439 |
end; |