1 (* Title: HOL/Tools/Nitpick/nitpick_preproc.ML
2 Author: Jasmin Blanchette, TU Muenchen
3 Copyright 2008, 2009, 2010
5 Nitpick's HOL preprocessor.
8 signature NITPICK_PREPROC =
10 type hol_context = Nitpick_HOL.hol_context
13 -> ((term list * term list) * (bool * bool)) * term * bool
16 structure Nitpick_Preproc : NITPICK_PREPROC =
22 (* polarity -> string -> bool *)
23 fun is_positive_existential polar quant_s =
24 (polar = Pos andalso quant_s = @{const_name Ex}) orelse
25 (polar = Neg andalso quant_s <> @{const_name Ex})
27 (** Binary coding of integers **)
29 (* If a formula contains a numeral whose absolute value is more than this
30 threshold, the unary coding is likely not to work well and we prefer the
32 val binary_int_threshold = 3
35 fun may_use_binary_ints (t1 $ t2) =
36 may_use_binary_ints t1 andalso may_use_binary_ints t2
37 | may_use_binary_ints (t as Const (s, _)) =
38 t <> @{const Suc} andalso
39 not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
40 @{const_name nat_gcd}, @{const_name nat_lcm},
41 @{const_name Frac}, @{const_name norm_frac}] s)
42 | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
43 | may_use_binary_ints _ = true
44 fun should_use_binary_ints (t1 $ t2) =
45 should_use_binary_ints t1 orelse should_use_binary_ints t2
46 | should_use_binary_ints (Const (s, T)) =
47 ((s = @{const_name times} orelse s = @{const_name div}) andalso
48 is_integer_type (body_type T)) orelse
49 (String.isPrefix numeral_prefix s andalso
50 let val n = the (Int.fromString (unprefix numeral_prefix s)) in
51 n < ~ binary_int_threshold orelse n > binary_int_threshold
53 | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
54 | should_use_binary_ints _ = false
58 (* theory -> term -> int Termtab.tab -> int Termtab.tab *)
59 fun add_to_uncurry_table thy t =
61 (* term -> term list -> int Termtab.tab -> int Termtab.tab *)
62 fun aux (t1 $ t2) args table =
63 let val table = aux t2 [] table in aux t1 (t2 :: args) table end
64 | aux (Abs (_, _, t')) _ table = aux t' [] table
65 | aux (t as Const (x as (s, _))) args table =
66 if is_built_in_const thy [(NONE, true)] true x orelse
67 is_constr_like thy x orelse
68 is_sel s orelse s = @{const_name Sigma} then
71 Termtab.map_default (t, 65536) (curry Int.min (length args)) table
72 | aux _ _ table = table
75 (* int -> int -> string *)
76 fun uncurry_prefix_for k j =
77 uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
79 (* int Termtab.tab term -> term *)
80 fun uncurry_term table t =
82 (* term -> term list -> term *)
83 fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args)
84 | aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args)
85 | aux (t as Const (s, T)) args =
86 (case Termtab.lookup table t of
90 val arg_Ts = strip_n_binders n T |> fst
92 if is_iterator_type (hd arg_Ts) then
94 else case find_index (not_equal bool_T) arg_Ts of
97 val ((before_args, tuple_args), after_args) =
98 args |> chop n |>> chop j
99 val ((before_arg_Ts, tuple_arg_Ts), rest_T) =
100 T |> strip_n_binders n |>> chop j
101 val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts
106 betapplys (Const (uncurry_prefix_for (n - j) j ^ s,
107 before_arg_Ts ---> tuple_T --> rest_T),
108 before_args @ [mk_flat_tuple tuple_T tuple_args] @
113 | NONE => betapplys (t, args))
114 | aux t args = betapplys (t, args)
119 (* hol_context -> typ -> term -> term *)
120 fun constr_expand (hol_ctxt as {thy, stds, ...}) T t =
122 Const x => if is_constr_like thy x then t else raise SAME ()
123 | _ => raise SAME ())
127 if is_pair_type T then
128 let val (T1, T2) = HOLogic.dest_prodT T in
129 (@{const_name Pair}, T1 --> T2 --> T)
132 datatype_constrs hol_ctxt T |> hd
133 val arg_Ts = binder_types T'
135 list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t)
136 (index_seq 0 (length arg_Ts)) arg_Ts)
139 (* hol_context -> bool -> term -> term *)
140 fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
144 fun box_relational_operator_type (Type ("fun", Ts)) =
145 Type ("fun", map box_relational_operator_type Ts)
146 | box_relational_operator_type (Type ("*", Ts)) =
147 Type ("*", map (box_type hol_ctxt InPair) Ts)
148 | box_relational_operator_type T = T
149 (* (term -> term) -> int -> term -> term *)
150 fun coerce_bound_no f j t =
152 t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
153 | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
154 | Bound j' => if j' = j then f t else t
156 (* typ -> typ -> term -> term *)
157 fun coerce_bound_0_in_term new_T old_T =
158 old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
159 (* typ list -> typ -> term -> term *)
160 and coerce_term Ts new_T old_T t =
161 if old_T = new_T then
164 case (new_T, old_T) of
165 (Type (new_s, new_Ts as [new_T1, new_T2]),
166 Type ("fun", [old_T1, old_T2])) =>
167 (case eta_expand Ts t 1 of
170 t' |> coerce_bound_0_in_term new_T1 old_T1
171 |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
172 |> Envir.eta_contract
174 ? construct_value thy stds
175 (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
177 | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
178 \coerce_term", [t']))
179 | (Type (new_s, new_Ts as [new_T1, new_T2]),
180 Type (old_s, old_Ts as [old_T1, old_T2])) =>
181 if old_s = @{type_name fun_box} orelse
182 old_s = @{type_name pair_box} orelse old_s = "*" then
183 case constr_expand hol_ctxt old_T t of
184 Const (@{const_name FunBox}, _) $ t1 =>
185 if new_s = "fun" then
186 coerce_term Ts new_T (Type ("fun", old_Ts)) t1
188 construct_value thy stds
189 (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
190 [coerce_term Ts (Type ("fun", new_Ts))
191 (Type ("fun", old_Ts)) t1]
192 | Const _ $ t1 $ t2 =>
193 construct_value thy stds
194 (if new_s = "*" then @{const_name Pair}
195 else @{const_name PairBox}, new_Ts ---> new_T)
196 [coerce_term Ts new_T1 old_T1 t1,
197 coerce_term Ts new_T2 old_T2 t2]
198 | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
201 raise TYPE ("coerce_term", [new_T, old_T], [t])
202 | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
203 (* indexname * typ -> typ * term -> typ option list -> typ option list *)
204 fun add_boxed_types_for_var (z as (_, T)) (T', t') =
206 Var z' => z' = z ? insert (op =) T'
207 | Const (@{const_name Pair}, _) $ t1 $ t2 =>
209 Type (_, [T1, T2]) =>
210 fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
211 | _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\
212 \add_boxed_types_for_var", [T'], []))
213 | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
214 (* typ list -> typ list -> term -> indexname * typ -> typ *)
215 fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
217 @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
218 | Const (s0, _) $ t1 $ _ =>
219 if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
221 val (t', args) = strip_comb t1
222 val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
224 case fold (add_boxed_types_for_var z)
225 (fst (strip_n_binders (length args) T') ~~ args) [] of
232 (* typ list -> typ list -> polarity -> string -> typ -> string -> typ
234 and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t =
237 if polar = Neut orelse is_positive_existential polar quant_s then
238 box_type hol_ctxt InFunLHS abs_T
241 val body_T = body_type quant_T
243 Const (quant_s, (abs_T' --> body_T) --> body_T)
244 $ Abs (abs_s, abs_T',
245 t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar)
247 (* typ list -> typ list -> string -> typ -> term -> term -> term *)
248 and do_equals new_Ts old_Ts s0 T0 t1 t2 =
250 val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2)
251 val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
252 val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
254 list_comb (Const (s0, T --> T --> body_type T0),
255 map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
257 (* string -> typ -> term *)
258 and do_description_operator s T =
259 let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
260 Const (s, (T1 --> bool_T) --> T1)
262 (* typ list -> typ list -> polarity -> term -> term *)
263 and do_term new_Ts old_Ts polar t =
265 Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
266 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
267 | Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 =>
268 do_equals new_Ts old_Ts s0 T0 t1 t2
269 | @{const "==>"} $ t1 $ t2 =>
270 @{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
271 $ do_term new_Ts old_Ts polar t2
272 | @{const Pure.conjunction} $ t1 $ t2 =>
273 @{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1
274 $ do_term new_Ts old_Ts polar t2
275 | @{const Trueprop} $ t1 =>
276 @{const Trueprop} $ do_term new_Ts old_Ts polar t1
277 | @{const Not} $ t1 =>
278 @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
279 | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
280 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
281 | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
282 do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
283 | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
284 do_equals new_Ts old_Ts s0 T0 t1 t2
285 | @{const "op &"} $ t1 $ t2 =>
286 @{const "op &"} $ do_term new_Ts old_Ts polar t1
287 $ do_term new_Ts old_Ts polar t2
288 | @{const "op |"} $ t1 $ t2 =>
289 @{const "op |"} $ do_term new_Ts old_Ts polar t1
290 $ do_term new_Ts old_Ts polar t2
291 | @{const "op -->"} $ t1 $ t2 =>
292 @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
293 $ do_term new_Ts old_Ts polar t2
294 | Const (s as @{const_name The}, T) => do_description_operator s T
295 | Const (s as @{const_name Eps}, T) => do_description_operator s T
296 | Const (s as @{const_name Tha}, T) => do_description_operator s T
297 | Const (x as (s, T)) =>
298 Const (s, if s = @{const_name converse} orelse
299 s = @{const_name trancl} then
300 box_relational_operator_type T
301 else if String.isPrefix quot_normal_prefix s then
302 let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
305 else if is_built_in_const thy stds fast_descrs x orelse
306 s = @{const_name Sigma} then
308 else if is_constr_like thy x then
309 box_type hol_ctxt InConstr T
311 orelse is_rep_fun thy x then
312 box_type hol_ctxt InSel T
314 box_type hol_ctxt InExpr T)
315 | t1 $ Abs (s, T, t2') =>
317 val t1 = do_term new_Ts old_Ts Neut t1
318 val T1 = fastype_of1 (new_Ts, t1)
319 val (s1, Ts1) = dest_Type T1
320 val T' = hd (snd (dest_Type (hd Ts1)))
321 val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
322 val T2 = fastype_of1 (new_Ts, t2)
323 val t2 = coerce_term new_Ts (hd Ts1) T2 t2
325 betapply (if s1 = "fun" then
328 select_nth_constr_arg thy stds
329 (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
330 (Type ("fun", Ts1)), t2)
334 val t1 = do_term new_Ts old_Ts Neut t1
335 val T1 = fastype_of1 (new_Ts, t1)
336 val (s1, Ts1) = dest_Type T1
337 val t2 = do_term new_Ts old_Ts Neut t2
338 val T2 = fastype_of1 (new_Ts, t2)
339 val t2 = coerce_term new_Ts (hd Ts1) T2 t2
341 betapply (if s1 = "fun" then
344 select_nth_constr_arg thy stds
345 (@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0
346 (Type ("fun", Ts1)), t2)
348 | Free (s, T) => Free (s, box_type hol_ctxt InExpr T)
349 | Var (z as (x, T)) =>
350 Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z
351 else box_type hol_ctxt InExpr T)
354 Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
355 in do_term [] [] Pos orig_t end
357 (** Destruction of constructors **)
359 val val_var_prefix = nitpick_prefix ^ "v"
361 (* typ list -> int -> int -> int -> term -> term *)
362 fun fresh_value_var Ts k n j t =
363 Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t))
365 (* typ list -> term -> bool *)
366 fun has_heavy_bounds_or_vars Ts t =
368 (* typ list -> bool *)
370 | aux [T] = is_fun_type T orelse is_pair_type T
372 in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
374 (* hol_context -> typ list -> bool -> int -> int -> term -> term list
375 -> term list -> term * term list *)
376 fun pull_out_constr_comb ({thy, stds, ...} : hol_context) Ts relax k level t
378 let val t_comb = list_comb (t, args) in
381 if not relax andalso is_constr thy stds x andalso
382 not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
383 has_heavy_bounds_or_vars Ts t_comb andalso
384 not (loose_bvar (t_comb, level)) then
386 val (j, seen) = case find_index (curry (op =) t_comb) seen of
387 ~1 => (0, t_comb :: seen)
389 in (fresh_value_var Ts k (length seen) j t_comb, seen) end
392 | _ => (t_comb, seen)
395 (* (term -> term) -> typ list -> int -> term list -> term list *)
396 fun equations_for_pulled_out_constrs mk_eq Ts k seen =
397 let val n = length seen in
398 map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t))
402 (* hol_context -> bool -> term -> term *)
403 fun pull_out_universal_constrs hol_ctxt def t =
405 val k = maxidx_of_term t + 1
406 (* typ list -> bool -> term -> term list -> term list -> term * term list *)
407 fun do_term Ts def t args seen =
409 (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
410 do_eq_or_imp Ts true def t0 t1 t2 seen
411 | (t0 as @{const "==>"}) $ t1 $ t2 =>
412 if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
413 | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
414 do_eq_or_imp Ts true def t0 t1 t2 seen
415 | (t0 as @{const "op -->"}) $ t1 $ t2 =>
416 do_eq_or_imp Ts false def t0 t1 t2 seen
418 let val (t', seen) = do_term (T :: Ts) def t' [] seen in
419 (list_comb (Abs (s, T, t'), args), seen)
422 let val (t2, seen) = do_term Ts def t2 [] seen in
423 do_term Ts def t1 (t2 :: args) seen
425 | _ => pull_out_constr_comb hol_ctxt Ts def k 0 t args seen
426 (* typ list -> bool -> bool -> term -> term -> term -> term list
427 -> term * term list *)
428 and do_eq_or_imp Ts eq def t0 t1 t2 seen =
430 val (t2, seen) = if eq andalso def then (t2, seen)
431 else do_term Ts false t2 [] seen
432 val (t1, seen) = do_term Ts false t1 [] seen
433 in (t0 $ t1 $ t2, seen) end
434 val (concl, seen) = do_term [] def t [] []
436 Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k
440 (* term -> term -> term *)
442 HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
444 (* hol_context -> term -> term *)
445 fun pull_out_existential_constrs hol_ctxt t =
447 val k = maxidx_of_term t + 1
448 (* typ list -> int -> term -> term list -> term list -> term * term list *)
449 fun aux Ts num_exists t args seen =
451 (t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) =>
453 val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] []
455 (* unit -> term list *)
456 fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen'
458 (equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen'
459 |> List.foldl s_conj t1 |> fold mk_exists (vars ())
460 |> curry3 Abs s1 T1 |> curry (op $) t0, seen)
463 let val (t2, seen) = aux Ts num_exists t2 [] seen in
464 aux Ts num_exists t1 (t2 :: args) seen
468 val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen)
469 in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end
471 if num_exists > 0 then
472 pull_out_constr_comb hol_ctxt Ts false k num_exists t args seen
474 (list_comb (t, args), seen)
475 in aux [] 0 t [] [] |> fst end
477 (* hol_context -> bool -> term -> term *)
478 fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
481 val num_occs_of_var =
482 fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
484 (* bool -> term -> term *)
485 fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
486 aux_eq careful true t0 t1 t2
487 | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
488 t0 $ aux false t1 $ aux careful t2
489 | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
490 aux_eq careful true t0 t1 t2
491 | aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) =
492 t0 $ aux false t1 $ aux careful t2
493 | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
494 | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
496 (* bool -> bool -> term -> term -> term -> term *)
497 and aux_eq careful pass1 t0 t1 t2 =
500 else if axiom andalso is_Var t2 andalso
501 num_occs_of_var (dest_Var t2) = 1 then
503 else case strip_comb t2 of
504 (* The first case is not as general as it could be. *)
505 (Const (@{const_name PairBox}, _),
506 [Const (@{const_name fst}, _) $ Var z1,
507 Const (@{const_name snd}, _) $ Var z2]) =>
508 if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
510 | (Const (x as (s, T)), args) =>
511 let val arg_Ts = binder_types T in
512 if length arg_Ts = length args andalso
513 (is_constr thy stds x orelse s = @{const_name Pair}) andalso
514 (not careful orelse not (is_Var t1) orelse
515 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
516 discriminate_value hol_ctxt x t1 ::
517 map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
522 | _ => raise SAME ())
523 |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
524 handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
525 else t0 $ aux false t2 $ aux false t1
526 (* styp -> term -> int -> typ -> term -> term *)
527 and sel_eq x t n nth_T nth_t =
528 HOLogic.eq_const nth_T $ nth_t
529 $ select_nth_constr_arg thy stds x t n nth_T
533 (** Destruction of universal and existential equalities **)
536 fun curry_assms (@{const "==>"} $ (@{const Trueprop}
537 $ (@{const "op &"} $ t1 $ t2)) $ t3) =
538 curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3))
539 | curry_assms (@{const "==>"} $ t1 $ t2) =
540 @{const "==>"} $ curry_assms t1 $ curry_assms t2
544 val destroy_universal_equalities =
546 (* term list -> (indexname * typ) list -> term -> term *)
549 @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
550 | _ => Logic.list_implies (rev prems, t)
551 (* term list -> (indexname * typ) list -> term -> term -> term *)
552 and aux_implies prems zs t1 t2 =
554 Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
555 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
556 aux_eq prems zs z t' t1 t2
557 | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
558 aux_eq prems zs z t' t1 t2
559 | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
560 (* term list -> (indexname * typ) list -> indexname * typ -> term -> term
562 and aux_eq prems zs z t' t1 t2 =
563 if not (member (op =) zs z) andalso
564 not (exists_subterm (curry (op =) (Var z)) t') then
565 aux prems zs (subst_free [(Var z, t')] t2)
567 aux (t1 :: prems) (Term.add_vars t1 zs) t2
570 (* theory -> (typ option * bool) list -> int -> term list -> term list
571 -> (term * term list) option *)
572 fun find_bound_assign thy stds j =
574 (* term list -> term list -> (term * term list) option *)
575 fun do_term _ [] = NONE
576 | do_term seen (t :: ts) =
578 (* bool -> term -> term -> (term * term list) option *)
579 fun do_eq pass1 t1 t2 =
580 (if loose_bvar1 (t2, j) then
581 if pass1 then do_eq false t2 t1 else raise SAME ()
583 Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME ()
584 | Const (s, Type ("fun", [T1, T2])) $ Bound j' =>
586 s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then
587 SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1)
591 | _ => raise SAME ())
592 handle SAME () => do_term (t :: seen) ts
595 Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2
596 | _ => do_term (t :: seen) ts
600 (* int -> term -> term -> term *)
601 fun subst_one_bound j arg t =
603 (* term * int -> term *)
604 fun aux (Bound i, lev) =
605 if i < lev then raise SAME ()
606 else if i = lev then incr_boundvars (lev - j) arg
608 | aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1))
610 (aux (f, lev) $ (aux (t, lev) handle SAME () => t)
611 handle SAME () => f $ aux (t, lev))
612 | aux _ = raise SAME ()
613 in aux (t, j) handle SAME () => t end
615 (* hol_context -> term -> term *)
616 fun destroy_existential_equalities ({thy, stds, ...} : hol_context) =
618 (* string list -> typ list -> term list -> term *)
619 fun kill [] [] ts = foldr1 s_conj ts
620 | kill (s :: ss) (T :: Ts) ts =
621 (case find_bound_assign thy stds (length ss) [] ts of
622 SOME (_, []) => @{const True}
623 | SOME (arg_t, ts) =>
624 kill ss Ts (map (subst_one_bound (length ss)
625 (incr_bv (~1, length ss + 1, arg_t))) ts)
627 Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
628 $ Abs (s, T, kill ss Ts ts))
629 | kill _ _ _ = raise UnequalLengths
630 (* string list -> typ list -> term -> term *)
631 fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =
632 gather (ss @ [s1]) (Ts @ [T1]) t1
633 | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
634 | gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2
636 | gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t))
639 (** Skolemization **)
641 (* int -> int -> string *)
642 fun skolem_prefix_for k j =
643 skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep
645 (* hol_context -> int -> term -> term *)
646 fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...})
649 (* int list -> int list *)
650 val incrs = map (Integer.add 1)
651 (* string list -> typ list -> int list -> int -> polarity -> term -> term *)
652 fun aux ss Ts js depth polar t =
654 (* string -> typ -> string -> typ -> term -> term *)
655 fun do_quantifier quant_s quant_T abs_s abs_T t =
656 if not (loose_bvar1 (t, 0)) then
657 aux ss Ts js depth polar (incr_boundvars ~1 t)
658 else if depth <= skolem_depth andalso
659 is_positive_existential polar quant_s then
661 val j = length (!skolems) + 1
662 val sko_s = skolem_prefix_for (length js) j ^ abs_s
663 val _ = Unsynchronized.change skolems (cons (sko_s, ss))
664 val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
666 val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
668 if null js then betapply (abs_t, sko_t)
669 else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
672 Const (quant_s, quant_T)
674 if is_higher_order_type abs_T then
677 aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
681 Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
682 do_quantifier s0 T0 s1 T1 t1
683 | @{const "==>"} $ t1 $ t2 =>
684 @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
685 $ aux ss Ts js depth polar t2
686 | @{const Pure.conjunction} $ t1 $ t2 =>
687 @{const Pure.conjunction} $ aux ss Ts js depth polar t1
688 $ aux ss Ts js depth polar t2
689 | @{const Trueprop} $ t1 =>
690 @{const Trueprop} $ aux ss Ts js depth polar t1
691 | @{const Not} $ t1 =>
692 @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
693 | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
694 do_quantifier s0 T0 s1 T1 t1
695 | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
696 do_quantifier s0 T0 s1 T1 t1
697 | @{const "op &"} $ t1 $ t2 =>
698 @{const "op &"} $ aux ss Ts js depth polar t1
699 $ aux ss Ts js depth polar t2
700 | @{const "op |"} $ t1 $ t2 =>
701 @{const "op |"} $ aux ss Ts js depth polar t1
702 $ aux ss Ts js depth polar t2
703 | @{const "op -->"} $ t1 $ t2 =>
704 @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
705 $ aux ss Ts js depth polar t2
706 | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
707 t0 $ t1 $ aux ss Ts js depth polar t2
708 | Const (x as (s, T)) =>
709 if is_inductive_pred hol_ctxt x andalso
710 not (is_well_founded_inductive_pred hol_ctxt x) then
712 val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
713 val (pref, connective, set_oper) =
715 (lbfp_prefix, @{const "op |"},
716 @{const_name semilattice_sup_class.sup})
718 (ubfp_prefix, @{const "op &"},
719 @{const_name semilattice_inf_class.inf})
721 fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
722 |> aux ss Ts js depth polar
723 fun neg () = Const (pref ^ s, T)
725 (case polar |> gfp ? flip_polarity of
729 if is_fun_type T then
731 val ((trunk_arg_Ts, rump_arg_T), body_T) =
732 T |> strip_type |>> split_last
733 val set_T = rump_arg_T --> body_T
734 (* (unit -> term) -> term *)
737 map Bound (length trunk_arg_Ts - 1 downto 0))
740 (Const (set_oper, set_T --> set_T --> set_T)
741 $ app pos $ app neg) trunk_arg_Ts
744 connective $ pos () $ neg ())
749 betapply (aux ss Ts [] (skolem_depth + 1) polar t1,
750 aux ss Ts [] depth Neut t2)
751 | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
754 in aux [] [] [] 0 Pos end
756 (** Function specialization **)
758 (* term -> term list *)
759 fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
760 | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
761 | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
763 | params_in_equation _ = []
765 (* styp -> styp -> int list -> term list -> term list -> term -> term *)
766 fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
768 val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0
770 val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t
771 val fixed_params = filter_indices fixed_js (params_in_equation t)
772 (* term list -> term -> term *)
773 fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args)
774 | aux args (t1 $ t2) = aux (aux [] t2 :: args) t1
777 list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
779 let val j = find_index (curry (op =) t) fixed_params in
780 list_comb (if j >= 0 then nth fixed_args j else t, args)
784 (* hol_context -> styp -> (int * term option) list *)
785 fun static_args_in_term ({ersatz_table, ...} : hol_context) x t =
787 (* term -> term list -> term list -> term list list *)
788 fun fun_calls (Abs (_, _, t)) _ = fun_calls t []
789 | fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args)
792 Const (x' as (s', T')) =>
793 x = x' orelse (case AList.lookup (op =) ersatz_table s' of
794 SOME s'' => x = (s'', T')
796 | _ => false) ? cons args
797 (* term list list -> term list list -> term list -> term list list *)
798 fun call_sets [] [] vs = [vs]
799 | call_sets [] uss vs = vs :: call_sets uss [] []
800 | call_sets ([] :: _) _ _ = []
801 | call_sets ((t :: ts) :: tss) uss vs =
802 OrdList.insert TermOrd.term_ord t vs |> call_sets tss (ts :: uss)
803 val sets = call_sets (fun_calls t [] []) [] []
804 val indexed_sets = sets ~~ (index_seq 0 (length sets))
806 fold_rev (fn (set, j) =>
808 [Var _] => AList.lookup (op =) indexed_sets set = SOME j
810 | [t as Const _] => cons (j, SOME t)
811 | [t as Free _] => cons (j, SOME t)
812 | _ => I) indexed_sets []
814 (* hol_context -> styp -> term list -> (int * term option) list *)
815 fun static_args_in_terms hol_ctxt x =
816 map (static_args_in_term hol_ctxt x)
817 #> fold1 (OrdList.inter (prod_ord int_ord (option_ord TermOrd.term_ord)))
819 (* (int * term option) list -> (int * term) list -> int list *)
820 fun overlapping_indices [] _ = []
821 | overlapping_indices _ [] = []
822 | overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') =
823 if j1 < j2 then overlapping_indices ps1' ps2
824 else if j1 > j2 then overlapping_indices ps1 ps2'
825 else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
827 (* typ list -> term -> bool *)
828 fun is_eligible_arg Ts t =
829 let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
831 (is_higher_order_type (fastype_of1 (Ts, t)) andalso
832 forall (not o is_higher_order_type) bad_Ts)
836 fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
838 (* If a constant's definition is picked up deeper than this threshold, we
839 prevent excessive specialization by not specializing it. *)
840 val special_max_depth = 20
842 val bound_var_prefix = "b"
844 (* hol_context -> int -> term -> term *)
845 fun specialize_consts_in_term (hol_ctxt as {specialize, simp_table,
846 special_funs, ...}) depth t =
847 if not specialize orelse depth > special_max_depth then
851 val blacklist = if depth = 0 then []
852 else case term_under_def t of Const x => [x] | _ => []
853 (* term list -> typ list -> term -> term *)
854 fun aux args Ts (Const (x as (s, T))) =
855 ((if not (member (op =) blacklist x) andalso not (null args) andalso
856 not (String.isPrefix special_prefix s) andalso
857 is_equational_fun hol_ctxt x then
859 val eligible_args = filter (is_eligible_arg Ts o snd)
860 (index_seq 0 (length args) ~~ args)
861 val _ = not (null eligible_args) orelse raise SAME ()
862 val old_axs = equational_fun_axioms hol_ctxt x
863 |> map (destroy_existential_equalities hol_ctxt)
864 val static_params = static_args_in_terms hol_ctxt x old_axs
865 val fixed_js = overlapping_indices static_params eligible_args
866 val _ = not (null fixed_js) orelse raise SAME ()
867 val fixed_args = filter_indices fixed_js args
868 val vars = fold Term.add_vars fixed_args []
869 |> sort (TermOrd.fast_indexname_ord o pairself fst)
870 val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js))
873 val live_args = filter_out_indices fixed_js args
874 val extra_args = map Var vars @ map Bound bound_js @ live_args
875 val extra_Ts = map snd vars @ filter_indices bound_js Ts
876 val k = maxidx_of_term t + 1
878 fun var_for_bound_no j =
879 Var ((bound_var_prefix ^
880 nat_subscript (find_index (curry (op =) j) bound_js
883 val fixed_args_in_axiom =
884 map (curry subst_bounds
885 (map var_for_bound_no (index_seq 0 (length Ts))))
888 case AList.lookup (op =) (!special_funs)
889 (x, fixed_js, fixed_args_in_axiom) of
890 SOME x' => list_comb (Const x', extra_args)
893 val extra_args_in_axiom =
894 map Var vars @ map var_for_bound_no bound_js
896 (special_prefix_for (length (!special_funs) + 1) ^ s,
897 extra_Ts @ filter_out_indices fixed_js (binder_types T)
900 map (specialize_fun_axiom x x' fixed_js
901 fixed_args_in_axiom extra_args_in_axiom) old_axs
903 Unsynchronized.change special_funs
904 (cons ((x, fixed_js, fixed_args_in_axiom), x'))
905 val _ = add_simps simp_table s' new_axs
906 in list_comb (Const x', extra_args) end
910 handle SAME () => list_comb (Const x, args))
911 | aux args Ts (Abs (s, T, t)) =
912 list_comb (Abs (s, T, aux [] (T :: Ts) t), args)
913 | aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1
914 | aux args _ t = list_comb (t, args)
917 type special_triple = int list * term list * styp
919 val cong_var_prefix = "c"
921 (* typ -> special_triple -> special_triple -> term *)
922 fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) =
924 val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2)
925 val Ts = binder_types T
926 val max_j = fold (fold Integer.max) [js1, js2] ~1
927 val (eqs, (args1, args2)) =
928 fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j)
929 (js1 ~~ ts1, js2 ~~ ts2) of
930 (SOME t1, SOME t2) => apfst (cons (t1, t2))
931 | (SOME t1, NONE) => apsnd (apsnd (cons t1))
932 | (NONE, SOME t2) => apsnd (apfst (cons t2))
934 let val v = Var ((cong_var_prefix ^ nat_subscript j, 0),
936 apsnd (pairself (cons v))
937 end) (max_j downto 0) ([], ([], []))
939 Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =)
940 |> map Logic.mk_equals,
941 Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
942 list_comb (Const x2, bounds2 @ args2)))
943 |> close_form (* TODO: needed? *)
946 (* hol_context -> styp list -> term list *)
947 fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =
951 |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
952 |> AList.group (op =)
953 |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)
954 |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
955 (* special_triple -> int *)
956 fun generality (js, _, _) = ~(length js)
957 (* special_triple -> special_triple -> bool *)
958 fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
959 x1 <> x2 andalso OrdList.subset (prod_ord int_ord TermOrd.term_ord)
961 (* typ -> special_triple list -> special_triple list -> special_triple list
962 -> term list -> term list *)
963 fun do_pass_1 _ [] [_] [_] = I
964 | do_pass_1 T skipped _ [] = do_pass_2 T skipped
965 | do_pass_1 T skipped all (z :: zs) =
966 case filter (is_more_specific z) all
967 |> sort (int_ord o pairself generality) of
968 [] => do_pass_1 T (z :: skipped) all zs
969 | (z' :: _) => cons (special_congruence_axiom T z z')
970 #> do_pass_1 T skipped all zs
971 (* typ -> special_triple list -> term list -> term list *)
972 and do_pass_2 _ [] = I
973 | do_pass_2 T (z :: zs) =
974 fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs
975 in fold (fn ((_, T), zs) => do_pass_1 T [] zs zs) groups [] end
977 (** Axiom selection **)
979 (* Similar to "Refute.specialize_type" but returns all matches rather than only
980 the first (preorder) match. *)
981 (* theory -> styp -> term -> term list *)
982 fun multi_specialize_type thy slack (s, T) t =
984 (* term -> (typ * term) list -> (typ * term) list *)
985 fun aux (Const (s', T')) ys =
987 ys |> (if AList.defined (op =) ys T' then
990 cons (T', Refute.monomorphic_term
991 (Sign.typ_match thy (T', T) Vartab.empty) t)
992 handle Type.TYPE_MATCH => I
997 raise NOT_SUPPORTED ("too much polymorphism in \
998 \axiom involving " ^ quote s))
1002 in map snd (fold_aterms aux t []) end
1004 (* theory -> bool -> const_table -> styp -> term list *)
1005 fun nondef_props_for_const thy slack table (x as (s, _)) =
1006 these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
1008 (* 'a Symtab.table -> 'a list *)
1009 fun all_table_entries table = Symtab.fold (append o snd) table []
1010 (* const_table -> string -> const_table *)
1011 fun extra_table table s = Symtab.make [(s, all_table_entries table)]
1013 (* int -> term -> term *)
1014 fun eval_axiom_for_term j t =
1015 Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t)
1018 val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals)
1020 (* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
1021 val axioms_max_depth = 255
1023 (* hol_context -> term -> (term list * term list) * (bool * bool) *)
1025 (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
1026 fast_descrs, evals, def_table, nondef_table, user_nondefs,
1029 type accumulator = styp list * (term list * term list)
1030 (* (term list * term list -> term list)
1031 -> ((term list -> term list) -> term list * term list
1032 -> term list * term list)
1033 -> int -> term -> accumulator -> accumulator *)
1034 fun add_axiom get app depth t (accum as (xs, axs)) =
1036 val t = t |> unfold_defs_in_term hol_ctxt
1037 |> skolemize_term_and_more hol_ctxt ~1
1039 if is_trivial_equation t then
1042 let val t' = t |> specialize_consts_in_term hol_ctxt depth in
1043 if exists (member (op aconv) (get axs)) [t, t'] then accum
1044 else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
1047 (* int -> term -> accumulator -> accumulator *)
1048 and add_def_axiom depth = add_axiom fst apfst depth
1049 and add_nondef_axiom depth = add_axiom snd apsnd depth
1050 and add_maybe_def_axiom depth t =
1051 (if head_of t <> @{const "==>"} then add_def_axiom
1052 else add_nondef_axiom) depth t
1053 and add_eq_axiom depth t =
1054 (if is_constr_pattern_formula thy t then add_def_axiom
1055 else add_nondef_axiom) depth t
1056 (* int -> term -> accumulator -> accumulator *)
1057 and add_axioms_for_term depth t (accum as (xs, axs)) =
1059 t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
1060 | Const (x as (s, T)) =>
1061 (if member (op =) xs x orelse
1062 is_built_in_const thy stds fast_descrs x then
1065 let val accum = (x :: xs, axs) in
1066 if depth > axioms_max_depth then
1067 raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
1068 \add_axioms_for_term",
1069 "too many nested axioms (" ^
1070 string_of_int depth ^ ")")
1071 else if Refute.is_const_of_class thy x then
1073 val class = Logic.class_of_const s
1074 val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
1076 val ax1 = try (Refute.specialize_type thy x) of_class
1077 val ax2 = Option.map (Refute.specialize_type thy x o snd)
1078 (Refute.get_classdef thy class)
1080 fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
1083 else if is_constr thy stds x then
1085 else if is_equational_fun hol_ctxt x then
1086 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
1088 else if is_abs_fun thy x then
1089 if is_quot_type thy (range_type T) then
1090 raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
1092 accum |> fold (add_nondef_axiom depth)
1093 (nondef_props_for_const thy false nondef_table x)
1094 |> is_funky_typedef thy (range_type T)
1095 ? fold (add_maybe_def_axiom depth)
1096 (nondef_props_for_const thy true
1097 (extra_table def_table s) x)
1098 else if is_rep_fun thy x then
1099 if is_quot_type thy (domain_type T) then
1100 raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
1102 accum |> fold (add_nondef_axiom depth)
1103 (nondef_props_for_const thy false nondef_table x)
1104 |> is_funky_typedef thy (range_type T)
1105 ? fold (add_maybe_def_axiom depth)
1106 (nondef_props_for_const thy true
1107 (extra_table def_table s) x)
1108 |> add_axioms_for_term depth
1109 (Const (mate_of_rep_fun thy x))
1110 |> fold (add_def_axiom depth)
1111 (inverse_axioms_for_rep_fun thy x)
1113 accum |> user_axioms <> SOME false
1114 ? fold (add_nondef_axiom depth)
1115 (nondef_props_for_const thy false nondef_table x)
1117 |> add_axioms_for_type depth T
1118 | Free (_, T) => add_axioms_for_type depth T accum
1119 | Var (_, T) => add_axioms_for_type depth T accum
1121 | Abs (_, T, t) => accum |> add_axioms_for_term depth t
1122 |> add_axioms_for_type depth T
1123 (* int -> typ -> accumulator -> accumulator *)
1124 and add_axioms_for_type depth T =
1126 Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts
1127 | Type ("*", Ts) => fold (add_axioms_for_type depth) Ts
1131 | TFree (_, S) => add_axioms_for_sort depth T S
1132 | TVar (_, S) => add_axioms_for_sort depth T S
1133 | Type (z as (_, Ts)) =>
1134 fold (add_axioms_for_type depth) Ts
1135 #> (if is_pure_typedef thy T then
1136 fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
1137 else if is_quot_type thy T then
1138 fold (add_def_axiom depth)
1139 (optimized_quot_type_axioms ctxt stds z)
1140 else if max_bisim_depth >= 0 andalso is_codatatype thy T then
1141 fold (add_maybe_def_axiom depth)
1142 (codatatype_bisim_axioms hol_ctxt T)
1145 (* int -> typ -> sort -> accumulator -> accumulator *)
1146 and add_axioms_for_sort depth T S =
1148 val supers = Sign.complete_sort thy S
1150 maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
1151 handle ERROR _ => [])) supers
1152 val monomorphic_class_axioms =
1153 map (fn t => case Term.add_tvars t [] of
1156 Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
1157 | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
1158 \add_axioms_for_sort", [t]))
1160 in fold (add_nondef_axiom depth) monomorphic_class_axioms end
1161 val (mono_user_nondefs, poly_user_nondefs) =
1162 List.partition (null o Term.hidden_polymorphism) user_nondefs
1163 val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
1165 val (xs, (defs, nondefs)) =
1166 ([], ([], [])) |> add_axioms_for_term 1 t
1167 |> fold_rev (add_def_axiom 1) eval_axioms
1168 |> user_axioms = SOME true
1169 ? fold (add_nondef_axiom 1) mono_user_nondefs
1170 val defs = defs @ special_congruence_axioms hol_ctxt xs
1172 ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
1173 null poly_user_nondefs))
1176 (** Simplification of constructor/selector terms **)
1178 (* theory -> term -> term *)
1179 fun simplify_constrs_and_sels thy t =
1181 (* term -> int -> term *)
1182 fun is_nth_sel_on t' n (Const (s, _) $ t) =
1183 (t = t' andalso is_sel_like_and_no_discr s andalso
1184 sel_no_from_name s = n)
1185 | is_nth_sel_on _ _ _ = false
1186 (* term -> term list -> term *)
1187 fun do_term (Const (@{const_name Rep_Frac}, _)
1188 $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 []
1189 | do_term (Const (@{const_name Abs_Frac}, _)
1190 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 []
1191 | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
1192 | do_term (t as Const (x as (s, T))) (args as _ :: _) =
1193 ((if is_constr_like thy x then
1194 if length args = num_binder_types T then
1196 Const (_, T') $ t' =>
1197 if domain_type T' = body_type T andalso
1198 forall (uncurry (is_nth_sel_on t'))
1199 (index_seq 0 (length args) ~~ args) then
1203 | _ => raise SAME ()
1206 else if is_sel_like_and_no_discr s then
1207 case strip_comb (hd args) of
1208 (Const (x' as (s', T')), ts') =>
1209 if is_constr_like thy x' andalso
1210 constr_name_for_sel_like s = s' andalso
1211 not (exists is_pair_type (binder_types T')) then
1212 list_comb (nth ts' (sel_no_from_name s), tl args)
1215 | _ => raise SAME ()
1218 handle SAME () => betapplys (t, args))
1219 | do_term (Abs (s, T, t')) args =
1220 betapplys (Abs (s, T, do_term t' []), args)
1221 | do_term t args = betapplys (t, args)
1224 (** Quantifier massaging: Distributing quantifiers **)
1227 fun distribute_quantifiers t =
1229 (t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) =>
1231 (t10 as @{const "op &"}) $ t11 $ t12 =>
1232 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
1233 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
1234 | (t10 as @{const Not}) $ t11 =>
1235 t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0)
1238 if not (loose_bvar1 (t1, 0)) then
1239 distribute_quantifiers (incr_boundvars ~1 t1)
1241 t0 $ Abs (s, T1, distribute_quantifiers t1))
1242 | (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) =>
1243 (case distribute_quantifiers t1 of
1244 (t10 as @{const "op |"}) $ t11 $ t12 =>
1245 t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11))
1246 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
1247 | (t10 as @{const "op -->"}) $ t11 $ t12 =>
1248 t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
1250 $ distribute_quantifiers (t0 $ Abs (s, T1, t12))
1251 | (t10 as @{const Not}) $ t11 =>
1252 t10 $ distribute_quantifiers (Const (@{const_name All}, T0)
1255 if not (loose_bvar1 (t1, 0)) then
1256 distribute_quantifiers (incr_boundvars ~1 t1)
1258 t0 $ Abs (s, T1, distribute_quantifiers t1))
1259 | t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2
1260 | Abs (s, T, t') => Abs (s, T, distribute_quantifiers t')
1263 (** Quantifier massaging: Pushing quantifiers inward **)
1265 (* int -> int -> (int -> int) -> term -> term *)
1266 fun renumber_bounds j n f t =
1268 t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2
1269 | Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t')
1271 Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j')
1274 (* Maximum number of quantifiers in a cluster for which the exponential
1275 algorithm is used. Larger clusters use a heuristic inspired by Claessen &
1276 Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
1278 val quantifier_cluster_threshold = 7
1281 val push_quantifiers_inward =
1283 (* string -> string list -> typ list -> term -> term *)
1284 fun aux quant_s ss Ts t =
1286 Const (s0, _) $ Abs (s1, T1, t1 as _ $ _) =>
1287 if s0 = quant_s then
1288 aux s0 (s1 :: ss) (T1 :: Ts) t1
1289 else if quant_s = "" andalso
1290 (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
1294 | _ => raise SAME ())
1298 if quant_s = "" then
1299 aux "" [] [] t1 $ aux "" [] [] t2
1302 val typical_card = 4
1303 (* ('a -> ''b list) -> 'a list -> ''b list *)
1304 fun big_union proj ps =
1305 fold (fold (insert (op =)) o proj) ps []
1306 val (ts, connective) = strip_any_connective t
1308 map (bounded_card_of_type 65536 typical_card []) Ts
1309 val t_costs = map size_of_term ts
1310 val num_Ts = length Ts
1312 val flip = curry (op -) (num_Ts - 1)
1313 val t_boundss = map (map flip o loose_bnos) ts
1314 (* (int list * int) list -> int list
1315 -> (int list * int) list *)
1316 fun merge costly_boundss [] = costly_boundss
1317 | merge costly_boundss (j :: js) =
1320 List.partition (fn (bounds, _) =>
1321 member (op =) bounds j)
1323 val yeas_bounds = big_union fst yeas
1324 val yeas_cost = Integer.sum (map snd yeas)
1326 in merge ((yeas_bounds, yeas_cost) :: nays) js end
1327 (* (int list * int) list -> int list -> int *)
1328 val cost = Integer.sum o map snd oo merge
1329 (* (int list * int) list -> int list -> int list *)
1330 fun heuristically_best_permutation _ [] = []
1331 | heuristically_best_permutation costly_boundss js =
1333 val (costly_boundss, (j, js)) =
1334 js |> map (`(merge costly_boundss o single))
1336 o pairself (Integer.sum o map snd o fst))
1337 |> split_list |>> hd ||> pairf hd tl
1339 j :: heuristically_best_permutation costly_boundss js
1342 if length Ts <= quantifier_cluster_threshold then
1343 all_permutations (index_seq 0 num_Ts)
1344 |> map (`(cost (t_boundss ~~ t_costs)))
1345 |> sort (int_ord o pairself fst) |> hd |> snd
1347 heuristically_best_permutation (t_boundss ~~ t_costs)
1348 (index_seq 0 num_Ts)
1349 val back_js = map (fn j => find_index (curry (op =) j) js)
1350 (index_seq 0 num_Ts)
1351 val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
1353 (* (term * int list) list -> term *)
1354 fun mk_connection [] =
1355 raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\
1356 \mk_connection", "")
1357 | mk_connection ts_cum_bounds =
1358 ts_cum_bounds |> map fst
1359 |> foldr1 (fn (t1, t2) => connective $ t1 $ t2)
1360 (* (term * int list) list -> int list -> term *)
1361 fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection
1362 | build ts_cum_bounds (j :: js) =
1365 List.partition (fn (_, bounds) =>
1366 member (op =) bounds j)
1368 ||> map (apfst (incr_boundvars ~1))
1373 let val T = nth Ts (flip j) in
1374 build ((Const (quant_s, (T --> bool_T) --> bool_T)
1375 $ Abs (nth ss (flip j), T,
1376 mk_connection yeas),
1377 big_union snd yeas) :: nays) js
1380 in build (ts ~~ t_boundss) js end
1381 | Abs (s, T, t') => Abs (s, T, aux "" [] [] t')
1385 (** Preprocessor entry point **)
1387 (* hol_context -> term
1388 -> ((term list * term list) * (bool * bool)) * term * bool *)
1389 fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
1390 boxes, skolemize, uncurry, ...}) t =
1392 val skolem_depth = if skolemize then 4 else ~1
1393 val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
1394 core_t) = t |> unfold_defs_in_term hol_ctxt
1396 |> skolemize_term_and_more hol_ctxt skolem_depth
1397 |> specialize_consts_in_term hol_ctxt 0
1398 |> `(axioms_for_term hol_ctxt)
1400 is_standard_datatype thy stds nat_T andalso
1403 | _ => forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
1404 (binary_ints = SOME true orelse
1405 exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
1406 val box = exists (not_equal (SOME false) o snd) boxes
1408 Termtab.empty |> uncurry
1409 ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
1410 (* bool -> term -> term *)
1412 binarize ? binarize_nat_and_int_in_term
1413 #> uncurry ? uncurry_term table
1414 #> box ? box_fun_and_pair_in_term hol_ctxt def
1415 #> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
1416 #> pull_out_existential_constrs hol_ctxt
1417 #> destroy_pulled_out_constrs hol_ctxt def)
1419 #> destroy_universal_equalities
1420 #> destroy_existential_equalities hol_ctxt
1421 #> simplify_constrs_and_sels thy
1422 #> distribute_quantifiers
1423 #> push_quantifiers_inward
1425 #> Term.map_abs_vars shortest_name
1427 (((map (do_rest true) def_ts, map (do_rest false) nondef_ts),
1428 (got_all_mono_user_axioms, no_poly_user_axioms)),
1429 do_rest false core_t, binarize)