author | nipkow |
Tue, 05 Nov 2019 14:57:41 +0100 | |
changeset 71033 | c1b63124245c |
parent 69593 | 3dda49e08b9d |
child 71937 | 92de7d74b8f8 |
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 |
|
68632 | 12 |
val add: term list -> attribute |
37117
59cee8807c29
eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
wenzelm
parents:
36945
diff
changeset
|
13 |
exception COOPER of string |
36804 | 14 |
val conv: Proof.context -> conv |
15 |
val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic |
|
23466 | 16 |
end; |
17 |
||
36799 | 18 |
structure Cooper: COOPER = |
36798 | 19 |
struct |
20 |
||
36799 | 21 |
type entry = simpset * term list; |
36798 | 22 |
|
68632 | 23 |
val allowed_consts = |
69593 | 24 |
[\<^term>\<open>(+) :: int => _\<close>, \<^term>\<open>(+) :: nat => _\<close>, |
25 |
\<^term>\<open>(-) :: int => _\<close>, \<^term>\<open>(-) :: nat => _\<close>, |
|
26 |
\<^term>\<open>(*) :: int => _\<close>, \<^term>\<open>(*) :: nat => _\<close>, |
|
27 |
\<^term>\<open>(div) :: int => _\<close>, \<^term>\<open>(div) :: nat => _\<close>, |
|
28 |
\<^term>\<open>(mod) :: int => _\<close>, \<^term>\<open>(mod) :: nat => _\<close>, |
|
29 |
\<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>, \<^term>\<open>HOL.implies\<close>, |
|
30 |
\<^term>\<open>(=) :: int => _\<close>, \<^term>\<open>(=) :: nat => _\<close>, \<^term>\<open>(=) :: bool => _\<close>, |
|
31 |
\<^term>\<open>(<) :: int => _\<close>, \<^term>\<open>(<) :: nat => _\<close>, |
|
32 |
\<^term>\<open>(<=) :: int => _\<close>, \<^term>\<open>(<=) :: nat => _\<close>, |
|
33 |
\<^term>\<open>(dvd) :: int => _\<close>, \<^term>\<open>(dvd) :: nat => _\<close>, |
|
34 |
\<^term>\<open>abs :: int => _\<close>, |
|
35 |
\<^term>\<open>max :: int => _\<close>, \<^term>\<open>max :: nat => _\<close>, |
|
36 |
\<^term>\<open>min :: int => _\<close>, \<^term>\<open>min :: nat => _\<close>, |
|
37 |
\<^term>\<open>uminus :: int => _\<close>, (*@ {term "uminus :: nat => _"},*) |
|
38 |
\<^term>\<open>Not\<close>, \<^term>\<open>Suc\<close>, |
|
39 |
\<^term>\<open>Ex :: (int => _) => _\<close>, \<^term>\<open>Ex :: (nat => _) => _\<close>, |
|
40 |
\<^term>\<open>All :: (int => _) => _\<close>, \<^term>\<open>All :: (nat => _) => _\<close>, |
|
41 |
\<^term>\<open>nat\<close>, \<^term>\<open>int\<close>, |
|
42 |
\<^term>\<open>Num.One\<close>, \<^term>\<open>Num.Bit0\<close>, \<^term>\<open>Num.Bit1\<close>, |
|
43 |
\<^term>\<open>Num.numeral :: num => int\<close>, \<^term>\<open>Num.numeral :: num => nat\<close>, |
|
44 |
\<^term>\<open>0::int\<close>, \<^term>\<open>1::int\<close>, \<^term>\<open>0::nat\<close>, \<^term>\<open>1::nat\<close>, |
|
45 |
\<^term>\<open>True\<close>, \<^term>\<open>False\<close>]; |
|
36798 | 46 |
|
47 |
structure Data = Generic_Data |
|
48 |
( |
|
49 |
type T = simpset * term list; |
|
50 |
val empty = (HOL_ss, allowed_consts); |
|
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
39159
diff
changeset
|
51 |
val extend = I; |
36798 | 52 |
fun merge ((ss1, ts1), (ss2, ts2)) = |
53 |
(merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2)); |
|
54 |
); |
|
55 |
||
56 |
val get = Data.get o Context.Proof; |
|
57 |
||
68632 | 58 |
fun add ts = Thm.declaration_attribute (fn th => fn context => |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
59 |
context |> Data.map (fn (ss, ts') => |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
60 |
(simpset_map (Context.proof_of context) (fn ctxt => ctxt addsimps [th]) ss, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
61 |
merge (op aconv) (ts', ts)))) |
36798 | 62 |
|
68632 | 63 |
fun del ts = Thm.declaration_attribute (fn th => fn context => |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
64 |
context |> Data.map (fn (ss, ts') => |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
65 |
(simpset_map (Context.proof_of context) (fn ctxt => ctxt delsimps [th]) ss, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
66 |
subtract (op aconv) ts' ts))) |
36798 | 67 |
|
27018 | 68 |
fun simp_thms_conv ctxt = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
69 |
Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms}); |
23484 | 70 |
val FWD = Drule.implies_elim_list; |
23466 | 71 |
|
69593 | 72 |
val true_tm = \<^cterm>\<open>True\<close>; |
73 |
val false_tm = \<^cterm>\<open>False\<close>; |
|
23466 | 74 |
val zdvd1_eq = @{thm "zdvd1_eq"}; |
69593 | 75 |
val presburger_ss = simpset_of (\<^context> addsimps [zdvd1_eq]); |
45196
78478d938cb8
inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
wenzelm
parents:
44121
diff
changeset
|
76 |
val lin_ss = |
69593 | 77 |
simpset_of (put_simpset presburger_ss \<^context> |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
56245
diff
changeset
|
78 |
addsimps (@{thm dvd_eq_mod_eq_0} :: zdvd1_eq :: @{thms ac_simps [where 'a=int]})); |
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset
|
79 |
|
23466 | 80 |
val iT = HOLogic.intT |
81 |
val bT = HOLogic.boolT; |
|
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
82 |
val dest_number = HOLogic.dest_number #> snd; |
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
83 |
val perhaps_number = try dest_number; |
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
84 |
val is_number = can dest_number; |
23466 | 85 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
86 |
val [miconj, midisj, mieq, mineq, milt, mile, migt, mige, midvd, mindvd, miP] = |
69593 | 87 |
map (Thm.instantiate' [SOME \<^ctyp>\<open>int\<close>] []) @{thms "minf"}; |
23466 | 88 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
89 |
val [infDconj, infDdisj, infDdvd,infDndvd,infDP] = |
69593 | 90 |
map (Thm.instantiate' [SOME \<^ctyp>\<open>int\<close>] []) @{thms "inf_period"}; |
23466 | 91 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
92 |
val [piconj, pidisj, pieq,pineq,pilt,pile,pigt,pige,pidvd,pindvd,piP] = |
69593 | 93 |
map (Thm.instantiate' [SOME \<^ctyp>\<open>int\<close>] []) @{thms "pinf"}; |
23466 | 94 |
|
69593 | 95 |
val [miP, piP] = map (Thm.instantiate' [SOME \<^ctyp>\<open>bool\<close>] []) [miP, piP]; |
23466 | 96 |
|
69593 | 97 |
val infDP = Thm.instantiate' (map SOME [\<^ctyp>\<open>int\<close>, \<^ctyp>\<open>bool\<close>]) [] infDP; |
23466 | 98 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
99 |
val [[asetconj, asetdisj, aseteq, asetneq, asetlt, asetle, |
23466 | 100 |
asetgt, asetge, asetdvd, asetndvd,asetP], |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
101 |
[bsetconj, bsetdisj, bseteq, bsetneq, bsetlt, bsetle, |
23466 | 102 |
bsetgt, bsetge, bsetdvd, bsetndvd,bsetP]] = [@{thms "aset"}, @{thms "bset"}]; |
103 |
||
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
104 |
val [cpmi, cppi] = [@{thm "cpmi"}, @{thm "cppi"}]; |
23466 | 105 |
|
69593 | 106 |
val unity_coeff_ex = Thm.instantiate' [SOME \<^ctyp>\<open>int\<close>] [] @{thm "unity_coeff_ex"}; |
23466 | 107 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
108 |
val [zdvd_mono,simp_from_to,all_not_ex] = |
23466 | 109 |
[@{thm "zdvd_mono"}, @{thm "simp_from_to"}, @{thm "all_not_ex"}]; |
110 |
||
111 |
val [dvd_uminus, dvd_uminus'] = @{thms "uminus_dvd_conv"}; |
|
112 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
113 |
val eval_ss = |
69593 | 114 |
simpset_of (put_simpset presburger_ss \<^context> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
115 |
addsimps [simp_from_to] delsimps [insert_iff, bex_triv]); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
116 |
fun eval_conv ctxt = Simplifier.rewrite (put_simpset eval_ss ctxt); |
23466 | 117 |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset
|
118 |
(* recognising cterm without moving to terms *) |
23466 | 119 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
120 |
datatype fm = And of cterm*cterm| Or of cterm*cterm| Eq of cterm | NEq of cterm |
23466 | 121 |
| Lt of cterm | Le of cterm | Gt of cterm | Ge of cterm |
122 |
| Dvd of cterm*cterm | NDvd of cterm*cterm | Nox |
|
123 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
124 |
fun whatis x ct = |
59582 | 125 |
( case Thm.term_of ct of |
69593 | 126 |
Const(\<^const_name>\<open>HOL.conj\<close>,_)$_$_ => And (Thm.dest_binop ct) |
127 |
| Const (\<^const_name>\<open>HOL.disj\<close>,_)$_$_ => Or (Thm.dest_binop ct) |
|
128 |
| Const (\<^const_name>\<open>HOL.eq\<close>,_)$y$_ => if Thm.term_of x aconv y then Eq (Thm.dest_arg ct) else Nox |
|
129 |
| Const (\<^const_name>\<open>Not\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_)$y$_) => |
|
59582 | 130 |
if Thm.term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox |
69593 | 131 |
| Const (\<^const_name>\<open>Orderings.less\<close>, _) $ y$ z => |
59582 | 132 |
if Thm.term_of x aconv y then Lt (Thm.dest_arg ct) |
133 |
else if Thm.term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox |
|
69593 | 134 |
| Const (\<^const_name>\<open>Orderings.less_eq\<close>, _) $ y $ z => |
59582 | 135 |
if Thm.term_of x aconv y then Le (Thm.dest_arg ct) |
136 |
else if Thm.term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox |
|
69593 | 137 |
| Const (\<^const_name>\<open>Rings.dvd\<close>,_)$_$(Const(\<^const_name>\<open>Groups.plus\<close>,_)$y$_) => |
59582 | 138 |
if Thm.term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox |
69593 | 139 |
| Const (\<^const_name>\<open>Not\<close>,_) $ (Const (\<^const_name>\<open>Rings.dvd\<close>,_)$_$(Const(\<^const_name>\<open>Groups.plus\<close>,_)$y$_)) => |
59582 | 140 |
if Thm.term_of x aconv y then |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
141 |
NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox |
23466 | 142 |
| _ => Nox) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
143 |
handle CTERM _ => Nox; |
23466 | 144 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
145 |
fun get_pmi_term t = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
146 |
let val (x,eq) = |
23466 | 147 |
(Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg) |
148 |
(Thm.dest_arg t) |
|
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45740
diff
changeset
|
149 |
in (Thm.lambda x o Thm.dest_arg o Thm.dest_arg) eq end; |
23466 | 150 |
|
59582 | 151 |
val get_pmi = get_pmi_term o Thm.cprop_of; |
23466 | 152 |
|
69593 | 153 |
val p_v' = (("P'", 0), \<^typ>\<open>int \<Rightarrow> bool\<close>); |
154 |
val q_v' = (("Q'", 0), \<^typ>\<open>int \<Rightarrow> bool\<close>); |
|
155 |
val p_v = (("P", 0), \<^typ>\<open>int \<Rightarrow> bool\<close>); |
|
156 |
val q_v = (("Q", 0), \<^typ>\<open>int \<Rightarrow> bool\<close>); |
|
23466 | 157 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
158 |
fun myfwd (th1, th2, th3) p q |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
159 |
[(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
|
160 |
let |
23466 | 161 |
val (mp', mq') = (get_pmi th_1, get_pmi th_1') |
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
42793
diff
changeset
|
162 |
val mi_th = FWD (Drule.instantiate_normalize ([],[(p_v,p),(q_v,q), (p_v',mp'),(q_v',mq')]) th1) |
23466 | 163 |
[th_1, th_1'] |
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
42793
diff
changeset
|
164 |
val infD_th = FWD (Drule.instantiate_normalize ([],[(p_v,mp'), (q_v, mq')]) th3) [th_3,th_3'] |
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
42793
diff
changeset
|
165 |
val set_th = FWD (Drule.instantiate_normalize ([],[(p_v,p), (q_v,q)]) th2) [th_2, th_2'] |
23466 | 166 |
in (mi_th, set_th, infD_th) |
167 |
end; |
|
168 |
||
60801 | 169 |
val inst' = fn cts => Thm.instantiate' [] (map SOME cts); |
170 |
val infDTrue = Thm.instantiate' [] [SOME true_tm] infDP; |
|
171 |
val infDFalse = Thm.instantiate' [] [SOME false_tm] infDP; |
|
23466 | 172 |
|
69593 | 173 |
val cadd = \<^cterm>\<open>(+) :: int => _\<close> |
174 |
val cmulC = \<^cterm>\<open>(*) :: int => _\<close> |
|
175 |
val cminus = \<^cterm>\<open>(-) :: int => _\<close> |
|
176 |
val cone = \<^cterm>\<open>1 :: int\<close> |
|
59582 | 177 |
val [addC, mulC, subC] = map Thm.term_of [cadd, cmulC, cminus] |
69593 | 178 |
val [zero, one] = [\<^term>\<open>0 :: int\<close>, \<^term>\<open>1 :: int\<close>]; |
23466 | 179 |
|
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
180 |
fun numeral1 f n = HOLogic.mk_number iT (f (dest_number n)); |
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
181 |
fun numeral2 f m n = HOLogic.mk_number iT (f (dest_number m) (dest_number n)); |
23466 | 182 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
183 |
val [minus1,plus1] = |
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45740
diff
changeset
|
184 |
map (fn c => fn t => Thm.apply (Thm.apply c t) cone) [cminus,cadd]; |
23466 | 185 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
186 |
fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle, |
23466 | 187 |
asetgt, asetge,asetdvd,asetndvd,asetP, |
188 |
infDdvd, infDndvd, asetconj, |
|
189 |
asetdisj, infDconj, infDdisj] cp = |
|
190 |
case (whatis x cp) of |
|
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45740
diff
changeset
|
191 |
And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.lambda x p) (Thm.lambda x q)) |
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45740
diff
changeset
|
192 |
| Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.lambda x p) (Thm.lambda x q)) |
23466 | 193 |
| Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse)) |
194 |
| NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue)) |
|
195 |
| Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse)) |
|
196 |
| Le t => ([], K (inst' [t] pile, FWD (inst' [t] asetle) [inS (plus1 t)], infDFalse)) |
|
197 |
| Gt t => ([], K (inst' [t] pigt, (inst' [t] asetgt), infDTrue)) |
|
198 |
| Ge t => ([], K (inst' [t] pige, (inst' [t] asetge), infDTrue)) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
199 |
| Dvd (d,s) => |
23466 | 200 |
([],let val dd = dvd d |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
201 |
in K (inst' [d,s] pidvd, FWD (inst' [d,s] asetdvd) [dd],FWD (inst' [d,s] infDdvd) [dd]) end) |
23466 | 202 |
| NDvd(d,s) => ([],let val dd = dvd d |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
203 |
in K (inst' [d,s] pindvd, FWD (inst' [d,s] asetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end) |
23466 | 204 |
| _ => ([], K (inst' [cp] piP, inst' [cp] asetP, inst' [cp] infDP)); |
205 |
||
206 |
fun decomp_minf x dvd inS [bseteq,bsetneq,bsetlt, bsetle, bsetgt, |
|
207 |
bsetge,bsetdvd,bsetndvd,bsetP, |
|
208 |
infDdvd, infDndvd, bsetconj, |
|
209 |
bsetdisj, infDconj, infDdisj] cp = |
|
210 |
case (whatis x cp) of |
|
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45740
diff
changeset
|
211 |
And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.lambda x p) (Thm.lambda x q)) |
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45740
diff
changeset
|
212 |
| Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.lambda x p) (Thm.lambda x q)) |
23466 | 213 |
| Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse)) |
214 |
| NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue)) |
|
215 |
| Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue)) |
|
216 |
| Le t => ([], K (inst' [t] mile, (inst' [t] bsetle), infDTrue)) |
|
217 |
| Gt t => ([], K (inst' [t] migt, FWD (inst' [t] bsetgt) [inS t], infDFalse)) |
|
218 |
| Ge t => ([], K (inst' [t] mige,FWD (inst' [t] bsetge) [inS (minus1 t)], infDFalse)) |
|
219 |
| Dvd (d,s) => ([],let val dd = dvd d |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
220 |
in K (inst' [d,s] midvd, FWD (inst' [d,s] bsetdvd) [dd] , FWD (inst' [d,s] infDdvd) [dd]) end) |
23466 | 221 |
| NDvd (d,s) => ([],let val dd = dvd d |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
222 |
in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end) |
23466 | 223 |
| _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP)) |
224 |
||
225 |
(* Canonical linear form for terms, formulae etc.. *) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
226 |
fun provelin ctxt t = Goal.prove ctxt [] [] t |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
227 |
(fn _ => EVERY [simp_tac (put_simpset lin_ss ctxt) 1, TRY (Lin_Arith.tac ctxt 1)]); |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
228 |
fun linear_cmul 0 tm = zero |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
229 |
| linear_cmul n tm = case tm of |
69593 | 230 |
Const (\<^const_name>\<open>Groups.plus\<close>, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b |
231 |
| Const (\<^const_name>\<open>Groups.times\<close>, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x |
|
232 |
| Const (\<^const_name>\<open>Groups.minus\<close>, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b |
|
233 |
| (m as Const (\<^const_name>\<open>Groups.uminus\<close>, _)) $ a => m $ linear_cmul n a |
|
25768 | 234 |
| _ => numeral1 (fn m => n * m) tm; |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
235 |
fun earlier [] x y = false |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
236 |
| earlier (h::t) x y = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
237 |
if h aconv y then false else if h aconv x then true else earlier t x y; |
23466 | 238 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
239 |
fun linear_add vars tm1 tm2 = case (tm1, tm2) of |
69593 | 240 |
(Const (\<^const_name>\<open>Groups.plus\<close>, _) $ (Const (\<^const_name>\<open>Groups.times\<close>, _) $ c1 $ x1) $ r1, |
241 |
Const (\<^const_name>\<open>Groups.plus\<close>, _) $ (Const (\<^const_name>\<open>Groups.times\<close>, _) $ c2 $ x2) $ r2) => |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
242 |
if x1 = x2 then |
33002 | 243 |
let val c = numeral2 Integer.add c1 c2 |
25768 | 244 |
in if c = zero then linear_add vars r1 r2 |
245 |
else addC$(mulC$c$x1)$(linear_add vars r1 r2) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
246 |
end |
25768 | 247 |
else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 |
248 |
else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 |
|
69593 | 249 |
| (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ (Const (\<^const_name>\<open>Groups.times\<close>, _) $ c1 $ x1) $ r1, _) => |
25768 | 250 |
addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2 |
69593 | 251 |
| (_, Const (\<^const_name>\<open>Groups.plus\<close>, _) $ (Const (\<^const_name>\<open>Groups.times\<close>, _) $ c2 $ x2) $ r2) => |
25768 | 252 |
addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2 |
33002 | 253 |
| (_, _) => numeral2 Integer.add tm1 tm2; |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
254 |
|
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
255 |
fun linear_neg tm = linear_cmul ~1 tm; |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
256 |
fun linear_sub vars tm1 tm2 = linear_add vars tm1 (linear_neg tm2); |
23466 | 257 |
|
36806 | 258 |
exception COOPER of string; |
23466 | 259 |
|
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
260 |
fun lint vars tm = if is_number tm then tm else case tm of |
69593 | 261 |
Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ t => linear_neg (lint vars t) |
262 |
| Const (\<^const_name>\<open>Groups.plus\<close>, _) $ s $ t => linear_add vars (lint vars s) (lint vars t) |
|
263 |
| Const (\<^const_name>\<open>Groups.minus\<close>, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t) |
|
264 |
| Const (\<^const_name>\<open>Groups.times\<close>, _) $ s $ t => |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
265 |
let val s' = lint vars s |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
266 |
val t' = lint vars t |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
267 |
in case perhaps_number s' of SOME n => linear_cmul n t' |
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
268 |
| NONE => (case perhaps_number t' of SOME n => linear_cmul n s' |
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
269 |
| NONE => raise COOPER "lint: not linear") |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
270 |
end |
25768 | 271 |
| _ => addC $ (mulC $ one $ tm) $ zero; |
23466 | 272 |
|
69593 | 273 |
fun lin (vs as _::_) (Const (\<^const_name>\<open>Not\<close>, _) $ (Const (\<^const_name>\<open>Orderings.less\<close>, T) $ s $ t)) = |
274 |
lin vs (Const (\<^const_name>\<open>Orderings.less_eq\<close>, T) $ t $ s) |
|
275 |
| lin (vs as _::_) (Const (\<^const_name>\<open>Not\<close>,_) $ (Const(\<^const_name>\<open>Orderings.less_eq\<close>, T) $ s $ t)) = |
|
276 |
lin vs (Const (\<^const_name>\<open>Orderings.less\<close>, T) $ t $ s) |
|
277 |
| lin vs (Const (\<^const_name>\<open>Not\<close>,T)$t) = Const (\<^const_name>\<open>Not\<close>,T)$ (lin vs t) |
|
278 |
| lin (vs as _::_) (Const(\<^const_name>\<open>Rings.dvd\<close>,_)$d$t) = |
|
279 |
HOLogic.mk_binrel \<^const_name>\<open>Rings.dvd\<close> (numeral1 abs d, lint vs t) |
|
280 |
| lin (vs as x::_) ((b as Const(\<^const_name>\<open>HOL.eq\<close>,_))$s$t) = |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
281 |
(case lint vs (subC$t$s) of |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
282 |
(t as _$(m$c$y)$r) => |
23466 | 283 |
if x <> y then b$zero$t |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
284 |
else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r |
23466 | 285 |
else b$(m$c$y)$(linear_neg r) |
286 |
| t => b$zero$t) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
287 |
| lin (vs as x::_) (b$s$t) = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
288 |
(case lint vs (subC$t$s) of |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
289 |
(t as _$(m$c$y)$r) => |
23466 | 290 |
if x <> y then b$zero$t |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
291 |
else if dest_number c < 0 then b$(m$(numeral1 ~ c)$y)$r |
23466 | 292 |
else b$(linear_neg r)$(m$c$y) |
293 |
| t => b$zero$t) |
|
294 |
| lin vs fm = fm; |
|
295 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
296 |
fun lint_conv ctxt vs ct = |
59582 | 297 |
let val t = Thm.term_of ct |
23466 | 298 |
in (provelin ctxt ((HOLogic.eq_const iT)$t$(lint vs t) |> HOLogic.mk_Trueprop)) |
299 |
RS eq_reflection |
|
300 |
end; |
|
301 |
||
69593 | 302 |
fun is_intrel_type T = T = \<^typ>\<open>int => int => bool\<close>; |
32398 | 303 |
|
304 |
fun is_intrel (b$_$_) = is_intrel_type (fastype_of b) |
|
69593 | 305 |
| is_intrel (\<^term>\<open>Not\<close>$(b$_$_)) = is_intrel_type (fastype_of b) |
23466 | 306 |
| is_intrel _ = false; |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
307 |
|
59582 | 308 |
fun linearize_conv ctxt vs ct = case Thm.term_of ct of |
69593 | 309 |
Const(\<^const_name>\<open>Rings.dvd\<close>,_)$_$_ => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
310 |
let |
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
311 |
val th = Conv.binop_conv (lint_conv ctxt vs) ct |
23466 | 312 |
val (d',t') = Thm.dest_binop (Thm.rhs_of th) |
59582 | 313 |
val (dt',tt') = (Thm.term_of d', Thm.term_of t') |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
314 |
in if is_number dt' andalso is_number tt' |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
315 |
then Conv.fconv_rule (Conv.arg_conv (Simplifier.rewrite (put_simpset presburger_ss ctxt))) th |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
316 |
else |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
317 |
let |
50321
df5553c4973f
add check to Cooper's algorithm that left-hand of dvd is a numeral
hoelzl
parents:
47476
diff
changeset
|
318 |
val dth = |
59582 | 319 |
case perhaps_number (Thm.term_of d') of |
50321
df5553c4973f
add check to Cooper's algorithm that left-hand of dvd is a numeral
hoelzl
parents:
47476
diff
changeset
|
320 |
SOME d => if d < 0 then |
df5553c4973f
add check to Cooper's algorithm that left-hand of dvd is a numeral
hoelzl
parents:
47476
diff
changeset
|
321 |
(Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (lint_conv ctxt vs))) |
df5553c4973f
add check to Cooper's algorithm that left-hand of dvd is a numeral
hoelzl
parents:
47476
diff
changeset
|
322 |
(Thm.transitive th (inst' [d',t'] dvd_uminus)) |
df5553c4973f
add check to Cooper's algorithm that left-hand of dvd is a numeral
hoelzl
parents:
47476
diff
changeset
|
323 |
handle TERM _ => th) |
df5553c4973f
add check to Cooper's algorithm that left-hand of dvd is a numeral
hoelzl
parents:
47476
diff
changeset
|
324 |
else th |
df5553c4973f
add check to Cooper's algorithm that left-hand of dvd is a numeral
hoelzl
parents:
47476
diff
changeset
|
325 |
| NONE => raise COOPER "linearize_conv: not linear" |
23466 | 326 |
val d'' = Thm.rhs_of dth |> Thm.dest_arg1 |
327 |
in |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
328 |
case tt' of |
69593 | 329 |
Const(\<^const_name>\<open>Groups.plus\<close>,_)$(Const(\<^const_name>\<open>Groups.times\<close>,_)$c$_)$_ => |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
330 |
let val x = dest_number c |
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
331 |
in if x < 0 then Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (lint_conv ctxt vs))) |
23466 | 332 |
(Thm.transitive dth (inst' [d'',t'] dvd_uminus')) |
333 |
else dth end |
|
334 |
| _ => dth |
|
335 |
end |
|
336 |
end |
|
69593 | 337 |
| Const (\<^const_name>\<open>Not\<close>,_)$(Const(\<^const_name>\<open>Rings.dvd\<close>,_)$_$_) => Conv.arg_conv (linearize_conv ctxt vs) ct |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
338 |
| t => if is_intrel t |
23466 | 339 |
then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop)) |
340 |
RS eq_reflection |
|
36945 | 341 |
else Thm.reflexive ct; |
23466 | 342 |
|
69593 | 343 |
val dvdc = \<^cterm>\<open>(dvd) :: int => _\<close>; |
23466 | 344 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
345 |
fun unify ctxt q = |
23466 | 346 |
let |
347 |
val (e,(cx,p)) = q |> Thm.dest_comb ||> Thm.dest_abs NONE |
|
59582 | 348 |
val x = Thm.term_of cx |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
349 |
val ins = insert (op = : int * int -> bool) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
350 |
fun h (acc,dacc) t = |
59582 | 351 |
case Thm.term_of t of |
69593 | 352 |
Const(s,_)$(Const(\<^const_name>\<open>Groups.times\<close>,_)$c$y)$ _ => |
23881 | 353 |
if x aconv y andalso member (op =) |
69593 | 354 |
[\<^const_name>\<open>HOL.eq\<close>, \<^const_name>\<open>Orderings.less\<close>, \<^const_name>\<open>Orderings.less_eq\<close>] s |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
355 |
then (ins (dest_number c) acc,dacc) else (acc,dacc) |
69593 | 356 |
| Const(s,_)$_$(Const(\<^const_name>\<open>Groups.times\<close>,_)$c$y) => |
23881 | 357 |
if x aconv y andalso member (op =) |
69593 | 358 |
[\<^const_name>\<open>Orderings.less\<close>, \<^const_name>\<open>Orderings.less_eq\<close>] s |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
359 |
then (ins (dest_number c) acc, dacc) else (acc,dacc) |
69593 | 360 |
| Const(\<^const_name>\<open>Rings.dvd\<close>,_)$_$(Const(\<^const_name>\<open>Groups.plus\<close>,_)$(Const(\<^const_name>\<open>Groups.times\<close>,_)$c$y)$_) => |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
361 |
if x aconv y then (acc,ins (dest_number c) dacc) else (acc,dacc) |
69593 | 362 |
| Const(\<^const_name>\<open>HOL.conj\<close>,_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
363 |
| Const(\<^const_name>\<open>HOL.disj\<close>,_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t) |
|
364 |
| Const (\<^const_name>\<open>Not\<close>,_)$_ => h (acc,dacc) (Thm.dest_arg t) |
|
23466 | 365 |
| _ => (acc, dacc) |
366 |
val (cs,ds) = h ([],[]) p |
|
33042 | 367 |
val l = Integer.lcms (union (op =) cs ds) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
368 |
fun cv k ct = |
59582 | 369 |
let val (tm as b$s$t) = Thm.term_of ct |
23466 | 370 |
in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t)) |
371 |
|> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
372 |
fun nzprop x = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
373 |
let |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
374 |
val th = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
375 |
Simplifier.rewrite (put_simpset lin_ss ctxt) |
69593 | 376 |
(Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply \<^cterm>\<open>Not\<close> |
377 |
(Thm.apply (Thm.apply \<^cterm>\<open>(=) :: int => _\<close> (Numeral.mk_cnumber \<^ctyp>\<open>int\<close> x)) |
|
378 |
\<^cterm>\<open>0::int\<close>))) |
|
36945 | 379 |
in Thm.equal_elim (Thm.symmetric th) TrueI end; |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
380 |
val notz = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
381 |
let val tab = fold Inttab.update |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
382 |
(ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
383 |
in |
59582 | 384 |
fn ct => the (Inttab.lookup tab (ct |> Thm.term_of |> dest_number)) |
51930
52fd62618631
prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents:
51717
diff
changeset
|
385 |
handle Option.Option => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
386 |
(writeln ("noz: Theorems-Table contains no entry for " ^ |
51930
52fd62618631
prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents:
51717
diff
changeset
|
387 |
Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
388 |
end |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
389 |
fun unit_conv t = |
59582 | 390 |
case Thm.term_of t of |
69593 | 391 |
Const(\<^const_name>\<open>HOL.conj\<close>,_)$_$_ => Conv.binop_conv unit_conv t |
392 |
| Const(\<^const_name>\<open>HOL.disj\<close>,_)$_$_ => Conv.binop_conv unit_conv t |
|
393 |
| Const (\<^const_name>\<open>Not\<close>,_)$_ => Conv.arg_conv unit_conv t |
|
394 |
| Const(s,_)$(Const(\<^const_name>\<open>Groups.times\<close>,_)$c$y)$ _ => |
|
23881 | 395 |
if x=y andalso member (op =) |
69593 | 396 |
[\<^const_name>\<open>HOL.eq\<close>, \<^const_name>\<open>Orderings.less\<close>, \<^const_name>\<open>Orderings.less_eq\<close>] s |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
397 |
then cv (l div dest_number c) t else Thm.reflexive t |
69593 | 398 |
| Const(s,_)$_$(Const(\<^const_name>\<open>Groups.times\<close>,_)$c$y) => |
23881 | 399 |
if x=y andalso member (op =) |
69593 | 400 |
[\<^const_name>\<open>Orderings.less\<close>, \<^const_name>\<open>Orderings.less_eq\<close>] s |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
401 |
then cv (l div dest_number c) t else Thm.reflexive t |
69593 | 402 |
| Const(\<^const_name>\<open>Rings.dvd\<close>,_)$d$(r as (Const(\<^const_name>\<open>Groups.plus\<close>,_)$(Const(\<^const_name>\<open>Groups.times\<close>,_)$c$y)$_)) => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
403 |
if x=y then |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
404 |
let |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
405 |
val k = l div dest_number c |
23466 | 406 |
val kt = HOLogic.mk_number iT k |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
407 |
val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t] |
23466 | 408 |
((Thm.dest_arg t |> funpow 2 Thm.dest_arg1 |> notz) RS zdvd_mono) |
409 |
val (d',t') = (mulC$kt$d, mulC$kt$r) |
|
410 |
val thc = (provelin ctxt ((HOLogic.eq_const iT)$d'$(lint [] d') |> HOLogic.mk_Trueprop)) |
|
411 |
RS eq_reflection |
|
412 |
val tht = (provelin ctxt ((HOLogic.eq_const iT)$t'$(linear_cmul k r) |> HOLogic.mk_Trueprop)) |
|
413 |
RS eq_reflection |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
414 |
in Thm.transitive th1 (Thm.combination (Drule.arg_cong_rule dvdc thc) tht) end |
23466 | 415 |
else Thm.reflexive t |
416 |
| _ => Thm.reflexive t |
|
417 |
val uth = unit_conv p |
|
69593 | 418 |
val clt = Numeral.mk_cnumber \<^ctyp>\<open>int\<close> l |
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45740
diff
changeset
|
419 |
val ltx = Thm.apply (Thm.apply cmulC clt) cx |
23466 | 420 |
val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth) |
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45740
diff
changeset
|
421 |
val th' = inst' [Thm.lambda ltx (Thm.rhs_of uth), clt] unity_coeff_ex |
36945 | 422 |
val thf = Thm.transitive th |
59582 | 423 |
(Thm.transitive (Thm.symmetric (Thm.beta_conversion true (Thm.cprop_of th' |> Thm.dest_arg1))) th') |
424 |
val (lth,rth) = Thm.dest_comb (Thm.cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true |
|
36945 | 425 |
||> Thm.beta_conversion true |>> Thm.symmetric |
426 |
in Thm.transitive (Thm.transitive lth thf) rth end; |
|
23466 | 427 |
|
428 |
||
69593 | 429 |
val emptyIS = \<^cterm>\<open>{}::int set\<close>; |
430 |
val insert_tm = \<^cterm>\<open>insert :: int => _\<close>; |
|
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45740
diff
changeset
|
431 |
fun mkISet cts = fold_rev (Thm.apply insert_tm #> Thm.apply) cts emptyIS; |
39159 | 432 |
val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1; |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60352
diff
changeset
|
433 |
val [A_v,B_v] = |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60352
diff
changeset
|
434 |
map (fn th => Thm.cprop_of th |> funpow 2 Thm.dest_arg |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60352
diff
changeset
|
435 |
|> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60352
diff
changeset
|
436 |
|> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg |
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60352
diff
changeset
|
437 |
|> Thm.term_of |> dest_Var) [asetP, bsetP]; |
23466 | 438 |
|
69593 | 439 |
val D_v = (("D", 0), \<^typ>\<open>int\<close>); |
23466 | 440 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
441 |
fun cooperex_conv ctxt vs q = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
442 |
let |
23466 | 443 |
|
444 |
val uth = unify ctxt q |
|
445 |
val (x,p) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of uth)) |
|
446 |
val ins = insert (op aconvc) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
447 |
fun h t (bacc,aacc,dacc) = |
23466 | 448 |
case (whatis x t) of |
449 |
And (p,q) => h q (h p (bacc,aacc,dacc)) |
|
450 |
| Or (p,q) => h q (h p (bacc,aacc,dacc)) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
451 |
| Eq t => (ins (minus1 t) bacc, |
23466 | 452 |
ins (plus1 t) aacc,dacc) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
453 |
| NEq t => (ins t bacc, |
23466 | 454 |
ins t aacc, dacc) |
455 |
| Lt t => (bacc, ins t aacc, dacc) |
|
456 |
| Le t => (bacc, ins (plus1 t) aacc,dacc) |
|
457 |
| Gt t => (ins t bacc, aacc,dacc) |
|
458 |
| Ge t => (ins (minus1 t) bacc, aacc,dacc) |
|
59582 | 459 |
| Dvd (d,_) => (bacc,aacc,insert (op =) (Thm.term_of d |> dest_number) dacc) |
460 |
| NDvd (d,_) => (bacc,aacc,insert (op =) (Thm.term_of d|> dest_number) dacc) |
|
23466 | 461 |
| _ => (bacc, aacc, dacc) |
462 |
val (b0,a0,ds) = h p ([],[],[]) |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
463 |
val d = Integer.lcms ds |
69593 | 464 |
val cd = Numeral.mk_cnumber \<^ctyp>\<open>int\<close> d |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
465 |
fun divprop x = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
466 |
let |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
467 |
val th = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
468 |
Simplifier.rewrite (put_simpset lin_ss ctxt) |
69593 | 469 |
(Thm.apply \<^cterm>\<open>Trueprop\<close> |
470 |
(Thm.apply (Thm.apply dvdc (Numeral.mk_cnumber \<^ctyp>\<open>int\<close> x)) cd)) |
|
36945 | 471 |
in Thm.equal_elim (Thm.symmetric th) TrueI end; |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
472 |
val dvd = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
473 |
let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in |
59582 | 474 |
fn ct => the (Inttab.lookup tab (Thm.term_of ct |> dest_number)) |
51930
52fd62618631
prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents:
51717
diff
changeset
|
475 |
handle Option.Option => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
476 |
(writeln ("dvd: Theorems-Table contains no entry for" ^ |
51930
52fd62618631
prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents:
51717
diff
changeset
|
477 |
Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option.Option) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
478 |
end |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
479 |
val dp = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
480 |
let val th = Simplifier.rewrite (put_simpset lin_ss ctxt) |
69593 | 481 |
(Thm.apply \<^cterm>\<open>Trueprop\<close> |
482 |
(Thm.apply (Thm.apply \<^cterm>\<open>(<) :: int => _\<close> \<^cterm>\<open>0::int\<close>) cd)) |
|
36945 | 483 |
in Thm.equal_elim (Thm.symmetric th) TrueI end; |
23466 | 484 |
(* A and B set *) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
485 |
local |
69593 | 486 |
val insI1 = Thm.instantiate' [SOME \<^ctyp>\<open>int\<close>] [] @{thm "insertI1"} |
487 |
val insI2 = Thm.instantiate' [SOME \<^ctyp>\<open>int\<close>] [] @{thm "insertI2"} |
|
23466 | 488 |
in |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
489 |
fun provein x S = |
59582 | 490 |
case Thm.term_of S of |
69593 | 491 |
Const(\<^const_name>\<open>Orderings.bot\<close>, _) => error "Unexpected error in Cooper, please email Amine Chaieb" |
492 |
| Const(\<^const_name>\<open>insert\<close>, _) $ y $ _ => |
|
23466 | 493 |
let val (cy,S') = Thm.dest_binop S |
60801 | 494 |
in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1 |
495 |
else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2) |
|
23466 | 496 |
(provein x S') |
497 |
end |
|
498 |
end |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
499 |
|
59582 | 500 |
val al = map (lint vs o Thm.term_of) a0 |
501 |
val bl = map (lint vs o Thm.term_of) b0 |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
502 |
val (sl,s0,f,abths,cpth) = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
503 |
if length (distinct (op aconv) bl) <= length (distinct (op aconv) al) |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
504 |
then |
23466 | 505 |
(bl,b0,decomp_minf, |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60352
diff
changeset
|
506 |
fn B => (map (fn th => Thm.implies_elim (Thm.instantiate ([],[(B_v,B), (D_v,cd)]) th) dp) |
23466 | 507 |
[bseteq,bsetneq,bsetlt, bsetle, bsetgt,bsetge])@ |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60352
diff
changeset
|
508 |
(map (Thm.instantiate ([],[(B_v,B), (D_v,cd)])) |
23466 | 509 |
[bsetdvd,bsetndvd,bsetP,infDdvd, infDndvd,bsetconj, |
510 |
bsetdisj,infDconj, infDdisj]), |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
511 |
cpmi) |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
512 |
else (al,a0,decomp_pinf,fn A => |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60352
diff
changeset
|
513 |
(map (fn th => Thm.implies_elim (Thm.instantiate ([],[(A_v,A), (D_v,cd)]) th) dp) |
23466 | 514 |
[aseteq,asetneq,asetlt, asetle, asetgt,asetge])@ |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60352
diff
changeset
|
515 |
(map (Thm.instantiate ([],[(A_v,A), (D_v,cd)])) |
23466 | 516 |
[asetdvd,asetndvd, asetP, infDdvd, infDndvd,asetconj, |
517 |
asetdisj,infDconj, infDdisj]),cppi) |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
518 |
val cpth = |
23466 | 519 |
let |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
520 |
val sths = map (fn (tl,t0) => |
59582 | 521 |
if tl = Thm.term_of t0 |
69593 | 522 |
then Thm.instantiate' [SOME \<^ctyp>\<open>int\<close>] [SOME t0] refl |
59582 | 523 |
else provelin ctxt ((HOLogic.eq_const iT)$tl$(Thm.term_of t0) |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
524 |
|> HOLogic.mk_Trueprop)) |
23466 | 525 |
(sl ~~ s0) |
59582 | 526 |
val csl = distinct (op aconvc) (map (Thm.cprop_of #> Thm.dest_arg #> Thm.dest_arg1) sths) |
23466 | 527 |
val S = mkISet csl |
59582 | 528 |
val inStab = fold (fn ct => fn tab => Termtab.update (Thm.term_of ct, provein ct S) tab) |
23466 | 529 |
csl Termtab.empty |
69593 | 530 |
val eqelem_th = Thm.instantiate' [SOME \<^ctyp>\<open>int\<close>] [NONE,NONE, SOME S] eqelem_imp_imp |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
531 |
val inS = |
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
532 |
let |
23466 | 533 |
val tab = fold Termtab.update |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
534 |
(map (fn eq => |
59582 | 535 |
let val (s,t) = Thm.cprop_of eq |> Thm.dest_arg |> Thm.dest_binop |
59848 | 536 |
val th = |
537 |
if s aconvc t |
|
538 |
then the (Termtab.lookup inStab (Thm.term_of s)) |
|
60801 | 539 |
else FWD (Thm.instantiate' [] [SOME s, SOME t] eqelem_th) |
59848 | 540 |
[eq, the (Termtab.lookup inStab (Thm.term_of s))] |
541 |
in (Thm.term_of t, th) end) sths) Termtab.empty |
|
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
542 |
in |
59582 | 543 |
fn ct => the (Termtab.lookup tab (Thm.term_of ct)) |
51930
52fd62618631
prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents:
51717
diff
changeset
|
544 |
handle Option.Option => |
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
545 |
(writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct)); |
51930
52fd62618631
prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents:
51717
diff
changeset
|
546 |
raise Option.Option) |
23466 | 547 |
end |
548 |
val (inf, nb, pd) = divide_and_conquer (f x dvd inS (abths S)) p |
|
549 |
in [dp, inf, nb, pd] MRS cpth |
|
550 |
end |
|
551 |
val cpth' = Thm.transitive uth (cpth RS eq_reflection) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
552 |
in Thm.transitive cpth' ((simp_thms_conv ctxt then_conv eval_conv ctxt) (Thm.rhs_of cpth')) |
23466 | 553 |
end; |
554 |
||
32429
54758ca53fd6
modernized messages -- eliminated old Display.print_cterm;
wenzelm
parents:
32398
diff
changeset
|
555 |
fun literals_conv bops uops env cv = |
23466 | 556 |
let fun h t = |
59582 | 557 |
case Thm.term_of t of |
36797
cb074cec7a30
dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
haftmann
parents:
36717
diff
changeset
|
558 |
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
|
559 |
| u$_ => if member (op aconv) uops u then Conv.arg_conv h t else cv env t |
23466 | 560 |
| _ => cv env t |
561 |
in h end; |
|
562 |
||
563 |
fun integer_nnf_conv ctxt env = |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
564 |
nnf_conv ctxt then_conv literals_conv [HOLogic.conj, HOLogic.disj] [] env (linearize_conv ctxt); |
23466 | 565 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
566 |
val conv_ss = |
69593 | 567 |
simpset_of (put_simpset HOL_basic_ss \<^context> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
568 |
addsimps (@{thms simp_thms} @ take 4 @{thms ex_simps} @ |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
569 |
[not_all, all_not_ex, @{thm ex_disj_distrib}])); |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
570 |
|
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
571 |
fun conv ctxt p = |
61075 | 572 |
Qelim.gen_qelim_conv ctxt |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
573 |
(Simplifier.rewrite (put_simpset conv_ss ctxt)) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
574 |
(Simplifier.rewrite (put_simpset presburger_ss ctxt)) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
575 |
(Simplifier.rewrite (put_simpset conv_ss ctxt)) |
59582 | 576 |
(cons o Thm.term_of) (Misc_Legacy.term_frees (Thm.term_of p)) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
577 |
(linearize_conv ctxt) (integer_nnf_conv ctxt) |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
578 |
(cooperex_conv ctxt) p |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
579 |
handle CTERM _ => raise COOPER "bad cterm" |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
580 |
| THM _ => raise COOPER "bad thm" |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
581 |
| TYPE _ => raise COOPER "bad type" |
23466 | 582 |
|
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
583 |
fun add_bools t = |
36807 | 584 |
let |
69593 | 585 |
val ops = [\<^term>\<open>(=) :: int => _\<close>, \<^term>\<open>(<) :: int => _\<close>, \<^term>\<open>(<=) :: int => _\<close>, |
586 |
\<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>, \<^term>\<open>HOL.implies\<close>, \<^term>\<open>(=) :: bool => _\<close>, |
|
587 |
\<^term>\<open>Not\<close>, \<^term>\<open>All :: (int => _) => _\<close>, |
|
588 |
\<^term>\<open>Ex :: (int => _) => _\<close>, \<^term>\<open>True\<close>, \<^term>\<open>False\<close>]; |
|
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
589 |
val is_op = member (op =) ops; |
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
590 |
val skip = not (fastype_of t = HOLogic.boolT) |
36807 | 591 |
in case t of |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
592 |
(l as f $ a) $ b => if skip orelse is_op f then add_bools b o add_bools l |
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
593 |
else insert (op aconv) t |
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
594 |
| f $ a => if skip orelse is_op f then add_bools a o add_bools f |
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
595 |
else insert (op aconv) t |
42284 | 596 |
| Abs p => add_bools (snd (Syntax_Trans.variant_abs p)) (* FIXME !? *) |
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
597 |
| _ => if skip orelse is_op t then I else insert (op aconv) t |
36807 | 598 |
end; |
599 |
||
36832 | 600 |
fun descend vs (abs as (_, xT, _)) = |
601 |
let |
|
42284 | 602 |
val (xn', p') = Syntax_Trans.variant_abs abs; (* FIXME !? *) |
36833
9628f969d843
represent de-Bruin indices simply by position in list
haftmann
parents:
36832
diff
changeset
|
603 |
in ((xn', xT) :: vs, p') end; |
36832 | 604 |
|
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
605 |
local structure Proc = Cooper_Procedure in |
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
606 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
607 |
fun num_of_term vs (Free vT) = Proc.Bound (Proc.nat_of_integer (find_index (fn vT' => vT' = vT) vs)) |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
608 |
| num_of_term vs (Term.Bound i) = Proc.Bound (Proc.nat_of_integer i) |
69593 | 609 |
| num_of_term vs \<^term>\<open>0::int\<close> = Proc.C (Proc.Int_of_integer 0) |
610 |
| num_of_term vs \<^term>\<open>1::int\<close> = Proc.C (Proc.Int_of_integer 1) |
|
611 |
| num_of_term vs (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) = |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
612 |
Proc.C (Proc.Int_of_integer (dest_number t)) |
69593 | 613 |
| num_of_term vs (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ t') = |
36832 | 614 |
Proc.Neg (num_of_term vs t') |
69593 | 615 |
| num_of_term vs (Const (\<^const_name>\<open>Groups.plus\<close>, _) $ t1 $ t2) = |
36832 | 616 |
Proc.Add (num_of_term vs t1, num_of_term vs t2) |
69593 | 617 |
| num_of_term vs (Const (\<^const_name>\<open>Groups.minus\<close>, _) $ t1 $ t2) = |
36832 | 618 |
Proc.Sub (num_of_term vs t1, num_of_term vs t2) |
69593 | 619 |
| num_of_term vs (Const (\<^const_name>\<open>Groups.times\<close>, _) $ t1 $ t2) = |
36832 | 620 |
(case perhaps_number t1 |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
621 |
of SOME n => Proc.Mul (Proc.Int_of_integer n, num_of_term vs t2) |
36832 | 622 |
| NONE => (case perhaps_number t2 |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
623 |
of SOME n => Proc.Mul (Proc.Int_of_integer n, num_of_term vs t1) |
36832 | 624 |
| NONE => raise COOPER "reification: unsupported kind of multiplication")) |
625 |
| num_of_term _ _ = raise COOPER "reification: bad term"; |
|
23689
0410269099dc
replaced code generator framework for reflected cooper
haftmann
parents:
23582
diff
changeset
|
626 |
|
69593 | 627 |
fun fm_of_term ps vs (Const (\<^const_name>\<open>True\<close>, _)) = Proc.T |
628 |
| fm_of_term ps vs (Const (\<^const_name>\<open>False\<close>, _)) = Proc.F |
|
629 |
| fm_of_term ps vs (Const (\<^const_name>\<open>HOL.conj\<close>, _) $ t1 $ t2) = |
|
36832 | 630 |
Proc.And (fm_of_term ps vs t1, fm_of_term ps vs t2) |
69593 | 631 |
| fm_of_term ps vs (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ t1 $ t2) = |
36832 | 632 |
Proc.Or (fm_of_term ps vs t1, fm_of_term ps vs t2) |
69593 | 633 |
| fm_of_term ps vs (Const (\<^const_name>\<open>HOL.implies\<close>, _) $ t1 $ t2) = |
36832 | 634 |
Proc.Imp (fm_of_term ps vs t1, fm_of_term ps vs t2) |
69593 | 635 |
| fm_of_term ps vs (\<^term>\<open>(=) :: bool => _ \<close> $ t1 $ t2) = |
36832 | 636 |
Proc.Iff (fm_of_term ps vs t1, fm_of_term ps vs t2) |
69593 | 637 |
| fm_of_term ps vs (Const (\<^const_name>\<open>Not\<close>, _) $ t') = |
61128 | 638 |
Proc.NOT (fm_of_term ps vs t') |
69593 | 639 |
| fm_of_term ps vs (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs abs) = |
36832 | 640 |
Proc.E (uncurry (fm_of_term ps) (descend vs abs)) |
69593 | 641 |
| fm_of_term ps vs (Const (\<^const_name>\<open>All\<close>, _) $ Abs abs) = |
36832 | 642 |
Proc.A (uncurry (fm_of_term ps) (descend vs abs)) |
69593 | 643 |
| fm_of_term ps vs (\<^term>\<open>(=) :: int => _\<close> $ t1 $ t2) = |
36832 | 644 |
Proc.Eq (Proc.Sub (num_of_term vs t1, num_of_term vs t2)) |
69593 | 645 |
| fm_of_term ps vs (Const (\<^const_name>\<open>Orderings.less_eq\<close>, _) $ t1 $ t2) = |
36832 | 646 |
Proc.Le (Proc.Sub (num_of_term vs t1, num_of_term vs t2)) |
69593 | 647 |
| fm_of_term ps vs (Const (\<^const_name>\<open>Orderings.less\<close>, _) $ t1 $ t2) = |
36832 | 648 |
Proc.Lt (Proc.Sub (num_of_term vs t1, num_of_term vs t2)) |
69593 | 649 |
| fm_of_term ps vs (Const (\<^const_name>\<open>Rings.dvd\<close>, _) $ t1 $ t2) = |
36832 | 650 |
(case perhaps_number t1 |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
651 |
of SOME n => Proc.Dvd (Proc.Int_of_integer n, num_of_term vs t2) |
36832 | 652 |
| NONE => raise COOPER "reification: unsupported dvd") |
36833
9628f969d843
represent de-Bruin indices simply by position in list
haftmann
parents:
36832
diff
changeset
|
653 |
| fm_of_term ps vs t = let val n = find_index (fn t' => t aconv t') ps |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
654 |
in if n > 0 then Proc.Closed (Proc.nat_of_integer n) else raise COOPER "reification: unknown term" end; |
23466 | 655 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
656 |
fun term_of_num vs (Proc.C i) = HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
657 |
| term_of_num vs (Proc.Bound n) = Free (nth vs (Proc.integer_of_nat n)) |
36832 | 658 |
| term_of_num vs (Proc.Neg t') = |
69593 | 659 |
\<^term>\<open>uminus :: int => _\<close> $ term_of_num vs t' |
36832 | 660 |
| term_of_num vs (Proc.Add (t1, t2)) = |
69593 | 661 |
\<^term>\<open>(+) :: int => _\<close> $ term_of_num vs t1 $ term_of_num vs t2 |
36832 | 662 |
| term_of_num vs (Proc.Sub (t1, t2)) = |
69593 | 663 |
\<^term>\<open>(-) :: int => _\<close> $ term_of_num vs t1 $ term_of_num vs t2 |
36832 | 664 |
| term_of_num vs (Proc.Mul (i, t2)) = |
69593 | 665 |
\<^term>\<open>(*) :: int => _\<close> $ HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t2 |
61128 | 666 |
| term_of_num vs (Proc.CN (n, i, t')) = |
36832 | 667 |
term_of_num vs (Proc.Add (Proc.Mul (i, Proc.Bound n), t')); |
23466 | 668 |
|
69593 | 669 |
fun term_of_fm ps vs Proc.T = \<^term>\<open>True\<close> |
670 |
| term_of_fm ps vs Proc.F = \<^term>\<open>False\<close> |
|
36832 | 671 |
| term_of_fm ps vs (Proc.And (t1, t2)) = HOLogic.conj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 |
672 |
| term_of_fm ps vs (Proc.Or (t1, t2)) = HOLogic.disj $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 |
|
673 |
| term_of_fm ps vs (Proc.Imp (t1, t2)) = HOLogic.imp $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 |
|
69593 | 674 |
| term_of_fm ps vs (Proc.Iff (t1, t2)) = \<^term>\<open>(=) :: bool => _\<close> $ term_of_fm ps vs t1 $ term_of_fm ps vs t2 |
61128 | 675 |
| term_of_fm ps vs (Proc.NOT t') = HOLogic.Not $ term_of_fm ps vs t' |
69593 | 676 |
| term_of_fm ps vs (Proc.Eq t') = \<^term>\<open>(=) :: int => _ \<close> $ term_of_num vs t'$ \<^term>\<open>0::int\<close> |
61128 | 677 |
| term_of_fm ps vs (Proc.NEq t') = term_of_fm ps vs (Proc.NOT (Proc.Eq t')) |
69593 | 678 |
| term_of_fm ps vs (Proc.Lt t') = \<^term>\<open>(<) :: int => _ \<close> $ term_of_num vs t' $ \<^term>\<open>0::int\<close> |
679 |
| term_of_fm ps vs (Proc.Le t') = \<^term>\<open>(<=) :: int => _ \<close> $ term_of_num vs t' $ \<^term>\<open>0::int\<close> |
|
680 |
| term_of_fm ps vs (Proc.Gt t') = \<^term>\<open>(<) :: int => _ \<close> $ \<^term>\<open>0::int\<close> $ term_of_num vs t' |
|
681 |
| term_of_fm ps vs (Proc.Ge t') = \<^term>\<open>(<=) :: int => _ \<close> $ \<^term>\<open>0::int\<close> $ term_of_num vs t' |
|
682 |
| term_of_fm ps vs (Proc.Dvd (i, t')) = \<^term>\<open>(dvd) :: int => _ \<close> $ |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
683 |
HOLogic.mk_number HOLogic.intT (Proc.integer_of_int i) $ term_of_num vs t' |
61128 | 684 |
| term_of_fm ps vs (Proc.NDvd (i, t')) = term_of_fm ps vs (Proc.NOT (Proc.Dvd (i, t'))) |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
50321
diff
changeset
|
685 |
| term_of_fm ps vs (Proc.Closed n) = nth ps (Proc.integer_of_nat n) |
61128 | 686 |
| term_of_fm ps vs (Proc.NClosed n) = term_of_fm ps vs (Proc.NOT (Proc.Closed n)); |
23466 | 687 |
|
36833
9628f969d843
represent de-Bruin indices simply by position in list
haftmann
parents:
36832
diff
changeset
|
688 |
fun procedure t = |
23713 | 689 |
let |
36833
9628f969d843
represent de-Bruin indices simply by position in list
haftmann
parents:
36832
diff
changeset
|
690 |
val vs = Term.add_frees t []; |
9628f969d843
represent de-Bruin indices simply by position in list
haftmann
parents:
36832
diff
changeset
|
691 |
val ps = add_bools t []; |
9628f969d843
represent de-Bruin indices simply by position in list
haftmann
parents:
36832
diff
changeset
|
692 |
in (term_of_fm ps vs o Proc.pa o fm_of_term ps vs) t end; |
23466 | 693 |
|
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
694 |
end; |
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
695 |
|
38808 | 696 |
val (_, oracle) = Context.>>> (Context.map_theory_result |
69593 | 697 |
(Thm.add_oracle (\<^binding>\<open>cooper\<close>, |
38808 | 698 |
(fn (ctxt, t) => |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59586
diff
changeset
|
699 |
(Thm.cterm_of ctxt o Logic.mk_equals o apply2 HOLogic.mk_Trueprop) |
38808 | 700 |
(t, procedure t))))); |
36802 | 701 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
702 |
val comp_ss = |
69593 | 703 |
simpset_of (put_simpset HOL_ss \<^context> addsimps @{thms semiring_norm}); |
36802 | 704 |
|
705 |
fun strip_objimp ct = |
|
706 |
(case Thm.term_of ct of |
|
69593 | 707 |
Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => |
36802 | 708 |
let val (A, B) = Thm.dest_binop ct |
709 |
in A :: strip_objimp B end |
|
710 |
| _ => [ct]); |
|
711 |
||
68632 | 712 |
fun strip_objall ct = |
713 |
case Thm.term_of ct of |
|
69593 | 714 |
Const (\<^const_name>\<open>All\<close>, _) $ Abs (xn,_,_) => |
36802 | 715 |
let val (a,(v,t')) = (apsnd (Thm.dest_abs (SOME xn)) o Thm.dest_comb) ct |
716 |
in apfst (cons (a,v)) (strip_objall t') |
|
717 |
end |
|
718 |
| _ => ([],ct); |
|
719 |
||
720 |
local |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
721 |
val all_maxscope_ss = |
69593 | 722 |
simpset_of (put_simpset HOL_basic_ss \<^context> |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
723 |
addsimps map (fn th => th RS sym) @{thms "all_simps"}) |
36802 | 724 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
725 |
fun thin_prems_tac ctxt P = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
726 |
simp_tac (put_simpset all_maxscope_ss ctxt) THEN' |
36802 | 727 |
CSUBGOAL (fn (p', i) => |
728 |
let |
|
729 |
val (qvs, p) = strip_objall (Thm.dest_arg p') |
|
730 |
val (ps, c) = split_last (strip_objimp p) |
|
731 |
val qs = filter P ps |
|
69593 | 732 |
val q = if P c then c else \<^cterm>\<open>False\<close> |
68632 | 733 |
val ng = fold_rev (fn (a,v) => fn t => Thm.apply a (Thm.lambda v t)) qvs |
69593 | 734 |
(fold_rev (fn p => fn q => Thm.apply (Thm.apply \<^cterm>\<open>HOL.implies\<close> p) q) qs q) |
735 |
val g = Thm.apply (Thm.apply \<^cterm>\<open>(==>)\<close> (Thm.apply \<^cterm>\<open>Trueprop\<close> ng)) p' |
|
736 |
val ntac = (case qs of [] => q aconvc \<^cterm>\<open>False\<close> |
|
36802 | 737 |
| _ => false) |
68632 | 738 |
in |
47476
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
739 |
if ntac then no_tac |
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
740 |
else |
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
741 |
(case try (fn () => |
54883
dd04a8b654fc
proper context for norm_hhf and derived operations;
wenzelm
parents:
54742
diff
changeset
|
742 |
Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) () of |
47476
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
743 |
NONE => no_tac |
60752 | 744 |
| SOME r => resolve_tac ctxt [r] i) |
36802 | 745 |
end) |
23466 | 746 |
end; |
36802 | 747 |
|
748 |
local |
|
68632 | 749 |
fun isnum t = case t of |
69593 | 750 |
Const(\<^const_name>\<open>Groups.zero\<close>,_) => true |
751 |
| Const(\<^const_name>\<open>Groups.one\<close>,_) => true |
|
752 |
| \<^term>\<open>Suc\<close>$s => isnum s |
|
753 |
| \<^term>\<open>nat\<close>$s => isnum s |
|
754 |
| \<^term>\<open>int\<close>$s => isnum s |
|
755 |
| Const(\<^const_name>\<open>Groups.uminus\<close>,_)$s => isnum s |
|
756 |
| Const(\<^const_name>\<open>Groups.plus\<close>,_)$l$r => isnum l andalso isnum r |
|
757 |
| Const(\<^const_name>\<open>Groups.times\<close>,_)$l$r => isnum l andalso isnum r |
|
758 |
| Const(\<^const_name>\<open>Groups.minus\<close>,_)$l$r => isnum l andalso isnum r |
|
759 |
| Const(\<^const_name>\<open>Power.power\<close>,_)$l$r => isnum l andalso isnum r |
|
760 |
| Const(\<^const_name>\<open>Rings.modulo\<close>,_)$l$r => isnum l andalso isnum r |
|
761 |
| Const(\<^const_name>\<open>Rings.divide\<close>,_)$l$r => isnum l andalso isnum r |
|
36831
3037d6810fca
tuned code; toward a tightended interface with generated code
haftmann
parents:
36807
diff
changeset
|
762 |
| _ => is_number t orelse can HOLogic.dest_nat t |
36802 | 763 |
|
68632 | 764 |
fun ty cts t = |
59586 | 765 |
if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (Thm.typ_of_cterm t)) |
68632 | 766 |
then false |
767 |
else case Thm.term_of t of |
|
69593 | 768 |
c$l$r => if member (op =) [\<^term>\<open>(*)::int => _\<close>, \<^term>\<open>(*)::nat => _\<close>] c |
59582 | 769 |
then not (isnum l orelse isnum r) |
770 |
else not (member (op aconv) cts c) |
|
771 |
| c$_ => not (member (op aconv) cts c) |
|
772 |
| c => not (member (op aconv) cts c) |
|
36802 | 773 |
|
774 |
val term_constants = |
|
775 |
let fun h acc t = case t of |
|
776 |
Const _ => insert (op aconv) t acc |
|
777 |
| a$b => h (h acc a) b |
|
778 |
| Abs (_,_,t) => h acc t |
|
779 |
| _ => acc |
|
780 |
in h [] end; |
|
68632 | 781 |
in |
782 |
fun is_relevant ctxt ct = |
|
59582 | 783 |
subset (op aconv) (term_constants (Thm.term_of ct), snd (get ctxt)) |
784 |
andalso |
|
69593 | 785 |
forall (fn Free (_, T) => member (op =) [\<^typ>\<open>int\<close>, \<^typ>\<open>nat\<close>] T) |
59582 | 786 |
(Misc_Legacy.term_frees (Thm.term_of ct)) |
787 |
andalso |
|
69593 | 788 |
forall (fn Var (_, T) => member (op =) [\<^typ>\<open>int\<close>, \<^typ>\<open>nat\<close>] T) |
59582 | 789 |
(Misc_Legacy.term_vars (Thm.term_of ct)); |
36802 | 790 |
|
791 |
fun int_nat_terms ctxt ct = |
|
68632 | 792 |
let |
36802 | 793 |
val cts = snd (get ctxt) |
794 |
fun h acc t = if ty cts t then insert (op aconvc) t acc else |
|
59582 | 795 |
case Thm.term_of t of |
36802 | 796 |
_$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t) |
797 |
| Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc)) |
|
798 |
| _ => acc |
|
799 |
in h [] ct end |
|
800 |
end; |
|
801 |
||
61075 | 802 |
fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st => |
68632 | 803 |
let |
61075 | 804 |
fun all x t = |
805 |
Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t) |
|
67559 | 806 |
val ts = sort Thm.fast_term_ord (f p) |
61075 | 807 |
val p' = fold_rev all ts p |
36945 | 808 |
in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end)); |
36802 | 809 |
|
810 |
local |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
811 |
val ss1 = |
69593 | 812 |
simpset_of (put_simpset comp_ss \<^context> |
68632 | 813 |
addsimps @{thms simp_thms} @ |
814 |
[@{thm "nat_numeral"} RS sym, @{thm int_dvd_int_iff [symmetric]}, @{thm "of_nat_add"}, @{thm "of_nat_mult"}] |
|
62348 | 815 |
@ map (fn r => r RS sym) [@{thm "int_int_eq"}, @{thm "zle_int"}, @{thm "of_nat_less_iff" [where ?'a = int]}] |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
816 |
|> Splitter.add_split @{thm "zdiff_int_split"}) |
36802 | 817 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
818 |
val ss2 = |
69593 | 819 |
simpset_of (put_simpset HOL_basic_ss \<^context> |
62348 | 820 |
addsimps [@{thm "nat_0_le"}, @{thm "of_nat_numeral"}, |
68632 | 821 |
@{thm "all_nat"}, @{thm "ex_nat"}, @{thm "zero_le_numeral"}, |
62348 | 822 |
@{thm "le_numeral_extra"(3)}, @{thm "of_nat_0"}, @{thm "of_nat_1"}, @{thm "Suc_eq_plus1"}] |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
823 |
|> fold Simplifier.add_cong [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
824 |
val div_mod_ss = |
69593 | 825 |
simpset_of (put_simpset HOL_basic_ss \<^context> |
64589 | 826 |
addsimps @{thms simp_thms |
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64589
diff
changeset
|
827 |
mod_eq_0_iff_dvd mod_add_left_eq mod_add_right_eq |
68632 | 828 |
mod_add_eq div_add1_eq [symmetric] div_add1_eq [symmetric] |
64589 | 829 |
mod_self mod_by_0 div_by_0 |
830 |
div_0 mod_0 div_by_1 mod_by_1 |
|
831 |
div_by_Suc_0 mod_by_Suc_0 Suc_eq_plus1 |
|
832 |
ac_simps} |
|
69593 | 833 |
addsimprocs [\<^simproc>\<open>cancel_div_mod_nat\<close>, \<^simproc>\<open>cancel_div_mod_int\<close>]) |
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45196
diff
changeset
|
834 |
val splits_ss = |
69593 | 835 |
simpset_of (put_simpset comp_ss \<^context> |
64243 | 836 |
addsimps [@{thm minus_div_mult_eq_mod [symmetric]}] |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
837 |
|> fold Splitter.add_split |
68632 | 838 |
[@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
839 |
@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}]) |
36802 | 840 |
in |
58820 | 841 |
|
68632 | 842 |
fun nat_to_int_tac ctxt = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
843 |
simp_tac (put_simpset ss1 ctxt) THEN_ALL_NEW |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
844 |
simp_tac (put_simpset ss2 ctxt) THEN_ALL_NEW |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
845 |
simp_tac (put_simpset comp_ss ctxt); |
36802 | 846 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
847 |
fun div_mod_tac ctxt = simp_tac (put_simpset div_mod_ss ctxt); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
848 |
fun splits_tac ctxt = simp_tac (put_simpset splits_ss ctxt); |
58820 | 849 |
|
36802 | 850 |
end; |
851 |
||
36804 | 852 |
fun core_tac ctxt = CSUBGOAL (fn (p, i) => |
36805 | 853 |
let |
68632 | 854 |
val cpth = |
52059 | 855 |
if Config.get ctxt quick_and_dirty |
59582 | 856 |
then oracle (ctxt, Envir.beta_norm (Envir.eta_long [] (Thm.term_of (Thm.dest_arg p)))) |
36804 | 857 |
else Conv.arg_conv (conv ctxt) p |
58820 | 858 |
val p' = Thm.rhs_of cpth |
859 |
val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p')) |
|
60752 | 860 |
in resolve_tac ctxt [th] i end |
36802 | 861 |
handle COOPER _ => no_tac); |
862 |
||
60752 | 863 |
fun finish_tac ctxt q = SUBGOAL (fn (_, i) => |
864 |
(if q then I else TRY) (resolve_tac ctxt [TrueI] i)); |
|
36802 | 865 |
|
47476
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
866 |
fun tac elim add_ths del_ths = Subgoal.FOCUS_PARAMS (fn {context = ctxt, ...} => |
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
867 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
868 |
val simpset_ctxt = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
869 |
put_simpset (fst (get ctxt)) ctxt delsimps del_ths addsimps add_ths |
47476
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
870 |
in |
69593 | 871 |
Method.insert_tac ctxt (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>arith\<close>)) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54489
diff
changeset
|
872 |
THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt |
47476
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
873 |
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
874 |
THEN_ALL_NEW simp_tac simpset_ctxt |
61075 | 875 |
THEN_ALL_NEW (TRY o generalize_tac ctxt (int_nat_terms ctxt)) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54489
diff
changeset
|
876 |
THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt |
47476
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
877 |
THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt)) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54489
diff
changeset
|
878 |
THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt |
47476
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
879 |
THEN_ALL_NEW div_mod_tac ctxt |
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
880 |
THEN_ALL_NEW splits_tac ctxt |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51143
diff
changeset
|
881 |
THEN_ALL_NEW simp_tac simpset_ctxt |
47476
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
882 |
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion |
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
883 |
THEN_ALL_NEW nat_to_int_tac ctxt |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54489
diff
changeset
|
884 |
THEN_ALL_NEW core_tac ctxt |
60752 | 885 |
THEN_ALL_NEW finish_tac ctxt elim |
47476
92d1c566ebbf
refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
wenzelm
parents:
47432
diff
changeset
|
886 |
end 1); |
36802 | 887 |
|
888 |
||
58820 | 889 |
(* attribute syntax *) |
36802 | 890 |
|
891 |
local |
|
892 |
||
893 |
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
|
894 |
||
895 |
val constsN = "consts"; |
|
896 |
val any_keyword = keyword constsN |
|
61476 | 897 |
val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm); |
59582 | 898 |
val terms = thms >> map (Thm.term_of o Drule.dest_term); |
36802 | 899 |
|
900 |
fun optional scan = Scan.optional scan []; |
|
901 |
||
902 |
in |
|
903 |
||
58820 | 904 |
val _ = |
905 |
Theory.setup |
|
69593 | 906 |
(Attrib.setup \<^binding>\<open>presburger\<close> |
58820 | 907 |
((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del || |
908 |
optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm" |
|
59657
2441a80fb6c1
eliminated unused arith "verbose" flag -- tools that need options can use the context;
wenzelm
parents:
59621
diff
changeset
|
909 |
#> Arith_Data.add_tactic "Presburger arithmetic" (tac true [] [])); |
36802 | 910 |
|
911 |
end; |
|
912 |
||
913 |
end; |