23466
|
1 |
(* Title: HOL/Tools/Presburger/cooper.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Amine Chaieb, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
|
6 |
signature COOPER =
|
|
7 |
sig
|
23484
|
8 |
val cooper_conv : Proof.context -> conv
|
23466
|
9 |
exception COOPER of string * exn
|
|
10 |
end;
|
|
11 |
|
|
12 |
structure Cooper: COOPER =
|
|
13 |
struct
|
|
14 |
open Conv;
|
|
15 |
open Normalizer;
|
23520
|
16 |
structure Integertab = TableFun(type key = Integer.int val ord = Integer.ord);
|
23466
|
17 |
exception COOPER of string * exn;
|
|
18 |
val simp_thms_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms);
|
|
19 |
|
23484
|
20 |
val FWD = Drule.implies_elim_list;
|
23466
|
21 |
|
|
22 |
val true_tm = @{cterm "True"};
|
|
23 |
val false_tm = @{cterm "False"};
|
|
24 |
val zdvd1_eq = @{thm "zdvd1_eq"};
|
|
25 |
val presburger_ss = @{simpset} addsimps [zdvd1_eq];
|
|
26 |
val lin_ss = presburger_ss addsimps (@{thm "dvd_eq_mod_eq_0"}::zdvd1_eq::@{thms zadd_ac});
|
|
27 |
(* Some types and constants *)
|
|
28 |
val iT = HOLogic.intT
|
|
29 |
val bT = HOLogic.boolT;
|
|
30 |
val dest_numeral = HOLogic.dest_number #> snd;
|
|
31 |
|
|
32 |
val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] =
|
|
33 |
map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"};
|
|
34 |
|
|
35 |
val [infDconj, infDdisj, infDdvd,infDndvd,infDP] =
|
|
36 |
map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"};
|
|
37 |
|
|
38 |
val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] =
|
|
39 |
map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"};
|
|
40 |
|
|
41 |
val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP];
|
|
42 |
|
|
43 |
val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP;
|
|
44 |
|
|
45 |
val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle,
|
|
46 |
asetgt, asetge, asetdvd, asetndvd,asetP],
|
|
47 |
[bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle,
|
|
48 |
bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]] = [@{thms "aset"}, @{thms "bset"}];
|
|
49 |
|
|
50 |
val [miex, cpmi, piex, cppi] = [@{thm "minusinfinity"}, @{thm "cpmi"},
|
|
51 |
@{thm "plusinfinity"}, @{thm "cppi"}];
|
|
52 |
|
|
53 |
val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"};
|
|
54 |
|
|
55 |
val [zdvd_mono,simp_from_to,all_not_ex] =
|
|
56 |
[@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}];
|
|
57 |
|
|
58 |
val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"};
|
|
59 |
|
|
60 |
val eval_ss = presburger_ss addsimps [simp_from_to] delsimps [insert_iff,bex_triv];
|
|
61 |
val eval_conv = Simplifier.rewrite eval_ss;
|
|
62 |
|
|
63 |
(* recongnising cterm without moving to terms *)
|
|
64 |
|
|
65 |
datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm
|
|
66 |
| Lt of cterm | Le of cterm | Gt of cterm | Ge of cterm
|
|
67 |
| Dvd of cterm*cterm | NDvd of cterm*cterm | Nox
|
|
68 |
|
|
69 |
fun whatis x ct =
|
|
70 |
( case (term_of ct) of
|
|
71 |
Const("op &",_)$_$_ => And (Thm.dest_binop ct)
|
|
72 |
| Const ("op |",_)$_$_ => Or (Thm.dest_binop ct)
|
|
73 |
| Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
|
|
74 |
| Const("Not",_) $ (Const ("op =",_)$y$_) =>
|
|
75 |
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
|
|
76 |
| Const ("Orderings.ord_class.less",_)$y$z =>
|
|
77 |
if term_of x aconv y then Lt (Thm.dest_arg ct)
|
|
78 |
else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
|
|
79 |
| Const ("Orderings.ord_class.less_eq",_)$y$z =>
|
|
80 |
if term_of x aconv y then Le (Thm.dest_arg ct)
|
|
81 |
else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
|
|
82 |
| Const ("Divides.dvd",_)$_$(Const(@{const_name "HOL.plus"},_)$y$_) =>
|
|
83 |
if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
|
|
84 |
| Const("Not",_) $ (Const ("Divides.dvd",_)$_$(Const(@{const_name "HOL.plus"},_)$y$_)) =>
|
|
85 |
if term_of x aconv y then
|
|
86 |
NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
|
|
87 |
| _ => Nox)
|
|
88 |
handle CTERM _ => Nox;
|
|
89 |
|
|
90 |
fun get_pmi_term t =
|
|
91 |
let val (x,eq) =
|
|
92 |
(Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg)
|
|
93 |
(Thm.dest_arg t)
|
|
94 |
in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end;
|
|
95 |
|
|
96 |
val get_pmi = get_pmi_term o cprop_of;
|
|
97 |
|
|
98 |
val p_v' = @{cpat "?P' :: int => bool"};
|
|
99 |
val q_v' = @{cpat "?Q' :: int => bool"};
|
|
100 |
val p_v = @{cpat "?P:: int => bool"};
|
|
101 |
val q_v = @{cpat "?Q:: int => bool"};
|
|
102 |
|
|
103 |
fun myfwd (th1, th2, th3) p q
|
|
104 |
[(th_1,th_2,th_3), (th_1',th_2',th_3')] =
|
|
105 |
let
|
|
106 |
val (mp', mq') = (get_pmi th_1, get_pmi th_1')
|
|
107 |
val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1)
|
|
108 |
[th_1, th_1']
|
|
109 |
val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3']
|
|
110 |
val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2']
|
|
111 |
in (mi_th, set_th, infD_th)
|
|
112 |
end;
|
|
113 |
|
|
114 |
val inst' = fn cts => instantiate' [] (map SOME cts);
|
|
115 |
val infDTrue = instantiate' [] [SOME true_tm] infDP;
|
|
116 |
val infDFalse = instantiate' [] [SOME false_tm] infDP;
|
|
117 |
|
|
118 |
val cadd = @{cterm "op + :: int => _"}
|
|
119 |
val cmulC = @{cterm "op * :: int => _"}
|
|
120 |
val cminus = @{cterm "op - :: int => _"}
|
|
121 |
val cone = @{cterm "1:: int"}
|
|
122 |
val cneg = @{cterm "uminus :: int => _"}
|
|
123 |
val [addC, mulC, subC, negC] = map term_of [cadd, cmulC, cminus, cneg]
|
|
124 |
val [zero, one] = [@{term "0::int"}, @{term "1::int"}];
|
|
125 |
|
|
126 |
val is_numeral = can dest_numeral;
|
|
127 |
|
|
128 |
fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n));
|
|
129 |
fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n));
|
|
130 |
|
|
131 |
val [minus1,plus1] =
|
|
132 |
map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];
|
|
133 |
|
|
134 |
fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle,
|
|
135 |
asetgt, asetge,asetdvd,asetndvd,asetP,
|
|
136 |
infDdvd, infDndvd, asetconj,
|
|
137 |
asetdisj, infDconj, infDdisj] cp =
|
|
138 |
case (whatis x cp) of
|
|
139 |
And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
|
|
140 |
| Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
|
|
141 |
| Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse))
|
|
142 |
| NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue))
|
|
143 |
| Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse))
|
|
144 |
| Le t => ([], K (inst' [t] pile, FWD (inst' [t] asetle) [inS (plus1 t)], infDFalse))
|
|
145 |
| Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue))
|
|
146 |
| Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue))
|
|
147 |
| Dvd (d,s) =>
|
|
148 |
([],let val dd = dvd d
|
|
149 |
in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end)
|
|
150 |
| NDvd(d,s) => ([],let val dd = dvd d
|
|
151 |
in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
|
|
152 |
| _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP));
|
|
153 |
|
|
154 |
fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt,
|
|
155 |
bsetge,bsetdvd,bsetndvd,bsetP,
|
|
156 |
infDdvd, infDndvd, bsetconj,
|
|
157 |
bsetdisj, infDconj, infDdisj] cp =
|
|
158 |
case (whatis x cp) of
|
|
159 |
And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
|
|
160 |
| Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
|
|
161 |
| Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse))
|
|
162 |
| NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue))
|
|
163 |
| Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue))
|
|
164 |
| Le t => ([], K (inst' [t] mile, (inst' [t] bsetle), infDTrue))
|
|
165 |
| Gt t => ([], K (inst' [t] migt, FWD (inst' [t] bsetgt) [inS t], infDFalse))
|
|
166 |
| Ge t => ([], K (inst' [t] mige,FWD (inst' [t] bsetge) [inS (minus1 t)], infDFalse))
|
|
167 |
| Dvd (d,s) => ([],let val dd = dvd d
|
|
168 |
in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end)
|
|
169 |
| NDvd (d,s) => ([],let val dd = dvd d
|
|
170 |
in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
|
|
171 |
| _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP))
|
|
172 |
|
|
173 |
(* Canonical linear form for terms, formulae etc.. *)
|
|
174 |
fun provelin ctxt t = Goal.prove ctxt [] [] t
|
|
175 |
(fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac 1)]);
|
|
176 |
fun linear_cmul 0 tm = zero
|
|
177 |
| linear_cmul n tm =
|
|
178 |
case tm of
|
|
179 |
Const("HOL.plus_class.plus",_)$a$b => addC$(linear_cmul n a)$(linear_cmul n b)
|
|
180 |
| Const ("HOL.times_class.times",_)$c$x => mulC$(numeral1 (Integer.mult n) c)$x
|
|
181 |
| Const("HOL.minus_class.minus",_)$a$b => subC$(linear_cmul n a)$(linear_cmul n b)
|
|
182 |
| (m as Const("HOL.minus_class.uminus",_))$a => m$(linear_cmul n a)
|
|
183 |
| _ => numeral1 (Integer.mult n) tm;
|
|
184 |
fun earlier [] x y = false
|
|
185 |
| earlier (h::t) x y =
|
|
186 |
if h aconv y then false else if h aconv x then true else earlier t x y;
|
|
187 |
|
|
188 |
fun linear_add vars tm1 tm2 =
|
|
189 |
case (tm1,tm2) of
|
|
190 |
(Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c1$x1)$r1,
|
|
191 |
Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) =>
|
|
192 |
if x1 = x2 then
|
|
193 |
let val c = numeral2 Integer.add c1 c2
|
|
194 |
in if c = zero then linear_add vars r1 r2
|
|
195 |
else addC$(mulC$c$x1)$(linear_add vars r1 r2)
|
|
196 |
end
|
|
197 |
else if earlier vars x1 x2 then addC$(mulC$ c1 $ x1)$(linear_add vars r1 tm2)
|
|
198 |
else addC$(mulC$c2$x2)$(linear_add vars tm1 r2)
|
|
199 |
| (Const("HOL.plus_class.plus",_) $ (Const("HOL.times_class.times",_)$c1$x1)$r1 ,_) =>
|
|
200 |
addC$(mulC$c1$x1)$(linear_add vars r1 tm2)
|
|
201 |
| (_, Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c2$x2)$r2) =>
|
|
202 |
addC$(mulC$c2$x2)$(linear_add vars tm1 r2)
|
|
203 |
| (_,_) => numeral2 Integer.add tm1 tm2;
|
|
204 |
|
|
205 |
fun linear_neg tm = linear_cmul ~1 tm;
|
|
206 |
fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2);
|
|
207 |
|
|
208 |
|
|
209 |
fun lint vars tm =
|
|
210 |
if is_numeral tm then tm
|
|
211 |
else case tm of
|
|
212 |
Const("HOL.minus_class.uminus",_)$t => linear_neg (lint vars t)
|
|
213 |
| Const("HOL.plus_class.plus",_) $ s $ t => linear_add vars (lint vars s) (lint vars t)
|
|
214 |
| Const("HOL.minus_class.minus",_) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
|
|
215 |
| Const ("HOL.times_class.times",_) $ s $ t =>
|
|
216 |
let val s' = lint vars s
|
|
217 |
val t' = lint vars t
|
|
218 |
in if is_numeral s' then (linear_cmul (dest_numeral s') t')
|
|
219 |
else if is_numeral t' then (linear_cmul (dest_numeral t') s')
|
|
220 |
else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm]))
|
|
221 |
end
|
|
222 |
| _ => addC$(mulC$one$tm)$zero;
|
|
223 |
|
|
224 |
fun lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less",T)$s$t)) =
|
|
225 |
lin vs (Const("Orderings.ord_class.less_eq",T)$t$s)
|
|
226 |
| lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less_eq",T)$s$t)) =
|
|
227 |
lin vs (Const("Orderings.ord_class.less",T)$t$s)
|
|
228 |
| lin vs (Const ("Not",T)$t) = Const ("Not",T)$ (lin vs t)
|
|
229 |
| lin (vs as x::_) (Const("Divides.dvd",_)$d$t) =
|
|
230 |
HOLogic.mk_binrel "Divides.dvd" (numeral1 abs d, lint vs t)
|
|
231 |
| lin (vs as x::_) ((b as Const("op =",_))$s$t) =
|
|
232 |
(case lint vs (subC$t$s) of
|
|
233 |
(t as a$(m$c$y)$r) =>
|
|
234 |
if x <> y then b$zero$t
|
|
235 |
else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
|
|
236 |
else b$(m$c$y)$(linear_neg r)
|
|
237 |
| t => b$zero$t)
|
|
238 |
| lin (vs as x::_) (b$s$t) =
|
|
239 |
(case lint vs (subC$t$s) of
|
|
240 |
(t as a$(m$c$y)$r) =>
|
|
241 |
if x <> y then b$zero$t
|
|
242 |
else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r
|
|
243 |
else b$(linear_neg r)$(m$c$y)
|
|
244 |
| t => b$zero$t)
|
|
245 |
| lin vs fm = fm;
|
|
246 |
|
|
247 |
fun lint_conv ctxt vs ct =
|
|
248 |
let val t = term_of ct
|
|
249 |
in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) |> HOLogic.mk_Trueprop))
|
|
250 |
RS eq_reflection
|
|
251 |
end;
|
|
252 |
|
|
253 |
fun is_intrel (b$_$_) = domain_type (fastype_of b) = HOLogic.intT
|
|
254 |
| is_intrel (@{term "Not"}$(b$_$_)) = domain_type (fastype_of b) = HOLogic.intT
|
|
255 |
| is_intrel _ = false;
|
|
256 |
|
|
257 |
fun linearize_conv ctxt vs ct =
|
|
258 |
case (term_of ct) of
|
|
259 |
Const("Divides.dvd",_)$d$t =>
|
|
260 |
let
|
|
261 |
val th = binop_conv (lint_conv ctxt vs) ct
|
|
262 |
val (d',t') = Thm.dest_binop (Thm.rhs_of th)
|
|
263 |
val (dt',tt') = (term_of d', term_of t')
|
|
264 |
in if is_numeral dt' andalso is_numeral tt'
|
|
265 |
then Conv.fconv_rule (arg_conv (Simplifier.rewrite presburger_ss)) th
|
|
266 |
else
|
|
267 |
let
|
|
268 |
val dth =
|
|
269 |
((if dest_numeral (term_of d') < 0 then
|
|
270 |
Conv.fconv_rule (arg_conv (arg1_conv (lint_conv ctxt vs)))
|
|
271 |
(Thm.transitive th (inst' [d',t'] dvd_uminus))
|
|
272 |
else th) handle TERM _ => th)
|
|
273 |
val d'' = Thm.rhs_of dth |> Thm.dest_arg1
|
|
274 |
in
|
|
275 |
case tt' of
|
|
276 |
Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$_)$_ =>
|
|
277 |
let val x = dest_numeral c
|
|
278 |
in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs)))
|
|
279 |
(Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
|
|
280 |
else dth end
|
|
281 |
| _ => dth
|
|
282 |
end
|
|
283 |
end
|
|
284 |
| Const("Not",_)$(Const("Divides.dvd",_)$_$_) => arg_conv (linearize_conv ctxt vs) ct
|
|
285 |
| t => if is_intrel t
|
|
286 |
then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
|
|
287 |
RS eq_reflection
|
|
288 |
else reflexive ct;
|
|
289 |
|
|
290 |
val dvdc = @{cterm "op dvd :: int => _"};
|
|
291 |
|
|
292 |
fun unify ctxt q =
|
|
293 |
let
|
|
294 |
val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE
|
|
295 |
val x = term_of cx
|
|
296 |
val ins = insert (op = : integer*integer -> bool)
|
|
297 |
fun h (acc,dacc) t =
|
|
298 |
case (term_of t) of
|
|
299 |
Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ =>
|
|
300 |
if x aconv y
|
|
301 |
andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"]
|
|
302 |
then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
|
|
303 |
| Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) =>
|
|
304 |
if x aconv y
|
|
305 |
andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"]
|
|
306 |
then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
|
|
307 |
| Const("Divides.dvd",_)$_$(Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_) =>
|
|
308 |
if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
|
|
309 |
| Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
|
|
310 |
| Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
|
|
311 |
| Const("Not",_)$_ => h (acc,dacc) (Thm.dest_arg t)
|
|
312 |
| _ => (acc, dacc)
|
|
313 |
val (cs,ds) = h ([],[]) p
|
23514
|
314 |
val l = fold Integer.lcm (cs union ds) 1
|
23466
|
315 |
fun cv k ct =
|
|
316 |
let val (tm as b$s$t) = term_of ct
|
|
317 |
in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
|
|
318 |
|> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end
|
|
319 |
fun nzprop x =
|
|
320 |
let
|
|
321 |
val th =
|
|
322 |
Simplifier.rewrite lin_ss
|
|
323 |
(Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
|
|
324 |
(Thm.capply (Thm.capply @{cterm "op = :: int => _"} (mk_cnumber @{ctyp "int"} x))
|
|
325 |
@{cterm "0::int"})))
|
|
326 |
in equal_elim (Thm.symmetric th) TrueI end;
|
|
327 |
val notz = let val tab = fold Integertab.update
|
|
328 |
(ds ~~ (map (fn x => nzprop (Integer.div l x)) ds)) Integertab.empty
|
|
329 |
in
|
|
330 |
(fn ct => (valOf (Integertab.lookup tab (ct |> term_of |> dest_numeral))
|
|
331 |
handle Option => (writeln "noz: Theorems-Table contains no entry for";
|
|
332 |
print_cterm ct ; raise Option)))
|
|
333 |
end
|
|
334 |
fun unit_conv t =
|
|
335 |
case (term_of t) of
|
|
336 |
Const("op &",_)$_$_ => binop_conv unit_conv t
|
|
337 |
| Const("op |",_)$_$_ => binop_conv unit_conv t
|
|
338 |
| Const("Not",_)$_ => arg_conv unit_conv t
|
|
339 |
| Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ =>
|
|
340 |
if x=y andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"]
|
|
341 |
then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
|
|
342 |
| Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) =>
|
|
343 |
if x=y andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"]
|
|
344 |
then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
|
|
345 |
| Const("Divides.dvd",_)$d$(r as (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_)) =>
|
|
346 |
if x=y then
|
|
347 |
let
|
|
348 |
val k = Integer.div l (dest_numeral c)
|
|
349 |
val kt = HOLogic.mk_number iT k
|
|
350 |
val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]
|
|
351 |
((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono)
|
|
352 |
val (d',t') = (mulC$kt$d, mulC$kt$r)
|
|
353 |
val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop))
|
|
354 |
RS eq_reflection
|
|
355 |
val tht = (provelin ctxt ((HOLogic.eq_const iT)$t'$(linear_cmul k r) |> HOLogic.mk_Trueprop))
|
|
356 |
RS eq_reflection
|
|
357 |
in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end
|
|
358 |
else Thm.reflexive t
|
|
359 |
| _ => Thm.reflexive t
|
|
360 |
val uth = unit_conv p
|
|
361 |
val clt = mk_cnumber @{ctyp "int"} l
|
|
362 |
val ltx = Thm.capply (Thm.capply cmulC clt) cx
|
|
363 |
val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
|
|
364 |
val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
|
|
365 |
val thf = transitive th
|
|
366 |
(transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
|
|
367 |
val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
|
|
368 |
||> beta_conversion true |>> Thm.symmetric
|
|
369 |
in transitive (transitive lth thf) rth end;
|
|
370 |
|
|
371 |
|
|
372 |
val emptyIS = @{cterm "{}::int set"};
|
|
373 |
val insert_tm = @{cterm "insert :: int => _"};
|
|
374 |
val mem_tm = Const("op :",[iT , HOLogic.mk_setT iT] ---> bT);
|
|
375 |
fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;
|
|
376 |
val cTrp = @{cterm "Trueprop"};
|
|
377 |
val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1;
|
|
378 |
val [A_tm,B_tm] = map (fn th => cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
|
|
379 |
|> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
|
|
380 |
[asetP,bsetP];
|
|
381 |
|
|
382 |
val D_tm = @{cpat "?D::int"};
|
|
383 |
|
|
384 |
val int_eq = (op =):integer*integer -> bool;
|
|
385 |
fun cooperex_conv ctxt vs q =
|
|
386 |
let
|
|
387 |
|
|
388 |
val uth = unify ctxt q
|
|
389 |
val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth))
|
|
390 |
val ins = insert (op aconvc)
|
|
391 |
fun h t (bacc,aacc,dacc) =
|
|
392 |
case (whatis x t) of
|
|
393 |
And (p,q) => h q (h p (bacc,aacc,dacc))
|
|
394 |
| Or (p,q) => h q (h p (bacc,aacc,dacc))
|
|
395 |
| Eq t => (ins (minus1 t) bacc,
|
|
396 |
ins (plus1 t) aacc,dacc)
|
|
397 |
| NEq t => (ins t bacc,
|
|
398 |
ins t aacc, dacc)
|
|
399 |
| Lt t => (bacc, ins t aacc, dacc)
|
|
400 |
| Le t => (bacc, ins (plus1 t) aacc,dacc)
|
|
401 |
| Gt t => (ins t bacc, aacc,dacc)
|
|
402 |
| Ge t => (ins (minus1 t) bacc, aacc,dacc)
|
|
403 |
| Dvd (d,s) => (bacc,aacc,insert int_eq (term_of d |> dest_numeral) dacc)
|
|
404 |
| NDvd (d,s) => (bacc,aacc,insert int_eq (term_of d|> dest_numeral) dacc)
|
|
405 |
| _ => (bacc, aacc, dacc)
|
|
406 |
val (b0,a0,ds) = h p ([],[],[])
|
23514
|
407 |
val d = fold Integer.lcm ds 1
|
23466
|
408 |
val cd = mk_cnumber @{ctyp "int"} d
|
|
409 |
val dt = term_of cd
|
|
410 |
fun divprop x =
|
|
411 |
let
|
|
412 |
val th =
|
|
413 |
Simplifier.rewrite lin_ss
|
|
414 |
(Thm.capply @{cterm Trueprop}
|
|
415 |
(Thm.capply (Thm.capply dvdc (mk_cnumber @{ctyp "int"} x)) cd))
|
|
416 |
in equal_elim (Thm.symmetric th) TrueI end;
|
|
417 |
val dvd = let val tab = fold Integertab.update
|
|
418 |
(ds ~~ (map divprop ds)) Integertab.empty in
|
|
419 |
(fn ct => (valOf (Integertab.lookup tab (term_of ct |> dest_numeral))
|
|
420 |
handle Option => (writeln "dvd: Theorems-Table contains no entry for";
|
|
421 |
print_cterm ct ; raise Option)))
|
|
422 |
end
|
|
423 |
val dp =
|
|
424 |
let val th = Simplifier.rewrite lin_ss
|
|
425 |
(Thm.capply @{cterm Trueprop}
|
|
426 |
(Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
|
|
427 |
in equal_elim (Thm.symmetric th) TrueI end;
|
|
428 |
(* A and B set *)
|
|
429 |
local
|
|
430 |
val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"}
|
|
431 |
val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"}
|
|
432 |
in
|
|
433 |
fun provein x S =
|
|
434 |
case term_of S of
|
|
435 |
Const("{}",_) => error "Unexpected error in Cooper please email Amine Chaieb"
|
|
436 |
| Const("insert",_)$y$_ =>
|
|
437 |
let val (cy,S') = Thm.dest_binop S
|
|
438 |
in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1
|
|
439 |
else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2)
|
|
440 |
(provein x S')
|
|
441 |
end
|
|
442 |
end
|
|
443 |
|
|
444 |
val al = map (lint vs o term_of) a0
|
|
445 |
val bl = map (lint vs o term_of) b0
|
|
446 |
val (sl,s0,f,abths,cpth) =
|
|
447 |
if length (distinct (op aconv) bl) <= length (distinct (op aconv) al)
|
|
448 |
then
|
|
449 |
(bl,b0,decomp_minf,
|
|
450 |
fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp)
|
|
451 |
[bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@
|
|
452 |
(map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]))
|
|
453 |
[bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj,
|
|
454 |
bsetdisj,infDconj, infDdisj]),
|
|
455 |
cpmi)
|
|
456 |
else (al,a0,decomp_pinf,fn A =>
|
|
457 |
(map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp)
|
|
458 |
[aseteq,asetneq,asetlt, asetle, asetgt,asetge])@
|
|
459 |
(map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]))
|
|
460 |
[asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj,
|
|
461 |
asetdisj,infDconj, infDdisj]),cppi)
|
|
462 |
val cpth =
|
|
463 |
let
|
|
464 |
val sths = map (fn (tl,t0) =>
|
|
465 |
if tl = term_of t0
|
|
466 |
then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl
|
|
467 |
else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0)
|
|
468 |
|> HOLogic.mk_Trueprop))
|
|
469 |
(sl ~~ s0)
|
|
470 |
val csl = distinct (op aconvc) (map (cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths)
|
|
471 |
val S = mkISet csl
|
|
472 |
val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab)
|
|
473 |
csl Termtab.empty
|
|
474 |
val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp
|
|
475 |
val inS =
|
|
476 |
let
|
|
477 |
fun transmem th0 th1 =
|
|
478 |
Thm.equal_elim
|
|
479 |
(Drule.arg_cong_rule cTrp (Drule.fun_cong_rule (Drule.arg_cong_rule
|
|
480 |
((Thm.dest_fun o Thm.dest_fun o Thm.dest_arg o cprop_of) th1) th0) S)) th1
|
|
481 |
val tab = fold Termtab.update
|
|
482 |
(map (fn eq =>
|
|
483 |
let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop
|
|
484 |
val th = if term_of s = term_of t
|
|
485 |
then valOf(Termtab.lookup inStab (term_of s))
|
|
486 |
else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
|
|
487 |
[eq, valOf(Termtab.lookup inStab (term_of s))]
|
|
488 |
in (term_of t, th) end)
|
|
489 |
sths) Termtab.empty
|
|
490 |
in fn ct =>
|
|
491 |
(valOf (Termtab.lookup tab (term_of ct))
|
|
492 |
handle Option => (writeln "inS: No theorem for " ; print_cterm ct ; raise Option))
|
|
493 |
end
|
|
494 |
val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p
|
|
495 |
in [dp, inf, nb, pd] MRS cpth
|
|
496 |
end
|
|
497 |
val cpth' = Thm.transitive uth (cpth RS eq_reflection)
|
|
498 |
in Thm.transitive cpth' ((simp_thms_conv then_conv eval_conv) (Thm.rhs_of cpth'))
|
|
499 |
end;
|
|
500 |
|
|
501 |
fun literals_conv bops uops env cv =
|
|
502 |
let fun h t =
|
|
503 |
case (term_of t) of
|
|
504 |
b$_$_ => if member (op aconv) bops b then binop_conv h t else cv env t
|
|
505 |
| u$_ => if member (op aconv) uops u then arg_conv h t else cv env t
|
|
506 |
| _ => cv env t
|
|
507 |
in h end;
|
|
508 |
|
|
509 |
fun integer_nnf_conv ctxt env =
|
|
510 |
nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt);
|
|
511 |
|
|
512 |
(* val my_term = ref (@{cterm "NOTHING"}); *)
|
|
513 |
local
|
|
514 |
val pcv = Simplifier.rewrite
|
|
515 |
(HOL_basic_ss addsimps (simp_thms @ (List.take(ex_simps,4))
|
|
516 |
@ [not_all,all_not_ex, ex_disj_distrib]))
|
|
517 |
val postcv = Simplifier.rewrite presburger_ss
|
|
518 |
fun conv ctxt p =
|
|
519 |
let val _ = () (* my_term := p *)
|
|
520 |
in
|
23523
|
521 |
Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of)
|
23466
|
522 |
(term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt)
|
|
523 |
(cooperex_conv ctxt) p
|
|
524 |
end
|
|
525 |
handle CTERM s => raise COOPER ("Cooper Failed", CTERM s)
|
|
526 |
| THM s => raise COOPER ("Cooper Failed", THM s)
|
23523
|
527 |
| TYPE s => raise COOPER ("Cooper Failed", TYPE s)
|
23466
|
528 |
in val cooper_conv = conv
|
|
529 |
end;
|
|
530 |
end;
|
|
531 |
|
|
532 |
|
|
533 |
|
|
534 |
structure Coopereif =
|
|
535 |
struct
|
|
536 |
|
|
537 |
open GeneratedCooper;
|
|
538 |
fun cooper s = raise Cooper.COOPER ("Cooper Oracle Failed", ERROR s);
|
|
539 |
fun i_of_term vs t =
|
|
540 |
case t of
|
|
541 |
Free(xn,xT) => (case AList.lookup (op aconv) vs t of
|
|
542 |
NONE => cooper "Variable not found in the list!!"
|
|
543 |
| SOME n => Bound n)
|
|
544 |
| @{term "0::int"} => C 0
|
|
545 |
| @{term "1::int"} => C 1
|
|
546 |
| Term.Bound i => Bound i
|
|
547 |
| Const(@{const_name "HOL.uminus"},_)$t' => Neg (i_of_term vs t')
|
|
548 |
| Const(@{const_name "HOL.plus"},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
|
|
549 |
| Const(@{const_name "HOL.minus"},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
|
|
550 |
| Const(@{const_name "HOL.times"},_)$t1$t2 =>
|
|
551 |
(Mul (HOLogic.dest_number t1 |> snd |> Integer.machine_int,i_of_term vs t2)
|
|
552 |
handle TERM _ =>
|
|
553 |
(Mul (HOLogic.dest_number t2 |> snd |> Integer.machine_int,i_of_term vs t1)
|
|
554 |
handle TERM _ => cooper "Reification: Unsupported kind of multiplication"))
|
|
555 |
| _ => (C (HOLogic.dest_number t |> snd |> Integer.machine_int)
|
|
556 |
handle TERM _ => cooper "Reification: unknown term");
|
|
557 |
|
|
558 |
fun qf_of_term ps vs t =
|
|
559 |
case t of
|
|
560 |
Const("True",_) => T
|
|
561 |
| Const("False",_) => F
|
|
562 |
| Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
|
|
563 |
| Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
|
|
564 |
| Const(@{const_name "Divides.dvd"},_)$t1$t2 =>
|
|
565 |
(Dvd(HOLogic.dest_number t1 |> snd |> Integer.machine_int, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
|
|
566 |
| @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
|
|
567 |
| @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
|
|
568 |
| Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
|
|
569 |
| Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)
|
|
570 |
| Const("op -->",_)$t1$t2 => Imp(qf_of_term ps vs t1,qf_of_term ps vs t2)
|
|
571 |
| Const("Not",_)$t' => NOT(qf_of_term ps vs t')
|
|
572 |
| Const("Ex",_)$Abs(xn,xT,p) =>
|
|
573 |
let val (xn',p') = variant_abs (xn,xT,p)
|
|
574 |
val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1+ n)) vs)
|
|
575 |
in E (qf_of_term ps vs' p')
|
|
576 |
end
|
|
577 |
| Const("All",_)$Abs(xn,xT,p) =>
|
|
578 |
let val (xn',p') = variant_abs (xn,xT,p)
|
|
579 |
val vs' = (Free (xn',xT), nat 0) :: (map (fn(v,n) => (v,1+ n)) vs)
|
|
580 |
in A (qf_of_term ps vs' p')
|
|
581 |
end
|
|
582 |
| _ =>(case AList.lookup (op aconv) ps t of
|
|
583 |
NONE => cooper "Reification: unknown term!"
|
|
584 |
| SOME n => Closed n);
|
|
585 |
|
|
586 |
local
|
|
587 |
val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"},
|
|
588 |
@{term "op = :: int => _"}, @{term "op < :: int => _"},
|
|
589 |
@{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"},
|
|
590 |
@{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}]
|
|
591 |
fun ty t = Bool.not (fastype_of t = HOLogic.boolT)
|
|
592 |
in
|
|
593 |
fun term_bools acc t =
|
|
594 |
case t of
|
|
595 |
(l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b
|
|
596 |
else insert (op aconv) t acc
|
|
597 |
| f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a
|
|
598 |
else insert (op aconv) t acc
|
|
599 |
| Abs p => term_bools acc (snd (variant_abs p))
|
|
600 |
| _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc
|
|
601 |
end;
|
|
602 |
|
|
603 |
|
|
604 |
fun start_vs t =
|
|
605 |
let
|
|
606 |
val fs = term_frees t
|
|
607 |
val ps = term_bools [] t
|
|
608 |
in (fs ~~ (0 upto (length fs - 1)), ps ~~ (0 upto (length ps - 1)))
|
|
609 |
end ;
|
|
610 |
|
|
611 |
val iT = HOLogic.intT;
|
|
612 |
val bT = HOLogic.boolT;
|
|
613 |
fun myassoc2 l v =
|
|
614 |
case l of
|
|
615 |
[] => NONE
|
|
616 |
| (x,v')::xs => if v = v' then SOME x
|
|
617 |
else myassoc2 xs v;
|
|
618 |
|
|
619 |
fun term_of_i vs t =
|
|
620 |
case t of
|
|
621 |
C i => HOLogic.mk_number HOLogic.intT (Integer.int i)
|
|
622 |
| Bound n => valOf (myassoc2 vs n)
|
|
623 |
| Neg t' => @{term "uminus :: int => _"}$(term_of_i vs t')
|
|
624 |
| Add(t1,t2) => @{term "op +:: int => _"}$ (term_of_i vs t1)$(term_of_i vs t2)
|
|
625 |
| Sub(t1,t2) => Const(@{const_name "HOL.minus"},[iT,iT] ---> iT)$
|
|
626 |
(term_of_i vs t1)$(term_of_i vs t2)
|
|
627 |
| Mul(i,t2) => Const(@{const_name "HOL.times"},[iT,iT] ---> iT)$
|
|
628 |
(HOLogic.mk_number HOLogic.intT (Integer.int i))$(term_of_i vs t2)
|
|
629 |
| CX(i,t')=> term_of_i vs (Add(Mul (i,Bound (nat 0)),t'));
|
|
630 |
|
|
631 |
fun term_of_qf ps vs t =
|
|
632 |
case t of
|
|
633 |
T => HOLogic.true_const
|
|
634 |
| F => HOLogic.false_const
|
|
635 |
| Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
|
|
636 |
| Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"}
|
|
637 |
| Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
|
|
638 |
| Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t'
|
|
639 |
| Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"}
|
|
640 |
| NEq t' => term_of_qf ps vs (NOT(Eq t'))
|
|
641 |
| Dvd(i,t') => @{term "op dvd :: int => _ "}$
|
|
642 |
(HOLogic.mk_number HOLogic.intT (Integer.int i))$(term_of_i vs t')
|
|
643 |
| NDvd(i,t')=> term_of_qf ps vs (NOT(Dvd(i,t')))
|
|
644 |
| NOT t' => HOLogic.Not$(term_of_qf ps vs t')
|
|
645 |
| And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
|
|
646 |
| Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
|
|
647 |
| Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2)
|
|
648 |
| Iff(t1,t2) => (HOLogic.eq_const bT)$(term_of_qf ps vs t1)$ (term_of_qf ps vs t2)
|
|
649 |
| Closed n => valOf (myassoc2 ps n)
|
|
650 |
| NClosed n => term_of_qf ps vs (NOT (Closed n))
|
|
651 |
| _ => cooper "If this is raised, Isabelle/HOL or generate_code is inconsistent!";
|
|
652 |
|
|
653 |
(* The oracle *)
|
|
654 |
fun cooper_oracle thy t =
|
|
655 |
let val (vs,ps) = start_vs t
|
|
656 |
in (equals propT) $ (HOLogic.mk_Trueprop t) $
|
|
657 |
(HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))
|
|
658 |
end;
|
|
659 |
|
|
660 |
end;
|