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