author | wenzelm |
Sat, 27 Feb 2010 23:13:01 +0100 | |
changeset 35408 | b48ab741683b |
parent 35386 | 45a4e19d3ebd |
child 35665 | ff2bf50505ab |
permissions | -rw-r--r-- |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Nitpick/nitpick_preproc.ML |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
3 |
Copyright 2008, 2009, 2010 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
4 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
5 |
Nitpick's HOL preprocessor. |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
6 |
*) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
7 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
8 |
signature NITPICK_PREPROC = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
9 |
sig |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
10 |
type hol_context = Nitpick_HOL.hol_context |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
11 |
val preprocess_term : |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
12 |
hol_context -> term -> term list * term list * bool * bool * bool |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
13 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
14 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
15 |
structure Nitpick_Preproc : NITPICK_PREPROC = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
16 |
struct |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
17 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
18 |
open Nitpick_Util |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
19 |
open Nitpick_HOL |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
20 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
21 |
(* polarity -> string -> bool *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
22 |
fun is_positive_existential polar quant_s = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
23 |
(polar = Pos andalso quant_s = @{const_name Ex}) orelse |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
24 |
(polar = Neg andalso quant_s <> @{const_name Ex}) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
25 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
26 |
(** Binary coding of integers **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
27 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
28 |
(* If a formula contains a numeral whose absolute value is more than this |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
29 |
threshold, the unary coding is likely not to work well and we prefer the |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
30 |
binary coding. *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
31 |
val binary_int_threshold = 3 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
32 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
33 |
(* term -> bool *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
34 |
fun may_use_binary_ints (t1 $ t2) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
35 |
may_use_binary_ints t1 andalso may_use_binary_ints t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
36 |
| may_use_binary_ints (t as Const (s, _)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
37 |
t <> @{const Suc} andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
38 |
not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
39 |
@{const_name nat_gcd}, @{const_name nat_lcm}, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
40 |
@{const_name Frac}, @{const_name norm_frac}] s) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
41 |
| may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
42 |
| may_use_binary_ints _ = true |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
43 |
fun should_use_binary_ints (t1 $ t2) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
44 |
should_use_binary_ints t1 orelse should_use_binary_ints t2 |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
45 |
| should_use_binary_ints (Const (s, T)) = |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
46 |
((s = @{const_name times} orelse s = @{const_name div}) andalso |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
47 |
is_integer_type (body_type T)) orelse |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
48 |
(String.isPrefix numeral_prefix s andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
49 |
let val n = the (Int.fromString (unprefix numeral_prefix s)) in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
50 |
n < ~ binary_int_threshold orelse n > binary_int_threshold |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
51 |
end) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
52 |
| should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
53 |
| should_use_binary_ints _ = false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
54 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
55 |
(** Uncurrying **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
56 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
57 |
(* theory -> term -> int Termtab.tab -> int Termtab.tab *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
58 |
fun add_to_uncurry_table thy t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
59 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
60 |
(* term -> term list -> int Termtab.tab -> int Termtab.tab *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
61 |
fun aux (t1 $ t2) args table = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
62 |
let val table = aux t2 [] table in aux t1 (t2 :: args) table end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
63 |
| aux (Abs (_, _, t')) _ table = aux t' [] table |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
64 |
| aux (t as Const (x as (s, _))) args table = |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
65 |
if is_built_in_const thy [(NONE, true)] true x orelse |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
66 |
is_constr_like thy x orelse |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
67 |
is_sel s orelse s = @{const_name Sigma} then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
68 |
table |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
69 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
70 |
Termtab.map_default (t, 65536) (curry Int.min (length args)) table |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
71 |
| aux _ _ table = table |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
72 |
in aux t [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
73 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
74 |
(* int -> int -> string *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
75 |
fun uncurry_prefix_for k j = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
76 |
uncurry_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
77 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
78 |
(* int Termtab.tab term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
79 |
fun uncurry_term table t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
80 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
81 |
(* term -> term list -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
82 |
fun aux (t1 $ t2) args = aux t1 (aux t2 [] :: args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
83 |
| aux (Abs (s, T, t')) args = betapplys (Abs (s, T, aux t' []), args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
84 |
| aux (t as Const (s, T)) args = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
85 |
(case Termtab.lookup table t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
86 |
SOME n => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
87 |
if n >= 2 then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
88 |
let |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
89 |
val arg_Ts = strip_n_binders n T |> fst |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
90 |
val j = |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
91 |
if is_iterator_type (hd arg_Ts) then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
92 |
1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
93 |
else case find_index (not_equal bool_T) arg_Ts of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
94 |
~1 => n |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
95 |
| j => j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
96 |
val ((before_args, tuple_args), after_args) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
97 |
args |> chop n |>> chop j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
98 |
val ((before_arg_Ts, tuple_arg_Ts), rest_T) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
99 |
T |> strip_n_binders n |>> chop j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
100 |
val tuple_T = HOLogic.mk_tupleT tuple_arg_Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
101 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
102 |
if n - j < 2 then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
103 |
betapplys (t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
104 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
105 |
betapplys (Const (uncurry_prefix_for (n - j) j ^ s, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
106 |
before_arg_Ts ---> tuple_T --> rest_T), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
107 |
before_args @ [mk_flat_tuple tuple_T tuple_args] @ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
108 |
after_args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
109 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
110 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
111 |
betapplys (t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
112 |
| NONE => betapplys (t, args)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
113 |
| aux t args = betapplys (t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
114 |
in aux t [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
115 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
116 |
(** Boxing **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
117 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
118 |
(* hol_context -> typ -> term -> term *) |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
119 |
fun constr_expand (hol_ctxt as {thy, stds, ...}) T t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
120 |
(case head_of t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
121 |
Const x => if is_constr_like thy x then t else raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
122 |
| _ => raise SAME ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
123 |
handle SAME () => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
124 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
125 |
val x' as (_, T') = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
126 |
if is_pair_type T then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
127 |
let val (T1, T2) = HOLogic.dest_prodT T in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
128 |
(@{const_name Pair}, T1 --> T2 --> T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
129 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
130 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
131 |
datatype_constrs hol_ctxt T |> hd |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
132 |
val arg_Ts = binder_types T' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
133 |
in |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
134 |
list_comb (Const x', map2 (select_nth_constr_arg thy stds x' t) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
135 |
(index_seq 0 (length arg_Ts)) arg_Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
136 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
137 |
|
35384 | 138 |
(* (term -> term) -> int -> term -> term *) |
139 |
fun coerce_bound_no f j t = |
|
140 |
case t of |
|
141 |
t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2 |
|
142 |
| Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t') |
|
143 |
| Bound j' => if j' = j then f t else t |
|
144 |
| _ => t |
|
145 |
(* hol_context -> typ -> typ -> term -> term *) |
|
146 |
fun coerce_bound_0_in_term hol_ctxt new_T old_T = |
|
147 |
old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0 |
|
148 |
(* hol_context -> typ list -> typ -> typ -> term -> term *) |
|
149 |
and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t = |
|
150 |
if old_T = new_T then |
|
151 |
t |
|
152 |
else |
|
153 |
case (new_T, old_T) of |
|
154 |
(Type (new_s, new_Ts as [new_T1, new_T2]), |
|
155 |
Type ("fun", [old_T1, old_T2])) => |
|
156 |
(case eta_expand Ts t 1 of |
|
157 |
Abs (s, _, t') => |
|
158 |
Abs (s, new_T1, |
|
159 |
t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1 |
|
160 |
|> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2) |
|
161 |
|> Envir.eta_contract |
|
162 |
|> new_s <> "fun" |
|
163 |
? construct_value thy stds |
|
164 |
(@{const_name FunBox}, Type ("fun", new_Ts) --> new_T) |
|
165 |
o single |
|
166 |
| t' => raise TERM ("Nitpick_Preproc.coerce_term", [t'])) |
|
167 |
| (Type (new_s, new_Ts as [new_T1, new_T2]), |
|
168 |
Type (old_s, old_Ts as [old_T1, old_T2])) => |
|
169 |
if old_s = @{type_name fun_box} orelse |
|
170 |
old_s = @{type_name pair_box} orelse old_s = "*" then |
|
171 |
case constr_expand hol_ctxt old_T t of |
|
172 |
Const (old_s, _) $ t1 => |
|
173 |
if new_s = "fun" then |
|
174 |
coerce_term hol_ctxt Ts new_T (Type ("fun", old_Ts)) t1 |
|
175 |
else |
|
176 |
construct_value thy stds |
|
177 |
(old_s, Type ("fun", new_Ts) --> new_T) |
|
178 |
[coerce_term hol_ctxt Ts (Type ("fun", new_Ts)) |
|
179 |
(Type ("fun", old_Ts)) t1] |
|
180 |
| Const _ $ t1 $ t2 => |
|
181 |
construct_value thy stds |
|
182 |
(if new_s = "*" then @{const_name Pair} |
|
183 |
else @{const_name PairBox}, new_Ts ---> new_T) |
|
184 |
[coerce_term hol_ctxt Ts new_T1 old_T1 t1, |
|
185 |
coerce_term hol_ctxt Ts new_T2 old_T2 t2] |
|
186 |
| t' => raise TERM ("Nitpick_Preproc.coerce_term", [t']) |
|
187 |
else |
|
188 |
raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t]) |
|
189 |
| _ => raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t]) |
|
190 |
||
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
191 |
(* hol_context -> bool -> term -> term *) |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
192 |
fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
193 |
orig_t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
194 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
195 |
(* typ -> typ *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
196 |
fun box_relational_operator_type (Type ("fun", Ts)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
197 |
Type ("fun", map box_relational_operator_type Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
198 |
| box_relational_operator_type (Type ("*", Ts)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
199 |
Type ("*", map (box_type hol_ctxt InPair) Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
200 |
| box_relational_operator_type T = T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
201 |
(* indexname * typ -> typ * term -> typ option list -> typ option list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
202 |
fun add_boxed_types_for_var (z as (_, T)) (T', t') = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
203 |
case t' of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
204 |
Var z' => z' = z ? insert (op =) T' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
205 |
| Const (@{const_name Pair}, _) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
206 |
(case T' of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
207 |
Type (_, [T1, T2]) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
208 |
fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
209 |
| _ => raise TYPE ("Nitpick_Preproc.box_fun_and_pair_in_term.\ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
210 |
\add_boxed_types_for_var", [T'], [])) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
211 |
| _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
212 |
(* typ list -> typ list -> term -> indexname * typ -> typ *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
213 |
fun box_var_in_def new_Ts old_Ts t (z as (_, T)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
214 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
215 |
@{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
216 |
| Const (s0, _) $ t1 $ _ => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
217 |
if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
218 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
219 |
val (t', args) = strip_comb t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
220 |
val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
221 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
222 |
case fold (add_boxed_types_for_var z) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
223 |
(fst (strip_n_binders (length args) T') ~~ args) [] of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
224 |
[T''] => T'' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
225 |
| _ => T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
226 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
227 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
228 |
T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
229 |
| _ => T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
230 |
(* typ list -> typ list -> polarity -> string -> typ -> string -> typ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
231 |
-> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
232 |
and do_quantifier new_Ts old_Ts polar quant_s quant_T abs_s abs_T t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
233 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
234 |
val abs_T' = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
235 |
if polar = Neut orelse is_positive_existential polar quant_s then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
236 |
box_type hol_ctxt InFunLHS abs_T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
237 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
238 |
abs_T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
239 |
val body_T = body_type quant_T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
240 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
241 |
Const (quant_s, (abs_T' --> body_T) --> body_T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
242 |
$ Abs (abs_s, abs_T', |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
243 |
t |> do_term (abs_T' :: new_Ts) (abs_T :: old_Ts) polar) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
244 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
245 |
(* typ list -> typ list -> string -> typ -> term -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
246 |
and do_equals new_Ts old_Ts s0 T0 t1 t2 = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
247 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
248 |
val (t1, t2) = pairself (do_term new_Ts old_Ts Neut) (t1, t2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
249 |
val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2) |
35408 | 250 |
val T = [T1, T2] |> sort Term_Ord.typ_ord |> List.last |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
251 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
252 |
list_comb (Const (s0, T --> T --> body_type T0), |
35384 | 253 |
map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2]) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
254 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
255 |
(* string -> typ -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
256 |
and do_description_operator s T = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
257 |
let val T1 = box_type hol_ctxt InFunLHS (range_type T) in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
258 |
Const (s, (T1 --> bool_T) --> T1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
259 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
260 |
(* typ list -> typ list -> polarity -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
261 |
and do_term new_Ts old_Ts polar t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
262 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
263 |
Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
264 |
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
265 |
| Const (s0 as @{const_name "=="}, T0) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
266 |
do_equals new_Ts old_Ts s0 T0 t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
267 |
| @{const "==>"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
268 |
@{const "==>"} $ do_term new_Ts old_Ts (flip_polarity polar) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
269 |
$ do_term new_Ts old_Ts polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
270 |
| @{const Pure.conjunction} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
271 |
@{const Pure.conjunction} $ do_term new_Ts old_Ts polar t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
272 |
$ do_term new_Ts old_Ts polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
273 |
| @{const Trueprop} $ t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
274 |
@{const Trueprop} $ do_term new_Ts old_Ts polar t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
275 |
| @{const Not} $ t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
276 |
@{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
277 |
| Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
278 |
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
279 |
| Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
280 |
do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
281 |
| Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
282 |
do_equals new_Ts old_Ts s0 T0 t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
283 |
| @{const "op &"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
284 |
@{const "op &"} $ do_term new_Ts old_Ts polar t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
285 |
$ do_term new_Ts old_Ts polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
286 |
| @{const "op |"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
287 |
@{const "op |"} $ do_term new_Ts old_Ts polar t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
288 |
$ do_term new_Ts old_Ts polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
289 |
| @{const "op -->"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
290 |
@{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
291 |
$ do_term new_Ts old_Ts polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
292 |
| Const (s as @{const_name The}, T) => do_description_operator s T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
293 |
| Const (s as @{const_name Eps}, T) => do_description_operator s T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
294 |
| Const (s as @{const_name Tha}, T) => do_description_operator s T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
295 |
| Const (x as (s, T)) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
296 |
Const (s, if s = @{const_name converse} orelse |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
297 |
s = @{const_name trancl} then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
298 |
box_relational_operator_type T |
35311 | 299 |
else if String.isPrefix quot_normal_prefix s then |
300 |
let val T' = box_type hol_ctxt InFunLHS (domain_type T) in |
|
301 |
T' --> T' |
|
302 |
end |
|
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
303 |
else if is_built_in_const thy stds fast_descrs x orelse |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
304 |
s = @{const_name Sigma} then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
305 |
T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
306 |
else if is_constr_like thy x then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
307 |
box_type hol_ctxt InConstr T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
308 |
else if is_sel s |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
309 |
orelse is_rep_fun thy x then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
310 |
box_type hol_ctxt InSel T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
311 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
312 |
box_type hol_ctxt InExpr T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
313 |
| t1 $ Abs (s, T, t2') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
314 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
315 |
val t1 = do_term new_Ts old_Ts Neut t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
316 |
val T1 = fastype_of1 (new_Ts, t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
317 |
val (s1, Ts1) = dest_Type T1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
318 |
val T' = hd (snd (dest_Type (hd Ts1))) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
319 |
val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
320 |
val T2 = fastype_of1 (new_Ts, t2) |
35384 | 321 |
val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
322 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
323 |
betapply (if s1 = "fun" then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
324 |
t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
325 |
else |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
326 |
select_nth_constr_arg thy stds |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
327 |
(@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
328 |
(Type ("fun", Ts1)), t2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
329 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
330 |
| t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
331 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
332 |
val t1 = do_term new_Ts old_Ts Neut t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
333 |
val T1 = fastype_of1 (new_Ts, t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
334 |
val (s1, Ts1) = dest_Type T1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
335 |
val t2 = do_term new_Ts old_Ts Neut t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
336 |
val T2 = fastype_of1 (new_Ts, t2) |
35384 | 337 |
val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
338 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
339 |
betapply (if s1 = "fun" then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
340 |
t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
341 |
else |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
342 |
select_nth_constr_arg thy stds |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
343 |
(@{const_name FunBox}, Type ("fun", Ts1) --> T1) t1 0 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
344 |
(Type ("fun", Ts1)), t2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
345 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
346 |
| Free (s, T) => Free (s, box_type hol_ctxt InExpr T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
347 |
| Var (z as (x, T)) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
348 |
Var (x, if def then box_var_in_def new_Ts old_Ts orig_t z |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
349 |
else box_type hol_ctxt InExpr T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
350 |
| Bound _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
351 |
| Abs (s, T, t') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
352 |
Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
353 |
in do_term [] [] Pos orig_t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
354 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
355 |
(** Destruction of constructors **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
356 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
357 |
val val_var_prefix = nitpick_prefix ^ "v" |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
358 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
359 |
(* typ list -> int -> int -> int -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
360 |
fun fresh_value_var Ts k n j t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
361 |
Var ((val_var_prefix ^ nat_subscript (n - j), k), fastype_of1 (Ts, t)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
362 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
363 |
(* typ list -> term -> bool *) |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
364 |
fun has_heavy_bounds_or_vars Ts t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
365 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
366 |
(* typ list -> bool *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
367 |
fun aux [] = false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
368 |
| aux [T] = is_fun_type T orelse is_pair_type T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
369 |
| aux _ = true |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
370 |
in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
371 |
|
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
372 |
(* hol_context -> typ list -> bool -> int -> int -> term -> term list |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
373 |
-> term list -> term * term list *) |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
374 |
fun pull_out_constr_comb ({thy, stds, ...} : hol_context) Ts relax k level t |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
375 |
args seen = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
376 |
let val t_comb = list_comb (t, args) in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
377 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
378 |
Const x => |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
379 |
if not relax andalso is_constr thy stds x andalso |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
380 |
not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
381 |
has_heavy_bounds_or_vars Ts t_comb andalso |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
382 |
not (loose_bvar (t_comb, level)) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
383 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
384 |
val (j, seen) = case find_index (curry (op =) t_comb) seen of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
385 |
~1 => (0, t_comb :: seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
386 |
| j => (j, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
387 |
in (fresh_value_var Ts k (length seen) j t_comb, seen) end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
388 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
389 |
(t_comb, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
390 |
| _ => (t_comb, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
391 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
392 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
393 |
(* (term -> term) -> typ list -> int -> term list -> term list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
394 |
fun equations_for_pulled_out_constrs mk_eq Ts k seen = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
395 |
let val n = length seen in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
396 |
map2 (fn j => fn t => mk_eq (fresh_value_var Ts k n j t, t)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
397 |
(index_seq 0 n) seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
398 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
399 |
|
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
400 |
(* hol_context -> bool -> term -> term *) |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
401 |
fun pull_out_universal_constrs hol_ctxt def t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
402 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
403 |
val k = maxidx_of_term t + 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
404 |
(* typ list -> bool -> term -> term list -> term list -> term * term list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
405 |
fun do_term Ts def t args seen = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
406 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
407 |
(t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
408 |
do_eq_or_imp Ts true def t0 t1 t2 seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
409 |
| (t0 as @{const "==>"}) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
410 |
if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
411 |
| (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
412 |
do_eq_or_imp Ts true def t0 t1 t2 seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
413 |
| (t0 as @{const "op -->"}) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
414 |
do_eq_or_imp Ts false def t0 t1 t2 seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
415 |
| Abs (s, T, t') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
416 |
let val (t', seen) = do_term (T :: Ts) def t' [] seen in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
417 |
(list_comb (Abs (s, T, t'), args), seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
418 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
419 |
| t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
420 |
let val (t2, seen) = do_term Ts def t2 [] seen in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
421 |
do_term Ts def t1 (t2 :: args) seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
422 |
end |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
423 |
| _ => pull_out_constr_comb hol_ctxt Ts def k 0 t args seen |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
424 |
(* typ list -> bool -> bool -> term -> term -> term -> term list |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
425 |
-> term * term list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
426 |
and do_eq_or_imp Ts eq def t0 t1 t2 seen = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
427 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
428 |
val (t2, seen) = if eq andalso def then (t2, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
429 |
else do_term Ts false t2 [] seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
430 |
val (t1, seen) = do_term Ts false t1 [] seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
431 |
in (t0 $ t1 $ t2, seen) end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
432 |
val (concl, seen) = do_term [] def t [] [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
433 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
434 |
Logic.list_implies (equations_for_pulled_out_constrs Logic.mk_equals [] k |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
435 |
seen, concl) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
436 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
437 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
438 |
(* term -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
439 |
fun mk_exists v t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
440 |
HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
441 |
|
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
442 |
(* hol_context -> term -> term *) |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
443 |
fun pull_out_existential_constrs hol_ctxt t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
444 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
445 |
val k = maxidx_of_term t + 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
446 |
(* typ list -> int -> term -> term list -> term list -> term * term list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
447 |
fun aux Ts num_exists t args seen = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
448 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
449 |
(t0 as Const (@{const_name Ex}, _)) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
450 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
451 |
val (t1, seen') = aux (T1 :: Ts) (num_exists + 1) t1 [] [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
452 |
val n = length seen' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
453 |
(* unit -> term list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
454 |
fun vars () = map2 (fresh_value_var Ts k n) (index_seq 0 n) seen' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
455 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
456 |
(equations_for_pulled_out_constrs HOLogic.mk_eq Ts k seen' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
457 |
|> List.foldl s_conj t1 |> fold mk_exists (vars ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
458 |
|> curry3 Abs s1 T1 |> curry (op $) t0, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
459 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
460 |
| t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
461 |
let val (t2, seen) = aux Ts num_exists t2 [] seen in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
462 |
aux Ts num_exists t1 (t2 :: args) seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
463 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
464 |
| Abs (s, T, t') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
465 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
466 |
val (t', seen) = aux (T :: Ts) 0 t' [] (map (incr_boundvars 1) seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
467 |
in (list_comb (Abs (s, T, t'), args), map (incr_boundvars ~1) seen) end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
468 |
| _ => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
469 |
if num_exists > 0 then |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
470 |
pull_out_constr_comb hol_ctxt Ts false k num_exists t args seen |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
471 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
472 |
(list_comb (t, args), seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
473 |
in aux [] 0 t [] [] |> fst end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
474 |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
475 |
val let_var_prefix = nitpick_prefix ^ "l" |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
476 |
val let_inline_threshold = 32 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
477 |
|
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
478 |
(* int -> typ -> term -> (term -> term) -> term *) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
479 |
fun hol_let n abs_T body_T f t = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
480 |
if n * size_of_term t <= let_inline_threshold then |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
481 |
f t |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
482 |
else |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
483 |
let val z = ((let_var_prefix, 0), abs_T) in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
484 |
Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
485 |
$ t $ abs_var z (incr_boundvars 1 (f (Var z))) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
486 |
end |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
487 |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
488 |
(* hol_context -> bool -> term -> term *) |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
489 |
fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
490 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
491 |
(* styp -> int *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
492 |
val num_occs_of_var = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
493 |
fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
494 |
| _ => I) t (K 0) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
495 |
(* bool -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
496 |
fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
497 |
aux_eq careful true t0 t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
498 |
| aux careful ((t0 as @{const "==>"}) $ t1 $ t2) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
499 |
t0 $ aux false t1 $ aux careful t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
500 |
| aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
501 |
aux_eq careful true t0 t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
502 |
| aux careful ((t0 as @{const "op -->"}) $ t1 $ t2) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
503 |
t0 $ aux false t1 $ aux careful t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
504 |
| aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
505 |
| aux careful (t1 $ t2) = aux careful t1 $ aux careful t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
506 |
| aux _ t = t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
507 |
(* bool -> bool -> term -> term -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
508 |
and aux_eq careful pass1 t0 t1 t2 = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
509 |
((if careful then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
510 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
511 |
else if axiom andalso is_Var t2 andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
512 |
num_occs_of_var (dest_Var t2) = 1 then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
513 |
@{const True} |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
514 |
else case strip_comb t2 of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
515 |
(* The first case is not as general as it could be. *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
516 |
(Const (@{const_name PairBox}, _), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
517 |
[Const (@{const_name fst}, _) $ Var z1, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
518 |
Const (@{const_name snd}, _) $ Var z2]) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
519 |
if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True} |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
520 |
else raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
521 |
| (Const (x as (s, T)), args) => |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
522 |
let |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
523 |
val (arg_Ts, dataT) = strip_type T |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
524 |
val n = length arg_Ts |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
525 |
in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
526 |
if length args = n andalso |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
527 |
(is_constr thy stds x orelse s = @{const_name Pair} orelse |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
528 |
x = (@{const_name Suc}, nat_T --> nat_T)) andalso |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
529 |
(not careful orelse not (is_Var t1) orelse |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
530 |
String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
531 |
hol_let (n + 1) dataT bool_T |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
532 |
(fn t1 => discriminate_value hol_ctxt x t1 :: |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
533 |
map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
534 |
|> foldr1 s_conj) t1 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
535 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
536 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
537 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
538 |
| _ => raise SAME ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
539 |
|> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
540 |
handle SAME () => if pass1 then aux_eq careful false t0 t2 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
541 |
else t0 $ aux false t2 $ aux false t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
542 |
(* styp -> term -> int -> typ -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
543 |
and sel_eq x t n nth_T nth_t = |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
544 |
HOLogic.eq_const nth_T $ nth_t |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
545 |
$ select_nth_constr_arg thy stds x t n nth_T |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
546 |
|> aux false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
547 |
in aux axiom t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
548 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
549 |
(** Destruction of universal and existential equalities **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
550 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
551 |
(* term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
552 |
fun curry_assms (@{const "==>"} $ (@{const Trueprop} |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
553 |
$ (@{const "op &"} $ t1 $ t2)) $ t3) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
554 |
curry_assms (Logic.list_implies ([t1, t2] |> map HOLogic.mk_Trueprop, t3)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
555 |
| curry_assms (@{const "==>"} $ t1 $ t2) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
556 |
@{const "==>"} $ curry_assms t1 $ curry_assms t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
557 |
| curry_assms t = t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
558 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
559 |
(* term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
560 |
val destroy_universal_equalities = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
561 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
562 |
(* term list -> (indexname * typ) list -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
563 |
fun aux prems zs t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
564 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
565 |
@{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
566 |
| _ => Logic.list_implies (rev prems, t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
567 |
(* term list -> (indexname * typ) list -> term -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
568 |
and aux_implies prems zs t1 t2 = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
569 |
case t1 of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
570 |
Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
571 |
| @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
572 |
aux_eq prems zs z t' t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
573 |
| @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
574 |
aux_eq prems zs z t' t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
575 |
| _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
576 |
(* term list -> (indexname * typ) list -> indexname * typ -> term -> term |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
577 |
-> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
578 |
and aux_eq prems zs z t' t1 t2 = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
579 |
if not (member (op =) zs z) andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
580 |
not (exists_subterm (curry (op =) (Var z)) t') then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
581 |
aux prems zs (subst_free [(Var z, t')] t2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
582 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
583 |
aux (t1 :: prems) (Term.add_vars t1 zs) t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
584 |
in aux [] [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
585 |
|
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
586 |
(* theory -> (typ option * bool) list -> int -> term list -> term list |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
587 |
-> (term * term list) option *) |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
588 |
fun find_bound_assign thy stds j = |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
589 |
let |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
590 |
(* term list -> term list -> (term * term list) option *) |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
591 |
fun do_term _ [] = NONE |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
592 |
| do_term seen (t :: ts) = |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
593 |
let |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
594 |
(* bool -> term -> term -> (term * term list) option *) |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
595 |
fun do_eq pass1 t1 t2 = |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
596 |
(if loose_bvar1 (t2, j) then |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
597 |
if pass1 then do_eq false t2 t1 else raise SAME () |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
598 |
else case t1 of |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
599 |
Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME () |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
600 |
| Const (s, Type ("fun", [T1, T2])) $ Bound j' => |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
601 |
if j' = j andalso |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
602 |
s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
603 |
SOME (construct_value thy stds (@{const_name FunBox}, T2 --> T1) |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
604 |
[t2], ts @ seen) |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
605 |
else |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
606 |
raise SAME () |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
607 |
| _ => raise SAME ()) |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
608 |
handle SAME () => do_term (t :: seen) ts |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
609 |
in |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
610 |
case t of |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
611 |
Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2 |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
612 |
| _ => do_term (t :: seen) ts |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
613 |
end |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
614 |
in do_term end |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
615 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
616 |
(* int -> term -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
617 |
fun subst_one_bound j arg t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
618 |
let |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
619 |
(* term * int -> term *) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
620 |
fun aux (Bound i, lev) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
621 |
if i < lev then raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
622 |
else if i = lev then incr_boundvars (lev - j) arg |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
623 |
else Bound (i - 1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
624 |
| aux (Abs (a, T, body), lev) = Abs (a, T, aux (body, lev + 1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
625 |
| aux (f $ t, lev) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
626 |
(aux (f, lev) $ (aux (t, lev) handle SAME () => t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
627 |
handle SAME () => f $ aux (t, lev)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
628 |
| aux _ = raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
629 |
in aux (t, j) handle SAME () => t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
630 |
|
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
631 |
(* hol_context -> term -> term *) |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
632 |
fun destroy_existential_equalities ({thy, stds, ...} : hol_context) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
633 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
634 |
(* string list -> typ list -> term list -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
635 |
fun kill [] [] ts = foldr1 s_conj ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
636 |
| kill (s :: ss) (T :: Ts) ts = |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
637 |
(case find_bound_assign thy stds (length ss) [] ts of |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
638 |
SOME (_, []) => @{const True} |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
639 |
| SOME (arg_t, ts) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
640 |
kill ss Ts (map (subst_one_bound (length ss) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
641 |
(incr_bv (~1, length ss + 1, arg_t))) ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
642 |
| NONE => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
643 |
Const (@{const_name Ex}, (T --> bool_T) --> bool_T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
644 |
$ Abs (s, T, kill ss Ts ts)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
645 |
| kill _ _ _ = raise UnequalLengths |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
646 |
(* string list -> typ list -> term -> term *) |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
647 |
fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
648 |
gather (ss @ [s1]) (Ts @ [T1]) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
649 |
| gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
650 |
| gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
651 |
| gather [] [] t = t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
652 |
| gather ss Ts t = kill ss Ts (conjuncts_of (gather [] [] t)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
653 |
in gather [] [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
654 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
655 |
(** Skolemization **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
656 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
657 |
(* int -> int -> string *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
658 |
fun skolem_prefix_for k j = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
659 |
skolem_prefix ^ string_of_int k ^ "@" ^ string_of_int j ^ name_sep |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
660 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
661 |
(* hol_context -> int -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
662 |
fun skolemize_term_and_more (hol_ctxt as {thy, def_table, skolems, ...}) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
663 |
skolem_depth = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
664 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
665 |
(* int list -> int list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
666 |
val incrs = map (Integer.add 1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
667 |
(* string list -> typ list -> int list -> int -> polarity -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
668 |
fun aux ss Ts js depth polar t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
669 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
670 |
(* string -> typ -> string -> typ -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
671 |
fun do_quantifier quant_s quant_T abs_s abs_T t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
672 |
if not (loose_bvar1 (t, 0)) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
673 |
aux ss Ts js depth polar (incr_boundvars ~1 t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
674 |
else if depth <= skolem_depth andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
675 |
is_positive_existential polar quant_s then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
676 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
677 |
val j = length (!skolems) + 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
678 |
val sko_s = skolem_prefix_for (length js) j ^ abs_s |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
679 |
val _ = Unsynchronized.change skolems (cons (sko_s, ss)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
680 |
val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
681 |
map Bound (rev js)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
682 |
val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
683 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
684 |
if null js then betapply (abs_t, sko_t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
685 |
else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
686 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
687 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
688 |
Const (quant_s, quant_T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
689 |
$ Abs (abs_s, abs_T, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
690 |
if is_higher_order_type abs_T then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
691 |
t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
692 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
693 |
aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
694 |
(depth + 1) polar t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
695 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
696 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
697 |
Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
698 |
do_quantifier s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
699 |
| @{const "==>"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
700 |
@{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
701 |
$ aux ss Ts js depth polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
702 |
| @{const Pure.conjunction} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
703 |
@{const Pure.conjunction} $ aux ss Ts js depth polar t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
704 |
$ aux ss Ts js depth polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
705 |
| @{const Trueprop} $ t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
706 |
@{const Trueprop} $ aux ss Ts js depth polar t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
707 |
| @{const Not} $ t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
708 |
@{const Not} $ aux ss Ts js depth (flip_polarity polar) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
709 |
| Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
710 |
do_quantifier s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
711 |
| Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
712 |
do_quantifier s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
713 |
| @{const "op &"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
714 |
@{const "op &"} $ aux ss Ts js depth polar t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
715 |
$ aux ss Ts js depth polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
716 |
| @{const "op |"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
717 |
@{const "op |"} $ aux ss Ts js depth polar t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
718 |
$ aux ss Ts js depth polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
719 |
| @{const "op -->"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
720 |
@{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
721 |
$ aux ss Ts js depth polar t2 |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
722 |
| (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
723 |
t0 $ t1 $ aux ss Ts js depth polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
724 |
| Const (x as (s, T)) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
725 |
if is_inductive_pred hol_ctxt x andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
726 |
not (is_well_founded_inductive_pred hol_ctxt x) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
727 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
728 |
val gfp = (fixpoint_kind_of_const thy def_table x = Gfp) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
729 |
val (pref, connective, set_oper) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
730 |
if gfp then |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
731 |
(lbfp_prefix, @{const "op |"}, |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
732 |
@{const_name semilattice_sup_class.sup}) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
733 |
else |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
734 |
(ubfp_prefix, @{const "op &"}, |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
735 |
@{const_name semilattice_inf_class.inf}) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
736 |
(* unit -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
737 |
fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
738 |
|> aux ss Ts js depth polar |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
739 |
fun neg () = Const (pref ^ s, T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
740 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
741 |
(case polar |> gfp ? flip_polarity of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
742 |
Pos => pos () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
743 |
| Neg => neg () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
744 |
| Neut => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
745 |
if is_fun_type T then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
746 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
747 |
val ((trunk_arg_Ts, rump_arg_T), body_T) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
748 |
T |> strip_type |>> split_last |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
749 |
val set_T = rump_arg_T --> body_T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
750 |
(* (unit -> term) -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
751 |
fun app f = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
752 |
list_comb (f (), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
753 |
map Bound (length trunk_arg_Ts - 1 downto 0)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
754 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
755 |
List.foldr absdummy |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
756 |
(Const (set_oper, set_T --> set_T --> set_T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
757 |
$ app pos $ app neg) trunk_arg_Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
758 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
759 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
760 |
connective $ pos () $ neg ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
761 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
762 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
763 |
Const x |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
764 |
| t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
765 |
betapply (aux ss Ts [] (skolem_depth + 1) polar t1, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
766 |
aux ss Ts [] depth Neut t2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
767 |
| Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
768 |
| _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
769 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
770 |
in aux [] [] [] 0 Pos end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
771 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
772 |
(** Function specialization **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
773 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
774 |
(* term -> term list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
775 |
fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
776 |
| params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
777 |
| params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
778 |
snd (strip_comb t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
779 |
| params_in_equation _ = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
780 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
781 |
(* styp -> styp -> int list -> term list -> term list -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
782 |
fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
783 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
784 |
val k = fold Integer.max (map maxidx_of_term (fixed_args @ extra_args)) 0 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
785 |
+ 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
786 |
val t = map_aterms (fn Var ((s, i), T) => Var ((s, k + i), T) | t' => t') t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
787 |
val fixed_params = filter_indices fixed_js (params_in_equation t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
788 |
(* term list -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
789 |
fun aux args (Abs (s, T, t)) = list_comb (Abs (s, T, aux [] t), args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
790 |
| aux args (t1 $ t2) = aux (aux [] t2 :: args) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
791 |
| aux args t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
792 |
if t = Const x then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
793 |
list_comb (Const x', extra_args @ filter_out_indices fixed_js args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
794 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
795 |
let val j = find_index (curry (op =) t) fixed_params in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
796 |
list_comb (if j >= 0 then nth fixed_args j else t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
797 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
798 |
in aux [] t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
799 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
800 |
(* hol_context -> styp -> (int * term option) list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
801 |
fun static_args_in_term ({ersatz_table, ...} : hol_context) x t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
802 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
803 |
(* term -> term list -> term list -> term list list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
804 |
fun fun_calls (Abs (_, _, t)) _ = fun_calls t [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
805 |
| fun_calls (t1 $ t2) args = fun_calls t2 [] #> fun_calls t1 (t2 :: args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
806 |
| fun_calls t args = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
807 |
(case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
808 |
Const (x' as (s', T')) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
809 |
x = x' orelse (case AList.lookup (op =) ersatz_table s' of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
810 |
SOME s'' => x = (s'', T') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
811 |
| NONE => false) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
812 |
| _ => false) ? cons args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
813 |
(* term list list -> term list list -> term list -> term list list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
814 |
fun call_sets [] [] vs = [vs] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
815 |
| call_sets [] uss vs = vs :: call_sets uss [] [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
816 |
| call_sets ([] :: _) _ _ = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
817 |
| call_sets ((t :: ts) :: tss) uss vs = |
35408 | 818 |
OrdList.insert Term_Ord.term_ord t vs |> call_sets tss (ts :: uss) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
819 |
val sets = call_sets (fun_calls t [] []) [] [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
820 |
val indexed_sets = sets ~~ (index_seq 0 (length sets)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
821 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
822 |
fold_rev (fn (set, j) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
823 |
case set of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
824 |
[Var _] => AList.lookup (op =) indexed_sets set = SOME j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
825 |
? cons (j, NONE) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
826 |
| [t as Const _] => cons (j, SOME t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
827 |
| [t as Free _] => cons (j, SOME t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
828 |
| _ => I) indexed_sets [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
829 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
830 |
(* hol_context -> styp -> term list -> (int * term option) list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
831 |
fun static_args_in_terms hol_ctxt x = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
832 |
map (static_args_in_term hol_ctxt x) |
35408 | 833 |
#> fold1 (OrdList.inter (prod_ord int_ord (option_ord Term_Ord.term_ord))) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
834 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
835 |
(* (int * term option) list -> (int * term) list -> int list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
836 |
fun overlapping_indices [] _ = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
837 |
| overlapping_indices _ [] = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
838 |
| overlapping_indices (ps1 as (j1, t1) :: ps1') (ps2 as (j2, t2) :: ps2') = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
839 |
if j1 < j2 then overlapping_indices ps1' ps2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
840 |
else if j1 > j2 then overlapping_indices ps1 ps2' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
841 |
else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
842 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
843 |
(* typ list -> term -> bool *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
844 |
fun is_eligible_arg Ts t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
845 |
let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
846 |
null bad_Ts orelse |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
847 |
(is_higher_order_type (fastype_of1 (Ts, t)) andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
848 |
forall (not o is_higher_order_type) bad_Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
849 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
850 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
851 |
(* int -> string *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
852 |
fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
853 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
854 |
(* If a constant's definition is picked up deeper than this threshold, we |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
855 |
prevent excessive specialization by not specializing it. *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
856 |
val special_max_depth = 20 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
857 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
858 |
val bound_var_prefix = "b" |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
859 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
860 |
(* hol_context -> int -> term -> term *) |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
861 |
fun specialize_consts_in_term (hol_ctxt as {specialize, simp_table, |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
862 |
special_funs, ...}) depth t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
863 |
if not specialize orelse depth > special_max_depth then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
864 |
t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
865 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
866 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
867 |
val blacklist = if depth = 0 then [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
868 |
else case term_under_def t of Const x => [x] | _ => [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
869 |
(* term list -> typ list -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
870 |
fun aux args Ts (Const (x as (s, T))) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
871 |
((if not (member (op =) blacklist x) andalso not (null args) andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
872 |
not (String.isPrefix special_prefix s) andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
873 |
is_equational_fun hol_ctxt x then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
874 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
875 |
val eligible_args = filter (is_eligible_arg Ts o snd) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
876 |
(index_seq 0 (length args) ~~ args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
877 |
val _ = not (null eligible_args) orelse raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
878 |
val old_axs = equational_fun_axioms hol_ctxt x |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
879 |
|> map (destroy_existential_equalities hol_ctxt) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
880 |
val static_params = static_args_in_terms hol_ctxt x old_axs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
881 |
val fixed_js = overlapping_indices static_params eligible_args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
882 |
val _ = not (null fixed_js) orelse raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
883 |
val fixed_args = filter_indices fixed_js args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
884 |
val vars = fold Term.add_vars fixed_args [] |
35408 | 885 |
|> sort (Term_Ord.fast_indexname_ord o pairself fst) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
886 |
val bound_js = fold (fn t => fn js => add_loose_bnos (t, 0, js)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
887 |
fixed_args [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
888 |
|> sort int_ord |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
889 |
val live_args = filter_out_indices fixed_js args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
890 |
val extra_args = map Var vars @ map Bound bound_js @ live_args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
891 |
val extra_Ts = map snd vars @ filter_indices bound_js Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
892 |
val k = maxidx_of_term t + 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
893 |
(* int -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
894 |
fun var_for_bound_no j = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
895 |
Var ((bound_var_prefix ^ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
896 |
nat_subscript (find_index (curry (op =) j) bound_js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
897 |
+ 1), k), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
898 |
nth Ts j) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
899 |
val fixed_args_in_axiom = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
900 |
map (curry subst_bounds |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
901 |
(map var_for_bound_no (index_seq 0 (length Ts)))) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
902 |
fixed_args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
903 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
904 |
case AList.lookup (op =) (!special_funs) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
905 |
(x, fixed_js, fixed_args_in_axiom) of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
906 |
SOME x' => list_comb (Const x', extra_args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
907 |
| NONE => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
908 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
909 |
val extra_args_in_axiom = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
910 |
map Var vars @ map var_for_bound_no bound_js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
911 |
val x' as (s', _) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
912 |
(special_prefix_for (length (!special_funs) + 1) ^ s, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
913 |
extra_Ts @ filter_out_indices fixed_js (binder_types T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
914 |
---> body_type T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
915 |
val new_axs = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
916 |
map (specialize_fun_axiom x x' fixed_js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
917 |
fixed_args_in_axiom extra_args_in_axiom) old_axs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
918 |
val _ = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
919 |
Unsynchronized.change special_funs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
920 |
(cons ((x, fixed_js, fixed_args_in_axiom), x')) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
921 |
val _ = add_simps simp_table s' new_axs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
922 |
in list_comb (Const x', extra_args) end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
923 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
924 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
925 |
raise SAME ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
926 |
handle SAME () => list_comb (Const x, args)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
927 |
| aux args Ts (Abs (s, T, t)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
928 |
list_comb (Abs (s, T, aux [] (T :: Ts) t), args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
929 |
| aux args Ts (t1 $ t2) = aux (aux [] Ts t2 :: args) Ts t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
930 |
| aux args _ t = list_comb (t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
931 |
in aux [] [] t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
932 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
933 |
type special_triple = int list * term list * styp |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
934 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
935 |
val cong_var_prefix = "c" |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
936 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
937 |
(* typ -> special_triple -> special_triple -> term *) |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
938 |
fun special_congruence_axiom T (js1, ts1, x1) (js2, ts2, x2) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
939 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
940 |
val (bounds1, bounds2) = pairself (map Var o special_bounds) (ts1, ts2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
941 |
val Ts = binder_types T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
942 |
val max_j = fold (fold Integer.max) [js1, js2] ~1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
943 |
val (eqs, (args1, args2)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
944 |
fold (fn j => case pairself (fn ps => AList.lookup (op =) ps j) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
945 |
(js1 ~~ ts1, js2 ~~ ts2) of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
946 |
(SOME t1, SOME t2) => apfst (cons (t1, t2)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
947 |
| (SOME t1, NONE) => apsnd (apsnd (cons t1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
948 |
| (NONE, SOME t2) => apsnd (apfst (cons t2)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
949 |
| (NONE, NONE) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
950 |
let val v = Var ((cong_var_prefix ^ nat_subscript j, 0), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
951 |
nth Ts j) in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
952 |
apsnd (pairself (cons v)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
953 |
end) (max_j downto 0) ([], ([], [])) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
954 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
955 |
Logic.list_implies (eqs |> filter_out (op =) |> distinct (op =) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
956 |
|> map Logic.mk_equals, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
957 |
Logic.mk_equals (list_comb (Const x1, bounds1 @ args1), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
958 |
list_comb (Const x2, bounds2 @ args2))) |
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35070
diff
changeset
|
959 |
|> close_form (* TODO: needed? *) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
960 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
961 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
962 |
(* hol_context -> styp list -> term list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
963 |
fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
964 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
965 |
val groups = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
966 |
!special_funs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
967 |
|> map (fn ((x, js, ts), x') => (x, (js, ts, x'))) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
968 |
|> AList.group (op =) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
969 |
|> filter_out (is_equational_fun_surely_complete hol_ctxt o fst) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
970 |
|> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x))) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
971 |
(* special_triple -> int *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
972 |
fun generality (js, _, _) = ~(length js) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
973 |
(* special_triple -> special_triple -> bool *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
974 |
fun is_more_specific (j1, t1, x1) (j2, t2, x2) = |
35408 | 975 |
x1 <> x2 andalso OrdList.subset (prod_ord int_ord Term_Ord.term_ord) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
976 |
(j2 ~~ t2, j1 ~~ t1) |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
977 |
(* typ -> special_triple list -> special_triple list -> special_triple list |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
978 |
-> term list -> term list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
979 |
fun do_pass_1 _ [] [_] [_] = I |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
980 |
| do_pass_1 T skipped _ [] = do_pass_2 T skipped |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
981 |
| do_pass_1 T skipped all (z :: zs) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
982 |
case filter (is_more_specific z) all |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
983 |
|> sort (int_ord o pairself generality) of |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
984 |
[] => do_pass_1 T (z :: skipped) all zs |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
985 |
| (z' :: _) => cons (special_congruence_axiom T z z') |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
986 |
#> do_pass_1 T skipped all zs |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
987 |
(* typ -> special_triple list -> term list -> term list *) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
988 |
and do_pass_2 _ [] = I |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
989 |
| do_pass_2 T (z :: zs) = |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
990 |
fold (cons o special_congruence_axiom T z) zs #> do_pass_2 T zs |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
991 |
in fold (fn ((_, T), zs) => do_pass_1 T [] zs zs) groups [] end |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
992 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
993 |
(** Axiom selection **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
994 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
995 |
(* Similar to "Refute.specialize_type" but returns all matches rather than only |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
996 |
the first (preorder) match. *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
997 |
(* theory -> styp -> term -> term list *) |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
998 |
fun multi_specialize_type thy slack (s, T) t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
999 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1000 |
(* term -> (typ * term) list -> (typ * term) list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1001 |
fun aux (Const (s', T')) ys = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1002 |
if s = s' then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1003 |
ys |> (if AList.defined (op =) ys T' then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1004 |
I |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1005 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1006 |
cons (T', Refute.monomorphic_term |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1007 |
(Sign.typ_match thy (T', T) Vartab.empty) t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1008 |
handle Type.TYPE_MATCH => I |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1009 |
| Refute.REFUTE _ => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1010 |
if slack then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1011 |
I |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1012 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1013 |
raise NOT_SUPPORTED ("too much polymorphism in \ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1014 |
\axiom involving " ^ quote s)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1015 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1016 |
ys |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1017 |
| aux _ ys = ys |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1018 |
in map snd (fold_aterms aux t []) end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1019 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1020 |
(* theory -> bool -> const_table -> styp -> term list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1021 |
fun nondef_props_for_const thy slack table (x as (s, _)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1022 |
these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1023 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1024 |
(* 'a Symtab.table -> 'a list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1025 |
fun all_table_entries table = Symtab.fold (append o snd) table [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1026 |
(* const_table -> string -> const_table *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1027 |
fun extra_table table s = Symtab.make [(s, all_table_entries table)] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1028 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1029 |
(* int -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1030 |
fun eval_axiom_for_term j t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1031 |
Logic.mk_equals (Const (eval_prefix ^ string_of_int j, fastype_of t), t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1032 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1033 |
(* term -> bool *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1034 |
val is_trivial_equation = the_default false o try (op aconv o Logic.dest_equals) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1035 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1036 |
(* Prevents divergence in case of cyclic or infinite axiom dependencies. *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1037 |
val axioms_max_depth = 255 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1038 |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1039 |
(* hol_context -> term -> term list * term list * bool * bool *) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1040 |
fun axioms_for_term |
35311 | 1041 |
(hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms, |
1042 |
fast_descrs, evals, def_table, nondef_table, user_nondefs, |
|
1043 |
...}) t = |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1044 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1045 |
type accumulator = styp list * (term list * term list) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1046 |
(* (term list * term list -> term list) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1047 |
-> ((term list -> term list) -> term list * term list |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1048 |
-> term list * term list) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1049 |
-> int -> term -> accumulator -> accumulator *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1050 |
fun add_axiom get app depth t (accum as (xs, axs)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1051 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1052 |
val t = t |> unfold_defs_in_term hol_ctxt |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1053 |
|> skolemize_term_and_more hol_ctxt ~1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1054 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1055 |
if is_trivial_equation t then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1056 |
accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1057 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1058 |
let val t' = t |> specialize_consts_in_term hol_ctxt depth in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1059 |
if exists (member (op aconv) (get axs)) [t, t'] then accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1060 |
else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1061 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1062 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1063 |
(* int -> term -> accumulator -> accumulator *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1064 |
and add_def_axiom depth = add_axiom fst apfst depth |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1065 |
and add_nondef_axiom depth = add_axiom snd apsnd depth |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1066 |
and add_maybe_def_axiom depth t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1067 |
(if head_of t <> @{const "==>"} then add_def_axiom |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1068 |
else add_nondef_axiom) depth t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1069 |
and add_eq_axiom depth t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1070 |
(if is_constr_pattern_formula thy t then add_def_axiom |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1071 |
else add_nondef_axiom) depth t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1072 |
(* int -> term -> accumulator -> accumulator *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1073 |
and add_axioms_for_term depth t (accum as (xs, axs)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1074 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1075 |
t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1076 |
| Const (x as (s, T)) => |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1077 |
(if member (op =) xs x orelse |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1078 |
is_built_in_const thy stds fast_descrs x then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1079 |
accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1080 |
else |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1081 |
let val accum = (x :: xs, axs) in |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1082 |
if depth > axioms_max_depth then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1083 |
raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1084 |
\add_axioms_for_term", |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1085 |
"too many nested axioms (" ^ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1086 |
string_of_int depth ^ ")") |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1087 |
else if Refute.is_const_of_class thy x then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1088 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1089 |
val class = Logic.class_of_const s |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1090 |
val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1091 |
class) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1092 |
val ax1 = try (Refute.specialize_type thy x) of_class |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1093 |
val ax2 = Option.map (Refute.specialize_type thy x o snd) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1094 |
(Refute.get_classdef thy class) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1095 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1096 |
fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2]) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1097 |
accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1098 |
end |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1099 |
else if is_constr thy stds x then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1100 |
accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1101 |
else if is_equational_fun hol_ctxt x then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1102 |
fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1103 |
accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1104 |
else if is_abs_fun thy x then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1105 |
if is_quot_type thy (range_type T) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1106 |
raise NOT_SUPPORTED "\"Abs_\" function of quotient type" |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1107 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1108 |
accum |> fold (add_nondef_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1109 |
(nondef_props_for_const thy false nondef_table x) |
35312 | 1110 |
|> (is_funky_typedef thy (range_type T) orelse |
1111 |
range_type T = nat_T) |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1112 |
? fold (add_maybe_def_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1113 |
(nondef_props_for_const thy true |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1114 |
(extra_table def_table s) x) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1115 |
else if is_rep_fun thy x then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1116 |
if is_quot_type thy (domain_type T) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1117 |
raise NOT_SUPPORTED "\"Rep_\" function of quotient type" |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1118 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1119 |
accum |> fold (add_nondef_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1120 |
(nondef_props_for_const thy false nondef_table x) |
35312 | 1121 |
|> (is_funky_typedef thy (range_type T) orelse |
1122 |
range_type T = nat_T) |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1123 |
? fold (add_maybe_def_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1124 |
(nondef_props_for_const thy true |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1125 |
(extra_table def_table s) x) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1126 |
|> add_axioms_for_term depth |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1127 |
(Const (mate_of_rep_fun thy x)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1128 |
|> fold (add_def_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1129 |
(inverse_axioms_for_rep_fun thy x) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1130 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1131 |
accum |> user_axioms <> SOME false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1132 |
? fold (add_nondef_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1133 |
(nondef_props_for_const thy false nondef_table x) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1134 |
end) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1135 |
|> add_axioms_for_type depth T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1136 |
| Free (_, T) => add_axioms_for_type depth T accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1137 |
| Var (_, T) => add_axioms_for_type depth T accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1138 |
| Bound _ => accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1139 |
| Abs (_, T, t) => accum |> add_axioms_for_term depth t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1140 |
|> add_axioms_for_type depth T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1141 |
(* int -> typ -> accumulator -> accumulator *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1142 |
and add_axioms_for_type depth T = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1143 |
case T of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1144 |
Type ("fun", Ts) => fold (add_axioms_for_type depth) Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1145 |
| Type ("*", Ts) => fold (add_axioms_for_type depth) Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1146 |
| @{typ prop} => I |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1147 |
| @{typ bool} => I |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1148 |
| @{typ unit} => I |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1149 |
| TFree (_, S) => add_axioms_for_sort depth T S |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1150 |
| TVar (_, S) => add_axioms_for_sort depth T S |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1151 |
| Type (z as (_, Ts)) => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1152 |
fold (add_axioms_for_type depth) Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1153 |
#> (if is_pure_typedef thy T then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1154 |
fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1155 |
else if is_quot_type thy T then |
35311 | 1156 |
fold (add_def_axiom depth) |
1157 |
(optimized_quot_type_axioms ctxt stds z) |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1158 |
else if max_bisim_depth >= 0 andalso is_codatatype thy T then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1159 |
fold (add_maybe_def_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1160 |
(codatatype_bisim_axioms hol_ctxt T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1161 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1162 |
I) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1163 |
(* int -> typ -> sort -> accumulator -> accumulator *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1164 |
and add_axioms_for_sort depth T S = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1165 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1166 |
val supers = Sign.complete_sort thy S |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1167 |
val class_axioms = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1168 |
maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1169 |
handle ERROR _ => [])) supers |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1170 |
val monomorphic_class_axioms = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1171 |
map (fn t => case Term.add_tvars t [] of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1172 |
[] => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1173 |
| [(x, S)] => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1174 |
Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1175 |
| _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1176 |
\add_axioms_for_sort", [t])) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1177 |
class_axioms |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1178 |
in fold (add_nondef_axiom depth) monomorphic_class_axioms end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1179 |
val (mono_user_nondefs, poly_user_nondefs) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1180 |
List.partition (null o Term.hidden_polymorphism) user_nondefs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1181 |
val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1182 |
evals |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1183 |
val (xs, (defs, nondefs)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1184 |
([], ([], [])) |> add_axioms_for_term 1 t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1185 |
|> fold_rev (add_def_axiom 1) eval_axioms |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1186 |
|> user_axioms = SOME true |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1187 |
? fold (add_nondef_axiom 1) mono_user_nondefs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1188 |
val defs = defs @ special_congruence_axioms hol_ctxt xs |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1189 |
val got_all_mono_user_axioms = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1190 |
(user_axioms = SOME true orelse null mono_user_nondefs) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1191 |
in (t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs) end |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1192 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1193 |
(** Simplification of constructor/selector terms **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1194 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1195 |
(* theory -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1196 |
fun simplify_constrs_and_sels thy t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1197 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1198 |
(* term -> int -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1199 |
fun is_nth_sel_on t' n (Const (s, _) $ t) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1200 |
(t = t' andalso is_sel_like_and_no_discr s andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1201 |
sel_no_from_name s = n) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1202 |
| is_nth_sel_on _ _ _ = false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1203 |
(* term -> term list -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1204 |
fun do_term (Const (@{const_name Rep_Frac}, _) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1205 |
$ (Const (@{const_name Abs_Frac}, _) $ t1)) [] = do_term t1 [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1206 |
| do_term (Const (@{const_name Abs_Frac}, _) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1207 |
$ (Const (@{const_name Rep_Frac}, _) $ t1)) [] = do_term t1 [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1208 |
| do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1209 |
| do_term (t as Const (x as (s, T))) (args as _ :: _) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1210 |
((if is_constr_like thy x then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1211 |
if length args = num_binder_types T then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1212 |
case hd args of |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1213 |
Const (_, T') $ t' => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1214 |
if domain_type T' = body_type T andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1215 |
forall (uncurry (is_nth_sel_on t')) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1216 |
(index_seq 0 (length args) ~~ args) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1217 |
t' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1218 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1219 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1220 |
| _ => raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1221 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1222 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1223 |
else if is_sel_like_and_no_discr s then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1224 |
case strip_comb (hd args) of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1225 |
(Const (x' as (s', T')), ts') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1226 |
if is_constr_like thy x' andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1227 |
constr_name_for_sel_like s = s' andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1228 |
not (exists is_pair_type (binder_types T')) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1229 |
list_comb (nth ts' (sel_no_from_name s), tl args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1230 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1231 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1232 |
| _ => raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1233 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1234 |
raise SAME ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1235 |
handle SAME () => betapplys (t, args)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1236 |
| do_term (Abs (s, T, t')) args = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1237 |
betapplys (Abs (s, T, do_term t' []), args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1238 |
| do_term t args = betapplys (t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1239 |
in do_term t [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1240 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1241 |
(** Quantifier massaging: Distributing quantifiers **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1242 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1243 |
(* term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1244 |
fun distribute_quantifiers t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1245 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1246 |
(t0 as Const (@{const_name All}, T0)) $ Abs (s, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1247 |
(case t1 of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1248 |
(t10 as @{const "op &"}) $ t11 $ t12 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1249 |
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1250 |
$ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1251 |
| (t10 as @{const Not}) $ t11 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1252 |
t10 $ distribute_quantifiers (Const (@{const_name Ex}, T0) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1253 |
$ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1254 |
| t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1255 |
if not (loose_bvar1 (t1, 0)) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1256 |
distribute_quantifiers (incr_boundvars ~1 t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1257 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1258 |
t0 $ Abs (s, T1, distribute_quantifiers t1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1259 |
| (t0 as Const (@{const_name Ex}, T0)) $ Abs (s, T1, t1) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1260 |
(case distribute_quantifiers t1 of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1261 |
(t10 as @{const "op |"}) $ t11 $ t12 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1262 |
t10 $ distribute_quantifiers (t0 $ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1263 |
$ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1264 |
| (t10 as @{const "op -->"}) $ t11 $ t12 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1265 |
t10 $ distribute_quantifiers (Const (@{const_name All}, T0) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1266 |
$ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1267 |
$ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1268 |
| (t10 as @{const Not}) $ t11 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1269 |
t10 $ distribute_quantifiers (Const (@{const_name All}, T0) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1270 |
$ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1271 |
| t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1272 |
if not (loose_bvar1 (t1, 0)) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1273 |
distribute_quantifiers (incr_boundvars ~1 t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1274 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1275 |
t0 $ Abs (s, T1, distribute_quantifiers t1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1276 |
| t1 $ t2 => distribute_quantifiers t1 $ distribute_quantifiers t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1277 |
| Abs (s, T, t') => Abs (s, T, distribute_quantifiers t') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1278 |
| _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1279 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1280 |
(** Quantifier massaging: Pushing quantifiers inward **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1281 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1282 |
(* int -> int -> (int -> int) -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1283 |
fun renumber_bounds j n f t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1284 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1285 |
t1 $ t2 => renumber_bounds j n f t1 $ renumber_bounds j n f t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1286 |
| Abs (s, T, t') => Abs (s, T, renumber_bounds (j + 1) n f t') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1287 |
| Bound j' => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1288 |
Bound (if j' >= j andalso j' < j + n then f (j' - j) + j else j') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1289 |
| _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1290 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1291 |
(* Maximum number of quantifiers in a cluster for which the exponential |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1292 |
algorithm is used. Larger clusters use a heuristic inspired by Claessen & |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1293 |
Soerensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1294 |
paper). *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1295 |
val quantifier_cluster_threshold = 7 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1296 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1297 |
(* term -> term *) |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1298 |
val push_quantifiers_inward = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1299 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1300 |
(* string -> string list -> typ list -> term -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1301 |
fun aux quant_s ss Ts t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1302 |
(case t of |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1303 |
Const (s0, _) $ Abs (s1, T1, t1 as _ $ _) => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1304 |
if s0 = quant_s then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1305 |
aux s0 (s1 :: ss) (T1 :: Ts) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1306 |
else if quant_s = "" andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1307 |
(s0 = @{const_name All} orelse s0 = @{const_name Ex}) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1308 |
aux s0 [s1] [T1] t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1309 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1310 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1311 |
| _ => raise SAME ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1312 |
handle SAME () => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1313 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1314 |
t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1315 |
if quant_s = "" then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1316 |
aux "" [] [] t1 $ aux "" [] [] t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1317 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1318 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1319 |
val typical_card = 4 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1320 |
(* ('a -> ''b list) -> 'a list -> ''b list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1321 |
fun big_union proj ps = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1322 |
fold (fold (insert (op =)) o proj) ps [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1323 |
val (ts, connective) = strip_any_connective t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1324 |
val T_costs = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1325 |
map (bounded_card_of_type 65536 typical_card []) Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1326 |
val t_costs = map size_of_term ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1327 |
val num_Ts = length Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1328 |
(* int -> int *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1329 |
val flip = curry (op -) (num_Ts - 1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1330 |
val t_boundss = map (map flip o loose_bnos) ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1331 |
(* (int list * int) list -> int list |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1332 |
-> (int list * int) list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1333 |
fun merge costly_boundss [] = costly_boundss |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1334 |
| merge costly_boundss (j :: js) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1335 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1336 |
val (yeas, nays) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1337 |
List.partition (fn (bounds, _) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1338 |
member (op =) bounds j) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1339 |
costly_boundss |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1340 |
val yeas_bounds = big_union fst yeas |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1341 |
val yeas_cost = Integer.sum (map snd yeas) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1342 |
* nth T_costs j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1343 |
in merge ((yeas_bounds, yeas_cost) :: nays) js end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1344 |
(* (int list * int) list -> int list -> int *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1345 |
val cost = Integer.sum o map snd oo merge |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1346 |
(* (int list * int) list -> int list -> int list *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1347 |
fun heuristically_best_permutation _ [] = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1348 |
| heuristically_best_permutation costly_boundss js = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1349 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1350 |
val (costly_boundss, (j, js)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1351 |
js |> map (`(merge costly_boundss o single)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1352 |
|> sort (int_ord |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1353 |
o pairself (Integer.sum o map snd o fst)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1354 |
|> split_list |>> hd ||> pairf hd tl |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1355 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1356 |
j :: heuristically_best_permutation costly_boundss js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1357 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1358 |
val js = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1359 |
if length Ts <= quantifier_cluster_threshold then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1360 |
all_permutations (index_seq 0 num_Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1361 |
|> map (`(cost (t_boundss ~~ t_costs))) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1362 |
|> sort (int_ord o pairself fst) |> hd |> snd |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1363 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1364 |
heuristically_best_permutation (t_boundss ~~ t_costs) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1365 |
(index_seq 0 num_Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1366 |
val back_js = map (fn j => find_index (curry (op =) j) js) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1367 |
(index_seq 0 num_Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1368 |
val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1369 |
ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1370 |
(* (term * int list) list -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1371 |
fun mk_connection [] = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1372 |
raise ARG ("Nitpick_Preproc.push_quantifiers_inward.aux.\ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1373 |
\mk_connection", "") |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1374 |
| mk_connection ts_cum_bounds = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1375 |
ts_cum_bounds |> map fst |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1376 |
|> foldr1 (fn (t1, t2) => connective $ t1 $ t2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1377 |
(* (term * int list) list -> int list -> term *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1378 |
fun build ts_cum_bounds [] = ts_cum_bounds |> mk_connection |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1379 |
| build ts_cum_bounds (j :: js) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1380 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1381 |
val (yeas, nays) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1382 |
List.partition (fn (_, bounds) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1383 |
member (op =) bounds j) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1384 |
ts_cum_bounds |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1385 |
||> map (apfst (incr_boundvars ~1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1386 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1387 |
if null yeas then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1388 |
build nays js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1389 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1390 |
let val T = nth Ts (flip j) in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1391 |
build ((Const (quant_s, (T --> bool_T) --> bool_T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1392 |
$ Abs (nth ss (flip j), T, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1393 |
mk_connection yeas), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1394 |
big_union snd yeas) :: nays) js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1395 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1396 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1397 |
in build (ts ~~ t_boundss) js end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1398 |
| Abs (s, T, t') => Abs (s, T, aux "" [] [] t') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1399 |
| _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1400 |
in aux "" [] [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1401 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1402 |
(** Preprocessor entry point **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1403 |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1404 |
(* hol_context -> term -> term list * term list * bool * bool * bool *) |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1405 |
fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs, |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1406 |
boxes, skolemize, uncurry, ...}) t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1407 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1408 |
val skolem_depth = if skolemize then 4 else ~1 |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1409 |
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1410 |
t |> unfold_defs_in_term hol_ctxt |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1411 |
|> close_form |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1412 |
|> skolemize_term_and_more hol_ctxt skolem_depth |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1413 |
|> specialize_consts_in_term hol_ctxt 0 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1414 |
|> axioms_for_term hol_ctxt |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1415 |
val binarize = |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1416 |
is_standard_datatype thy stds nat_T andalso |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1417 |
case binary_ints of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1418 |
SOME false => false |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1419 |
| _ => forall may_use_binary_ints (nondef_ts @ def_ts) andalso |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1420 |
(binary_ints = SOME true orelse |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1421 |
exists should_use_binary_ints (nondef_ts @ def_ts)) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1422 |
val box = exists (not_equal (SOME false) o snd) boxes |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1423 |
val uncurry = uncurry andalso box |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1424 |
val table = |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1425 |
Termtab.empty |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1426 |
|> uncurry ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts) |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1427 |
(* bool -> term -> term *) |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1428 |
fun do_rest def = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1429 |
binarize ? binarize_nat_and_int_in_term |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1430 |
#> uncurry ? uncurry_term table |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1431 |
#> box ? box_fun_and_pair_in_term hol_ctxt def |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1432 |
#> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def |
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1433 |
#> pull_out_existential_constrs hol_ctxt |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1434 |
#> destroy_pulled_out_constrs hol_ctxt def) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1435 |
#> curry_assms |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1436 |
#> destroy_universal_equalities |
35220
2bcdae5f4fdb
added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
blanchet
parents:
35190
diff
changeset
|
1437 |
#> destroy_existential_equalities hol_ctxt |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1438 |
#> simplify_constrs_and_sels thy |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1439 |
#> distribute_quantifiers |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1440 |
#> push_quantifiers_inward |
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35070
diff
changeset
|
1441 |
#> close_form |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1442 |
#> Term.map_abs_vars shortest_name |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1443 |
val nondef_ts = map (do_rest false) nondef_ts |
35384 | 1444 |
val def_ts = map (do_rest true) def_ts |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1445 |
in |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1446 |
(nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1447 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1448 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1449 |
end; |