author | wenzelm |
Mon, 20 Jun 2005 22:13:58 +0200 | |
changeset 16485 | 77ae3bfa8b76 |
parent 16473 | b24c820a0b85 |
child 16733 | 236dfafbeb63 |
permissions | -rw-r--r-- |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/arith_data.ML |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, Stefan Berghofer and Tobias Nipkow |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
4 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
5 |
Various arithmetic proof procedures. |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
6 |
*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
7 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
8 |
(*---------------------------------------------------------------------------*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
9 |
(* 1. Cancellation of common terms *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
10 |
(*---------------------------------------------------------------------------*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
11 |
|
13517 | 12 |
structure NatArithUtils = |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
13 |
struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
14 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
15 |
(** abstract syntax of structure nat: 0, Suc, + **) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
16 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
17 |
(* mk_sum, mk_norm_sum *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
18 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
19 |
val one = HOLogic.mk_nat 1; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
20 |
val mk_plus = HOLogic.mk_binop "op +"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
21 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
22 |
fun mk_sum [] = HOLogic.zero |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
23 |
| mk_sum [t] = t |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
24 |
| mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
25 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
26 |
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
27 |
fun mk_norm_sum ts = |
15570 | 28 |
let val (ones, sums) = List.partition (equal one) ts in |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
29 |
funpow (length ones) HOLogic.mk_Suc (mk_sum sums) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
30 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
31 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
32 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
33 |
(* dest_sum *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
34 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
35 |
val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
36 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
37 |
fun dest_sum tm = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
38 |
if HOLogic.is_zero tm then [] |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
39 |
else |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
40 |
(case try HOLogic.dest_Suc tm of |
15531 | 41 |
SOME t => one :: dest_sum t |
42 |
| NONE => |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
43 |
(case try dest_plus tm of |
15531 | 44 |
SOME (t, u) => dest_sum t @ dest_sum u |
45 |
| NONE => [tm])); |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
46 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
47 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
48 |
(** generic proof tools **) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
49 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
50 |
(* prove conversions *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
51 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
52 |
val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
53 |
|
13517 | 54 |
fun prove_conv expand_tac norm_tac sg tu = |
55 |
mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu)) |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
56 |
(K [expand_tac, norm_tac])) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
57 |
handle ERROR => error ("The error(s) above occurred while trying to prove " ^ |
13517 | 58 |
(string_of_cterm (cterm_of sg (mk_eqv tu)))); |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
59 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
60 |
val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s" |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
61 |
(fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
62 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
63 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
64 |
(* rewriting *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
65 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
66 |
fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules)); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
67 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
68 |
val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right]; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
69 |
val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right]; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
70 |
|
13517 | 71 |
fun prep_simproc (name, pats, proc) = |
72 |
Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc; |
|
73 |
||
74 |
end; |
|
75 |
||
76 |
signature ARITH_DATA = |
|
77 |
sig |
|
78 |
val nat_cancel_sums_add: simproc list |
|
79 |
val nat_cancel_sums: simproc list |
|
80 |
end; |
|
81 |
||
82 |
structure ArithData: ARITH_DATA = |
|
83 |
struct |
|
84 |
||
85 |
open NatArithUtils; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
86 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
87 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
88 |
(** cancel common summands **) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
89 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
90 |
structure Sum = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
91 |
struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
92 |
val mk_sum = mk_norm_sum; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
93 |
val dest_sum = dest_sum; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
94 |
val prove_conv = prove_conv; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
95 |
val norm_tac = simp_all add_rules THEN simp_all add_ac; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
96 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
97 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
98 |
fun gen_uncancel_tac rule ct = |
15531 | 99 |
rtac (instantiate' [] [NONE, SOME ct] (rule RS subst_equals)) 1; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
100 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
101 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
102 |
(* nat eq *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
103 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
104 |
structure EqCancelSums = CancelSumsFun |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
105 |
(struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
106 |
open Sum; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
107 |
val mk_bal = HOLogic.mk_eq; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
108 |
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT; |
14331 | 109 |
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
110 |
end); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
111 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
112 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
113 |
(* nat less *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
114 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
115 |
structure LessCancelSums = CancelSumsFun |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
116 |
(struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
117 |
open Sum; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
118 |
val mk_bal = HOLogic.mk_binrel "op <"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
119 |
val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT; |
14331 | 120 |
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
121 |
end); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
122 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
123 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
124 |
(* nat le *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
125 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
126 |
structure LeCancelSums = CancelSumsFun |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
127 |
(struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
128 |
open Sum; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
129 |
val mk_bal = HOLogic.mk_binrel "op <="; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
130 |
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT; |
14331 | 131 |
val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
132 |
end); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
133 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
134 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
135 |
(* nat diff *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
136 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
137 |
structure DiffCancelSums = CancelSumsFun |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
138 |
(struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
139 |
open Sum; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
140 |
val mk_bal = HOLogic.mk_binop "op -"; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
141 |
val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
142 |
val uncancel_tac = gen_uncancel_tac diff_cancel; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
143 |
end); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
144 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
145 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
146 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
147 |
(** prepare nat_cancel simprocs **) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
148 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
149 |
val nat_cancel_sums_add = map prep_simproc |
13462 | 150 |
[("nateq_cancel_sums", |
151 |
["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], EqCancelSums.proc), |
|
152 |
("natless_cancel_sums", |
|
153 |
["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"], LessCancelSums.proc), |
|
154 |
("natle_cancel_sums", |
|
155 |
["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"], LeCancelSums.proc)]; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
156 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
157 |
val nat_cancel_sums = nat_cancel_sums_add @ |
13462 | 158 |
[prep_simproc ("natdiff_cancel_sums", |
159 |
["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], DiffCancelSums.proc)]; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
160 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
161 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
162 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
163 |
open ArithData; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
164 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
165 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
166 |
(*---------------------------------------------------------------------------*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
167 |
(* 2. Linear arithmetic *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
168 |
(*---------------------------------------------------------------------------*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
169 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
170 |
(* Parameters data for general linear arithmetic functor *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
171 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
172 |
structure LA_Logic: LIN_ARITH_LOGIC = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
173 |
struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
174 |
val ccontr = ccontr; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
175 |
val conjI = conjI; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
176 |
val notI = notI; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
177 |
val sym = sym; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
178 |
val not_lessD = linorder_not_less RS iffD1; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
179 |
val not_leD = linorder_not_le RS iffD1; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
180 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
181 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
182 |
fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
183 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
184 |
val mk_Trueprop = HOLogic.mk_Trueprop; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
185 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
186 |
fun neg_prop(TP$(Const("Not",_)$t)) = TP$t |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
187 |
| neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
188 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
189 |
fun is_False thm = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
190 |
let val _ $ t = #prop(rep_thm thm) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
191 |
in t = Const("False",HOLogic.boolT) end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
192 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
193 |
fun is_nat(t) = fastype_of1 t = HOLogic.natT; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
194 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
195 |
fun mk_nat_thm sg t = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
196 |
let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT)) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
197 |
in instantiate ([],[(cn,ct)]) le0 end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
198 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
199 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
200 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
201 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
202 |
(* arith theory data *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
203 |
|
16424 | 204 |
structure ArithTheoryData = TheoryDataFun |
205 |
(struct |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
206 |
val name = "HOL/arith"; |
15185 | 207 |
type T = {splits: thm list, inj_consts: (string * typ)list, discrete: string list, presburger: (int -> tactic) option}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
208 |
|
15531 | 209 |
val empty = {splits = [], inj_consts = [], discrete = [], presburger = NONE}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
210 |
val copy = I; |
16424 | 211 |
val extend = I; |
212 |
fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, presburger= presburger1}, |
|
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
213 |
{splits= splits2, inj_consts= inj_consts2, discrete= discrete2, presburger= presburger2}) = |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
214 |
{splits = Drule.merge_rules (splits1, splits2), |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
215 |
inj_consts = merge_lists inj_consts1 inj_consts2, |
15185 | 216 |
discrete = merge_lists discrete1 discrete2, |
15531 | 217 |
presburger = (case presburger1 of NONE => presburger2 | p => p)}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
218 |
fun print _ _ = (); |
16424 | 219 |
end); |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
220 |
|
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
221 |
fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} => |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
222 |
{splits= thm::splits, inj_consts= inj_consts, discrete= discrete, presburger= presburger}) thy, thm); |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
223 |
|
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
224 |
fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} => |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
225 |
{splits = splits, inj_consts = inj_consts, discrete = d :: discrete, presburger= presburger}); |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
226 |
|
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
227 |
fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,presburger} => |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
228 |
{splits = splits, inj_consts = c :: inj_consts, discrete = discrete, presburger = presburger}); |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
229 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
230 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
231 |
structure LA_Data_Ref: LIN_ARITH_DATA = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
232 |
struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
233 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
234 |
(* Decomposition of terms *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
235 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
236 |
fun nT (Type("fun",[N,_])) = N = HOLogic.natT |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
237 |
| nT _ = false; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
238 |
|
15531 | 239 |
fun add_atom(t,m,(p,i)) = (case assoc(p,t) of NONE => ((t,m)::p,i) |
240 |
| SOME n => (overwrite(p,(t,ratadd(n,m))), i)); |
|
10693 | 241 |
|
242 |
exception Zero; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
243 |
|
10693 | 244 |
fun rat_of_term(numt,dent) = |
245 |
let val num = HOLogic.dest_binum numt and den = HOLogic.dest_binum dent |
|
246 |
in if den = 0 then raise Zero else int_ratdiv(num,den) end; |
|
10718 | 247 |
|
248 |
(* Warning: in rare cases number_of encloses a non-numeral, |
|
249 |
in which case dest_binum raises TERM; hence all the handles below. |
|
11334
a16eaf2a1edd
Allow Suc-numerals as coefficients in lin-arith formulae
nipkow
parents:
10906
diff
changeset
|
250 |
Same for Suc-terms that turn out not to be numerals - |
a16eaf2a1edd
Allow Suc-numerals as coefficients in lin-arith formulae
nipkow
parents:
10906
diff
changeset
|
251 |
although the simplifier should eliminate those anyway... |
10718 | 252 |
*) |
253 |
||
11334
a16eaf2a1edd
Allow Suc-numerals as coefficients in lin-arith formulae
nipkow
parents:
10906
diff
changeset
|
254 |
fun number_of_Sucs (Const("Suc",_) $ n) = number_of_Sucs n + 1 |
a16eaf2a1edd
Allow Suc-numerals as coefficients in lin-arith formulae
nipkow
parents:
10906
diff
changeset
|
255 |
| number_of_Sucs t = if HOLogic.is_zero t then 0 |
a16eaf2a1edd
Allow Suc-numerals as coefficients in lin-arith formulae
nipkow
parents:
10906
diff
changeset
|
256 |
else raise TERM("number_of_Sucs",[]) |
a16eaf2a1edd
Allow Suc-numerals as coefficients in lin-arith formulae
nipkow
parents:
10906
diff
changeset
|
257 |
|
10718 | 258 |
(* decompose nested multiplications, bracketing them to the right and combining all |
259 |
their coefficients |
|
260 |
*) |
|
261 |
||
13499 | 262 |
fun demult inj_consts = |
263 |
let |
|
10718 | 264 |
fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of |
265 |
Const("Numeral.number_of",_)$n |
|
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15958
diff
changeset
|
266 |
=> demult(t,ratmul(m,rat_of_intinf(HOLogic.dest_binum n))) |
12480
32e67277a4b9
tuned conversion from terms to "polynomials" for arith_tac: takes care
nipkow
parents:
12338
diff
changeset
|
267 |
| Const("uminus",_)$(Const("Numeral.number_of",_)$n) |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15958
diff
changeset
|
268 |
=> demult(t,ratmul(m,rat_of_intinf(~(HOLogic.dest_binum n)))) |
11334
a16eaf2a1edd
Allow Suc-numerals as coefficients in lin-arith formulae
nipkow
parents:
10906
diff
changeset
|
269 |
| Const("Suc",_) $ _ |
a16eaf2a1edd
Allow Suc-numerals as coefficients in lin-arith formulae
nipkow
parents:
10906
diff
changeset
|
270 |
=> demult(t,ratmul(m,rat_of_int(number_of_Sucs s))) |
10718 | 271 |
| Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m) |
272 |
| Const("HOL.divide",_) $ numt $ (Const("Numeral.number_of",_)$dent) => |
|
273 |
let val den = HOLogic.dest_binum dent |
|
274 |
in if den = 0 then raise Zero |
|
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15958
diff
changeset
|
275 |
else demult(mC $ numt $ t,ratmul(m, ratinv(rat_of_intinf den))) |
10718 | 276 |
end |
277 |
| _ => atomult(mC,s,t,m) |
|
278 |
) handle TERM _ => atomult(mC,s,t,m)) |
|
279 |
| demult(atom as Const("HOL.divide",_) $ t $ (Const("Numeral.number_of",_)$dent), m) = |
|
280 |
(let val den = HOLogic.dest_binum dent |
|
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15958
diff
changeset
|
281 |
in if den = 0 then raise Zero else demult(t,ratmul(m, ratinv(rat_of_intinf den))) end |
15531 | 282 |
handle TERM _ => (SOME atom,m)) |
283 |
| demult(Const("0",_),m) = (NONE, rat_of_int 0) |
|
284 |
| demult(Const("1",_),m) = (NONE, m) |
|
10718 | 285 |
| demult(t as Const("Numeral.number_of",_)$n,m) = |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15958
diff
changeset
|
286 |
((NONE,ratmul(m,rat_of_intinf(HOLogic.dest_binum n))) |
15531 | 287 |
handle TERM _ => (SOME t,m)) |
12480
32e67277a4b9
tuned conversion from terms to "polynomials" for arith_tac: takes care
nipkow
parents:
12338
diff
changeset
|
288 |
| demult(Const("uminus",_)$t, m) = demult(t,ratmul(m,rat_of_int(~1))) |
13499 | 289 |
| demult(t as Const f $ x, m) = |
15531 | 290 |
(if f mem inj_consts then SOME x else SOME t,m) |
291 |
| demult(atom,m) = (SOME atom,m) |
|
10718 | 292 |
|
15531 | 293 |
and atomult(mC,atom,t,m) = (case demult(t,m) of (NONE,m') => (SOME atom,m') |
294 |
| (SOME t',m') => (SOME(mC $ atom $ t'),m')) |
|
13499 | 295 |
in demult end; |
10718 | 296 |
|
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
297 |
fun decomp2 inj_consts (rel,lhs,rhs) = |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
298 |
let |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
299 |
(* Turn term into list of summand * multiplicity plus a constant *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
300 |
fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
301 |
| poly(all as Const("op -",T) $ s $ t, m, pi) = |
15958 | 302 |
if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,ratneg m,pi)) |
303 |
| poly(all as Const("uminus",T) $ t, m, pi) = |
|
304 |
if nT T then add_atom(all,m,pi) else poly(t,ratneg m,pi) |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
305 |
| poly(Const("0",_), _, pi) = pi |
11464 | 306 |
| poly(Const("1",_), m, (p,i)) = (p,ratadd(i,m)) |
10693 | 307 |
| poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,ratadd(i,m))) |
10718 | 308 |
| poly(t as Const("op *",_) $ _ $ _, m, pi as (p,i)) = |
13499 | 309 |
(case demult inj_consts (t,m) of |
15531 | 310 |
(NONE,m') => (p,ratadd(i,m)) |
311 |
| (SOME u,m') => add_atom(u,m',pi)) |
|
10718 | 312 |
| poly(t as Const("HOL.divide",_) $ _ $ _, m, pi as (p,i)) = |
13499 | 313 |
(case demult inj_consts (t,m) of |
15531 | 314 |
(NONE,m') => (p,ratadd(i,m')) |
315 |
| (SOME u,m') => add_atom(u,m',pi)) |
|
10718 | 316 |
| poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) = |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15958
diff
changeset
|
317 |
((p,ratadd(i,ratmul(m,rat_of_intinf(HOLogic.dest_binum t)))) |
10718 | 318 |
handle TERM _ => add_atom all) |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
319 |
| poly(all as Const f $ x, m, pi) = |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
320 |
if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi) |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
321 |
| poly x = add_atom x; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
322 |
|
10718 | 323 |
val (p,i) = poly(lhs,rat_of_int 1,([],rat_of_int 0)) |
324 |
and (q,j) = poly(rhs,rat_of_int 1,([],rat_of_int 0)) |
|
10693 | 325 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
326 |
in case rel of |
15531 | 327 |
"op <" => SOME(p,i,"<",q,j) |
328 |
| "op <=" => SOME(p,i,"<=",q,j) |
|
329 |
| "op =" => SOME(p,i,"=",q,j) |
|
330 |
| _ => NONE |
|
331 |
end handle Zero => NONE; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
332 |
|
15531 | 333 |
fun negate(SOME(x,i,rel,y,j,d)) = SOME(x,i,"~"^rel,y,j,d) |
334 |
| negate NONE = NONE; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
335 |
|
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
336 |
fun of_lin_arith_sort sg U = |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
337 |
Type.of_sort (Sign.tsig_of sg) (U,["Ring_and_Field.ordered_idom"]) |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
338 |
|
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
339 |
fun allows_lin_arith sg discrete (U as Type(D,[])) = |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
340 |
if of_lin_arith_sort sg U |
15185 | 341 |
then (true, D mem discrete) |
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
342 |
else (* special cases *) |
15185 | 343 |
if D mem discrete then (true,true) else (false,false) |
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
344 |
| allows_lin_arith sg discrete U = (of_lin_arith_sort sg U, false); |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
345 |
|
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
346 |
fun decomp1 (sg,discrete,inj_consts) (T,xxx) = |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
347 |
(case T of |
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
348 |
Type("fun",[U,_]) => |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
349 |
(case allows_lin_arith sg discrete U of |
15531 | 350 |
(true,d) => (case decomp2 inj_consts xxx of NONE => NONE |
351 |
| SOME(p,i,rel,q,j) => SOME(p,i,rel,q,j,d)) |
|
352 |
| (false,_) => NONE) |
|
353 |
| _ => NONE); |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
354 |
|
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
355 |
fun decomp2 data (_$(Const(rel,T)$lhs$rhs)) = decomp1 data (T,(rel,lhs,rhs)) |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
356 |
| decomp2 data (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) = |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
357 |
negate(decomp1 data (T,(rel,lhs,rhs))) |
15531 | 358 |
| decomp2 data _ = NONE |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
359 |
|
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
360 |
fun decomp sg = |
16424 | 361 |
let val {discrete, inj_consts, ...} = ArithTheoryData.get sg |
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
362 |
in decomp2 (sg,discrete,inj_consts) end |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
363 |
|
16358 | 364 |
fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n) |
10693 | 365 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
366 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
367 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
368 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
369 |
structure Fast_Arith = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
370 |
Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
371 |
|
13499 | 372 |
val fast_arith_tac = Fast_Arith.lin_arith_tac false |
373 |
and fast_ex_arith_tac = Fast_Arith.lin_arith_tac |
|
14517 | 374 |
and trace_arith = Fast_Arith.trace |
375 |
and fast_arith_neq_limit = Fast_Arith.fast_arith_neq_limit; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
376 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
377 |
local |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
378 |
|
13902
b41fc9a31975
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
nipkow
parents:
13877
diff
changeset
|
379 |
val isolateSuc = |
b41fc9a31975
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
nipkow
parents:
13877
diff
changeset
|
380 |
let val thy = theory "Nat" |
b41fc9a31975
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
nipkow
parents:
13877
diff
changeset
|
381 |
in prove_goal thy "Suc(i+j) = i+j + Suc 0" |
b41fc9a31975
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
nipkow
parents:
13877
diff
changeset
|
382 |
(fn _ => [simp_tac (simpset_of thy) 1]) |
b41fc9a31975
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
nipkow
parents:
13877
diff
changeset
|
383 |
end; |
b41fc9a31975
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
nipkow
parents:
13877
diff
changeset
|
384 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
385 |
(* reduce contradictory <= to False. |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
386 |
Most of the work is done by the cancel tactics. |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
387 |
*) |
12931
2c0251fada94
solved the problem that Larry's simproce cancle_numerals(?) returns
nipkow
parents:
12480
diff
changeset
|
388 |
val add_rules = |
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14356
diff
changeset
|
389 |
[add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, |
15184 | 390 |
One_nat_def,isolateSuc, |
16473
b24c820a0b85
moving some generic inequalities from integer arith to nat arith
paulson
parents:
16424
diff
changeset
|
391 |
order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one, |
b24c820a0b85
moving some generic inequalities from integer arith to nat arith
paulson
parents:
16424
diff
changeset
|
392 |
zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero]; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
393 |
|
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14356
diff
changeset
|
394 |
val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
395 |
(fn prems => [cut_facts_tac prems 1, |
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14356
diff
changeset
|
396 |
blast_tac (claset() addIs [add_mono]) 1])) |
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
397 |
["(i <= j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)", |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
398 |
"(i = j) & (k <= l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)", |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
399 |
"(i <= j) & (k = l) ==> i + k <= j + (l::'a::pordered_ab_semigroup_add)", |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
400 |
"(i = j) & (k = l) ==> i + k = j + (l::'a::pordered_ab_semigroup_add)" |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
401 |
]; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
402 |
|
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
403 |
val mono_ss = simpset() addsimps |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
404 |
[add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono]; |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
405 |
|
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
406 |
val add_mono_thms_ordered_field = |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
407 |
map (fn s => prove_goal (the_context ()) s |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
408 |
(fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1])) |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
409 |
["(i<j) & (k=l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)", |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
410 |
"(i=j) & (k<l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)", |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
411 |
"(i<j) & (k<=l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)", |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
412 |
"(i<=j) & (k<l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)", |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
413 |
"(i<j) & (k<l) ==> i+k < j+(l::'a::pordered_cancel_ab_semigroup_add)"]; |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
414 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
415 |
in |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
416 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
417 |
val init_lin_arith_data = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
418 |
Fast_Arith.setup @ |
15921 | 419 |
[Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} => |
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
420 |
{add_mono_thms = add_mono_thms @ |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
421 |
add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field, |
10693 | 422 |
mult_mono_thms = mult_mono_thms, |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
423 |
inj_thms = inj_thms, |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
424 |
lessD = lessD @ [Suc_leI], |
15923 | 425 |
neqE = [linorder_neqE_nat, |
16485 | 426 |
get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")], |
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset
|
427 |
simpset = HOL_basic_ss addsimps add_rules |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset
|
428 |
addsimprocs [ab_group_add_cancel.sum_conv, |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset
|
429 |
ab_group_add_cancel.rel_conv] |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset
|
430 |
(*abel_cancel helps it work in abstract algebraic domains*) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset
|
431 |
addsimprocs nat_cancel_sums_add}), |
15185 | 432 |
ArithTheoryData.init, arith_discrete "nat"]; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
433 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
434 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
435 |
|
13462 | 436 |
val fast_nat_arith_simproc = |
437 |
Simplifier.simproc (Theory.sign_of (the_context ())) "fast_nat_arith" |
|
438 |
["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] Fast_Arith.lin_arith_prover; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
439 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
440 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
441 |
(* Because of fast_nat_arith_simproc, the arithmetic solver is really only |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
442 |
useful to detect inconsistencies among the premises for subgoals which are |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
443 |
*not* themselves (in)equalities, because the latter activate |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
444 |
fast_nat_arith_simproc anyway. However, it seems cheaper to activate the |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
445 |
solver all the time rather than add the additional check. *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
446 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
447 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
448 |
(* arith proof method *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
449 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
450 |
(* FIXME: K true should be replaced by a sensible test to speed things up |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
451 |
in case there are lots of irrelevant terms involved; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
452 |
elimination of min/max can be optimized: |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
453 |
(max m n + k <= r) = (m+k <= r & n+k <= r) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
454 |
(l <= min m n + k) = (l <= m+k & l <= n+k) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
455 |
*) |
10516 | 456 |
local |
457 |
||
13499 | 458 |
fun raw_arith_tac ex i st = |
459 |
refute_tac (K true) |
|
16424 | 460 |
(REPEAT o split_tac (#splits (ArithTheoryData.get (Thm.sign_of_thm st)))) |
14509 | 461 |
((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex) |
462 |
i st; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
463 |
|
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
464 |
fun presburger_tac i st = |
16424 | 465 |
(case ArithTheoryData.get (sign_of_thm st) of |
15531 | 466 |
{presburger = SOME tac, ...} => |
16485 | 467 |
(warning "Simple arithmetic decision procedure failed, trying full Presburger arithmetic..."; tac i st) |
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
468 |
| _ => no_tac st); |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
469 |
|
10516 | 470 |
in |
471 |
||
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
472 |
val simple_arith_tac = FIRST' [fast_arith_tac, |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
473 |
ObjectLogic.atomize_tac THEN' raw_arith_tac true]; |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
474 |
|
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
475 |
val arith_tac = FIRST' [fast_arith_tac, |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
476 |
ObjectLogic.atomize_tac THEN' raw_arith_tac true, |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
477 |
presburger_tac]; |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
478 |
|
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
479 |
val silent_arith_tac = FIRST' [fast_arith_tac, |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
480 |
ObjectLogic.atomize_tac THEN' raw_arith_tac false, |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
481 |
presburger_tac]; |
10516 | 482 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
483 |
fun arith_method prems = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
484 |
Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac)); |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
485 |
|
10516 | 486 |
end; |
487 |
||
15195 | 488 |
(* antisymmetry: |
15197 | 489 |
combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y |
15195 | 490 |
|
491 |
local |
|
492 |
val antisym = mk_meta_eq order_antisym |
|
493 |
val not_lessD = linorder_not_less RS iffD1 |
|
494 |
fun prp t thm = (#prop(rep_thm thm) = t) |
|
495 |
in |
|
496 |
fun antisym_eq prems thm = |
|
497 |
let |
|
498 |
val r = #prop(rep_thm thm); |
|
499 |
in |
|
500 |
case r of |
|
501 |
Tr $ ((c as Const("op <=",T)) $ s $ t) => |
|
502 |
let val r' = Tr $ (c $ t $ s) |
|
503 |
in |
|
504 |
case Library.find_first (prp r') prems of |
|
15531 | 505 |
NONE => |
15195 | 506 |
let val r' = Tr $ (HOLogic.not_const $ (Const("op <",T) $ s $ t)) |
507 |
in case Library.find_first (prp r') prems of |
|
15531 | 508 |
NONE => [] |
509 |
| SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)] |
|
15195 | 510 |
end |
15531 | 511 |
| SOME thm' => [thm' RS (thm RS antisym)] |
15195 | 512 |
end |
513 |
| Tr $ (Const("Not",_) $ (Const("op <",T) $ s $ t)) => |
|
514 |
let val r' = Tr $ (Const("op <=",T) $ s $ t) |
|
515 |
in |
|
516 |
case Library.find_first (prp r') prems of |
|
15531 | 517 |
NONE => |
15195 | 518 |
let val r' = Tr $ (HOLogic.not_const $ (Const("op <",T) $ t $ s)) |
519 |
in case Library.find_first (prp r') prems of |
|
15531 | 520 |
NONE => [] |
521 |
| SOME thm' => |
|
15195 | 522 |
[(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)] |
523 |
end |
|
15531 | 524 |
| SOME thm' => [thm' RS ((thm RS not_lessD) RS antisym)] |
15195 | 525 |
end |
526 |
| _ => [] |
|
527 |
end |
|
528 |
handle THM _ => [] |
|
529 |
end; |
|
15197 | 530 |
*) |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
531 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
532 |
(* theory setup *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
533 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
534 |
val arith_setup = |
15197 | 535 |
[Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @ |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
536 |
init_lin_arith_data @ |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
537 |
[Simplifier.change_simpset_of (op addSolver) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
538 |
(mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac), |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
539 |
Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc], |
15221 | 540 |
Method.add_methods |
541 |
[("arith", (arith_method o #2) oo Method.syntax Args.bang_facts, |
|
542 |
"decide linear arithmethic")], |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
543 |
Attrib.add_attributes [("arith_split", |
15221 | 544 |
(Attrib.no_args arith_split_add, |
545 |
Attrib.no_args Attrib.undef_local_attribute), |
|
9893 | 546 |
"declaration of split rules for arithmetic procedure")]]; |