author | haftmann |
Mon, 10 May 2010 15:21:13 +0200 | |
changeset 36805 | 929b23461a14 |
parent 36804 | f4ad04780669 |
child 36806 | fc27b0465a4c |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: HOL/Tools/Qelim/cooper.ML |
23466 | 2 |
Author: Amine Chaieb, TU Muenchen |
36802 | 3 |
|
4 |
Presburger arithmetic by Cooper's algorithm. |
|
23466 | 5 |
*) |
6 |
||
36799 | 7 |
signature COOPER = |
36798 | 8 |
sig |
9 |
type entry |
|
10 |
val get: Proof.context -> entry |
|
11 |
val del: term list -> attribute |
|
12 |
val add: term list -> attribute |
|
36804 | 13 |
val conv: Proof.context -> conv |
14 |
val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic |
|
15 |
val method: (Proof.context -> Method.method) context_parser |
|
36802 | 16 |
exception COOPER of string * exn |
36798 | 17 |
val setup: theory -> theory |
23466 | 18 |
end; |
19 |
||
36799 | 20 |
structure Cooper: COOPER = |
36798 | 21 |
struct |
22 |
||
36799 | 23 |
type entry = simpset * term list; |
36798 | 24 |
|
25 |
val allowed_consts = |
|
26 |
[@{term "op + :: int => _"}, @{term "op + :: nat => _"}, |
|
27 |
@{term "op - :: int => _"}, @{term "op - :: nat => _"}, |
|
28 |
@{term "op * :: int => _"}, @{term "op * :: nat => _"}, |
|
29 |
@{term "op div :: int => _"}, @{term "op div :: nat => _"}, |
|
30 |
@{term "op mod :: int => _"}, @{term "op mod :: nat => _"}, |
|
31 |
@{term "op &"}, @{term "op |"}, @{term "op -->"}, |
|
32 |
@{term "op = :: int => _"}, @{term "op = :: nat => _"}, @{term "op = :: bool => _"}, |
|
33 |
@{term "op < :: int => _"}, @{term "op < :: nat => _"}, |
|
34 |
@{term "op <= :: int => _"}, @{term "op <= :: nat => _"}, |
|
35 |
@{term "op dvd :: int => _"}, @{term "op dvd :: nat => _"}, |
|
36 |
@{term "abs :: int => _"}, |
|
37 |
@{term "max :: int => _"}, @{term "max :: nat => _"}, |
|
38 |
@{term "min :: int => _"}, @{term "min :: nat => _"}, |
|
39 |
@{term "uminus :: int => _"}, (*@ {term "uminus :: nat => _"},*) |
|
40 |
@{term "Not"}, @{term "Suc"}, |
|
41 |
@{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"}, |
|
42 |
@{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"}, |
|
43 |
@{term "nat"}, @{term "int"}, |
|
44 |
@{term "Int.Bit0"}, @{term "Int.Bit1"}, |
|
45 |
@{term "Int.Pls"}, @{term "Int.Min"}, |
|
46 |
@{term "Int.number_of :: int => int"}, @{term "Int.number_of :: int => nat"}, |
|
47 |
@{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"}, |
|
48 |
@{term "True"}, @{term "False"}]; |
|
49 |
||
50 |
structure Data = Generic_Data |
|
51 |
( |
|
52 |
type T = simpset * term list; |
|
53 |
val empty = (HOL_ss, allowed_consts); |
|
54 |
val extend = I; |
|
55 |
fun merge ((ss1, ts1), (ss2, ts2)) = |
|
56 |
(merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2)); |
|
57 |
); |
|
58 |
||
59 |
val get = Data.get o Context.Proof; |
|
60 |
||
61 |
fun add ts = Thm.declaration_attribute (fn th => fn context => |
|
62 |
context |> Data.map (fn (ss,ts') => |
|
63 |
(ss addsimps [th], merge (op aconv) (ts',ts) ))) |
|
64 |
||
65 |
fun del ts = Thm.declaration_attribute (fn th => fn context => |
|
66 |
context |> Data.map (fn (ss,ts') => |
|
67 |
(ss delsimps [th], subtract (op aconv) ts' ts ))) |
|
68 |
||
27018 | 69 |
fun simp_thms_conv ctxt = |
35410 | 70 |
Simplifier.rewrite (Simplifier.context ctxt HOL_basic_ss addsimps @{thms simp_thms}); |
23484 | 71 |
val FWD = Drule.implies_elim_list; |
23466 | 72 |
|
73 |
val true_tm = @{cterm "True"}; |
|
74 |
val false_tm = @{cterm "False"}; |
|
75 |
val zdvd1_eq = @{thm "zdvd1_eq"}; |
|
76 |
val presburger_ss = @{simpset} addsimps [zdvd1_eq]; |
|
30595
c87a3350f5a9
proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
wenzelm
parents:
30448
diff
changeset
|
77 |
val lin_ss = presburger_ss addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms zadd_ac}); |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset
|
78 |
|
23466 | 79 |
val iT = HOLogic.intT |
80 |
val bT = HOLogic.boolT; |
|
81 |
val dest_numeral = HOLogic.dest_number #> snd; |
|
82 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
83 |
val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] = |
23466 | 84 |
map(instantiate' [SOME @{ctyp "int"}] []) @{thms "minf"}; |
85 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
86 |
val [infDconj, infDdisj, infDdvd,infDndvd,infDP] = |
23466 | 87 |
map(instantiate' [SOME @{ctyp "int"}] []) @{thms "inf_period"}; |
88 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
89 |
val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] = |
23466 | 90 |
map (instantiate' [SOME @{ctyp "int"}] []) @{thms "pinf"}; |
91 |
||
92 |
val [miP, piP] = map (instantiate' [SOME @{ctyp "bool"}] []) [miP, piP]; |
|
93 |
||
94 |
val infDP = instantiate' (map SOME [@{ctyp "int"}, @{ctyp "bool"}]) [] infDP; |
|
95 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
96 |
val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle, |
23466 | 97 |
asetgt, asetge, asetdvd, asetndvd,asetP], |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
98 |
[bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle, |
23466 | 99 |
bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]] = [@{thms "aset"}, @{thms "bset"}]; |
100 |
||
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
101 |
val [cpmi, cppi] = [@{thm "cpmi"}, @{thm "cppi"}]; |
23466 | 102 |
|
103 |
val unity_coeff_ex = instantiate' [SOME @{ctyp "int"}] [] @{thm "unity_coeff_ex"}; |
|
104 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
105 |
val [zdvd_mono,simp_from_to,all_not_ex] = |
23466 | 106 |
[@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}]; |
107 |
||
108 |
val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"}; |
|
109 |
||
110 |
val eval_ss = presburger_ss addsimps [simp_from_to] delsimps [insert_iff,bex_triv]; |
|
111 |
val eval_conv = Simplifier.rewrite eval_ss; |
|
112 |
||
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset
|
113 |
(* recognising cterm without moving to terms *) |
23466 | 114 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
115 |
datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm |
23466 | 116 |
| Lt of cterm | Le of cterm | Gt of cterm | Ge of cterm |
117 |
| Dvd of cterm*cterm | NDvd of cterm*cterm | Nox |
|
118 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
119 |
fun whatis x ct = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
120 |
( case (term_of ct) of |
23466 | 121 |
Const("op &",_)$_$_ => And (Thm.dest_binop ct) |
122 |
| Const ("op |",_)$_$_ => Or (Thm.dest_binop ct) |
|
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
123 |
| Const ("op =",_)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
124 |
| Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) => |
23466 | 125 |
if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset
|
126 |
| Const (@{const_name Orderings.less}, _) $ y$ z => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
127 |
if term_of x aconv y then Lt (Thm.dest_arg ct) |
23466 | 128 |
else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset
|
129 |
| Const (@{const_name Orderings.less_eq}, _) $ y $ z => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
130 |
if term_of x aconv y then Le (Thm.dest_arg ct) |
23466 | 131 |
else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
132 |
| Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_) => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
133 |
if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
134 |
| Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_)) => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
135 |
if term_of x aconv y then |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
136 |
NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox |
23466 | 137 |
| _ => Nox) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
138 |
handle CTERM _ => Nox; |
23466 | 139 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
140 |
fun get_pmi_term t = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
141 |
let val (x,eq) = |
23466 | 142 |
(Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg) |
143 |
(Thm.dest_arg t) |
|
144 |
in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end; |
|
145 |
||
146 |
val get_pmi = get_pmi_term o cprop_of; |
|
147 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
148 |
val p_v' = @{cpat "?P' :: int => bool"}; |
23466 | 149 |
val q_v' = @{cpat "?Q' :: int => bool"}; |
150 |
val p_v = @{cpat "?P:: int => bool"}; |
|
151 |
val q_v = @{cpat "?Q:: int => bool"}; |
|
152 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
153 |
fun myfwd (th1, th2, th3) p q |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
154 |
[(th_1,th_2,th_3), (th_1',th_2',th_3')] = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
155 |
let |
23466 | 156 |
val (mp', mq') = (get_pmi th_1, get_pmi th_1') |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
157 |
val mi_th = FWD (instantiate ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1) |
23466 | 158 |
[th_1, th_1'] |
159 |
val infD_th = FWD (instantiate ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3'] |
|
160 |
val set_th = FWD (instantiate ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2'] |
|
161 |
in (mi_th, set_th, infD_th) |
|
162 |
end; |
|
163 |
||
164 |
val inst' = fn cts => instantiate' [] (map SOME cts); |
|
165 |
val infDTrue = instantiate' [] [SOME true_tm] infDP; |
|
166 |
val infDFalse = instantiate' [] [SOME false_tm] infDP; |
|
167 |
||
168 |
val cadd = @{cterm "op + :: int => _"} |
|
169 |
val cmulC = @{cterm "op * :: int => _"} |
|
170 |
val cminus = @{cterm "op - :: int => _"} |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset
|
171 |
val cone = @{cterm "1 :: int"} |
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
172 |
val [addC, mulC, subC] = map term_of [cadd, cmulC, cminus] |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset
|
173 |
val [zero, one] = [@{term "0 :: int"}, @{term "1 :: int"}]; |
23466 | 174 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
175 |
val is_numeral = can dest_numeral; |
23466 | 176 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
177 |
fun numeral1 f n = HOLogic.mk_number iT (f (dest_numeral n)); |
23466 | 178 |
fun numeral2 f m n = HOLogic.mk_number iT (f (dest_numeral m) (dest_numeral n)); |
179 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
180 |
val [minus1,plus1] = |
23466 | 181 |
map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd]; |
182 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
183 |
fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle, |
23466 | 184 |
asetgt, asetge,asetdvd,asetndvd,asetP, |
185 |
infDdvd, infDndvd, asetconj, |
|
186 |
asetdisj, infDconj, infDdisj] cp = |
|
187 |
case (whatis x cp) of |
|
188 |
And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q)) |
|
189 |
| Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q)) |
|
190 |
| Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse)) |
|
191 |
| NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue)) |
|
192 |
| Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse)) |
|
193 |
| Le t => ([], K (inst' [t] pile, FWD (inst' [t] asetle) [inS (plus1 t)], infDFalse)) |
|
194 |
| Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue)) |
|
195 |
| Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue)) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
196 |
| Dvd (d,s) => |
23466 | 197 |
([],let val dd = dvd d |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
198 |
in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end) |
23466 | 199 |
| NDvd(d,s) => ([],let val dd = dvd d |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
200 |
in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end) |
23466 | 201 |
| _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP)); |
202 |
||
203 |
fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt, |
|
204 |
bsetge,bsetdvd,bsetndvd,bsetP, |
|
205 |
infDdvd, infDndvd, bsetconj, |
|
206 |
bsetdisj, infDconj, infDdisj] cp = |
|
207 |
case (whatis x cp) of |
|
208 |
And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q)) |
|
209 |
| Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q)) |
|
210 |
| Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse)) |
|
211 |
| NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue)) |
|
212 |
| Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue)) |
|
213 |
| Le t => ([], K (inst' [t] mile, (inst' [t] bsetle), infDTrue)) |
|
214 |
| Gt t => ([], K (inst' [t] migt, FWD (inst' [t] bsetgt) [inS t], infDFalse)) |
|
215 |
| Ge t => ([], K (inst' [t] mige,FWD (inst' [t] bsetge) [inS (minus1 t)], infDFalse)) |
|
216 |
| Dvd (d,s) => ([],let val dd = dvd d |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
217 |
in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end) |
23466 | 218 |
| NDvd (d,s) => ([],let val dd = dvd d |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
219 |
in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end) |
23466 | 220 |
| _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP)) |
221 |
||
222 |
(* Canonical linear form for terms, formulae etc.. *) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
223 |
fun provelin ctxt t = Goal.prove ctxt [] [] t |
31101
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
30686
diff
changeset
|
224 |
(fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]); |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
225 |
fun linear_cmul 0 tm = zero |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
226 |
| linear_cmul n tm = case tm of |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
227 |
Const (@{const_name Groups.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
228 |
| Const (@{const_name Groups.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
229 |
| Const (@{const_name Groups.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
230 |
| (m as Const (@{const_name Groups.uminus}, _)) $ a => m $ linear_cmul n a |
25768 | 231 |
| _ => numeral1 (fn m => n * m) tm; |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
232 |
fun earlier [] x y = false |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
233 |
| earlier (h::t) x y = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
234 |
if h aconv y then false else if h aconv x then true else earlier t x y; |
23466 | 235 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
236 |
fun linear_add vars tm1 tm2 = case (tm1, tm2) of |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
237 |
(Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
238 |
Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
239 |
if x1 = x2 then |
33002 | 240 |
let val c = numeral2 Integer.add c1 c2 |
25768 | 241 |
in if c = zero then linear_add vars r1 r2 |
242 |
else addC$(mulC$c$x1)$(linear_add vars r1 r2) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
243 |
end |
25768 | 244 |
else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 |
245 |
else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
246 |
| (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, _) => |
25768 | 247 |
addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
248 |
| (_, Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) => |
25768 | 249 |
addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 |
33002 | 250 |
| (_, _) => numeral2 Integer.add tm1 tm2; |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
251 |
|
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
252 |
fun linear_neg tm = linear_cmul ~1 tm; |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
253 |
fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); |
23466 | 254 |
|
36802 | 255 |
exception COOPER of string * exn; |
256 |
||
257 |
fun cooper s = raise COOPER ("Cooper failed", ERROR s); |
|
23466 | 258 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
259 |
fun lint vars tm = if is_numeral tm then tm else case tm of |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
260 |
Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t) |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
261 |
| Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t) |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
262 |
| Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t) |
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
263 |
| Const (@{const_name Groups.times}, _) $ s $ t => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
264 |
let val s' = lint vars s |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
265 |
val t' = lint vars t |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
266 |
in if is_numeral s' then (linear_cmul (dest_numeral s') t') |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
267 |
else if is_numeral t' then (linear_cmul (dest_numeral t') s') |
23466 | 268 |
else raise COOPER ("Cooper Failed", TERM ("lint: not linear",[tm])) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
269 |
end |
25768 | 270 |
| _ => addC $ (mulC $ one $ tm) $ zero; |
23466 | 271 |
|
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset
|
272 |
fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Orderings.less}, T) $ s $ t)) = |
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset
|
273 |
lin vs (Const (@{const_name Orderings.less_eq}, T) $ t $ s) |
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset
|
274 |
| lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Orderings.less_eq}, T) $ s $ t)) = |
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset
|
275 |
lin vs (Const (@{const_name Orderings.less}, T) $ t $ s) |
25768 | 276 |
| lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t) |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset
|
277 |
| lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) = |
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset
|
278 |
HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
279 |
| lin (vs as x::_) ((b as Const("op =",_))$s$t) = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
280 |
(case lint vs (subC$t$s) of |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
281 |
(t as a$(m$c$y)$r) => |
23466 | 282 |
if x <> y then b$zero$t |
283 |
else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r |
|
284 |
else b$(m$c$y)$(linear_neg r) |
|
285 |
| t => b$zero$t) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
286 |
| lin (vs as x::_) (b$s$t) = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
287 |
(case lint vs (subC$t$s) of |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
288 |
(t as a$(m$c$y)$r) => |
23466 | 289 |
if x <> y then b$zero$t |
290 |
else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r |
|
291 |
else b$(linear_neg r)$(m$c$y) |
|
292 |
| t => b$zero$t) |
|
293 |
| lin vs fm = fm; |
|
294 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
295 |
fun lint_conv ctxt vs ct = |
23466 | 296 |
let val t = term_of ct |
297 |
in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) |> HOLogic.mk_Trueprop)) |
|
298 |
RS eq_reflection |
|
299 |
end; |
|
300 |
||
32398 | 301 |
fun is_intrel_type T = T = @{typ "int => int => bool"}; |
302 |
||
303 |
fun is_intrel (b$_$_) = is_intrel_type (fastype_of b) |
|
304 |
| is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b) |
|
23466 | 305 |
| is_intrel _ = false; |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
306 |
|
25768 | 307 |
fun linearize_conv ctxt vs ct = case term_of ct of |
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset
|
308 |
Const(@{const_name Rings.dvd},_)$d$t => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
309 |
let |
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
310 |
val th = Conv.binop_conv (lint_conv ctxt vs) ct |
23466 | 311 |
val (d',t') = Thm.dest_binop (Thm.rhs_of th) |
312 |
val (dt',tt') = (term_of d', term_of t') |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
313 |
in if is_numeral dt' andalso is_numeral tt' |
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
314 |
then Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite presburger_ss)) th |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
315 |
else |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
316 |
let |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
317 |
val dth = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
318 |
((if dest_numeral (term_of d') < 0 then |
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
319 |
Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs))) |
23466 | 320 |
(Thm.transitive th (inst' [d',t'] dvd_uminus)) |
321 |
else th) handle TERM _ => th) |
|
322 |
val d'' = Thm.rhs_of dth |> Thm.dest_arg1 |
|
323 |
in |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
324 |
case tt' of |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
325 |
Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ => |
23466 | 326 |
let val x = dest_numeral c |
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
327 |
in if x < 0 then Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (lint_conv ctxt vs))) |
23466 | 328 |
(Thm.transitive dth (inst' [d'',t'] dvd_uminus')) |
329 |
else dth end |
|
330 |
| _ => dth |
|
331 |
end |
|
332 |
end |
|
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
333 |
| Const (@{const_name Not},_)$(Const(@{const_name Rings.dvd},_)$_$_) => Conv.arg_conv (linearize_conv ctxt vs) ct |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
334 |
| t => if is_intrel t |
23466 | 335 |
then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop)) |
336 |
RS eq_reflection |
|
337 |
else reflexive ct; |
|
338 |
||
339 |
val dvdc = @{cterm "op dvd :: int => _"}; |
|
340 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
341 |
fun unify ctxt q = |
23466 | 342 |
let |
343 |
val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
344 |
val x = term_of cx |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
345 |
val ins = insert (op = : int * int -> bool) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
346 |
fun h (acc,dacc) t = |
23466 | 347 |
case (term_of t) of |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
348 |
Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ => |
23881 | 349 |
if x aconv y andalso member (op =) |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset
|
350 |
["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s |
23466 | 351 |
then (ins (dest_numeral c) acc,dacc) else (acc,dacc) |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
352 |
| Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) => |
23881 | 353 |
if x aconv y andalso member (op =) |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset
|
354 |
[@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s |
23466 | 355 |
then (ins (dest_numeral c) acc, dacc) else (acc,dacc) |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
356 |
| Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) => |
23466 | 357 |
if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc) |
358 |
| Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
|
359 |
| Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
|
25768 | 360 |
| Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t) |
23466 | 361 |
| _ => (acc, dacc) |
362 |
val (cs,ds) = h ([],[]) p |
|
33042 | 363 |
val l = Integer.lcms (union (op =) cs ds) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
364 |
fun cv k ct = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
365 |
let val (tm as b$s$t) = term_of ct |
23466 | 366 |
in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t)) |
367 |
|> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
368 |
fun nzprop x = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
369 |
let |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
370 |
val th = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
371 |
Simplifier.rewrite lin_ss |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
372 |
(Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
373 |
(Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x)) |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset
|
374 |
@{cterm "0::int"}))) |
23466 | 375 |
in equal_elim (Thm.symmetric th) TrueI end; |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
376 |
val notz = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
377 |
let val tab = fold Inttab.update |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
378 |
(ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
379 |
in |
33035 | 380 |
fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_numeral)) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
381 |
handle Option => |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
382 |
(writeln ("noz: Theorems-Table contains no entry for " ^ |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
383 |
Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option) |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
384 |
end |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
385 |
fun unit_conv t = |
23466 | 386 |
case (term_of t) of |
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
387 |
Const("op &",_)$_$_ => Conv.binop_conv unit_conv t |
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
388 |
| Const("op |",_)$_$_ => Conv.binop_conv unit_conv t |
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
389 |
| Const (@{const_name Not},_)$_ => Conv.arg_conv unit_conv t |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
390 |
| Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ => |
23881 | 391 |
if x=y andalso member (op =) |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset
|
392 |
["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
393 |
then cv (l div dest_numeral c) t else Thm.reflexive t |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
394 |
| Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) => |
23881 | 395 |
if x=y andalso member (op =) |
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset
|
396 |
[@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
397 |
then cv (l div dest_numeral c) t else Thm.reflexive t |
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
398 |
| Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_)) => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
399 |
if x=y then |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
400 |
let |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
401 |
val k = l div dest_numeral c |
23466 | 402 |
val kt = HOLogic.mk_number iT k |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
403 |
val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] |
23466 | 404 |
((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono) |
405 |
val (d',t') = (mulC$kt$d, mulC$kt$r) |
|
406 |
val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop)) |
|
407 |
RS eq_reflection |
|
408 |
val tht = (provelin ctxt ((HOLogic.eq_const iT)$t'$(linear_cmul k r) |> HOLogic.mk_Trueprop)) |
|
409 |
RS eq_reflection |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
410 |
in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end |
23466 | 411 |
else Thm.reflexive t |
412 |
| _ => Thm.reflexive t |
|
413 |
val uth = unit_conv p |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset
|
414 |
val clt = Numeral.mk_cnumber @{ctyp "int"} l |
23466 | 415 |
val ltx = Thm.capply (Thm.capply cmulC clt) cx |
416 |
val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth) |
|
417 |
val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
418 |
val thf = transitive th |
23466 | 419 |
(transitive (symmetric (beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th') |
420 |
val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true |
|
421 |
||> beta_conversion true |>> Thm.symmetric |
|
422 |
in transitive (transitive lth thf) rth end; |
|
423 |
||
424 |
||
425 |
val emptyIS = @{cterm "{}::int set"}; |
|
426 |
val insert_tm = @{cterm "insert :: int => _"}; |
|
427 |
fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS; |
|
428 |
val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1; |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
429 |
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 |
23466 | 430 |
|> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg) |
431 |
[asetP,bsetP]; |
|
432 |
||
433 |
val D_tm = @{cpat "?D::int"}; |
|
434 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
435 |
fun cooperex_conv ctxt vs q = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
436 |
let |
23466 | 437 |
|
438 |
val uth = unify ctxt q |
|
439 |
val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth)) |
|
440 |
val ins = insert (op aconvc) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
441 |
fun h t (bacc,aacc,dacc) = |
23466 | 442 |
case (whatis x t) of |
443 |
And (p,q) => h q (h p (bacc,aacc,dacc)) |
|
444 |
| Or (p,q) => h q (h p (bacc,aacc,dacc)) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
445 |
| Eq t => (ins (minus1 t) bacc, |
23466 | 446 |
ins (plus1 t) aacc,dacc) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
447 |
| NEq t => (ins t bacc, |
23466 | 448 |
ins t aacc, dacc) |
449 |
| Lt t => (bacc, ins t aacc, dacc) |
|
450 |
| Le t => (bacc, ins (plus1 t) aacc,dacc) |
|
451 |
| Gt t => (ins t bacc, aacc,dacc) |
|
452 |
| Ge t => (ins (minus1 t) bacc, aacc,dacc) |
|
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
453 |
| Dvd (d,_) => (bacc,aacc,insert (op =) (term_of d |> dest_numeral) dacc) |
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
454 |
| NDvd (d,_) => (bacc,aacc,insert (op =) (term_of d|> dest_numeral) dacc) |
23466 | 455 |
| _ => (bacc, aacc, dacc) |
456 |
val (b0,a0,ds) = h p ([],[],[]) |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
457 |
val d = Integer.lcms ds |
23582 | 458 |
val cd = Numeral.mk_cnumber @{ctyp "int"} d |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
459 |
fun divprop x = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
460 |
let |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
461 |
val th = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
462 |
Simplifier.rewrite lin_ss |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
463 |
(Thm.capply @{cterm Trueprop} |
23582 | 464 |
(Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd)) |
23466 | 465 |
in equal_elim (Thm.symmetric th) TrueI end; |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
466 |
val dvd = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
467 |
let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in |
33035 | 468 |
fn ct => the (Inttab.lookup tab (term_of ct |> dest_numeral)) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
469 |
handle Option => |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
470 |
(writeln ("dvd: Theorems-Table contains no entry for" ^ |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
471 |
Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option) |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
472 |
end |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
473 |
val dp = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
474 |
let val th = Simplifier.rewrite lin_ss |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
475 |
(Thm.capply @{cterm Trueprop} |
23466 | 476 |
(Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd)) |
477 |
in equal_elim (Thm.symmetric th) TrueI end; |
|
478 |
(* A and B set *) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
479 |
local |
23466 | 480 |
val insI1 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI1"} |
481 |
val insI2 = instantiate' [SOME @{ctyp "int"}] [] @{thm "insertI2"} |
|
482 |
in |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
483 |
fun provein x S = |
23466 | 484 |
case term_of S of |
32264
0be31453f698
Set.UNIV and Set.empty are mere abbreviations for top and bot
haftmann
parents:
31101
diff
changeset
|
485 |
Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb" |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
486 |
| Const(@{const_name insert}, _) $ y $ _ => |
23466 | 487 |
let val (cy,S') = Thm.dest_binop S |
488 |
in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
489 |
else implies_elim (instantiate' [] [SOME x, SOME S', SOME cy] insI2) |
23466 | 490 |
(provein x S') |
491 |
end |
|
492 |
end |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
493 |
|
23466 | 494 |
val al = map (lint vs o term_of) a0 |
495 |
val bl = map (lint vs o term_of) b0 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
496 |
val (sl,s0,f,abths,cpth) = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
497 |
if length (distinct (op aconv) bl) <= length (distinct (op aconv) al) |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
498 |
then |
23466 | 499 |
(bl,b0,decomp_minf, |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
500 |
fn B => (map (fn th => implies_elim (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)]) th) dp) |
23466 | 501 |
[bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@ |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
502 |
(map (Thm.instantiate ([],[(B_tm,B), (D_tm,cd)])) |
23466 | 503 |
[bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj, |
504 |
bsetdisj,infDconj, infDdisj]), |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
505 |
cpmi) |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
506 |
else (al,a0,decomp_pinf,fn A => |
23466 | 507 |
(map (fn th => implies_elim (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)]) th) dp) |
508 |
[aseteq,asetneq,asetlt, asetle, asetgt,asetge])@ |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
509 |
(map (Thm.instantiate ([],[(A_tm,A), (D_tm,cd)])) |
23466 | 510 |
[asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj, |
511 |
asetdisj,infDconj, infDdisj]),cppi) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
512 |
val cpth = |
23466 | 513 |
let |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
514 |
val sths = map (fn (tl,t0) => |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
515 |
if tl = term_of t0 |
23466 | 516 |
then instantiate' [SOME @{ctyp "int"}] [SOME t0] refl |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
517 |
else provelin ctxt ((HOLogic.eq_const iT)$tl$(term_of t0) |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
518 |
|> HOLogic.mk_Trueprop)) |
23466 | 519 |
(sl ~~ s0) |
520 |
val csl = distinct (op aconvc) (map (cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths) |
|
521 |
val S = mkISet csl |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
522 |
val inStab = fold (fn ct => fn tab => Termtab.update (term_of ct, provein ct S) tab) |
23466 | 523 |
csl Termtab.empty |
524 |
val eqelem_th = instantiate' [SOME @{ctyp "int"}] [NONE,NONE, SOME S] eqelem_imp_imp |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
525 |
val inS = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
526 |
let |
23466 | 527 |
val tab = fold Termtab.update |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
528 |
(map (fn eq => |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
529 |
let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
530 |
val th = if term_of s = term_of t |
33035 | 531 |
then the (Termtab.lookup inStab (term_of s)) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
532 |
else FWD (instantiate' [] [SOME s, SOME t] eqelem_th) |
33035 | 533 |
[eq, the (Termtab.lookup inStab (term_of s))] |
23466 | 534 |
in (term_of t, th) end) |
535 |
sths) Termtab.empty |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
536 |
in |
33035 | 537 |
fn ct => the (Termtab.lookup tab (term_of ct)) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
538 |
handle Option => |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
539 |
(writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct)); |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
540 |
raise Option) |
23466 | 541 |
end |
542 |
val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p |
|
543 |
in [dp, inf, nb, pd] MRS cpth |
|
544 |
end |
|
545 |
val cpth' = Thm.transitive uth (cpth RS eq_reflection) |
|
27018 | 546 |
in Thm.transitive cpth' ((simp_thms_conv ctxt then_conv eval_conv) (Thm.rhs_of cpth')) |
23466 | 547 |
end; |
548 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
549 |
fun literals_conv bops uops env cv = |
23466 | 550 |
let fun h t = |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
551 |
case (term_of t) of |
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
552 |
b$_$_ => if member (op aconv) bops b then Conv.binop_conv h t else cv env t |
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
553 |
| u$_ => if member (op aconv) uops u then Conv.arg_conv h t else cv env t |
23466 | 554 |
| _ => cv env t |
555 |
in h end; |
|
556 |
||
557 |
fun integer_nnf_conv ctxt env = |
|
558 |
nnf_conv then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt); |
|
559 |
||
560 |
local |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
561 |
val pcv = Simplifier.rewrite |
35410 | 562 |
(HOL_basic_ss addsimps (@{thms simp_thms} @ List.take(@{thms ex_simps}, 4) |
563 |
@ [not_all, all_not_ex, @{thm ex_disj_distrib}])) |
|
23466 | 564 |
val postcv = Simplifier.rewrite presburger_ss |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
565 |
fun conv ctxt p = |
24298 | 566 |
let val _ = () |
23466 | 567 |
in |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
568 |
Qelim.gen_qelim_conv pcv postcv pcv (cons o term_of) |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
569 |
(OldTerm.term_frees (term_of p)) (linearize_conv ctxt) (integer_nnf_conv ctxt) |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
570 |
(cooperex_conv ctxt) p |
23466 | 571 |
end |
572 |
handle CTERM s => raise COOPER ("Cooper Failed", CTERM s) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
573 |
| THM s => raise COOPER ("Cooper Failed", THM s) |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
574 |
| TYPE s => raise COOPER ("Cooper Failed", TYPE s) |
36804 | 575 |
in val conv = conv |
23466 | 576 |
end; |
577 |
||
23713 | 578 |
fun i_of_term vs t = case t |
579 |
of Free (xn, xT) => (case AList.lookup (op aconv) vs t |
|
580 |
of NONE => cooper "Variable not found in the list!" |
|
36798 | 581 |
| SOME n => Cooper_Procedure.Bound n) |
582 |
| @{term "0::int"} => Cooper_Procedure.C 0 |
|
583 |
| @{term "1::int"} => Cooper_Procedure.C 1 |
|
584 |
| Term.Bound i => Cooper_Procedure.Bound i |
|
585 |
| Const(@{const_name Groups.uminus},_)$t' => Cooper_Procedure.Neg (i_of_term vs t') |
|
586 |
| Const(@{const_name Groups.plus},_)$t1$t2 => Cooper_Procedure.Add (i_of_term vs t1,i_of_term vs t2) |
|
587 |
| Const(@{const_name Groups.minus},_)$t1$t2 => Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2) |
|
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35092
diff
changeset
|
588 |
| Const(@{const_name Groups.times},_)$t1$t2 => |
36798 | 589 |
(Cooper_Procedure.Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
590 |
handle TERM _ => |
36798 | 591 |
(Cooper_Procedure.Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1) |
23713 | 592 |
handle TERM _ => cooper "Reification: Unsupported kind of multiplication")) |
36798 | 593 |
| _ => (Cooper_Procedure.C (HOLogic.dest_number t |> snd) |
23713 | 594 |
handle TERM _ => cooper "Reification: unknown term"); |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset
|
595 |
|
23713 | 596 |
fun qf_of_term ps vs t = case t |
36798 | 597 |
of Const("True",_) => Cooper_Procedure.T |
598 |
| Const("False",_) => Cooper_Procedure.F |
|
599 |
| Const(@{const_name Orderings.less},_)$t1$t2 => Cooper_Procedure.Lt (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2)) |
|
600 |
| Const(@{const_name Orderings.less_eq},_)$t1$t2 => Cooper_Procedure.Le (Cooper_Procedure.Sub(i_of_term vs t1,i_of_term vs t2)) |
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
34974
diff
changeset
|
601 |
| Const(@{const_name Rings.dvd},_)$t1$t2 => |
36802 | 602 |
(Cooper_Procedure.Dvd (HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle TERM _ => cooper "Reification: unsupported dvd") |
36798 | 603 |
| @{term "op = :: int => _"}$t1$t2 => Cooper_Procedure.Eq (Cooper_Procedure.Sub (i_of_term vs t1,i_of_term vs t2)) |
604 |
| @{term "op = :: bool => _ "}$t1$t2 => Cooper_Procedure.Iff(qf_of_term ps vs t1,qf_of_term ps vs t2) |
|
605 |
| Const("op &",_)$t1$t2 => Cooper_Procedure.And(qf_of_term ps vs t1,qf_of_term ps vs t2) |
|
606 |
| Const("op |",_)$t1$t2 => Cooper_Procedure.Or(qf_of_term ps vs t1,qf_of_term ps vs t2) |
|
607 |
| Const("op -->",_)$t1$t2 => Cooper_Procedure.Imp(qf_of_term ps vs t1,qf_of_term ps vs t2) |
|
608 |
| Const (@{const_name Not},_)$t' => Cooper_Procedure.Not(qf_of_term ps vs t') |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
609 |
| Const("Ex",_)$Abs(xn,xT,p) => |
23713 | 610 |
let val (xn',p') = variant_abs (xn,xT,p) |
611 |
val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs) |
|
36798 | 612 |
in Cooper_Procedure.E (qf_of_term ps vs' p') |
23713 | 613 |
end |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
614 |
| Const("All",_)$Abs(xn,xT,p) => |
23713 | 615 |
let val (xn',p') = variant_abs (xn,xT,p) |
616 |
val vs' = (Free (xn',xT), 0) :: (map (fn(v,n) => (v,1+ n)) vs) |
|
36798 | 617 |
in Cooper_Procedure.A (qf_of_term ps vs' p') |
23713 | 618 |
end |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
619 |
| _ =>(case AList.lookup (op aconv) ps t of |
23713 | 620 |
NONE => cooper "Reification: unknown term!" |
36798 | 621 |
| SOME n => Cooper_Procedure.Closed n); |
23466 | 622 |
|
623 |
local |
|
624 |
val ops = [@{term "op &"}, @{term "op |"}, @{term "op -->"}, @{term "op = :: bool => _"}, |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
625 |
@{term "op = :: int => _"}, @{term "op < :: int => _"}, |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
626 |
@{term "op <= :: int => _"}, @{term "Not"}, @{term "All:: (int => _) => _"}, |
23466 | 627 |
@{term "Ex:: (int => _) => _"}, @{term "True"}, @{term "False"}] |
628 |
fun ty t = Bool.not (fastype_of t = HOLogic.boolT) |
|
629 |
in |
|
630 |
fun term_bools acc t = |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
631 |
case t of |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36527
diff
changeset
|
632 |
(l as f $ a) $ b => if ty t orelse member (op =) ops f then term_bools (term_bools acc l)b |
23466 | 633 |
else insert (op aconv) t acc |
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36527
diff
changeset
|
634 |
| f $ a => if ty t orelse member (op =) ops f then term_bools (term_bools acc f) a |
23466 | 635 |
else insert (op aconv) t acc |
636 |
| Abs p => term_bools acc (snd (variant_abs p)) |
|
36692
54b64d4ad524
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents:
36527
diff
changeset
|
637 |
| _ => if ty t orelse member (op =) ops t then acc else insert (op aconv) t acc |
23466 | 638 |
end; |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
639 |
|
23466 | 640 |
fun myassoc2 l v = |
641 |
case l of |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
642 |
[] => NONE |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset
|
643 |
| (x,v')::xs => if v = v' then SOME x |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
644 |
else myassoc2 xs v; |
23466 | 645 |
|
23713 | 646 |
fun term_of_i vs t = case t |
36798 | 647 |
of Cooper_Procedure.C i => HOLogic.mk_number HOLogic.intT i |
648 |
| Cooper_Procedure.Bound n => the (myassoc2 vs n) |
|
649 |
| Cooper_Procedure.Neg t' => @{term "uminus :: int => _"} $ term_of_i vs t' |
|
650 |
| Cooper_Procedure.Add (t1, t2) => @{term "op + :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2 |
|
651 |
| Cooper_Procedure.Sub (t1, t2) => @{term "op - :: int => _"} $ term_of_i vs t1 $ term_of_i vs t2 |
|
652 |
| Cooper_Procedure.Mul (i, t2) => @{term "op * :: int => _"} $ |
|
23713 | 653 |
HOLogic.mk_number HOLogic.intT i $ term_of_i vs t2 |
36798 | 654 |
| Cooper_Procedure.Cn (n, i, t') => term_of_i vs (Cooper_Procedure.Add (Cooper_Procedure.Mul (i, Cooper_Procedure.Bound n), t')); |
23466 | 655 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
656 |
fun term_of_qf ps vs t = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
657 |
case t of |
36798 | 658 |
Cooper_Procedure.T => HOLogic.true_const |
659 |
| Cooper_Procedure.F => HOLogic.false_const |
|
660 |
| Cooper_Procedure.Lt t' => @{term "op < :: int => _ "}$ term_of_i vs t'$ @{term "0::int"} |
|
661 |
| Cooper_Procedure.Le t' => @{term "op <= :: int => _ "}$ term_of_i vs t' $ @{term "0::int"} |
|
662 |
| Cooper_Procedure.Gt t' => @{term "op < :: int => _ "}$ @{term "0::int"}$ term_of_i vs t' |
|
663 |
| Cooper_Procedure.Ge t' => @{term "op <= :: int => _ "}$ @{term "0::int"}$ term_of_i vs t' |
|
664 |
| Cooper_Procedure.Eq t' => @{term "op = :: int => _ "}$ term_of_i vs t'$ @{term "0::int"} |
|
665 |
| Cooper_Procedure.NEq t' => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Eq t')) |
|
666 |
| Cooper_Procedure.Dvd(i,t') => @{term "op dvd :: int => _ "} $ |
|
23713 | 667 |
HOLogic.mk_number HOLogic.intT i $ term_of_i vs t' |
36798 | 668 |
| Cooper_Procedure.NDvd(i,t')=> term_of_qf ps vs (Cooper_Procedure.Not(Cooper_Procedure.Dvd(i,t'))) |
669 |
| Cooper_Procedure.Not t' => HOLogic.Not$(term_of_qf ps vs t') |
|
670 |
| Cooper_Procedure.And(t1,t2) => HOLogic.conj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) |
|
671 |
| Cooper_Procedure.Or(t1,t2) => HOLogic.disj$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) |
|
672 |
| Cooper_Procedure.Imp(t1,t2) => HOLogic.imp$(term_of_qf ps vs t1)$(term_of_qf ps vs t2) |
|
673 |
| Cooper_Procedure.Iff(t1,t2) => @{term "op = :: bool => _"} $ term_of_qf ps vs t1 $ term_of_qf ps vs t2 |
|
674 |
| Cooper_Procedure.Closed n => the (myassoc2 ps n) |
|
675 |
| Cooper_Procedure.NClosed n => term_of_qf ps vs (Cooper_Procedure.Not (Cooper_Procedure.Closed n)) |
|
29787 | 676 |
| _ => cooper "If this is raised, Isabelle/HOL or code generator is inconsistent!"; |
23466 | 677 |
|
36805 | 678 |
fun invoke t = |
23713 | 679 |
let |
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
28397
diff
changeset
|
680 |
val (vs, ps) = pairself (map_index swap) (OldTerm.term_frees t, term_bools [] t); |
23713 | 681 |
in |
36805 | 682 |
Logic.mk_equals (HOLogic.mk_Trueprop t, |
683 |
HOLogic.mk_Trueprop (term_of_qf ps vs (Cooper_Procedure.pa (qf_of_term ps vs t)))) |
|
23713 | 684 |
end; |
23466 | 685 |
|
36804 | 686 |
val (_, oracle) = Context.>>> (Context.map_theory_result |
36805 | 687 |
(Thm.add_oracle (Binding.name "cooper", |
688 |
(fn (ctxt, t) => Thm.cterm_of (ProofContext.theory_of ctxt) (invoke t))))); |
|
36802 | 689 |
|
690 |
val comp_ss = HOL_ss addsimps @{thms semiring_norm}; |
|
691 |
||
692 |
fun strip_objimp ct = |
|
693 |
(case Thm.term_of ct of |
|
694 |
Const ("op -->", _) $ _ $ _ => |
|
695 |
let val (A, B) = Thm.dest_binop ct |
|
696 |
in A :: strip_objimp B end |
|
697 |
| _ => [ct]); |
|
698 |
||
699 |
fun strip_objall ct = |
|
700 |
case term_of ct of |
|
701 |
Const ("All", _) $ Abs (xn,xT,p) => |
|
702 |
let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct |
|
703 |
in apfst (cons (a,v)) (strip_objall t') |
|
704 |
end |
|
705 |
| _ => ([],ct); |
|
706 |
||
707 |
local |
|
708 |
val all_maxscope_ss = |
|
709 |
HOL_basic_ss addsimps map (fn th => th RS sym) @{thms "all_simps"} |
|
710 |
in |
|
711 |
fun thin_prems_tac P = simp_tac all_maxscope_ss THEN' |
|
712 |
CSUBGOAL (fn (p', i) => |
|
713 |
let |
|
714 |
val (qvs, p) = strip_objall (Thm.dest_arg p') |
|
715 |
val (ps, c) = split_last (strip_objimp p) |
|
716 |
val qs = filter P ps |
|
717 |
val q = if P c then c else @{cterm "False"} |
|
718 |
val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs |
|
719 |
(fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm "op -->"} p) q) qs q) |
|
720 |
val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p' |
|
721 |
val ntac = (case qs of [] => q aconvc @{cterm "False"} |
|
722 |
| _ => false) |
|
723 |
in |
|
724 |
if ntac then no_tac |
|
725 |
else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i |
|
726 |
end) |
|
23466 | 727 |
end; |
36802 | 728 |
|
729 |
local |
|
730 |
fun isnum t = case t of |
|
731 |
Const(@{const_name Groups.zero},_) => true |
|
732 |
| Const(@{const_name Groups.one},_) => true |
|
733 |
| @{term "Suc"}$s => isnum s |
|
734 |
| @{term "nat"}$s => isnum s |
|
735 |
| @{term "int"}$s => isnum s |
|
736 |
| Const(@{const_name Groups.uminus},_)$s => isnum s |
|
737 |
| Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r |
|
738 |
| Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r |
|
739 |
| Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r |
|
740 |
| Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r |
|
741 |
| Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r |
|
742 |
| Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r |
|
743 |
| _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t |
|
744 |
||
745 |
fun ty cts t = |
|
746 |
if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false |
|
747 |
else case term_of t of |
|
748 |
c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c |
|
749 |
then not (isnum l orelse isnum r) |
|
750 |
else not (member (op aconv) cts c) |
|
751 |
| c$_ => not (member (op aconv) cts c) |
|
752 |
| c => not (member (op aconv) cts c) |
|
753 |
||
754 |
val term_constants = |
|
755 |
let fun h acc t = case t of |
|
756 |
Const _ => insert (op aconv) t acc |
|
757 |
| a$b => h (h acc a) b |
|
758 |
| Abs (_,_,t) => h acc t |
|
759 |
| _ => acc |
|
760 |
in h [] end; |
|
761 |
in |
|
762 |
fun is_relevant ctxt ct = |
|
763 |
subset (op aconv) (term_constants (term_of ct) , snd (get ctxt)) |
|
764 |
andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct)) |
|
765 |
andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct)); |
|
766 |
||
767 |
fun int_nat_terms ctxt ct = |
|
768 |
let |
|
769 |
val cts = snd (get ctxt) |
|
770 |
fun h acc t = if ty cts t then insert (op aconvc) t acc else |
|
771 |
case (term_of t) of |
|
772 |
_$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) |
|
773 |
| Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc)) |
|
774 |
| _ => acc |
|
775 |
in h [] ct end |
|
776 |
end; |
|
777 |
||
778 |
fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st => |
|
779 |
let |
|
780 |
fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"} |
|
781 |
fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t) |
|
782 |
val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p) |
|
783 |
val p' = fold_rev gen ts p |
|
784 |
in implies_intr p' (implies_elim st (fold forall_elim ts (assume p'))) end)); |
|
785 |
||
786 |
local |
|
787 |
val ss1 = comp_ss |
|
788 |
addsimps @{thms simp_thms} @ [@{thm "nat_number_of_def"}, @{thm "zdvd_int"}] |
|
789 |
@ map (fn r => r RS sym) |
|
790 |
[@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "zless_int"}, @{thm "zadd_int"}, |
|
791 |
@{thm "zmult_int"}] |
|
792 |
addsplits [@{thm "zdiff_int_split"}] |
|
793 |
||
794 |
val ss2 = HOL_basic_ss |
|
795 |
addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"}, |
|
796 |
@{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, |
|
797 |
@{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}] |
|
798 |
addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}] |
|
799 |
val div_mod_ss = HOL_basic_ss addsimps @{thms simp_thms} |
|
800 |
@ map (symmetric o mk_meta_eq) |
|
801 |
[@{thm "dvd_eq_mod_eq_0"}, |
|
802 |
@{thm "mod_add_left_eq"}, @{thm "mod_add_right_eq"}, |
|
803 |
@{thm "mod_add_eq"}, @{thm "div_add1_eq"}, @{thm "zdiv_zadd1_eq"}] |
|
804 |
@ [@{thm "mod_self"}, @{thm "zmod_self"}, @{thm "mod_by_0"}, |
|
805 |
@{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, |
|
806 |
@{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, |
|
807 |
@{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, |
|
808 |
@{thm "mod_1"}, @{thm "Suc_eq_plus1"}] |
|
809 |
@ @{thms add_ac} |
|
810 |
addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc] |
|
811 |
val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits |
|
812 |
[@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, |
|
813 |
@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] |
|
814 |
in |
|
815 |
fun nat_to_int_tac ctxt = |
|
816 |
simp_tac (Simplifier.context ctxt ss1) THEN_ALL_NEW |
|
817 |
simp_tac (Simplifier.context ctxt ss2) THEN_ALL_NEW |
|
818 |
simp_tac (Simplifier.context ctxt comp_ss); |
|
819 |
||
820 |
fun div_mod_tac ctxt i = simp_tac (Simplifier.context ctxt div_mod_ss) i; |
|
821 |
fun splits_tac ctxt i = simp_tac (Simplifier.context ctxt splits_ss) i; |
|
822 |
end; |
|
823 |
||
36804 | 824 |
fun core_tac ctxt = CSUBGOAL (fn (p, i) => |
36805 | 825 |
let |
36802 | 826 |
val cpth = |
827 |
if !quick_and_dirty |
|
36805 | 828 |
then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p)))) |
36804 | 829 |
else Conv.arg_conv (conv ctxt) p |
36802 | 830 |
val p' = Thm.rhs_of cpth |
831 |
val th = implies_intr p' (equal_elim (symmetric cpth) (assume p')) |
|
832 |
in rtac th i end |
|
833 |
handle COOPER _ => no_tac); |
|
834 |
||
835 |
fun finish_tac q = SUBGOAL (fn (_, i) => |
|
836 |
(if q then I else TRY) (rtac TrueI i)); |
|
837 |
||
36804 | 838 |
fun tac elim add_ths del_ths ctxt = |
36802 | 839 |
let val ss = Simplifier.context ctxt (fst (get ctxt)) delsimps del_ths addsimps add_ths |
840 |
val aprems = Arith_Data.get_arith_facts ctxt |
|
841 |
in |
|
842 |
Method.insert_tac aprems |
|
843 |
THEN_ALL_NEW Object_Logic.full_atomize_tac |
|
844 |
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
|
845 |
THEN_ALL_NEW simp_tac ss |
|
846 |
THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt)) |
|
847 |
THEN_ALL_NEW Object_Logic.full_atomize_tac |
|
848 |
THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt)) |
|
849 |
THEN_ALL_NEW Object_Logic.full_atomize_tac |
|
850 |
THEN_ALL_NEW div_mod_tac ctxt |
|
851 |
THEN_ALL_NEW splits_tac ctxt |
|
852 |
THEN_ALL_NEW simp_tac ss |
|
853 |
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
|
854 |
THEN_ALL_NEW nat_to_int_tac ctxt |
|
36804 | 855 |
THEN_ALL_NEW (core_tac ctxt) |
36802 | 856 |
THEN_ALL_NEW finish_tac elim |
857 |
end; |
|
858 |
||
36804 | 859 |
val method = |
36802 | 860 |
let |
861 |
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K () |
|
862 |
fun simple_keyword k = Scan.lift (Args.$$$ k) >> K () |
|
863 |
val addN = "add" |
|
864 |
val delN = "del" |
|
865 |
val elimN = "elim" |
|
866 |
val any_keyword = keyword addN || keyword delN || simple_keyword elimN |
|
867 |
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
|
868 |
in |
|
869 |
Scan.optional (simple_keyword elimN >> K false) true -- |
|
870 |
Scan.optional (keyword addN |-- thms) [] -- |
|
871 |
Scan.optional (keyword delN |-- thms) [] >> |
|
872 |
(fn ((elim, add_ths), del_ths) => fn ctxt => |
|
36804 | 873 |
SIMPLE_METHOD' (tac elim add_ths del_ths ctxt)) |
36802 | 874 |
end; |
875 |
||
876 |
||
877 |
(* theory setup *) |
|
878 |
||
879 |
local |
|
880 |
||
881 |
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
|
882 |
||
883 |
val constsN = "consts"; |
|
884 |
val any_keyword = keyword constsN |
|
885 |
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
|
886 |
val terms = thms >> map (term_of o Drule.dest_term); |
|
887 |
||
888 |
fun optional scan = Scan.optional scan []; |
|
889 |
||
890 |
in |
|
891 |
||
892 |
val setup = |
|
893 |
Attrib.setup @{binding presburger} |
|
894 |
((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del || |
|
895 |
optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm" |
|
36804 | 896 |
#> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] [])); |
36802 | 897 |
|
898 |
end; |
|
899 |
||
900 |
end; |