author | blanchet |
Tue, 01 Jun 2010 17:51:41 +0200 | |
changeset 37271 | 694aebcd602b |
parent 37260 | dde817e6dfb1 |
child 37476 | 0681e46b4022 |
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 : |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
12 |
hol_context -> (typ option * bool option) list |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
13 |
-> (typ option * bool option) list -> term |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
14 |
-> term list * term list * bool * bool * bool |
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35807
diff
changeset
|
15 |
end; |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
16 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
17 |
structure Nitpick_Preproc : NITPICK_PREPROC = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
18 |
struct |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
19 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
20 |
open Nitpick_Util |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
21 |
open Nitpick_HOL |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
22 |
open Nitpick_Mono |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
23 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
24 |
fun is_positive_existential polar quant_s = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
25 |
(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
|
26 |
(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
|
27 |
|
37271 | 28 |
val is_descr = |
29 |
member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The}, |
|
30 |
@{const_name safe_Eps}] |
|
31 |
||
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
32 |
(** Binary coding of integers **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
33 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
34 |
(* 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
|
35 |
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
|
36 |
binary coding. *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
37 |
val binary_int_threshold = 3 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
38 |
|
35718 | 39 |
val may_use_binary_ints = |
40 |
let |
|
41 |
fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) = |
|
42 |
aux def t1 andalso aux false t2 |
|
43 |
| aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2 |
|
44 |
| aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) = |
|
45 |
aux def t1 andalso aux false t2 |
|
46 |
| aux def (@{const "op -->"} $ t1 $ t2) = aux false t1 andalso aux def t2 |
|
47 |
| aux def (t1 $ t2) = aux def t1 andalso aux def t2 |
|
48 |
| aux def (t as Const (s, _)) = |
|
49 |
(not def orelse t <> @{const Suc}) andalso |
|
50 |
not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, |
|
51 |
@{const_name nat_gcd}, @{const_name nat_lcm}, |
|
52 |
@{const_name Frac}, @{const_name norm_frac}] s) |
|
53 |
| aux def (Abs (_, _, t')) = aux def t' |
|
54 |
| aux _ _ = true |
|
55 |
in aux end |
|
56 |
val should_use_binary_ints = |
|
57 |
let |
|
58 |
fun aux (t1 $ t2) = aux t1 orelse aux t2 |
|
59 |
| aux (Const (s, T)) = |
|
60 |
((s = @{const_name times} orelse s = @{const_name div}) andalso |
|
61 |
is_integer_type (body_type T)) orelse |
|
62 |
(String.isPrefix numeral_prefix s andalso |
|
63 |
let val n = the (Int.fromString (unprefix numeral_prefix s)) in |
|
64 |
n < ~ binary_int_threshold orelse n > binary_int_threshold |
|
65 |
end) |
|
66 |
| aux (Abs (_, _, t')) = aux t' |
|
67 |
| aux _ = false |
|
68 |
in aux end |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
69 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
70 |
(** Uncurrying **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
71 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
72 |
fun add_to_uncurry_table ctxt t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
73 |
let |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
74 |
val thy = ProofContext.theory_of ctxt |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
75 |
fun aux (t1 $ t2) args table = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
76 |
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
|
77 |
| aux (Abs (_, _, t')) _ table = aux t' [] table |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
78 |
| 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
|
79 |
if is_built_in_const thy [(NONE, true)] true x orelse |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
80 |
is_constr_like ctxt x orelse |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
81 |
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
|
82 |
table |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
83 |
else |
36384 | 84 |
Termtab.map_default (t, 65536) (Integer.min (length args)) table |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
85 |
| aux _ _ table = table |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
86 |
in aux t [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
87 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
88 |
fun uncurry_prefix_for k j = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
89 |
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
|
90 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
91 |
fun uncurry_term table t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
92 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
93 |
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
|
94 |
| 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
|
95 |
| aux (t as Const (s, T)) args = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
96 |
(case Termtab.lookup table t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
97 |
SOME n => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
98 |
if n >= 2 then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
99 |
let |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
100 |
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
|
101 |
val j = |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
102 |
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
|
103 |
1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
104 |
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
|
105 |
~1 => n |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
106 |
| j => j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
107 |
val ((before_args, tuple_args), after_args) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
108 |
args |> chop n |>> chop j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
109 |
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
|
110 |
T |> strip_n_binders n |>> chop j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
111 |
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
|
112 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
113 |
if n - j < 2 then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
114 |
betapplys (t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
115 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
116 |
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
|
117 |
before_arg_Ts ---> tuple_T --> rest_T), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
118 |
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
|
119 |
after_args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
120 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
121 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
122 |
betapplys (t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
123 |
| NONE => betapplys (t, args)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
124 |
| aux t args = betapplys (t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
125 |
in aux t [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
126 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
127 |
(** Boxing **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
128 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
129 |
fun box_fun_and_pair_in_term (hol_ctxt as {ctxt, thy, stds, fast_descrs, ...}) |
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
130 |
def orig_t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
131 |
let |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
132 |
fun box_relational_operator_type (Type (@{type_name fun}, Ts)) = |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
133 |
Type (@{type_name fun}, map box_relational_operator_type Ts) |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
134 |
| box_relational_operator_type (Type (@{type_name "*"}, Ts)) = |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
135 |
Type (@{type_name "*"}, map (box_type hol_ctxt InPair) Ts) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
136 |
| box_relational_operator_type T = T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
137 |
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
|
138 |
case t' of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
139 |
Var z' => z' = z ? insert (op =) T' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
140 |
| Const (@{const_name Pair}, _) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
141 |
(case T' of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
142 |
Type (_, [T1, T2]) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
143 |
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
|
144 |
| _ => 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
|
145 |
\add_boxed_types_for_var", [T'], [])) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
146 |
| _ => 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
|
147 |
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
|
148 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
149 |
@{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
|
150 |
| Const (s0, _) $ t1 $ _ => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
151 |
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
|
152 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
153 |
val (t', args) = strip_comb t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
154 |
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
|
155 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
156 |
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
|
157 |
(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
|
158 |
[T''] => T'' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
159 |
| _ => T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
160 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
161 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
162 |
T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
163 |
| _ => T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
164 |
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
|
165 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
166 |
val abs_T' = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
167 |
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
|
168 |
box_type hol_ctxt InFunLHS abs_T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
169 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
170 |
abs_T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
171 |
val body_T = body_type quant_T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
172 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
173 |
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
|
174 |
$ Abs (abs_s, abs_T', |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
175 |
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
|
176 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
177 |
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
|
178 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
179 |
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
|
180 |
val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2) |
35408 | 181 |
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
|
182 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
183 |
list_comb (Const (s0, T --> T --> body_type T0), |
35384 | 184 |
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
|
185 |
end |
37271 | 186 |
and do_descr s T = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
187 |
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
|
188 |
Const (s, (T1 --> bool_T) --> T1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
189 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
190 |
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
|
191 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
192 |
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
|
193 |
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
|
194 |
| 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
|
195 |
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
|
196 |
| @{const "==>"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
197 |
@{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
|
198 |
$ 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
|
199 |
| @{const Pure.conjunction} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
200 |
@{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
|
201 |
$ 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
|
202 |
| @{const Trueprop} $ t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
203 |
@{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
|
204 |
| @{const Not} $ t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
205 |
@{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
|
206 |
| 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
|
207 |
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
|
208 |
| 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
|
209 |
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
|
210 |
| 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
|
211 |
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
|
212 |
| @{const "op &"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
213 |
@{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
|
214 |
$ 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
|
215 |
| @{const "op |"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
216 |
@{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
|
217 |
$ 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
|
218 |
| @{const "op -->"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
219 |
@{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
|
220 |
$ 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
|
221 |
| Const (x as (s, T)) => |
37271 | 222 |
if is_descr s then |
223 |
do_descr s T |
|
224 |
else |
|
225 |
Const (s, if s = @{const_name converse} orelse |
|
226 |
s = @{const_name trancl} then |
|
227 |
box_relational_operator_type T |
|
228 |
else if String.isPrefix quot_normal_prefix s then |
|
229 |
let val T' = box_type hol_ctxt InFunLHS (domain_type T) in |
|
230 |
T' --> T' |
|
231 |
end |
|
232 |
else if is_built_in_const thy stds fast_descrs x orelse |
|
233 |
s = @{const_name Sigma} then |
|
234 |
T |
|
235 |
else if is_constr_like ctxt x then |
|
236 |
box_type hol_ctxt InConstr T |
|
237 |
else if is_sel s orelse is_rep_fun ctxt x then |
|
238 |
box_type hol_ctxt InSel T |
|
239 |
else |
|
240 |
box_type hol_ctxt InExpr T) |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
241 |
| t1 $ Abs (s, T, t2') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
242 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
243 |
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
|
244 |
val T1 = fastype_of1 (new_Ts, t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
245 |
val (s1, Ts1) = dest_Type T1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
246 |
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
|
247 |
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
|
248 |
val T2 = fastype_of1 (new_Ts, t2) |
35384 | 249 |
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
|
250 |
in |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
251 |
betapply (if s1 = @{type_name fun} then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
252 |
t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
253 |
else |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
254 |
select_nth_constr_arg ctxt stds |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
255 |
(@{const_name FunBox}, |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
256 |
Type (@{type_name fun}, Ts1) --> T1) t1 0 |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
257 |
(Type (@{type_name fun}, Ts1)), t2) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
258 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
259 |
| t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
260 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
261 |
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
|
262 |
val T1 = fastype_of1 (new_Ts, t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
263 |
val (s1, Ts1) = dest_Type T1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
264 |
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
|
265 |
val T2 = fastype_of1 (new_Ts, t2) |
35384 | 266 |
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
|
267 |
in |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
268 |
betapply (if s1 = @{type_name fun} then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
269 |
t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
270 |
else |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
271 |
select_nth_constr_arg ctxt stds |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
272 |
(@{const_name FunBox}, |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
273 |
Type (@{type_name fun}, Ts1) --> T1) t1 0 |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
274 |
(Type (@{type_name fun}, Ts1)), t2) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
275 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
276 |
| 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
|
277 |
| Var (z as (x, T)) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
278 |
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
|
279 |
else box_type hol_ctxt InExpr T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
280 |
| Bound _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
281 |
| Abs (s, T, t') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
282 |
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
|
283 |
in do_term [] [] Pos orig_t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
284 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
285 |
(** Destruction of constructors **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
286 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
287 |
val val_var_prefix = nitpick_prefix ^ "v" |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
288 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
289 |
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
|
290 |
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
|
291 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
292 |
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
|
293 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
294 |
fun aux [] = false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
295 |
| 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
|
296 |
| aux _ = true |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
297 |
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
|
298 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
299 |
fun pull_out_constr_comb ({ctxt, stds, ...} : hol_context) Ts relax k level 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
|
300 |
args seen = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
301 |
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
|
302 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
303 |
Const x => |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
304 |
if not relax andalso is_constr ctxt stds x andalso |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
305 |
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
|
306 |
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
|
307 |
not (loose_bvar (t_comb, level)) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
308 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
309 |
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
|
310 |
~1 => (0, t_comb :: seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
311 |
| j => (j, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
312 |
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
|
313 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
314 |
(t_comb, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
315 |
| _ => (t_comb, seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
316 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
317 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
318 |
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
|
319 |
let val n = length seen in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
320 |
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
|
321 |
(index_seq 0 n) seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
322 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
323 |
|
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
|
324 |
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
|
325 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
326 |
val k = maxidx_of_term t + 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
327 |
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
|
328 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
329 |
(t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
330 |
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
|
331 |
| (t0 as @{const "==>"}) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
332 |
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
|
333 |
| (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
|
334 |
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
|
335 |
| (t0 as @{const "op -->"}) $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
336 |
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
|
337 |
| Abs (s, T, t') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
338 |
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
|
339 |
(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
|
340 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
341 |
| t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
342 |
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
|
343 |
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
|
344 |
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
|
345 |
| _ => 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
|
346 |
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
|
347 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
348 |
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
|
349 |
else do_term Ts false t2 [] seen |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
350 |
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
|
351 |
in (t0 $ t1 $ t2, seen) end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
352 |
val (concl, seen) = do_term [] def t [] [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
353 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
354 |
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
|
355 |
seen, concl) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
356 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
357 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
358 |
fun mk_exists v t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
359 |
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
|
360 |
|
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
|
361 |
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
|
362 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
363 |
val k = maxidx_of_term t + 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
364 |
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
|
365 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
366 |
(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
|
367 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
368 |
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
|
369 |
val n = length seen' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
370 |
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
|
371 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
372 |
(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
|
373 |
|> 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
|
374 |
|> 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
|
375 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
376 |
| t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
377 |
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
|
378 |
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
|
379 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
380 |
| Abs (s, T, t') => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
381 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
382 |
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
|
383 |
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
|
384 |
| _ => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
385 |
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
|
386 |
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
|
387 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
388 |
(list_comb (t, args), seen) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
389 |
in aux [] 0 t [] [] |> fst end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
390 |
|
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
391 |
val let_var_prefix = nitpick_prefix ^ "l" |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
392 |
val let_inline_threshold = 32 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
393 |
|
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
394 |
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
|
395 |
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
|
396 |
f t |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
397 |
else |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
398 |
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
|
399 |
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
|
400 |
$ 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
|
401 |
end |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
402 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
403 |
fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
404 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
405 |
val num_occs_of_var = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
406 |
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
|
407 |
| _ => I) t (K 0) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
408 |
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
|
409 |
aux_eq careful true t0 t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
410 |
| aux careful ((t0 as @{const "==>"}) $ t1 $ t2) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
411 |
t0 $ aux false t1 $ aux careful t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
412 |
| 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
|
413 |
aux_eq careful true t0 t1 t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
414 |
| 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
|
415 |
t0 $ aux false t1 $ aux careful t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
416 |
| 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
|
417 |
| 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
|
418 |
| aux _ t = t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
419 |
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
|
420 |
((if careful then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
421 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
422 |
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
|
423 |
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
|
424 |
@{const True} |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
425 |
else case strip_comb t2 of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
426 |
(* 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
|
427 |
(Const (@{const_name PairBox}, _), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
428 |
[Const (@{const_name fst}, _) $ Var z1, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
429 |
Const (@{const_name snd}, _) $ Var z2]) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
430 |
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
|
431 |
else raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
432 |
| (Const (x as (s, T)), args) => |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
433 |
let |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
434 |
val (arg_Ts, dataT) = strip_type T |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
435 |
val n = length arg_Ts |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
436 |
in |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
437 |
if length args = n andalso |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
438 |
(is_constr ctxt stds x orelse s = @{const_name Pair} orelse |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
439 |
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
|
440 |
(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
|
441 |
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
|
442 |
hol_let (n + 1) dataT bool_T |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
443 |
(fn t1 => discriminate_value hol_ctxt x t1 :: |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
444 |
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
|
445 |
|> foldr1 s_conj) t1 |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
446 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
447 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
448 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
449 |
| _ => raise SAME ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
450 |
|> 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
|
451 |
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
|
452 |
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
|
453 |
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
|
454 |
HOLogic.eq_const nth_T $ nth_t |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
455 |
$ select_nth_constr_arg ctxt stds x t n nth_T |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
456 |
|> aux false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
457 |
in aux axiom t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
458 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
459 |
(** Destruction of universal and existential equalities **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
460 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
461 |
fun curry_assms (@{const "==>"} $ (@{const Trueprop} |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
462 |
$ (@{const "op &"} $ t1 $ t2)) $ t3) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
463 |
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
|
464 |
| curry_assms (@{const "==>"} $ t1 $ t2) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
465 |
@{const "==>"} $ curry_assms t1 $ curry_assms t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
466 |
| curry_assms t = t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
467 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
468 |
val destroy_universal_equalities = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
469 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
470 |
fun aux prems zs t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
471 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
472 |
@{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
|
473 |
| _ => Logic.list_implies (rev prems, t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
474 |
and aux_implies prems zs t1 t2 = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
475 |
case t1 of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
476 |
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
|
477 |
| @{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
|
478 |
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
|
479 |
| @{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
|
480 |
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
|
481 |
| _ => 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
|
482 |
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
|
483 |
if not (member (op =) zs z) andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
484 |
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
|
485 |
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
|
486 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
487 |
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
|
488 |
in aux [] [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
489 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
490 |
fun find_bound_assign ctxt stds j = |
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
|
491 |
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
|
492 |
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
|
493 |
| 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
|
494 |
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
|
495 |
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
|
496 |
(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
|
497 |
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
|
498 |
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
|
499 |
Bound j' => if j' = j then SOME (t2, ts @ seen) else raise SAME () |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
500 |
| Const (s, Type (@{type_name fun}, [T1, T2])) $ Bound j' => |
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
|
501 |
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
|
502 |
s = nth_sel_name_for_constr_name @{const_name FunBox} 0 then |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
503 |
SOME (construct_value ctxt stds |
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
504 |
(@{const_name FunBox}, T2 --> T1) [t2], |
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
505 |
ts @ seen) |
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
|
506 |
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
|
507 |
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
|
508 |
| _ => 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
|
509 |
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
|
510 |
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
|
511 |
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
|
512 |
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
|
513 |
| _ => 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
|
514 |
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
|
515 |
in do_term end |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
516 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
517 |
fun subst_one_bound j arg t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
518 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
519 |
fun aux (Bound i, lev) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
520 |
if i < lev then raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
521 |
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
|
522 |
else Bound (i - 1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
523 |
| 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
|
524 |
| aux (f $ t, lev) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
525 |
(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
|
526 |
handle SAME () => f $ aux (t, lev)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
527 |
| aux _ = raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
528 |
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
|
529 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
530 |
fun destroy_existential_equalities ({ctxt, stds, ...} : hol_context) = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
531 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
532 |
fun kill [] [] ts = foldr1 s_conj ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
533 |
| kill (s :: ss) (T :: Ts) ts = |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
534 |
(case find_bound_assign ctxt stds (length ss) [] ts of |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
535 |
SOME (_, []) => @{const True} |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
536 |
| SOME (arg_t, ts) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
537 |
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
|
538 |
(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
|
539 |
| NONE => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
540 |
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
|
541 |
$ Abs (s, T, kill ss Ts ts)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
542 |
| kill _ _ _ = raise UnequalLengths |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
543 |
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
|
544 |
gather (ss @ [s1]) (Ts @ [T1]) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
545 |
| 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
|
546 |
| gather [] [] (t1 $ t2) = gather [] [] t1 $ gather [] [] t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
547 |
| gather [] [] t = t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
548 |
| 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
|
549 |
in gather [] [] end |
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 |
(** Skolemization **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
552 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
553 |
fun skolem_prefix_for k j = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
554 |
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
|
555 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
556 |
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
|
557 |
skolem_depth = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
558 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
559 |
val incrs = map (Integer.add 1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
560 |
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
|
561 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
562 |
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
|
563 |
if not (loose_bvar1 (t, 0)) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
564 |
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
|
565 |
else if depth <= skolem_depth andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
566 |
is_positive_existential polar quant_s then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
567 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
568 |
val j = length (!skolems) + 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
569 |
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
|
570 |
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
|
571 |
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
|
572 |
map Bound (rev js)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
573 |
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
|
574 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
575 |
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
|
576 |
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
|
577 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
578 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
579 |
Const (quant_s, quant_T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
580 |
$ Abs (abs_s, abs_T, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
581 |
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
|
582 |
t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
583 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
584 |
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
|
585 |
(depth + 1) polar t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
586 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
587 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
588 |
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
|
589 |
do_quantifier s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
590 |
| @{const "==>"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
591 |
@{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
|
592 |
$ aux ss Ts js depth polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
593 |
| @{const Pure.conjunction} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
594 |
@{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
|
595 |
$ aux ss Ts js depth polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
596 |
| @{const Trueprop} $ t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
597 |
@{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
|
598 |
| @{const Not} $ t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
599 |
@{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
|
600 |
| 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
|
601 |
do_quantifier s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
602 |
| 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
|
603 |
do_quantifier s0 T0 s1 T1 t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
604 |
| @{const "op &"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
605 |
@{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
|
606 |
$ aux ss Ts js depth polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
607 |
| @{const "op |"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
608 |
@{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
|
609 |
$ aux ss Ts js depth polar t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
610 |
| @{const "op -->"} $ t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
611 |
@{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
|
612 |
$ aux ss Ts js depth polar t2 |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
613 |
| (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
|
614 |
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
|
615 |
| Const (x as (s, T)) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
616 |
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
|
617 |
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
|
618 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
619 |
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
|
620 |
val (pref, connective, set_oper) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
621 |
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
|
622 |
(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
|
623 |
@{const_name semilattice_sup_class.sup}) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
624 |
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
|
625 |
(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
|
626 |
@{const_name semilattice_inf_class.inf}) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
627 |
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
|
628 |
|> aux ss Ts js depth polar |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
629 |
fun neg () = Const (pref ^ s, T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
630 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
631 |
(case polar |> gfp ? flip_polarity of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
632 |
Pos => pos () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
633 |
| Neg => neg () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
634 |
| Neut => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
635 |
if is_fun_type T then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
636 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
637 |
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
|
638 |
T |> strip_type |>> split_last |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
639 |
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
|
640 |
fun app f = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
641 |
list_comb (f (), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
642 |
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
|
643 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
644 |
List.foldr absdummy |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
645 |
(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
|
646 |
$ app pos $ app neg) trunk_arg_Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
647 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
648 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
649 |
connective $ pos () $ neg ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
650 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
651 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
652 |
Const x |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
653 |
| t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
654 |
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
|
655 |
aux ss Ts [] depth Neut t2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
656 |
| 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
|
657 |
| _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
658 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
659 |
in aux [] [] [] 0 Pos end |
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 |
(** Function specialization **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
662 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
663 |
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
|
664 |
| 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
|
665 |
| 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
|
666 |
snd (strip_comb t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
667 |
| params_in_equation _ = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
668 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
669 |
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
|
670 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
671 |
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
|
672 |
+ 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
673 |
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
|
674 |
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
|
675 |
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
|
676 |
| 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
|
677 |
| aux args t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
678 |
if t = Const x then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
679 |
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
|
680 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
681 |
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
|
682 |
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
|
683 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
684 |
in aux [] t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
685 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
686 |
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
|
687 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
688 |
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
|
689 |
| 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
|
690 |
| fun_calls t args = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
691 |
(case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
692 |
Const (x' as (s', T')) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
693 |
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
|
694 |
SOME s'' => x = (s'', T') |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
695 |
| NONE => false) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
696 |
| _ => false) ? cons args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
697 |
fun call_sets [] [] vs = [vs] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
698 |
| 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
|
699 |
| call_sets ([] :: _) _ _ = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
700 |
| call_sets ((t :: ts) :: tss) uss vs = |
35408 | 701 |
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
|
702 |
val sets = call_sets (fun_calls t [] []) [] [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
703 |
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
|
704 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
705 |
fold_rev (fn (set, j) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
706 |
case set of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
707 |
[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
|
708 |
? cons (j, NONE) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
709 |
| [t as Const _] => cons (j, SOME t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
710 |
| [t as Free _] => cons (j, SOME t) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
711 |
| _ => I) indexed_sets [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
712 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
713 |
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
|
714 |
map (static_args_in_term hol_ctxt x) |
35408 | 715 |
#> 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
|
716 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
717 |
fun overlapping_indices [] _ = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
718 |
| overlapping_indices _ [] = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
719 |
| 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
|
720 |
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
|
721 |
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
|
722 |
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
|
723 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
724 |
fun is_eligible_arg Ts t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
725 |
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
|
726 |
null bad_Ts orelse |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
727 |
(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
|
728 |
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
|
729 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
730 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
731 |
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
|
732 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
733 |
(* 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
|
734 |
prevent excessive specialization by not specializing it. *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
735 |
val special_max_depth = 20 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
736 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
737 |
val bound_var_prefix = "b" |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
738 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
739 |
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
|
740 |
special_funs, ...}) depth t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
741 |
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
|
742 |
t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
743 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
744 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
745 |
val blacklist = if depth = 0 then [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
746 |
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
|
747 |
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
|
748 |
((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
|
749 |
not (String.isPrefix special_prefix s) andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
750 |
is_equational_fun hol_ctxt x then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
751 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
752 |
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
|
753 |
(index_seq 0 (length args) ~~ args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
754 |
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
|
755 |
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
|
756 |
|> map (destroy_existential_equalities hol_ctxt) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
757 |
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
|
758 |
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
|
759 |
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
|
760 |
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
|
761 |
val vars = fold Term.add_vars fixed_args [] |
35408 | 762 |
|> 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
|
763 |
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
|
764 |
fixed_args [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
765 |
|> sort int_ord |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
766 |
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
|
767 |
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
|
768 |
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
|
769 |
val k = maxidx_of_term t + 1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
770 |
fun var_for_bound_no j = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
771 |
Var ((bound_var_prefix ^ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
772 |
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
|
773 |
+ 1), k), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
774 |
nth Ts j) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
775 |
val fixed_args_in_axiom = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
776 |
map (curry subst_bounds |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
777 |
(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
|
778 |
fixed_args |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
779 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
780 |
case AList.lookup (op =) (!special_funs) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
781 |
(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
|
782 |
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
|
783 |
| NONE => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
784 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
785 |
val extra_args_in_axiom = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
786 |
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
|
787 |
val x' as (s', _) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
788 |
(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
|
789 |
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
|
790 |
---> body_type T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
791 |
val new_axs = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
792 |
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
|
793 |
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
|
794 |
val _ = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
795 |
Unsynchronized.change special_funs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
796 |
(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
|
797 |
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
|
798 |
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
|
799 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
800 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
801 |
raise SAME ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
802 |
handle SAME () => list_comb (Const x, args)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
803 |
| aux args Ts (Abs (s, T, t)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
804 |
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
|
805 |
| 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
|
806 |
| aux args _ t = list_comb (t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
807 |
in aux [] [] t end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
808 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
809 |
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
|
810 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
811 |
val cong_var_prefix = "c" |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
812 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
813 |
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
|
814 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
815 |
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
|
816 |
val Ts = binder_types T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
817 |
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
|
818 |
val (eqs, (args1, args2)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
819 |
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
|
820 |
(js1 ~~ ts1, js2 ~~ ts2) of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
821 |
(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
|
822 |
| (SOME t1, NONE) => apsnd (apsnd (cons t1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
823 |
| (NONE, SOME t2) => apsnd (apfst (cons t2)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
824 |
| (NONE, NONE) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
825 |
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
|
826 |
nth Ts j) in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
827 |
apsnd (pairself (cons v)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
828 |
end) (max_j downto 0) ([], ([], [])) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
829 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
830 |
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
|
831 |
|> map Logic.mk_equals, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
832 |
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
|
833 |
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
|
834 |
|> close_form (* TODO: needed? *) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
835 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
836 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
837 |
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
|
838 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
839 |
val groups = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
840 |
!special_funs |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
841 |
|> 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
|
842 |
|> AList.group (op =) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
843 |
|> 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
|
844 |
|> 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
|
845 |
fun generality (js, _, _) = ~(length js) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
846 |
fun is_more_specific (j1, t1, x1) (j2, t2, x2) = |
35408 | 847 |
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
|
848 |
(j2 ~~ t2, j1 ~~ t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
849 |
fun do_pass_1 _ [] [_] [_] = I |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
850 |
| 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
|
851 |
| 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
|
852 |
case filter (is_more_specific z) all |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
853 |
|> sort (int_ord o pairself generality) of |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
854 |
[] => do_pass_1 T (z :: skipped) all zs |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
855 |
| (z' :: _) => cons (special_congruence_axiom T z z') |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
856 |
#> do_pass_1 T skipped all zs |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
857 |
and do_pass_2 _ [] = I |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
858 |
| do_pass_2 T (z :: zs) = |
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
859 |
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
|
860 |
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
|
861 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
862 |
(** Axiom selection **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
863 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
864 |
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
|
865 |
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
|
866 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
867 |
fun eval_axiom_for_term j t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
868 |
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
|
869 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
870 |
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
|
871 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
872 |
(* 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
|
873 |
val axioms_max_depth = 255 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
874 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
875 |
fun axioms_for_term |
35311 | 876 |
(hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms, |
35807
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35718
diff
changeset
|
877 |
fast_descrs, evals, def_table, nondef_table, |
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35718
diff
changeset
|
878 |
choice_spec_table, user_nondefs, ...}) t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
879 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
880 |
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
|
881 |
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
|
882 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
883 |
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
|
884 |
|> skolemize_term_and_more hol_ctxt ~1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
885 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
886 |
if is_trivial_equation t then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
887 |
accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
888 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
889 |
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
|
890 |
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
|
891 |
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
|
892 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
893 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
894 |
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
|
895 |
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
|
896 |
and add_maybe_def_axiom depth t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
897 |
(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
|
898 |
else add_nondef_axiom) depth t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
899 |
and add_eq_axiom depth t = |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
900 |
(if is_constr_pattern_formula ctxt t then add_def_axiom |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
901 |
else add_nondef_axiom) depth t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
902 |
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
|
903 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
904 |
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
|
905 |
| 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
|
906 |
(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
|
907 |
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
|
908 |
accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
909 |
else |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
910 |
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
|
911 |
if depth > axioms_max_depth then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
912 |
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
|
913 |
\add_axioms_for_term", |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
914 |
"too many nested axioms (" ^ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
915 |
string_of_int depth ^ ")") |
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset
|
916 |
else if is_of_class_const thy x then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
917 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
918 |
val class = Logic.class_of_const s |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
919 |
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
|
920 |
class) |
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36389
diff
changeset
|
921 |
val ax1 = try (specialize_type thy x) of_class |
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36389
diff
changeset
|
922 |
val ax2 = Option.map (specialize_type thy x o snd) |
37260
dde817e6dfb1
added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
blanchet
parents:
37256
diff
changeset
|
923 |
(get_class_def thy class) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
924 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
925 |
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
|
926 |
accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
927 |
end |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
928 |
else if is_constr ctxt stds x then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
929 |
accum |
37271 | 930 |
else if is_descr (original_name s) then |
931 |
fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x) |
|
932 |
accum |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
933 |
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
|
934 |
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
|
935 |
accum |
35807
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35718
diff
changeset
|
936 |
else if is_choice_spec_fun hol_ctxt x then |
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35718
diff
changeset
|
937 |
fold (add_nondef_axiom depth) |
e4d1b5cbd429
added support for "specification" and "ax_specification" constructs to Nitpick
blanchet
parents:
35718
diff
changeset
|
938 |
(nondef_props_for_const thy true choice_spec_table x) accum |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
939 |
else if is_abs_fun ctxt x then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
940 |
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
|
941 |
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
|
942 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
943 |
accum |> fold (add_nondef_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
944 |
(nondef_props_for_const thy false nondef_table x) |
35312 | 945 |
|> (is_funky_typedef thy (range_type T) orelse |
946 |
range_type T = nat_T) |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
947 |
? fold (add_maybe_def_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
948 |
(nondef_props_for_const thy true |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
949 |
(extra_table def_table s) x) |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
950 |
else if is_rep_fun ctxt x then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
951 |
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
|
952 |
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
|
953 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
954 |
accum |> fold (add_nondef_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
955 |
(nondef_props_for_const thy false nondef_table x) |
35312 | 956 |
|> (is_funky_typedef thy (range_type T) orelse |
957 |
range_type T = nat_T) |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
958 |
? fold (add_maybe_def_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
959 |
(nondef_props_for_const thy true |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
960 |
(extra_table def_table s) x) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
961 |
|> add_axioms_for_term depth |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
962 |
(Const (mate_of_rep_fun ctxt x)) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
963 |
|> fold (add_def_axiom depth) |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
964 |
(inverse_axioms_for_rep_fun ctxt x) |
37253 | 965 |
else if s = @{const_name TYPE} then |
966 |
accum |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
967 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
968 |
accum |> user_axioms <> SOME false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
969 |
? fold (add_nondef_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
970 |
(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
|
971 |
end) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
972 |
|> add_axioms_for_type depth T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
973 |
| 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
|
974 |
| 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
|
975 |
| Bound _ => accum |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
976 |
| 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
|
977 |
|> add_axioms_for_type depth T |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
978 |
and add_axioms_for_type depth T = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
979 |
case T of |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
980 |
Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
981 |
| Type (@{type_name "*"}, Ts) => fold (add_axioms_for_type depth) Ts |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
982 |
| @{typ prop} => I |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
983 |
| @{typ bool} => I |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
984 |
| @{typ unit} => I |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
985 |
| 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
|
986 |
| 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
|
987 |
| Type (z as (_, Ts)) => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
988 |
fold (add_axioms_for_type depth) Ts |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
989 |
#> (if is_pure_typedef ctxt T then |
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
990 |
fold (add_maybe_def_axiom depth) (optimized_typedef_axioms ctxt z) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
991 |
else if is_quot_type thy T then |
35311 | 992 |
fold (add_def_axiom depth) |
993 |
(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
|
994 |
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
|
995 |
fold (add_maybe_def_axiom depth) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
996 |
(codatatype_bisim_axioms hol_ctxt T) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
997 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
998 |
I) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
999 |
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
|
1000 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1001 |
val supers = Sign.complete_sort thy S |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1002 |
val class_axioms = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1003 |
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
|
1004 |
handle ERROR _ => [])) supers |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1005 |
val monomorphic_class_axioms = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1006 |
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
|
1007 |
[] => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1008 |
| [(x, S)] => |
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36389
diff
changeset
|
1009 |
monomorphic_term (Vartab.make [(x, (S, T))]) t |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1010 |
| _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\ |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1011 |
\add_axioms_for_sort", [t])) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1012 |
class_axioms |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1013 |
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
|
1014 |
val (mono_user_nondefs, poly_user_nondefs) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1015 |
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
|
1016 |
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
|
1017 |
evals |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1018 |
val (xs, (defs, nondefs)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1019 |
([], ([], [])) |> add_axioms_for_term 1 t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1020 |
|> 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
|
1021 |
|> user_axioms = SOME true |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1022 |
? 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
|
1023 |
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
|
1024 |
val got_all_mono_user_axioms = |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1025 |
(user_axioms = SOME true orelse null mono_user_nondefs) |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1026 |
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
|
1027 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1028 |
(** Simplification of constructor/selector terms **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1029 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1030 |
fun simplify_constrs_and_sels ctxt t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1031 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1032 |
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
|
1033 |
(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
|
1034 |
sel_no_from_name s = n) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1035 |
| is_nth_sel_on _ _ _ = false |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1036 |
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
|
1037 |
$ (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
|
1038 |
| do_term (Const (@{const_name Abs_Frac}, _) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1039 |
$ (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
|
1040 |
| 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
|
1041 |
| do_term (t as Const (x as (s, T))) (args as _ :: _) = |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1042 |
((if is_constr_like ctxt x then |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1043 |
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
|
1044 |
case hd args of |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1045 |
Const (_, T') $ t' => |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1046 |
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
|
1047 |
forall (uncurry (is_nth_sel_on t')) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1048 |
(index_seq 0 (length args) ~~ args) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1049 |
t' |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1050 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1051 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1052 |
| _ => raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1053 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1054 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1055 |
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
|
1056 |
case strip_comb (hd args) of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1057 |
(Const (x' as (s', T')), ts') => |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1058 |
if is_constr_like ctxt x' andalso |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1059 |
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
|
1060 |
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
|
1061 |
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
|
1062 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1063 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1064 |
| _ => raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1065 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1066 |
raise SAME ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1067 |
handle SAME () => betapplys (t, args)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1068 |
| do_term (Abs (s, T, t')) args = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1069 |
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
|
1070 |
| do_term t args = betapplys (t, args) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1071 |
in do_term t [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1072 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1073 |
(** Quantifier massaging: Distributing quantifiers **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1074 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1075 |
fun distribute_quantifiers t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1076 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1077 |
(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
|
1078 |
(case t1 of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1079 |
(t10 as @{const "op &"}) $ t11 $ t12 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1080 |
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
|
1081 |
$ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1082 |
| (t10 as @{const Not}) $ t11 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1083 |
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
|
1084 |
$ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1085 |
| t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1086 |
if not (loose_bvar1 (t1, 0)) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1087 |
distribute_quantifiers (incr_boundvars ~1 t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1088 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1089 |
t0 $ Abs (s, T1, distribute_quantifiers t1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1090 |
| (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
|
1091 |
(case distribute_quantifiers t1 of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1092 |
(t10 as @{const "op |"}) $ t11 $ t12 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1093 |
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
|
1094 |
$ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1095 |
| (t10 as @{const "op -->"}) $ t11 $ t12 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1096 |
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
|
1097 |
$ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1098 |
$ distribute_quantifiers (t0 $ Abs (s, T1, t12)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1099 |
| (t10 as @{const Not}) $ t11 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1100 |
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
|
1101 |
$ Abs (s, T1, t11)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1102 |
| t1 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1103 |
if not (loose_bvar1 (t1, 0)) then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1104 |
distribute_quantifiers (incr_boundvars ~1 t1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1105 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1106 |
t0 $ Abs (s, T1, distribute_quantifiers t1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1107 |
| 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
|
1108 |
| 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
|
1109 |
| _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1110 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1111 |
(** Quantifier massaging: Pushing quantifiers inward **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1112 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1113 |
fun renumber_bounds j n f t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1114 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1115 |
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
|
1116 |
| 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
|
1117 |
| Bound j' => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1118 |
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
|
1119 |
| _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1120 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1121 |
(* 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
|
1122 |
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
|
1123 |
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
|
1124 |
paper). *) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1125 |
val quantifier_cluster_threshold = 7 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1126 |
|
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1127 |
val push_quantifiers_inward = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1128 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1129 |
fun aux quant_s ss Ts t = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1130 |
(case t of |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1131 |
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
|
1132 |
if s0 = quant_s then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1133 |
aux s0 (s1 :: ss) (T1 :: Ts) t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1134 |
else if quant_s = "" andalso |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1135 |
(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
|
1136 |
aux s0 [s1] [T1] t1 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1137 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1138 |
raise SAME () |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1139 |
| _ => raise SAME ()) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1140 |
handle SAME () => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1141 |
case t of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1142 |
t1 $ t2 => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1143 |
if quant_s = "" then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1144 |
aux "" [] [] t1 $ aux "" [] [] t2 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1145 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1146 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1147 |
val typical_card = 4 |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1148 |
fun big_union proj ps = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1149 |
fold (fold (insert (op =)) o proj) ps [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1150 |
val (ts, connective) = strip_any_connective t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1151 |
val T_costs = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1152 |
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
|
1153 |
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
|
1154 |
val num_Ts = length Ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1155 |
val flip = curry (op -) (num_Ts - 1) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1156 |
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
|
1157 |
fun merge costly_boundss [] = costly_boundss |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1158 |
| merge costly_boundss (j :: js) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1159 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1160 |
val (yeas, nays) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1161 |
List.partition (fn (bounds, _) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1162 |
member (op =) bounds j) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1163 |
costly_boundss |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1164 |
val yeas_bounds = big_union fst yeas |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1165 |
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
|
1166 |
* nth T_costs j |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1167 |
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
|
1168 |
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
|
1169 |
fun heuristically_best_permutation _ [] = [] |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1170 |
| heuristically_best_permutation costly_boundss js = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1171 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1172 |
val (costly_boundss, (j, js)) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1173 |
js |> map (`(merge costly_boundss o single)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1174 |
|> sort (int_ord |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1175 |
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
|
1176 |
|> split_list |>> hd ||> pairf hd tl |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1177 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1178 |
j :: heuristically_best_permutation costly_boundss js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1179 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1180 |
val js = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1181 |
if length Ts <= quantifier_cluster_threshold then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1182 |
all_permutations (index_seq 0 num_Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1183 |
|> map (`(cost (t_boundss ~~ t_costs))) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1184 |
|> 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
|
1185 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1186 |
heuristically_best_permutation (t_boundss ~~ t_costs) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1187 |
(index_seq 0 num_Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1188 |
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
|
1189 |
(index_seq 0 num_Ts) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1190 |
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
|
1191 |
ts |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1192 |
fun mk_connection [] = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1193 |
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
|
1194 |
\mk_connection", "") |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1195 |
| mk_connection ts_cum_bounds = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1196 |
ts_cum_bounds |> map fst |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1197 |
|> foldr1 (fn (t1, t2) => connective $ t1 $ t2) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1198 |
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
|
1199 |
| build ts_cum_bounds (j :: js) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1200 |
let |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1201 |
val (yeas, nays) = |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1202 |
List.partition (fn (_, bounds) => |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1203 |
member (op =) bounds j) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1204 |
ts_cum_bounds |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1205 |
||> map (apfst (incr_boundvars ~1)) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1206 |
in |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1207 |
if null yeas then |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1208 |
build nays js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1209 |
else |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1210 |
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
|
1211 |
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
|
1212 |
$ Abs (nth ss (flip j), T, |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1213 |
mk_connection yeas), |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1214 |
big_union snd yeas) :: nays) js |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1215 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1216 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1217 |
in build (ts ~~ t_boundss) js end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1218 |
| 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
|
1219 |
| _ => t |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1220 |
in aux "" [] [] end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1221 |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1222 |
(** Inference of finite functions **) |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1223 |
|
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1224 |
fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1225 |
(nondef_ts, def_ts) = |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1226 |
let |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1227 |
val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1228 |
|> filter_out (fn Type (@{type_name fun_box}, _) => true |
35672 | 1229 |
| @{typ signed_bit} => true |
1230 |
| @{typ unsigned_bit} => true |
|
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1231 |
| T => is_small_finite_type hol_ctxt T orelse |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1232 |
triple_lookup (type_match thy) monos T |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1233 |
= SOME (SOME false)) |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1234 |
in fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) end |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1235 |
|
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1236 |
(** Preprocessor entry point **) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1237 |
|
36389
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset
|
1238 |
val max_skolem_depth = 4 |
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset
|
1239 |
|
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1240 |
fun preprocess_term (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, |
36389
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset
|
1241 |
boxes, ...}) finitizes monos t = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1242 |
let |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1243 |
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
|
1244 |
t |> unfold_defs_in_term hol_ctxt |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1245 |
|> close_form |
36389
8228b3a4a2ba
remove "skolemize" option from Nitpick, since Skolemization is always useful
blanchet
parents:
36388
diff
changeset
|
1246 |
|> skolemize_term_and_more hol_ctxt max_skolem_depth |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1247 |
|> specialize_consts_in_term hol_ctxt 0 |
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1248 |
|> axioms_for_term hol_ctxt |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1249 |
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
|
1250 |
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
|
1251 |
case binary_ints of |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1252 |
SOME false => false |
35718 | 1253 |
| _ => forall (may_use_binary_ints false) nondef_ts andalso |
1254 |
forall (may_use_binary_ints true) 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
|
1255 |
(binary_ints = SOME true orelse |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1256 |
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
|
1257 |
val box = exists (not_equal (SOME false) o snd) boxes |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1258 |
val table = |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1259 |
Termtab.empty |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1260 |
|> box ? fold (add_to_uncurry_table ctxt) (nondef_ts @ def_ts) |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1261 |
fun do_rest def = |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1262 |
binarize ? binarize_nat_and_int_in_term |
36388 | 1263 |
#> box ? uncurry_term table |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1264 |
#> 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
|
1265 |
#> 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
|
1266 |
#> pull_out_existential_constrs hol_ctxt |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1267 |
#> destroy_pulled_out_constrs hol_ctxt def) |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1268 |
#> curry_assms |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1269 |
#> 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
|
1270 |
#> destroy_existential_equalities hol_ctxt |
37256
0dca1ec52999
thread along context instead of theory for typedef lookup
blanchet
parents:
37253
diff
changeset
|
1271 |
#> simplify_constrs_and_sels ctxt |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1272 |
#> distribute_quantifiers |
35280
54ab4921f826
fixed a few bugs in Nitpick and removed unreferenced variables
blanchet
parents:
35220
diff
changeset
|
1273 |
#> push_quantifiers_inward |
35078
6fd1052fe463
optimization to quantifiers in Nitpick's handling of simp rules + renamed some SAT solvers
blanchet
parents:
35070
diff
changeset
|
1274 |
#> close_form |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1275 |
#> Term.map_abs_vars shortest_name |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1276 |
val nondef_ts = map (do_rest false) nondef_ts |
35384 | 1277 |
val def_ts = map (do_rest true) def_ts |
35665
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1278 |
val (nondef_ts, def_ts) = |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1279 |
finitize_all_types_of_funs hol_ctxt binarize finitizes monos |
ff2bf50505ab
added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
blanchet
parents:
35408
diff
changeset
|
1280 |
(nondef_ts, def_ts) |
35070
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1281 |
in |
35386
45a4e19d3ebd
more work on the new monotonicity stuff in Nitpick
blanchet
parents:
35385
diff
changeset
|
1282 |
(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
|
1283 |
end |
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1284 |
|
96136eb6218f
split "nitpick_hol.ML" into two files to make it more manageable;
blanchet
parents:
diff
changeset
|
1285 |
end; |