|
1 (* Title: HOL/BNF/Tools/bnf_util.ML |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Library for bounded natural functors. |
|
6 *) |
|
7 |
|
8 signature BNF_UTIL = |
|
9 sig |
|
10 val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list |
|
11 val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
|
12 val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> |
|
13 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list |
|
14 val map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) -> |
|
15 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list |
|
16 val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> |
|
17 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list |
|
18 val map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) -> |
|
19 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list |
|
20 val map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j) -> |
|
21 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> |
|
22 'i list -> 'j list |
|
23 val map10: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k) -> |
|
24 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> |
|
25 'i list -> 'j list -> 'k list |
|
26 val map11: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l) -> |
|
27 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> |
|
28 'i list -> 'j list -> 'k list -> 'l list |
|
29 val map12: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm) -> |
|
30 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> |
|
31 'i list -> 'j list -> 'k list -> 'l list -> 'm list |
|
32 val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c |
|
33 val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) -> |
|
34 'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd |
|
35 val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) -> |
|
36 'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e |
|
37 val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) -> |
|
38 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f -> 'g list * 'f |
|
39 val fold_map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h * 'g) -> |
|
40 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g |
|
41 val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) -> |
|
42 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h |
|
43 val interleave: 'a list -> 'a list -> 'a list |
|
44 val transpose: 'a list list -> 'a list list |
|
45 val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list |
|
46 |
|
47 val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context |
|
48 val mk_TFrees: int -> Proof.context -> typ list * Proof.context |
|
49 val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context |
|
50 val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context |
|
51 val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context |
|
52 val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context |
|
53 val mk_Freesss: string -> typ list list list -> Proof.context -> |
|
54 term list list list * Proof.context |
|
55 val mk_Freessss: string -> typ list list list list -> Proof.context -> |
|
56 term list list list list * Proof.context |
|
57 val mk_Frees': string -> typ list -> Proof.context -> |
|
58 (term list * (string * typ) list) * Proof.context |
|
59 val mk_Freess': string -> typ list list -> Proof.context -> |
|
60 (term list list * (string * typ) list list) * Proof.context |
|
61 val nonzero_string_of_int: int -> string |
|
62 |
|
63 val strip_typeN: int -> typ -> typ list * typ |
|
64 |
|
65 val mk_predT: typ list -> typ |
|
66 val mk_pred1T: typ -> typ |
|
67 val mk_pred2T: typ -> typ -> typ |
|
68 val mk_optionT: typ -> typ |
|
69 val mk_relT: typ * typ -> typ |
|
70 val dest_relT: typ -> typ * typ |
|
71 val mk_sumT: typ * typ -> typ |
|
72 |
|
73 val ctwo: term |
|
74 val fst_const: typ -> term |
|
75 val snd_const: typ -> term |
|
76 val Id_const: typ -> term |
|
77 |
|
78 val mk_Ball: term -> term -> term |
|
79 val mk_Bex: term -> term -> term |
|
80 val mk_Card_order: term -> term |
|
81 val mk_Field: term -> term |
|
82 val mk_Gr: term -> term -> term |
|
83 val mk_IfN: typ -> term list -> term list -> term |
|
84 val mk_Trueprop_eq: term * term -> term |
|
85 val mk_UNION: term -> term -> term |
|
86 val mk_Union: typ -> term |
|
87 val mk_card_binop: string -> (typ * typ -> typ) -> term -> term -> term |
|
88 val mk_card_of: term -> term |
|
89 val mk_card_order: term -> term |
|
90 val mk_ccexp: term -> term -> term |
|
91 val mk_cexp: term -> term -> term |
|
92 val mk_cinfinite: term -> term |
|
93 val mk_collect: term list -> typ -> term |
|
94 val mk_converse: term -> term |
|
95 val mk_cprod: term -> term -> term |
|
96 val mk_csum: term -> term -> term |
|
97 val mk_dir_image: term -> term -> term |
|
98 val mk_image: term -> term |
|
99 val mk_in: term list -> term list -> typ -> term |
|
100 val mk_ordLeq: term -> term -> term |
|
101 val mk_rel_comp: term * term -> term |
|
102 val mk_subset: term -> term -> term |
|
103 val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term |
|
104 |
|
105 val list_all_free: term list -> term -> term |
|
106 val list_exists_free: term list -> term -> term |
|
107 |
|
108 (*parameterized terms*) |
|
109 val mk_nthN: int -> term -> int -> term |
|
110 |
|
111 (*parameterized thms*) |
|
112 val mk_Un_upper: int -> int -> thm |
|
113 val mk_conjIN: int -> thm |
|
114 val mk_conjunctN: int -> int -> thm |
|
115 val conj_dests: int -> thm -> thm list |
|
116 val mk_disjIN: int -> int -> thm |
|
117 val mk_nthI: int -> int -> thm |
|
118 val mk_nth_conv: int -> int -> thm |
|
119 val mk_ordLeq_csum: int -> int -> thm -> thm |
|
120 val mk_UnIN: int -> int -> thm |
|
121 |
|
122 val ctrans: thm |
|
123 val o_apply: thm |
|
124 val set_mp: thm |
|
125 val set_rev_mp: thm |
|
126 val subset_UNIV: thm |
|
127 val Pair_eqD: thm |
|
128 val Pair_eqI: thm |
|
129 val mk_sym: thm -> thm |
|
130 val mk_trans: thm -> thm -> thm |
|
131 val mk_unabs_def: int -> thm -> thm |
|
132 |
|
133 val is_refl: thm -> bool |
|
134 val no_refl: thm list -> thm list |
|
135 val no_reflexive: thm list -> thm list |
|
136 |
|
137 val fold_thms: Proof.context -> thm list -> thm -> thm |
|
138 val unfold_thms: Proof.context -> thm list -> thm -> thm |
|
139 |
|
140 val mk_permute: ''a list -> ''a list -> 'b list -> 'b list |
|
141 val find_indices: ''a list -> ''a list -> int list |
|
142 |
|
143 val certifyT: Proof.context -> typ -> ctyp |
|
144 val certify: Proof.context -> term -> cterm |
|
145 |
|
146 val parse_binding_colon: Token.T list -> binding * Token.T list |
|
147 val parse_opt_binding_colon: Token.T list -> binding * Token.T list |
|
148 |
|
149 val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term -> |
|
150 (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory |
|
151 |
|
152 val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic |
|
153 val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int -> |
|
154 tactic |
|
155 val CONJ_WRAP_GEN: tactic -> ('a -> tactic) -> 'a list -> tactic |
|
156 val CONJ_WRAP_GEN': (int -> tactic) -> ('a -> int -> tactic) -> 'a list -> int -> tactic |
|
157 val CONJ_WRAP: ('a -> tactic) -> 'a list -> tactic |
|
158 val CONJ_WRAP': ('a -> int -> tactic) -> 'a list -> int -> tactic |
|
159 end; |
|
160 |
|
161 structure BNF_Util : BNF_UTIL = |
|
162 struct |
|
163 |
|
164 (* Library proper *) |
|
165 |
|
166 fun map3 _ [] [] [] = [] |
|
167 | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s |
|
168 | map3 _ _ _ _ = raise ListPair.UnequalLengths; |
|
169 |
|
170 fun map4 _ [] [] [] [] = [] |
|
171 | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s |
|
172 | map4 _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
173 |
|
174 fun map5 _ [] [] [] [] [] = [] |
|
175 | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) = |
|
176 f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s |
|
177 | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
178 |
|
179 fun map6 _ [] [] [] [] [] [] = [] |
|
180 | map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) = |
|
181 f x1 x2 x3 x4 x5 x6 :: map6 f x1s x2s x3s x4s x5s x6s |
|
182 | map6 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
183 |
|
184 fun map7 _ [] [] [] [] [] [] [] = [] |
|
185 | map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) = |
|
186 f x1 x2 x3 x4 x5 x6 x7 :: map7 f x1s x2s x3s x4s x5s x6s x7s |
|
187 | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
188 |
|
189 fun map8 _ [] [] [] [] [] [] [] [] = [] |
|
190 | map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) = |
|
191 f x1 x2 x3 x4 x5 x6 x7 x8 :: map8 f x1s x2s x3s x4s x5s x6s x7s x8s |
|
192 | map8 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
193 |
|
194 fun map9 _ [] [] [] [] [] [] [] [] [] = [] |
|
195 | map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) |
|
196 (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) = |
|
197 f x1 x2 x3 x4 x5 x6 x7 x8 x9 :: map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s |
|
198 | map9 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
199 |
|
200 fun map10 _ [] [] [] [] [] [] [] [] [] [] = [] |
|
201 | map10 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) |
|
202 (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) = |
|
203 f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 :: map10 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s |
|
204 | map10 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
205 |
|
206 fun map11 _ [] [] [] [] [] [] [] [] [] [] [] = [] |
|
207 | map11 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) |
|
208 (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) = |
|
209 f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 :: map11 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s |
|
210 | map11 _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
211 |
|
212 fun map12 _ [] [] [] [] [] [] [] [] [] [] [] [] = [] |
|
213 | map12 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) |
|
214 (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) = |
|
215 f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 :: |
|
216 map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s |
|
217 | map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
218 |
|
219 fun fold_map2 _ [] [] acc = ([], acc) |
|
220 | fold_map2 f (x1::x1s) (x2::x2s) acc = |
|
221 let |
|
222 val (x, acc') = f x1 x2 acc; |
|
223 val (xs, acc'') = fold_map2 f x1s x2s acc'; |
|
224 in (x :: xs, acc'') end |
|
225 | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths; |
|
226 |
|
227 fun fold_map3 _ [] [] [] acc = ([], acc) |
|
228 | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc = |
|
229 let |
|
230 val (x, acc') = f x1 x2 x3 acc; |
|
231 val (xs, acc'') = fold_map3 f x1s x2s x3s acc'; |
|
232 in (x :: xs, acc'') end |
|
233 | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
234 |
|
235 fun fold_map4 _ [] [] [] [] acc = ([], acc) |
|
236 | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc = |
|
237 let |
|
238 val (x, acc') = f x1 x2 x3 x4 acc; |
|
239 val (xs, acc'') = fold_map4 f x1s x2s x3s x4s acc'; |
|
240 in (x :: xs, acc'') end |
|
241 | fold_map4 _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
242 |
|
243 fun fold_map5 _ [] [] [] [] [] acc = ([], acc) |
|
244 | fold_map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) acc = |
|
245 let |
|
246 val (x, acc') = f x1 x2 x3 x4 x5 acc; |
|
247 val (xs, acc'') = fold_map5 f x1s x2s x3s x4s x5s acc'; |
|
248 in (x :: xs, acc'') end |
|
249 | fold_map5 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
250 |
|
251 fun fold_map6 _ [] [] [] [] [] [] acc = ([], acc) |
|
252 | fold_map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) acc = |
|
253 let |
|
254 val (x, acc') = f x1 x2 x3 x4 x5 x6 acc; |
|
255 val (xs, acc'') = fold_map6 f x1s x2s x3s x4s x5s x6s acc'; |
|
256 in (x :: xs, acc'') end |
|
257 | fold_map6 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
258 |
|
259 fun fold_map7 _ [] [] [] [] [] [] [] acc = ([], acc) |
|
260 | fold_map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) acc = |
|
261 let |
|
262 val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 acc; |
|
263 val (xs, acc'') = fold_map7 f x1s x2s x3s x4s x5s x6s x7s acc'; |
|
264 in (x :: xs, acc'') end |
|
265 | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
266 |
|
267 (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*) |
|
268 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt); |
|
269 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt); |
|
270 |
|
271 val parse_binding_colon = Parse.binding --| @{keyword ":"}; |
|
272 val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty; |
|
273 |
|
274 (*TODO: is this really different from Typedef.add_typedef_global?*) |
|
275 fun typedef def opt_name typ set opt_morphs tac lthy = |
|
276 let |
|
277 val ((name, info), (lthy, lthy_old)) = |
|
278 lthy |
|
279 |> Typedef.add_typedef def opt_name typ set opt_morphs tac |
|
280 ||> `Local_Theory.restore; |
|
281 val phi = Proof_Context.export_morphism lthy_old lthy; |
|
282 in |
|
283 ((name, Typedef.transform_info phi info), lthy) |
|
284 end; |
|
285 |
|
286 (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*) |
|
287 fun WRAP gen_before gen_after xs core_tac = |
|
288 fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac; |
|
289 |
|
290 fun WRAP' gen_before gen_after xs core_tac = |
|
291 fold_rev (fn x => fn tac => gen_before x THEN' tac THEN' gen_after x) xs core_tac; |
|
292 |
|
293 fun CONJ_WRAP_GEN conj_tac gen_tac xs = |
|
294 let val (butlast, last) = split_last xs; |
|
295 in WRAP (fn thm => conj_tac THEN gen_tac thm) (K all_tac) butlast (gen_tac last) end; |
|
296 |
|
297 fun CONJ_WRAP_GEN' conj_tac gen_tac xs = |
|
298 let val (butlast, last) = split_last xs; |
|
299 in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end; |
|
300 |
|
301 (*not eta-converted because of monotype restriction*) |
|
302 fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac; |
|
303 fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac; |
|
304 |
|
305 |
|
306 |
|
307 (* Term construction *) |
|
308 |
|
309 (** Fresh variables **) |
|
310 |
|
311 fun nonzero_string_of_int 0 = "" |
|
312 | nonzero_string_of_int n = string_of_int n; |
|
313 |
|
314 val mk_TFrees' = apfst (map TFree) oo Variable.invent_types; |
|
315 |
|
316 fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS); |
|
317 val mk_TFreess = fold_map mk_TFrees; |
|
318 |
|
319 fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n); |
|
320 |
|
321 fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names; |
|
322 fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts); |
|
323 fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss; |
|
324 fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss; |
|
325 fun mk_Freessss x Tssss = fold_map2 mk_Freesss (mk_names (length Tssss) x) Tssss; |
|
326 fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts)); |
|
327 fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list; |
|
328 |
|
329 |
|
330 (** Types **) |
|
331 |
|
332 fun strip_typeN 0 T = ([], T) |
|
333 | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T |
|
334 | strip_typeN _ T = raise TYPE ("strip_typeN", [T], []); |
|
335 |
|
336 fun mk_predT Ts = Ts ---> HOLogic.boolT; |
|
337 fun mk_pred1T T = mk_predT [T]; |
|
338 fun mk_pred2T T U = mk_predT [T, U]; |
|
339 fun mk_optionT T = Type (@{type_name option}, [T]); |
|
340 val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT; |
|
341 val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT; |
|
342 fun mk_sumT (LT, RT) = Type (@{type_name Sum_Type.sum}, [LT, RT]); |
|
343 fun mk_partial_funT (ranT, domT) = domT --> mk_optionT ranT; |
|
344 |
|
345 |
|
346 (** Constants **) |
|
347 |
|
348 fun fst_const T = Const (@{const_name fst}, T --> fst (HOLogic.dest_prodT T)); |
|
349 fun snd_const T = Const (@{const_name snd}, T --> snd (HOLogic.dest_prodT T)); |
|
350 fun Id_const T = Const (@{const_name Id}, mk_relT (T, T)); |
|
351 |
|
352 |
|
353 (** Operators **) |
|
354 |
|
355 val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
|
356 |
|
357 fun mk_IfN _ _ [t] = t |
|
358 | mk_IfN T (c :: cs) (t :: ts) = |
|
359 Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts; |
|
360 |
|
361 fun mk_converse R = |
|
362 let |
|
363 val RT = dest_relT (fastype_of R); |
|
364 val RST = mk_relT (snd RT, fst RT); |
|
365 in Const (@{const_name converse}, fastype_of R --> RST) $ R end; |
|
366 |
|
367 fun mk_rel_comp (R, S) = |
|
368 let |
|
369 val RT = fastype_of R; |
|
370 val ST = fastype_of S; |
|
371 val RST = mk_relT (fst (dest_relT RT), snd (dest_relT ST)); |
|
372 in Const (@{const_name relcomp}, RT --> ST --> RST) $ R $ S end; |
|
373 |
|
374 fun mk_Gr A f = |
|
375 let val ((AT, BT), FT) = `dest_funT (fastype_of f); |
|
376 in Const (@{const_name Gr}, HOLogic.mk_setT AT --> FT --> mk_relT (AT, BT)) $ A $ f end; |
|
377 |
|
378 fun mk_image f = |
|
379 let val (T, U) = dest_funT (fastype_of f); |
|
380 in Const (@{const_name image}, |
|
381 (T --> U) --> (HOLogic.mk_setT T) --> (HOLogic.mk_setT U)) $ f end; |
|
382 |
|
383 fun mk_Ball X f = |
|
384 Const (@{const_name Ball}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f; |
|
385 |
|
386 fun mk_Bex X f = |
|
387 Const (@{const_name Bex}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f; |
|
388 |
|
389 fun mk_UNION X f = |
|
390 let val (T, U) = dest_funT (fastype_of f); |
|
391 in Const (@{const_name SUPR}, fastype_of X --> (T --> U) --> U) $ X $ f end; |
|
392 |
|
393 fun mk_Union T = |
|
394 Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T); |
|
395 |
|
396 fun mk_Field r = |
|
397 let val T = fst (dest_relT (fastype_of r)); |
|
398 in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end; |
|
399 |
|
400 fun mk_card_order bd = |
|
401 let |
|
402 val T = fastype_of bd; |
|
403 val AT = fst (dest_relT T); |
|
404 in |
|
405 Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $ |
|
406 (HOLogic.mk_UNIV AT) $ bd |
|
407 end; |
|
408 |
|
409 fun mk_Card_order bd = |
|
410 let |
|
411 val T = fastype_of bd; |
|
412 val AT = fst (dest_relT T); |
|
413 in |
|
414 Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $ |
|
415 mk_Field bd $ bd |
|
416 end; |
|
417 |
|
418 fun mk_cinfinite bd = |
|
419 Const (@{const_name cinfinite}, fastype_of bd --> HOLogic.boolT) $ bd; |
|
420 |
|
421 fun mk_ordLeq t1 t2 = |
|
422 HOLogic.mk_mem (HOLogic.mk_prod (t1, t2), |
|
423 Const (@{const_name ordLeq}, mk_relT (fastype_of t1, fastype_of t2))); |
|
424 |
|
425 fun mk_card_of A = |
|
426 let |
|
427 val AT = fastype_of A; |
|
428 val T = HOLogic.dest_setT AT; |
|
429 in |
|
430 Const (@{const_name card_of}, AT --> mk_relT (T, T)) $ A |
|
431 end; |
|
432 |
|
433 fun mk_dir_image r f = |
|
434 let val (T, U) = dest_funT (fastype_of f); |
|
435 in Const (@{const_name dir_image}, mk_relT (T, T) --> (T --> U) --> mk_relT (U, U)) $ r $ f end; |
|
436 |
|
437 (*FIXME: "x"?*) |
|
438 (*(nth sets i) must be of type "T --> 'ai set"*) |
|
439 fun mk_in As sets T = |
|
440 let |
|
441 fun in_single set A = |
|
442 let val AT = fastype_of A; |
|
443 in Const (@{const_name less_eq}, |
|
444 AT --> AT --> HOLogic.boolT) $ (set $ Free ("x", T)) $ A end; |
|
445 in |
|
446 if length sets > 0 |
|
447 then HOLogic.mk_Collect ("x", T, foldr1 (HOLogic.mk_conj) (map2 in_single sets As)) |
|
448 else HOLogic.mk_UNIV T |
|
449 end; |
|
450 |
|
451 fun mk_wpull A B1 B2 f1 f2 pseudo p1 p2 = |
|
452 let |
|
453 val AT = fastype_of A; |
|
454 val BT1 = fastype_of B1; |
|
455 val BT2 = fastype_of B2; |
|
456 val FT1 = fastype_of f1; |
|
457 val FT2 = fastype_of f2; |
|
458 val PT1 = fastype_of p1; |
|
459 val PT2 = fastype_of p2; |
|
460 val T1 = HOLogic.dest_setT BT1; |
|
461 val T2 = HOLogic.dest_setT BT2; |
|
462 val domP = domain_type PT1; |
|
463 val ranF = range_type FT1; |
|
464 val _ = if is_some pseudo orelse |
|
465 (HOLogic.dest_setT AT = domP andalso |
|
466 domain_type FT1 = T1 andalso |
|
467 domain_type FT2 = T2 andalso |
|
468 domain_type PT2 = domP andalso |
|
469 range_type PT1 = T1 andalso |
|
470 range_type PT2 = T2 andalso |
|
471 range_type FT2 = ranF) |
|
472 then () else raise TYPE ("mk_wpull", [BT1, BT2, FT1, FT2, PT1, PT2], []); |
|
473 in |
|
474 (case pseudo of |
|
475 NONE => Const (@{const_name wpull}, |
|
476 AT --> BT1 --> BT2 --> FT1 --> FT2 --> PT1 --> PT2 --> HOLogic.boolT) $ |
|
477 A $ B1 $ B2 $ f1 $ f2 $ p1 $ p2 |
|
478 | SOME (e1, e2) => Const (@{const_name wppull}, |
|
479 AT --> BT1 --> BT2 --> FT1 --> FT2 --> fastype_of e1 --> fastype_of e2 --> |
|
480 PT1 --> PT2 --> HOLogic.boolT) $ |
|
481 A $ B1 $ B2 $ f1 $ f2 $ e1 $ e2 $ p1 $ p2) |
|
482 end; |
|
483 |
|
484 fun mk_subset t1 t2 = |
|
485 Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2; |
|
486 |
|
487 fun mk_card_binop binop typop t1 t2 = |
|
488 let |
|
489 val (T1, relT1) = `(fst o dest_relT) (fastype_of t1); |
|
490 val (T2, relT2) = `(fst o dest_relT) (fastype_of t2); |
|
491 in |
|
492 Const (binop, relT1 --> relT2 --> mk_relT (typop (T1, T2), typop (T1, T2))) $ t1 $ t2 |
|
493 end; |
|
494 |
|
495 val mk_csum = mk_card_binop @{const_name csum} mk_sumT; |
|
496 val mk_cprod = mk_card_binop @{const_name cprod} HOLogic.mk_prodT; |
|
497 val mk_cexp = mk_card_binop @{const_name cexp} mk_partial_funT; |
|
498 val mk_ccexp = mk_card_binop @{const_name ccexp} mk_partial_funT; |
|
499 val ctwo = @{term ctwo}; |
|
500 |
|
501 fun mk_collect xs defT = |
|
502 let val T = (case xs of [] => defT | (x::_) => fastype_of x); |
|
503 in Const (@{const_name collect}, HOLogic.mk_setT T --> T) $ (HOLogic.mk_set T xs) end; |
|
504 |
|
505 fun mk_permute src dest xs = map (nth xs o (fn x => find_index ((curry op =) x) src)) dest; |
|
506 |
|
507 val list_all_free = |
|
508 fold_rev (fn free => fn P => |
|
509 let val (x, T) = Term.dest_Free free; |
|
510 in HOLogic.all_const T $ Term.absfree (x, T) P end); |
|
511 |
|
512 val list_exists_free = |
|
513 fold_rev (fn free => fn P => |
|
514 let val (x, T) = Term.dest_Free free; |
|
515 in HOLogic.exists_const T $ Term.absfree (x, T) P end); |
|
516 |
|
517 fun find_indices xs ys = map_filter I |
|
518 (map_index (fn (i, y) => if member (op =) xs y then SOME i else NONE) ys); |
|
519 |
|
520 fun mk_trans thm1 thm2 = trans OF [thm1, thm2]; |
|
521 fun mk_sym thm = sym OF [thm]; |
|
522 |
|
523 (*TODO: antiquote heavily used theorems once*) |
|
524 val ctrans = @{thm ordLeq_transitive}; |
|
525 val o_apply = @{thm o_apply}; |
|
526 val set_mp = @{thm set_mp}; |
|
527 val set_rev_mp = @{thm set_rev_mp}; |
|
528 val subset_UNIV = @{thm subset_UNIV}; |
|
529 val Pair_eqD = @{thm iffD1[OF Pair_eq]}; |
|
530 val Pair_eqI = @{thm iffD2[OF Pair_eq]}; |
|
531 |
|
532 fun mk_nthN 1 t 1 = t |
|
533 | mk_nthN _ t 1 = HOLogic.mk_fst t |
|
534 | mk_nthN 2 t 2 = HOLogic.mk_snd t |
|
535 | mk_nthN n t m = mk_nthN (n - 1) (HOLogic.mk_snd t) (m - 1); |
|
536 |
|
537 fun mk_nth_conv n m = |
|
538 let |
|
539 fun thm b = if b then @{thm fst_snd} else @{thm snd_snd} |
|
540 fun mk_nth_conv _ 1 1 = refl |
|
541 | mk_nth_conv _ _ 1 = @{thm fst_conv} |
|
542 | mk_nth_conv _ 2 2 = @{thm snd_conv} |
|
543 | mk_nth_conv b _ 2 = @{thm snd_conv} RS thm b |
|
544 | mk_nth_conv b n m = mk_nth_conv false (n - 1) (m - 1) RS thm b; |
|
545 in mk_nth_conv (not (m = n)) n m end; |
|
546 |
|
547 fun mk_nthI 1 1 = @{thm TrueE[OF TrueI]} |
|
548 | mk_nthI n m = fold (curry op RS) (replicate (m - 1) @{thm sndI}) |
|
549 (if m = n then @{thm TrueE[OF TrueI]} else @{thm fstI}); |
|
550 |
|
551 fun mk_conjunctN 1 1 = @{thm TrueE[OF TrueI]} |
|
552 | mk_conjunctN _ 1 = conjunct1 |
|
553 | mk_conjunctN 2 2 = conjunct2 |
|
554 | mk_conjunctN n m = conjunct2 RS (mk_conjunctN (n - 1) (m - 1)); |
|
555 |
|
556 fun conj_dests n thm = map (fn k => thm RS mk_conjunctN n k) (1 upto n); |
|
557 |
|
558 fun mk_conjIN 1 = @{thm TrueE[OF TrueI]} |
|
559 | mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI); |
|
560 |
|
561 fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]} |
|
562 | mk_disjIN _ 1 = disjI1 |
|
563 | mk_disjIN 2 2 = disjI2 |
|
564 | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2; |
|
565 |
|
566 fun mk_ordLeq_csum 1 1 thm = thm |
|
567 | mk_ordLeq_csum _ 1 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum1}] |
|
568 | mk_ordLeq_csum 2 2 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum2}] |
|
569 | mk_ordLeq_csum n m thm = @{thm ordLeq_transitive} OF |
|
570 [mk_ordLeq_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}]; |
|
571 |
|
572 local |
|
573 fun mk_Un_upper' 0 = subset_refl |
|
574 | mk_Un_upper' 1 = @{thm Un_upper1} |
|
575 | mk_Un_upper' k = Library.foldr (op RS o swap) |
|
576 (replicate (k - 1) @{thm subset_trans[OF Un_upper1]}, @{thm Un_upper1}); |
|
577 in |
|
578 fun mk_Un_upper 1 1 = subset_refl |
|
579 | mk_Un_upper n 1 = mk_Un_upper' (n - 2) RS @{thm subset_trans[OF Un_upper1]} |
|
580 | mk_Un_upper n m = mk_Un_upper' (n - m) RS @{thm subset_trans[OF Un_upper2]}; |
|
581 end; |
|
582 |
|
583 local |
|
584 fun mk_UnIN' 0 = @{thm UnI2} |
|
585 | mk_UnIN' m = mk_UnIN' (m - 1) RS @{thm UnI1}; |
|
586 in |
|
587 fun mk_UnIN 1 1 = @{thm TrueE[OF TrueI]} |
|
588 | mk_UnIN n 1 = Library.foldr1 (op RS o swap) (replicate (n - 1) @{thm UnI1}) |
|
589 | mk_UnIN n m = mk_UnIN' (n - m) |
|
590 end; |
|
591 |
|
592 fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys); |
|
593 |
|
594 fun transpose [] = [] |
|
595 | transpose ([] :: xss) = transpose xss |
|
596 | transpose xss = map hd xss :: transpose (map tl xss); |
|
597 |
|
598 fun seq_conds f n k xs = |
|
599 if k = n then |
|
600 map (f false) (take (k - 1) xs) |
|
601 else |
|
602 let val (negs, pos) = split_last (take k xs) in |
|
603 map (f false) negs @ [f true pos] |
|
604 end; |
|
605 |
|
606 fun mk_unabs_def 0 thm = thm |
|
607 | mk_unabs_def n thm = mk_unabs_def (n - 1) thm RS @{thm spec[OF iffD1[OF fun_eq_iff]]}; |
|
608 |
|
609 fun is_refl thm = |
|
610 op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of thm))) |
|
611 handle TERM _ => false; |
|
612 |
|
613 val no_refl = filter_out is_refl; |
|
614 val no_reflexive = filter_out Thm.is_reflexive; |
|
615 |
|
616 fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms); |
|
617 fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms); |
|
618 |
|
619 end; |