author | blanchet |
Thu, 20 Sep 2012 17:35:49 +0200 | |
changeset 49484 | 0194a18f80cf |
parent 49482 | e6d6869eed08 |
child 49498 | acc583e14167 |
permissions | -rw-r--r-- |
49457 | 1 |
(* Title: HOL/Codatatype/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 |
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 |
|
49457 | 8 |
signature BNF_FP = |
48975
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 |
49484 | 25 |
val disc_coiter_iffN: string |
49338 | 26 |
val disc_coitersN: string |
49484 | 27 |
val disc_corec_iffN: string |
49338 | 28 |
val disc_corecsN: string |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
29 |
val exhaustN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
val fldN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
val fld_exhaustN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
val fld_induct2N: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
33 |
val fld_inductN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
34 |
val fld_injectN: string |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
35 |
val fld_iterN: string |
49338 | 36 |
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
|
37 |
val fld_itersN: string |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
38 |
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
|
39 |
val fld_recsN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
40 |
val fld_unfN: string |
49231 | 41 |
val fld_unf_coitersN: string |
42 |
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
|
43 |
val hsetN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
44 |
val hset_recN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
45 |
val inductN: string |
49019 | 46 |
val injectN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
47 |
val isNodeN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
val iterN: string |
49338 | 49 |
val itersN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
50 |
val lsbisN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
51 |
val map_simpsN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
val map_uniqueN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
53 |
val min_algN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
54 |
val morN: string |
49020
f379cf5d71bd
more work on BNF sugar -- up to derivation of nchotomy
blanchet
parents:
49019
diff
changeset
|
55 |
val nchotomyN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
val pred_coinductN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
val pred_coinduct_uptoN: string |
49456 | 58 |
val pred_simpN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
59 |
val recN: string |
49338 | 60 |
val recsN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
61 |
val rel_coinductN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
62 |
val rel_coinduct_uptoN: string |
49456 | 63 |
val rel_simpN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
val rvN: string |
49338 | 65 |
val sel_coitersN: string |
66 |
val sel_corecsN: string |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
67 |
val set_inclN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
val set_set_inclN: string |
49438 | 69 |
val simpsN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
70 |
val strTN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
val str_initN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
72 |
val sum_bdN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
73 |
val sum_bdTN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
74 |
val unfN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
75 |
val unf_coinductN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
76 |
val unf_coinduct_uptoN: string |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
77 |
val unf_coiterN: string |
49338 | 78 |
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
|
79 |
val unf_coitersN: string |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49125
diff
changeset
|
80 |
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
|
81 |
val unf_corecsN: string |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
val unf_exhaustN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
83 |
val unf_fldN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
84 |
val unf_injectN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
85 |
val uniqueN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
val uptoN: string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
88 |
val mk_exhaustN: string -> string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
89 |
val mk_injectN: string -> string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
val mk_nchotomyN: string -> string |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
91 |
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
|
92 |
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
|
93 |
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
|
94 |
|
49337 | 95 |
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
|
96 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
97 |
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
|
98 |
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
|
99 |
|
49330
276ff43ee0b1
reuse generated names (they look better + slightly more efficient)
blanchet
parents:
49327
diff
changeset
|
100 |
val retype_free: typ -> term -> term |
276ff43ee0b1
reuse generated names (they look better + slightly more efficient)
blanchet
parents:
49327
diff
changeset
|
101 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
102 |
val mk_sumTN: typ list -> typ |
49264 | 103 |
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
|
104 |
|
49368 | 105 |
val id_const: typ -> term |
106 |
val id_abs: typ -> term |
|
107 |
||
49121 | 108 |
val Inl_const: typ -> typ -> term |
109 |
val Inr_const: typ -> typ -> term |
|
110 |
||
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
111 |
val mk_Inl: typ -> term -> term |
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
112 |
val mk_Inr: typ -> term -> term |
49121 | 113 |
val mk_InN: typ list -> term -> int -> term |
49264 | 114 |
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
|
115 |
val mk_sum_case: term * term -> term |
49129 | 116 |
val mk_sum_caseN: term list -> term |
49264 | 117 |
val mk_sum_caseN_balanced: term list -> term |
49121 | 118 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
119 |
val dest_sumT: typ -> typ * typ |
49176 | 120 |
val dest_sumTN: int -> typ -> typ list |
49264 | 121 |
val dest_sumTN_balanced: int -> typ -> typ list |
49176 | 122 |
val dest_tupleT: int -> typ -> typ list |
123 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
124 |
val mk_Field: term -> term |
49275 | 125 |
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
|
126 |
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
|
127 |
|
49125 | 128 |
val mk_sumEN: int -> thm |
49264 | 129 |
val mk_sumEN_balanced: int -> thm |
49335 | 130 |
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
|
131 |
val mk_sum_casesN: int -> int -> thm |
49264 | 132 |
val mk_sum_casesN_balanced: int -> int -> thm |
49125 | 133 |
|
48975
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 |
|
49457 | 145 |
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
|
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 |
49456 | 226 |
val simpN = "_simp"; |
227 |
val rel_simpN = relN ^ simpN; |
|
228 |
val pred_simpN = predN ^ simpN; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
229 |
val uptoN = "upto" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
230 |
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
|
231 |
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
|
232 |
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
|
233 |
val hsetN = "Hset" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
234 |
val hset_recN = hsetN ^ "_rec" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
235 |
val set_inclN = "set_incl" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
236 |
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
|
237 |
|
49338 | 238 |
val caseN = "case" |
49342 | 239 |
val discN = "disc" |
240 |
val disc_coitersN = discN ^ "_" ^ coitersN |
|
241 |
val disc_corecsN = discN ^ "_" ^ corecsN |
|
49482 | 242 |
val iffN = "_iff" |
49484 | 243 |
val disc_coiter_iffN = discN ^ "_" ^ coiterN ^ iffN |
244 |
val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN |
|
49342 | 245 |
val selN = "sel" |
246 |
val sel_coitersN = selN ^ "_" ^ coitersN |
|
247 |
val sel_corecsN = selN ^ "_" ^ corecsN |
|
49338 | 248 |
|
49337 | 249 |
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
|
250 |
|
49330
276ff43ee0b1
reuse generated names (they look better + slightly more efficient)
blanchet
parents:
49327
diff
changeset
|
251 |
fun retype_free T (Free (s, _)) = Free (s, T); |
276ff43ee0b1
reuse generated names (they look better + slightly more efficient)
blanchet
parents:
49327
diff
changeset
|
252 |
|
49264 | 253 |
fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T'); |
254 |
||
255 |
fun dest_sumTN 1 T = [T] |
|
256 |
| dest_sumTN n (Type (@{type_name sum}, [T, T'])) = T :: dest_sumTN (n - 1) T'; |
|
257 |
||
258 |
val dest_sumTN_balanced = Balanced_Tree.dest dest_sumT; |
|
259 |
||
260 |
(* TODO: move something like this to "HOLogic"? *) |
|
261 |
fun dest_tupleT 0 @{typ unit} = [] |
|
262 |
| dest_tupleT 1 T = [T] |
|
263 |
| dest_tupleT n (Type (@{type_name prod}, [T, T'])) = T :: dest_tupleT (n - 1) T'; |
|
264 |
||
265 |
val mk_sumTN = Library.foldr1 mk_sumT; |
|
266 |
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
|
267 |
|
49368 | 268 |
fun id_const T = Const (@{const_name id}, T --> T); |
269 |
fun id_abs T = Abs (Name.uu, T, Bound 0); |
|
270 |
||
49121 | 271 |
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
|
272 |
fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t; |
49121 | 273 |
|
274 |
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
|
275 |
fun mk_Inr LT t = Inr_const LT (fastype_of t) $ t; |
49121 | 276 |
|
277 |
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
|
278 |
| 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
|
279 |
| mk_InN (LT :: Ts) t m = mk_Inr LT (mk_InN Ts t (m - 1)) |
49121 | 280 |
| mk_InN Ts t _ = raise (TYPE ("mk_InN", Ts, [t])); |
281 |
||
49264 | 282 |
fun mk_InN_balanced sum_T n t k = |
283 |
let |
|
284 |
fun repair_types T (Const (s as @{const_name Inl}, _) $ t) = repair_inj_types T s fst t |
|
285 |
| repair_types T (Const (s as @{const_name Inr}, _) $ t) = repair_inj_types T s snd t |
|
286 |
| repair_types _ t = t |
|
287 |
and repair_inj_types T s get t = |
|
288 |
let val T' = get (dest_sumT T) in |
|
289 |
Const (s, T' --> T) $ repair_types T' t |
|
290 |
end; |
|
291 |
in |
|
292 |
Balanced_Tree.access {left = mk_Inl dummyT, right = mk_Inr dummyT, init = t} n k |
|
293 |
|> repair_types sum_T |
|
294 |
end; |
|
295 |
||
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
296 |
fun mk_sum_case (f, g) = |
49129 | 297 |
let |
298 |
val fT = fastype_of f; |
|
299 |
val gT = fastype_of g; |
|
300 |
in |
|
301 |
Const (@{const_name sum_case}, |
|
302 |
fT --> gT --> mk_sumT (domain_type fT, domain_type gT) --> range_type fT) $ f $ g |
|
303 |
end; |
|
304 |
||
49264 | 305 |
val mk_sum_caseN = Library.foldr1 mk_sum_case; |
306 |
val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case; |
|
49176 | 307 |
|
49275 | 308 |
fun mk_If p t f = |
309 |
let val T = fastype_of t; |
|
310 |
in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end; |
|
311 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
312 |
fun mk_Field r = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
313 |
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
|
314 |
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
|
315 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
316 |
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
|
317 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
318 |
(*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
|
319 |
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
|
320 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
321 |
(* 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
|
322 |
fun split_conj_thm th = |
49119 | 323 |
((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
|
324 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
325 |
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
|
326 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
327 |
fun split n i th = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
328 |
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
|
329 |
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
|
330 |
|
49255
2ecc533d6697
use balanced sums for constructors (to gracefully handle 100 constructors or more)
blanchet
parents:
49240
diff
changeset
|
331 |
fun mk_sumEN 1 = @{thm one_pointE} |
49240 | 332 |
| mk_sumEN 2 = @{thm sumE} |
333 |
| mk_sumEN n = |
|
334 |
(fold (fn i => fn thm => @{thm obj_sum_step} RSN (i, thm)) (2 upto n - 1) @{thm obj_sumE}) OF |
|
335 |
replicate n (impI RS allI); |
|
49125 | 336 |
|
49335 | 337 |
fun mk_obj_sumEN_balanced n = |
338 |
Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f}))) |
|
339 |
(replicate n asm_rl); |
|
340 |
||
341 |
fun mk_sumEN_balanced' n all_impIs = mk_obj_sumEN_balanced n OF all_impIs RS @{thm obj_one_pointE}; |
|
342 |
||
343 |
fun mk_sumEN_balanced 1 = @{thm one_pointE} (*optimization*) |
|
49264 | 344 |
| mk_sumEN_balanced 2 = @{thm sumE} (*optimization*) |
49335 | 345 |
| mk_sumEN_balanced n = mk_sumEN_balanced' n (replicate n (impI RS allI)); |
346 |
||
347 |
fun mk_tupled_allIN 0 = @{thm unit_all_impI} |
|
348 |
| mk_tupled_allIN 1 = @{thm impI[THEN allI]} |
|
349 |
| mk_tupled_allIN 2 = @{thm prod_all_impI} (*optimization*) |
|
350 |
| mk_tupled_allIN n = mk_tupled_allIN (n - 1) RS @{thm prod_all_impI_step}; |
|
351 |
||
352 |
fun mk_sumEN_tupled_balanced ms = |
|
353 |
let val n = length ms in |
|
354 |
if forall (curry (op =) 1) ms then mk_sumEN_balanced n |
|
355 |
else mk_sumEN_balanced' n (map mk_tupled_allIN ms) |
|
356 |
end; |
|
49264 | 357 |
|
358 |
fun mk_sum_casesN 1 1 = refl |
|
49130
3c26e17b2849
implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset
|
359 |
| mk_sum_casesN _ 1 = @{thm sum.cases(1)} |
3c26e17b2849
implemented "mk_case_tac" -- and got rid of "cheat_tac"
blanchet
parents:
49129
diff
changeset
|
360 |
| mk_sum_casesN 2 2 = @{thm sum.cases(2)} |
49264 | 361 |
| mk_sum_casesN n k = trans OF [@{thm sum_case_step(2)}, mk_sum_casesN (n - 1) (k - 1)]; |
362 |
||
363 |
fun mk_sum_step base step thm = |
|
364 |
if Thm.eq_thm_prop (thm, refl) then base else trans OF [step, thm]; |
|
365 |
||
366 |
fun mk_sum_casesN_balanced 1 1 = refl |
|
367 |
| mk_sum_casesN_balanced n k = |
|
368 |
Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)}, |
|
369 |
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
|
370 |
|
49141 | 371 |
(* FIXME: because of "@ lhss", the output could contain type variables that are not in the input; |
372 |
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
|
373 |
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
|
374 |
(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
|
375 |
| 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
|
376 |
(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
|
377 |
|
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
378 |
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
|
379 |
let |
49337 | 380 |
val name = mk_common_name bs; |
49425 | 381 |
fun qualify i = |
382 |
let val namei = name ^ nonzero_string_of_int i; |
|
383 |
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
|
384 |
|
49132 | 385 |
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
|
386 |
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
|
387 |
val Ds = fold (fold Term.add_tfreesT) deadss []; |
49132 | 388 |
|
49156 | 389 |
val _ = (case Library.inter (op =) Ds lhss of [] => () |
49132 | 390 |
| A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \ |
391 |
\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
|
392 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
393 |
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
|
394 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
395 |
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
|
396 |
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
|
397 |
|
49132 | 398 |
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
|
399 |
|
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
400 |
val ((bnfs'', deadss), lthy'') = |
49223 | 401 |
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
|
402 |
|>> split_list; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
403 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
404 |
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
|
405 |
|
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
406 |
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
|
407 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
408 |
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
|
409 |
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
|
410 |
timer; (bnfs'', res) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
411 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
412 |
|
49169 | 413 |
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
|
414 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
415 |
val timer = time (Timer.startRealTimer ()); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
416 |
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
|
417 |
val sort = fp_sort lhss (SOME resBs); |
49425 | 418 |
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
|
419 |
val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list) |
49425 | 420 |
(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
|
421 |
(empty_unfold, lthy)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
422 |
in |
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49176
diff
changeset
|
423 |
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
|
424 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
425 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
426 |
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
|
427 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
428 |
val timer = time (Timer.startRealTimer ()); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
429 |
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
|
430 |
val sort = fp_sort lhss NONE; |
49425 | 431 |
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
|
432 |
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
|
433 |
(fold_map2 (fn b => fn rawT => |
49425 | 434 |
(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
|
435 |
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
|
436 |
in |
49207 | 437 |
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
|
438 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
439 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
440 |
end; |