separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
1 (* Title: HOL/Codatatype/Tools/bnf_util.ML
2 Author: Dmitriy Traytel, TU Muenchen
5 Library for bounded natural functors.
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 ->
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
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
63 val strip_typeN: int -> typ -> typ list * typ
65 val mk_optionT: typ -> typ
66 val mk_relT: typ * typ -> typ
67 val dest_relT: typ -> typ * typ
68 val mk_sumT: typ * typ -> typ
71 val fst_const: typ -> term
72 val snd_const: typ -> term
73 val Id_const: typ -> term
75 val mk_Ball: term -> term -> term
76 val mk_Bex: term -> term -> term
77 val mk_Card_order: term -> term
78 val mk_Field: term -> term
79 val mk_Gr: term -> term -> term
80 val mk_IfN: typ -> term list -> term list -> term
81 val mk_Trueprop_eq: term * term -> term
82 val mk_UNION: term -> term -> term
83 val mk_Union: typ -> term
84 val mk_card_binop: string -> (typ * typ -> typ) -> term -> term -> term
85 val mk_card_of: term -> term
86 val mk_card_order: term -> term
87 val mk_ccexp: term -> term -> term
88 val mk_cexp: term -> term -> term
89 val mk_cinfinite: term -> term
90 val mk_collect: term list -> typ -> term
91 val mk_converse: term -> term
92 val mk_cprod: term -> term -> term
93 val mk_csum: term -> term -> term
94 val mk_dir_image: term -> term -> term
95 val mk_image: term -> term
96 val mk_in: term list -> term list -> typ -> term
97 val mk_ordLeq: term -> term -> term
98 val mk_rel_comp: term * term -> term
99 val mk_subset: term -> term -> term
100 val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term
102 val list_all_free: term list -> term -> term
103 val list_exists_free: term list -> term -> term
105 (*parameterized terms*)
106 val mk_nthN: int -> term -> int -> term
108 (*parameterized thms*)
109 val mk_Un_upper: int -> int -> thm
110 val mk_conjIN: int -> thm
111 val mk_conjunctN: int -> int -> thm
112 val conj_dests: int -> thm -> thm list
113 val mk_disjIN: int -> int -> thm
114 val mk_nthI: int -> int -> thm
115 val mk_nth_conv: int -> int -> thm
116 val mk_ordLeq_csum: int -> int -> thm -> thm
117 val mk_UnIN: int -> int -> thm
121 val mk_sym: thm -> thm
122 val mk_trans: thm -> thm -> thm
123 val mk_unabs_def: int -> thm -> thm
125 val mk_permute: ''a list -> ''a list -> 'b list -> 'b list
126 val find_indices: ''a list -> ''a list -> int list
128 val certifyT: Proof.context -> typ -> ctyp
129 val certify: Proof.context -> term -> cterm
131 val parse_binding_colon: Token.T list -> binding * Token.T list
132 val parse_opt_binding_colon: Token.T list -> binding * Token.T list
134 val typedef: bool -> binding option -> binding * (string * sort) list * mixfix -> term ->
135 (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory
137 val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic
138 val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int ->
140 val CONJ_WRAP_GEN: tactic -> ('a -> tactic) -> 'a list -> tactic
141 val CONJ_WRAP_GEN': (int -> tactic) -> ('a -> int -> tactic) -> 'a list -> int -> tactic
142 val CONJ_WRAP: ('a -> tactic) -> 'a list -> tactic
143 val CONJ_WRAP': ('a -> int -> tactic) -> 'a list -> int -> tactic
146 structure BNF_Util : BNF_UTIL =
151 fun map3 _ [] [] [] = []
152 | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
153 | map3 _ _ _ _ = raise ListPair.UnequalLengths;
155 fun map4 _ [] [] [] [] = []
156 | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s
157 | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
159 fun map5 _ [] [] [] [] [] = []
160 | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) =
161 f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s
162 | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
164 fun map6 _ [] [] [] [] [] [] = []
165 | map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) =
166 f x1 x2 x3 x4 x5 x6 :: map6 f x1s x2s x3s x4s x5s x6s
167 | map6 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
169 fun map7 _ [] [] [] [] [] [] [] = []
170 | map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) =
171 f x1 x2 x3 x4 x5 x6 x7 :: map7 f x1s x2s x3s x4s x5s x6s x7s
172 | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
174 fun map8 _ [] [] [] [] [] [] [] [] = []
175 | map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) =
176 f x1 x2 x3 x4 x5 x6 x7 x8 :: map8 f x1s x2s x3s x4s x5s x6s x7s x8s
177 | map8 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
179 fun map9 _ [] [] [] [] [] [] [] [] [] = []
180 | map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
181 (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) =
182 f x1 x2 x3 x4 x5 x6 x7 x8 x9 :: map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s
183 | map9 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
185 fun map10 _ [] [] [] [] [] [] [] [] [] [] = []
186 | map10 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
187 (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) =
188 f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 :: map10 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s
189 | map10 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
191 fun map11 _ [] [] [] [] [] [] [] [] [] [] [] = []
192 | map11 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
193 (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) =
194 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
195 | map11 _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
197 fun map12 _ [] [] [] [] [] [] [] [] [] [] [] [] = []
198 | map12 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
199 (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) =
200 f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ::
201 map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s
202 | map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
204 fun fold_map2 _ [] [] acc = ([], acc)
205 | fold_map2 f (x1::x1s) (x2::x2s) acc =
207 val (x, acc') = f x1 x2 acc;
208 val (xs, acc'') = fold_map2 f x1s x2s acc';
209 in (x :: xs, acc'') end
210 | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths;
212 fun fold_map3 _ [] [] [] acc = ([], acc)
213 | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc =
215 val (x, acc') = f x1 x2 x3 acc;
216 val (xs, acc'') = fold_map3 f x1s x2s x3s acc';
217 in (x :: xs, acc'') end
218 | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths;
220 fun fold_map4 _ [] [] [] [] acc = ([], acc)
221 | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
223 val (x, acc') = f x1 x2 x3 x4 acc;
224 val (xs, acc'') = fold_map4 f x1s x2s x3s x4s acc';
225 in (x :: xs, acc'') end
226 | fold_map4 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
228 fun fold_map5 _ [] [] [] [] [] acc = ([], acc)
229 | fold_map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) acc =
231 val (x, acc') = f x1 x2 x3 x4 x5 acc;
232 val (xs, acc'') = fold_map5 f x1s x2s x3s x4s x5s acc';
233 in (x :: xs, acc'') end
234 | fold_map5 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
236 fun fold_map6 _ [] [] [] [] [] [] acc = ([], acc)
237 | fold_map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) acc =
239 val (x, acc') = f x1 x2 x3 x4 x5 x6 acc;
240 val (xs, acc'') = fold_map6 f x1s x2s x3s x4s x5s x6s acc';
241 in (x :: xs, acc'') end
242 | fold_map6 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
244 fun fold_map7 _ [] [] [] [] [] [] [] acc = ([], acc)
245 | fold_map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) acc =
247 val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 acc;
248 val (xs, acc'') = fold_map7 f x1s x2s x3s x4s x5s x6s x7s acc';
249 in (x :: xs, acc'') end
250 | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
252 (*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*)
253 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt);
254 fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt);
256 val parse_binding_colon = Parse.binding --| @{keyword ":"};
257 val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
259 (*TODO: is this really different from Typedef.add_typedef_global?*)
260 fun typedef def opt_name typ set opt_morphs tac lthy =
262 val ((name, info), (lthy, lthy_old)) =
264 |> Typedef.add_typedef def opt_name typ set opt_morphs tac
265 ||> `Local_Theory.restore;
266 val phi = Proof_Context.export_morphism lthy_old lthy;
268 ((name, Typedef.transform_info phi info), lthy)
271 (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*)
272 fun WRAP gen_before gen_after xs core_tac =
273 fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac;
275 fun WRAP' gen_before gen_after xs core_tac =
276 fold_rev (fn x => fn tac => gen_before x THEN' tac THEN' gen_after x) xs core_tac;
278 fun CONJ_WRAP_GEN conj_tac gen_tac xs =
279 let val (butlast, last) = split_last xs;
280 in WRAP (fn thm => conj_tac THEN gen_tac thm) (K all_tac) butlast (gen_tac last) end;
282 fun CONJ_WRAP_GEN' conj_tac gen_tac xs =
283 let val (butlast, last) = split_last xs;
284 in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end;
286 (*not eta-converted because of monotype restriction*)
287 fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac;
288 fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac;
292 (* Term construction *)
294 (** Fresh variables **)
296 fun nonzero_string_of_int 0 = ""
297 | nonzero_string_of_int n = string_of_int n;
299 val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
301 fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
302 val mk_TFreess = fold_map mk_TFrees;
304 fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n);
306 fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names;
307 fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
308 fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
309 fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss;
310 fun mk_Freessss x Tssss = fold_map2 mk_Freesss (mk_names (length Tssss) x) Tssss;
311 fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
312 fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
317 fun strip_typeN 0 T = ([], T)
318 | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T
319 | strip_typeN n T = raise TYPE ("strip_typeN", [T], []);
321 fun mk_optionT T = Type (@{type_name option}, [T]);
322 val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT;
323 val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT;
324 fun mk_sumT (LT, RT) = Type (@{type_name Sum_Type.sum}, [LT, RT]);
325 fun mk_partial_funT (ranT, domT) = domT --> mk_optionT ranT;
330 fun fst_const T = Const (@{const_name fst}, T --> fst (HOLogic.dest_prodT T));
331 fun snd_const T = Const (@{const_name snd}, T --> snd (HOLogic.dest_prodT T));
332 fun Id_const T = Const (@{const_name Id}, mk_relT (T, T));
337 val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
339 fun mk_IfN _ _ [t] = t
340 | mk_IfN T (c :: cs) (t :: ts) =
341 Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts;
345 val RT = dest_relT (fastype_of R);
346 val RST = mk_relT (snd RT, fst RT);
347 in Const (@{const_name converse}, fastype_of R --> RST) $ R end;
349 fun mk_rel_comp (R, S) =
351 val RT = fastype_of R;
352 val ST = fastype_of S;
353 val RST = mk_relT (fst (dest_relT RT), snd (dest_relT ST));
354 in Const (@{const_name relcomp}, RT --> ST --> RST) $ R $ S end;
357 let val ((AT, BT), FT) = `dest_funT (fastype_of f);
358 in Const (@{const_name Gr}, HOLogic.mk_setT AT --> FT --> mk_relT (AT, BT)) $ A $ f end;
361 let val (T, U) = dest_funT (fastype_of f);
362 in Const (@{const_name image},
363 (T --> U) --> (HOLogic.mk_setT T) --> (HOLogic.mk_setT U)) $ f end;
366 Const (@{const_name Ball}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f;
369 Const (@{const_name Bex}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f;
372 let val (T, U) = dest_funT (fastype_of f);
373 in Const (@{const_name SUPR}, fastype_of X --> (T --> U) --> U) $ X $ f end;
376 Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T);
379 let val T = fst (dest_relT (fastype_of r));
380 in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;
382 fun mk_card_order bd =
384 val T = fastype_of bd;
385 val AT = fst (dest_relT T);
387 Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $
388 (HOLogic.mk_UNIV AT) $ bd
391 fun mk_Card_order bd =
393 val T = fastype_of bd;
394 val AT = fst (dest_relT T);
396 Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $
400 fun mk_cinfinite bd =
401 Const (@{const_name cinfinite}, fastype_of bd --> HOLogic.boolT) $ bd;
403 fun mk_ordLeq t1 t2 =
404 HOLogic.mk_mem (HOLogic.mk_prod (t1, t2),
405 Const (@{const_name ordLeq}, mk_relT (fastype_of t1, fastype_of t2)));
409 val AT = fastype_of A;
410 val T = HOLogic.dest_setT AT;
412 Const (@{const_name card_of}, AT --> mk_relT (T, T)) $ A
415 fun mk_dir_image r f =
416 let val (T, U) = dest_funT (fastype_of f);
417 in Const (@{const_name dir_image}, mk_relT (T, T) --> (T --> U) --> mk_relT (U, U)) $ r $ f end;
420 (*(nth sets i) must be of type "T --> 'ai set"*)
421 fun mk_in As sets T =
423 fun in_single set A =
424 let val AT = fastype_of A;
425 in Const (@{const_name less_eq},
426 AT --> AT --> HOLogic.boolT) $ (set $ Free ("x", T)) $ A end;
429 then HOLogic.mk_Collect ("x", T, foldr1 (HOLogic.mk_conj) (map2 in_single sets As))
430 else HOLogic.mk_UNIV T
433 fun mk_wpull A B1 B2 f1 f2 pseudo p1 p2 =
435 val AT = fastype_of A;
436 val BT1 = fastype_of B1;
437 val BT2 = fastype_of B2;
438 val FT1 = fastype_of f1;
439 val FT2 = fastype_of f2;
440 val PT1 = fastype_of p1;
441 val PT2 = fastype_of p2;
442 val T1 = HOLogic.dest_setT BT1;
443 val T2 = HOLogic.dest_setT BT2;
444 val domP = domain_type PT1;
445 val ranF = range_type FT1;
446 val _ = if is_some pseudo orelse
447 (HOLogic.dest_setT AT = domP andalso
448 domain_type FT1 = T1 andalso
449 domain_type FT2 = T2 andalso
450 domain_type PT2 = domP andalso
451 range_type PT1 = T1 andalso
452 range_type PT2 = T2 andalso
453 range_type FT2 = ranF)
454 then () else raise TYPE ("mk_wpull", [BT1, BT2, FT1, FT2, PT1, PT2], []);
457 NONE => Const (@{const_name wpull},
458 AT --> BT1 --> BT2 --> FT1 --> FT2 --> PT1 --> PT2 --> HOLogic.boolT) $
459 A $ B1 $ B2 $ f1 $ f2 $ p1 $ p2
460 | SOME (e1, e2) => Const (@{const_name wppull},
461 AT --> BT1 --> BT2 --> FT1 --> FT2 --> fastype_of e1 --> fastype_of e2 -->
462 PT1 --> PT2 --> HOLogic.boolT) $
463 A $ B1 $ B2 $ f1 $ f2 $ e1 $ e2 $ p1 $ p2)
466 fun mk_subset t1 t2 =
467 Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;
469 fun mk_card_binop binop typop t1 t2 =
471 val (T1, relT1) = `(fst o dest_relT) (fastype_of t1);
472 val (T2, relT2) = `(fst o dest_relT) (fastype_of t2);
474 Const (binop, relT1 --> relT2 --> mk_relT (typop (T1, T2), typop (T1, T2))) $ t1 $ t2
477 val mk_csum = mk_card_binop @{const_name csum} mk_sumT;
478 val mk_cprod = mk_card_binop @{const_name cprod} HOLogic.mk_prodT;
479 val mk_cexp = mk_card_binop @{const_name cexp} mk_partial_funT;
480 val mk_ccexp = mk_card_binop @{const_name ccexp} mk_partial_funT;
481 val ctwo = @{term ctwo};
483 fun mk_collect xs defT =
484 let val T = (case xs of [] => defT | (x::_) => fastype_of x);
485 in Const (@{const_name collect}, HOLogic.mk_setT T --> T) $ (HOLogic.mk_set T xs) end;
487 fun mk_permute src dest xs = map (nth xs o (fn x => find_index ((curry op =) x) src)) dest;
490 fold_rev (fn free => fn P =>
491 let val (x, T) = Term.dest_Free free;
492 in HOLogic.all_const T $ Term.absfree (x, T) P end);
494 val list_exists_free =
495 fold_rev (fn free => fn P =>
496 let val (x, T) = Term.dest_Free free;
497 in HOLogic.exists_const T $ Term.absfree (x, T) P end);
499 fun find_indices xs ys = map_filter I
500 (map_index (fn (i, y) => if member (op =) xs y then SOME i else NONE) ys);
502 fun mk_trans thm1 thm2 = trans OF [thm1, thm2];
503 fun mk_sym thm = sym OF [thm];
505 (*TODO: antiquote heavily used theorems once*)
506 val ctrans = @{thm ordLeq_transitive};
507 val o_apply = @{thm o_apply};
509 fun mk_nthN 1 t 1 = t
510 | mk_nthN _ t 1 = HOLogic.mk_fst t
511 | mk_nthN 2 t 2 = HOLogic.mk_snd t
512 | mk_nthN n t m = mk_nthN (n - 1) (HOLogic.mk_snd t) (m - 1);
514 fun mk_nth_conv n m =
516 fun thm b = if b then @{thm fst_snd} else @{thm snd_snd}
517 fun mk_nth_conv _ 1 1 = refl
518 | mk_nth_conv _ _ 1 = @{thm fst_conv}
519 | mk_nth_conv _ 2 2 = @{thm snd_conv}
520 | mk_nth_conv b _ 2 = @{thm snd_conv} RS thm b
521 | mk_nth_conv b n m = mk_nth_conv false (n - 1) (m - 1) RS thm b;
522 in mk_nth_conv (not (m = n)) n m end;
524 fun mk_nthI 1 1 = @{thm TrueE[OF TrueI]}
525 | mk_nthI n m = fold (curry op RS) (replicate (m - 1) @{thm sndI})
526 (if m = n then @{thm TrueE[OF TrueI]} else @{thm fstI});
528 fun mk_conjunctN 1 1 = @{thm TrueE[OF TrueI]}
529 | mk_conjunctN _ 1 = conjunct1
530 | mk_conjunctN 2 2 = conjunct2
531 | mk_conjunctN n m = conjunct2 RS (mk_conjunctN (n - 1) (m - 1));
533 fun conj_dests n thm = map (fn k => thm RS mk_conjunctN n k) (1 upto n);
535 fun mk_conjIN 1 = @{thm TrueE[OF TrueI]}
536 | mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI);
538 fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]}
539 | mk_disjIN _ 1 = disjI1
540 | mk_disjIN 2 2 = disjI2
541 | mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2;
543 fun mk_ordLeq_csum 1 1 thm = thm
544 | mk_ordLeq_csum _ 1 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum1}]
545 | mk_ordLeq_csum 2 2 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum2}]
546 | mk_ordLeq_csum n m thm = @{thm ordLeq_transitive} OF
547 [mk_ordLeq_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}];
550 fun mk_Un_upper' 0 = subset_refl
551 | mk_Un_upper' 1 = @{thm Un_upper1}
552 | mk_Un_upper' k = Library.foldr (op RS o swap)
553 (replicate (k - 1) @{thm subset_trans[OF Un_upper1]}, @{thm Un_upper1});
555 fun mk_Un_upper 1 1 = subset_refl
556 | mk_Un_upper n 1 = mk_Un_upper' (n - 2) RS @{thm subset_trans[OF Un_upper1]}
557 | mk_Un_upper n m = mk_Un_upper' (n - m) RS @{thm subset_trans[OF Un_upper2]};
561 fun mk_UnIN' 0 = @{thm UnI2}
562 | mk_UnIN' m = mk_UnIN' (m - 1) RS @{thm UnI1};
564 fun mk_UnIN 1 1 = @{thm TrueE[OF TrueI]}
565 | mk_UnIN n 1 = Library.foldr1 (op RS o swap) (replicate (n - 1) @{thm UnI1})
566 | mk_UnIN n m = mk_UnIN' (n - m)
569 fun interleave xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys);
571 fun transpose [] = []
572 | transpose ([] :: xss) = transpose xss
573 | transpose xss = map hd xss :: transpose (map tl xss);
575 fun seq_conds f n k xs =
577 map (f false) (take (k - 1) xs)
579 let val (negs, pos) = split_last (take k xs) in
580 map (f false) negs @ [f true pos]
583 fun mk_unabs_def 0 thm = thm
584 | mk_unabs_def n thm = mk_unabs_def (n - 1) thm RS @{thm spec[OF iffD1[OF fun_eq_iff]]};