author | wenzelm |
Thu, 22 Dec 2005 00:28:36 +0100 | |
changeset 18457 | 356a9f711899 |
parent 18394 | fa0674cd6df1 |
child 18708 | 4b3dadb4fe33 |
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 |
|
17985 | 52 |
fun prove_conv expand_tac norm_tac sg ss tu = (* FIXME avoid standard *) |
53 |
mk_meta_eq (standard (Goal.prove sg [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq tu)) |
|
17989 | 54 |
(K (EVERY [expand_tac, norm_tac ss])))); |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
55 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
56 |
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
|
57 |
(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
|
58 |
|
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 |
(* rewriting *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
61 |
|
18328 | 62 |
fun simp_all_tac rules = |
63 |
let val ss0 = HOL_ss addsimps rules |
|
64 |
in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end; |
|
9436
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 |
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
|
67 |
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
|
68 |
|
13517 | 69 |
fun prep_simproc (name, pats, proc) = |
16834 | 70 |
Simplifier.simproc (the_context ()) name pats proc; |
13517 | 71 |
|
72 |
end; |
|
73 |
||
74 |
signature ARITH_DATA = |
|
75 |
sig |
|
76 |
val nat_cancel_sums_add: simproc list |
|
77 |
val nat_cancel_sums: simproc list |
|
78 |
end; |
|
79 |
||
80 |
structure ArithData: ARITH_DATA = |
|
81 |
struct |
|
82 |
||
83 |
open NatArithUtils; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
84 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
85 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
86 |
(** cancel common summands **) |
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 |
structure Sum = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
89 |
struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
90 |
val mk_sum = mk_norm_sum; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
91 |
val dest_sum = dest_sum; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
92 |
val prove_conv = prove_conv; |
18328 | 93 |
val norm_tac1 = simp_all_tac add_rules; |
94 |
val norm_tac2 = simp_all_tac add_ac; |
|
95 |
fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss; |
|
9436
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 |
|
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16485
diff
changeset
|
186 |
fun atomize thm = case #prop(rep_thm thm) of |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16485
diff
changeset
|
187 |
Const("Trueprop",_) $ (Const("op &",_) $ _ $ _) => |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16485
diff
changeset
|
188 |
atomize(thm RS conjunct1) @ atomize(thm RS conjunct2) |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16485
diff
changeset
|
189 |
| _ => [thm]; |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16485
diff
changeset
|
190 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
191 |
fun neg_prop(TP$(Const("Not",_)$t)) = TP$t |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
192 |
| 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
|
193 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
194 |
fun is_False thm = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
195 |
let val _ $ t = #prop(rep_thm thm) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
196 |
in t = Const("False",HOLogic.boolT) end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
197 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
198 |
fun is_nat(t) = fastype_of1 t = HOLogic.natT; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
199 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
200 |
fun mk_nat_thm sg t = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
201 |
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
|
202 |
in instantiate ([],[(cn,ct)]) le0 end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
203 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
204 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
205 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
206 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
207 |
(* arith theory data *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
208 |
|
16424 | 209 |
structure ArithTheoryData = TheoryDataFun |
210 |
(struct |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
211 |
val name = "HOL/arith"; |
15185 | 212 |
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
|
213 |
|
15531 | 214 |
val empty = {splits = [], inj_consts = [], discrete = [], presburger = NONE}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
215 |
val copy = I; |
16424 | 216 |
val extend = I; |
217 |
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
|
218 |
{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
|
219 |
{splits = Drule.merge_rules (splits1, splits2), |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
220 |
inj_consts = merge_lists inj_consts1 inj_consts2, |
15185 | 221 |
discrete = merge_lists discrete1 discrete2, |
15531 | 222 |
presburger = (case presburger1 of NONE => presburger2 | p => p)}; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
223 |
fun print _ _ = (); |
16424 | 224 |
end); |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
225 |
|
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
226 |
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
|
227 |
{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
|
228 |
|
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
229 |
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
|
230 |
{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
|
231 |
|
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
232 |
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
|
233 |
{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
|
234 |
|
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 |
structure LA_Data_Ref: LIN_ARITH_DATA = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
237 |
struct |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
238 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
239 |
(* Decomposition of terms *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
240 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
241 |
fun nT (Type("fun",[N,_])) = N = HOLogic.natT |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
242 |
| nT _ = false; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
243 |
|
17325 | 244 |
fun add_atom(t,m,(p,i)) = (case AList.lookup (op =) p t of NONE => ((t, m) :: p, i) |
17951 | 245 |
| SOME n => (AList.update (op =) (t, Rat.add (n, m)) p, i)); |
10693 | 246 |
|
247 |
exception Zero; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
248 |
|
17951 | 249 |
fun rat_of_term (numt,dent) = |
10693 | 250 |
let val num = HOLogic.dest_binum numt and den = HOLogic.dest_binum dent |
17951 | 251 |
in if den = 0 then raise Zero else Rat.rat_of_quotient (num,den) end; |
10718 | 252 |
|
253 |
(* Warning: in rare cases number_of encloses a non-numeral, |
|
254 |
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
|
255 |
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
|
256 |
although the simplifier should eliminate those anyway... |
10718 | 257 |
*) |
258 |
||
11334
a16eaf2a1edd
Allow Suc-numerals as coefficients in lin-arith formulae
nipkow
parents:
10906
diff
changeset
|
259 |
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
|
260 |
| 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
|
261 |
else raise TERM("number_of_Sucs",[]) |
a16eaf2a1edd
Allow Suc-numerals as coefficients in lin-arith formulae
nipkow
parents:
10906
diff
changeset
|
262 |
|
10718 | 263 |
(* decompose nested multiplications, bracketing them to the right and combining all |
264 |
their coefficients |
|
265 |
*) |
|
266 |
||
13499 | 267 |
fun demult inj_consts = |
268 |
let |
|
10718 | 269 |
fun demult((mC as Const("op *",_)) $ s $ t,m) = ((case s of |
270 |
Const("Numeral.number_of",_)$n |
|
17951 | 271 |
=> demult(t,Rat.mult(m,Rat.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
|
272 |
| Const("uminus",_)$(Const("Numeral.number_of",_)$n) |
17951 | 273 |
=> demult(t,Rat.mult(m,Rat.rat_of_intinf(~(HOLogic.dest_binum n)))) |
11334
a16eaf2a1edd
Allow Suc-numerals as coefficients in lin-arith formulae
nipkow
parents:
10906
diff
changeset
|
274 |
| Const("Suc",_) $ _ |
17951 | 275 |
=> demult(t,Rat.mult(m,Rat.rat_of_int(number_of_Sucs s))) |
10718 | 276 |
| Const("op *",_) $ s1 $ s2 => demult(mC $ s1 $ (mC $ s2 $ t),m) |
277 |
| Const("HOL.divide",_) $ numt $ (Const("Numeral.number_of",_)$dent) => |
|
278 |
let val den = HOLogic.dest_binum dent |
|
279 |
in if den = 0 then raise Zero |
|
17951 | 280 |
else demult(mC $ numt $ t,Rat.mult(m, Rat.inv(Rat.rat_of_intinf den))) |
10718 | 281 |
end |
282 |
| _ => atomult(mC,s,t,m) |
|
283 |
) handle TERM _ => atomult(mC,s,t,m)) |
|
284 |
| demult(atom as Const("HOL.divide",_) $ t $ (Const("Numeral.number_of",_)$dent), m) = |
|
285 |
(let val den = HOLogic.dest_binum dent |
|
17951 | 286 |
in if den = 0 then raise Zero else demult(t,Rat.mult(m, Rat.inv(Rat.rat_of_intinf den))) end |
15531 | 287 |
handle TERM _ => (SOME atom,m)) |
17951 | 288 |
| demult(Const("0",_),m) = (NONE, Rat.rat_of_int 0) |
15531 | 289 |
| demult(Const("1",_),m) = (NONE, m) |
10718 | 290 |
| demult(t as Const("Numeral.number_of",_)$n,m) = |
17951 | 291 |
((NONE,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum n))) |
15531 | 292 |
handle TERM _ => (SOME t,m)) |
17951 | 293 |
| demult(Const("uminus",_)$t, m) = demult(t,Rat.mult(m,Rat.rat_of_int(~1))) |
13499 | 294 |
| demult(t as Const f $ x, m) = |
15531 | 295 |
(if f mem inj_consts then SOME x else SOME t,m) |
296 |
| demult(atom,m) = (SOME atom,m) |
|
10718 | 297 |
|
15531 | 298 |
and atomult(mC,atom,t,m) = (case demult(t,m) of (NONE,m') => (SOME atom,m') |
299 |
| (SOME t',m') => (SOME(mC $ atom $ t'),m')) |
|
13499 | 300 |
in demult end; |
10718 | 301 |
|
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
302 |
fun decomp2 inj_consts (rel,lhs,rhs) = |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
303 |
let |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
304 |
(* Turn term into list of summand * multiplicity plus a constant *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
305 |
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
|
306 |
| poly(all as Const("op -",T) $ s $ t, m, pi) = |
17951 | 307 |
if nT T then add_atom(all,m,pi) else poly(s,m,poly(t,Rat.neg m,pi)) |
15958 | 308 |
| poly(all as Const("uminus",T) $ t, m, pi) = |
17951 | 309 |
if nT T then add_atom(all,m,pi) else poly(t,Rat.neg m,pi) |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
310 |
| poly(Const("0",_), _, pi) = pi |
17951 | 311 |
| poly(Const("1",_), m, (p,i)) = (p,Rat.add(i,m)) |
312 |
| poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,Rat.add(i,m))) |
|
10718 | 313 |
| poly(t as Const("op *",_) $ _ $ _, m, pi as (p,i)) = |
13499 | 314 |
(case demult inj_consts (t,m) of |
17951 | 315 |
(NONE,m') => (p,Rat.add(i,m)) |
15531 | 316 |
| (SOME u,m') => add_atom(u,m',pi)) |
10718 | 317 |
| poly(t as Const("HOL.divide",_) $ _ $ _, m, pi as (p,i)) = |
13499 | 318 |
(case demult inj_consts (t,m) of |
17951 | 319 |
(NONE,m') => (p,Rat.add(i,m')) |
15531 | 320 |
| (SOME u,m') => add_atom(u,m',pi)) |
10718 | 321 |
| poly(all as (Const("Numeral.number_of",_)$t,m,(p,i))) = |
17951 | 322 |
((p,Rat.add(i,Rat.mult(m,Rat.rat_of_intinf(HOLogic.dest_binum t)))) |
10718 | 323 |
handle TERM _ => add_atom all) |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
324 |
| poly(all as Const f $ x, m, pi) = |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
325 |
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
|
326 |
| poly x = add_atom x; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
327 |
|
17951 | 328 |
val (p,i) = poly(lhs,Rat.rat_of_int 1,([],Rat.rat_of_int 0)) |
329 |
and (q,j) = poly(rhs,Rat.rat_of_int 1,([],Rat.rat_of_int 0)) |
|
10693 | 330 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
331 |
in case rel of |
15531 | 332 |
"op <" => SOME(p,i,"<",q,j) |
333 |
| "op <=" => SOME(p,i,"<=",q,j) |
|
334 |
| "op =" => SOME(p,i,"=",q,j) |
|
335 |
| _ => NONE |
|
336 |
end handle Zero => NONE; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
337 |
|
15531 | 338 |
fun negate(SOME(x,i,rel,y,j,d)) = SOME(x,i,"~"^rel,y,j,d) |
339 |
| negate NONE = NONE; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
340 |
|
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
341 |
fun of_lin_arith_sort sg U = |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
342 |
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
|
343 |
|
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
344 |
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
|
345 |
if of_lin_arith_sort sg U |
15185 | 346 |
then (true, D mem discrete) |
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
347 |
else (* special cases *) |
15185 | 348 |
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
|
349 |
| 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
|
350 |
|
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
351 |
fun decomp1 (sg,discrete,inj_consts) (T,xxx) = |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
352 |
(case T of |
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
353 |
Type("fun",[U,_]) => |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
354 |
(case allows_lin_arith sg discrete U of |
15531 | 355 |
(true,d) => (case decomp2 inj_consts xxx of NONE => NONE |
356 |
| SOME(p,i,rel,q,j) => SOME(p,i,rel,q,j,d)) |
|
357 |
| (false,_) => NONE) |
|
358 |
| _ => 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 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
|
361 |
| decomp2 data (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) = |
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
362 |
negate(decomp1 data (T,(rel,lhs,rhs))) |
15531 | 363 |
| decomp2 data _ = NONE |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
364 |
|
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
365 |
fun decomp sg = |
16424 | 366 |
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
|
367 |
in decomp2 (sg,discrete,inj_consts) end |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
368 |
|
16358 | 369 |
fun number_of(n,T) = HOLogic.number_of_const T $ (HOLogic.mk_bin n) |
10693 | 370 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
371 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
372 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
373 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
374 |
structure Fast_Arith = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
375 |
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
|
376 |
|
13499 | 377 |
val fast_arith_tac = Fast_Arith.lin_arith_tac false |
378 |
and fast_ex_arith_tac = Fast_Arith.lin_arith_tac |
|
14517 | 379 |
and trace_arith = Fast_Arith.trace |
380 |
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
|
381 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
382 |
local |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
383 |
|
13902
b41fc9a31975
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
nipkow
parents:
13877
diff
changeset
|
384 |
val isolateSuc = |
b41fc9a31975
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
nipkow
parents:
13877
diff
changeset
|
385 |
let val thy = theory "Nat" |
b41fc9a31975
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
nipkow
parents:
13877
diff
changeset
|
386 |
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
|
387 |
(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
|
388 |
end; |
b41fc9a31975
added isolate_Suc to counteract deficiencies in one of Larry's simprocs.
nipkow
parents:
13877
diff
changeset
|
389 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
390 |
(* reduce contradictory <= to False. |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
391 |
Most of the work is done by the cancel tactics. |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
392 |
*) |
12931
2c0251fada94
solved the problem that Larry's simproce cancle_numerals(?) returns
nipkow
parents:
12480
diff
changeset
|
393 |
val add_rules = |
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14356
diff
changeset
|
394 |
[add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq, |
15184 | 395 |
One_nat_def,isolateSuc, |
17875 | 396 |
order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one, |
16473
b24c820a0b85
moving some generic inequalities from integer arith to nat arith
paulson
parents:
16424
diff
changeset
|
397 |
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
|
398 |
|
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14356
diff
changeset
|
399 |
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
|
400 |
(fn prems => [cut_facts_tac prems 1, |
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14356
diff
changeset
|
401 |
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
|
402 |
["(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
|
403 |
"(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
|
404 |
"(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
|
405 |
"(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
|
406 |
]; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
407 |
|
15121
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
408 |
val mono_ss = simpset() addsimps |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
409 |
[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
|
410 |
|
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
411 |
val add_mono_thms_ordered_field = |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
412 |
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
|
413 |
(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
|
414 |
["(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
|
415 |
"(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
|
416 |
"(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
|
417 |
"(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
|
418 |
"(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
|
419 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
420 |
in |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
421 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
422 |
val init_lin_arith_data = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
423 |
Fast_Arith.setup @ |
15921 | 424 |
[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
|
425 |
{add_mono_thms = add_mono_thms @ |
1198032bad25
Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents:
14738
diff
changeset
|
426 |
add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field, |
10693 | 427 |
mult_mono_thms = mult_mono_thms, |
10574
8f98f0301d67
Linear arithmetic now copes with mixed nat/int formulae.
nipkow
parents:
10516
diff
changeset
|
428 |
inj_thms = inj_thms, |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
429 |
lessD = lessD @ [Suc_leI], |
15923 | 430 |
neqE = [linorder_neqE_nat, |
16485 | 431 |
get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")], |
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset
|
432 |
simpset = HOL_basic_ss addsimps add_rules |
17875 | 433 |
addsimprocs [ab_group_add_cancel.sum_conv, |
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset
|
434 |
ab_group_add_cancel.rel_conv] |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset
|
435 |
(*abel_cancel helps it work in abstract algebraic domains*) |
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15221
diff
changeset
|
436 |
addsimprocs nat_cancel_sums_add}), |
15185 | 437 |
ArithTheoryData.init, arith_discrete "nat"]; |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
438 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
439 |
end; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
440 |
|
13462 | 441 |
val fast_nat_arith_simproc = |
16834 | 442 |
Simplifier.simproc (the_context ()) "fast_nat_arith" |
13462 | 443 |
["(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
|
444 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
445 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
446 |
(* 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
|
447 |
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
|
448 |
*not* themselves (in)equalities, because the latter activate |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
449 |
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
|
450 |
solver all the time rather than add the additional check. *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
451 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
452 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
453 |
(* arith proof method *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
454 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
455 |
(* 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
|
456 |
in case there are lots of irrelevant terms involved; |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
457 |
elimination of min/max can be optimized: |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
458 |
(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
|
459 |
(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
|
460 |
*) |
10516 | 461 |
local |
18394
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
462 |
(* a simpset for computations subject to optimazation !!! *) |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
463 |
(* |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
464 |
val binarith = map thm |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
465 |
["Pls_0_eq", "Min_1_eq", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
466 |
"bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
467 |
"bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
468 |
"bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
469 |
"bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
470 |
"bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
471 |
"bin_add_Pls_right", "bin_add_Min_right"]; |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
472 |
val intarithrel = |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
473 |
(map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
474 |
"int_le_number_of_eq","int_iszero_number_of_0", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
475 |
"int_less_number_of_eq_neg"]) @ |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
476 |
(map (fn s => thm s RS thm "lift_bool") |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
477 |
["int_iszero_number_of_Pls","int_iszero_number_of_1", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
478 |
"int_neg_number_of_Min"])@ |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
479 |
(map (fn s => thm s RS thm "nlift_bool") |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
480 |
["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]); |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
481 |
|
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
482 |
val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
483 |
"int_number_of_diff_sym", "int_number_of_mult_sym"]; |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
484 |
val natarith = map thm ["add_nat_number_of", "diff_nat_number_of", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
485 |
"mult_nat_number_of", "eq_nat_number_of", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
486 |
"less_nat_number_of"] |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
487 |
val powerarith = |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
488 |
(map thm ["nat_number_of", "zpower_number_of_even", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
489 |
"zpower_Pls", "zpower_Min"]) @ |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
490 |
[(Tactic.simplify true [thm "zero_eq_Numeral0_nring", |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
491 |
thm "one_eq_Numeral1_nring"] |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
492 |
(thm "zpower_number_of_odd"))] |
10516 | 493 |
|
18394
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
494 |
val comp_arith = binarith @ intarith @ intarithrel @ natarith |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
495 |
@ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"]; |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
496 |
|
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
497 |
val comp_ss = HOL_basic_ss addsimps comp_arith addsimps simp_thms; |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
498 |
*) |
13499 | 499 |
fun raw_arith_tac ex i st = |
500 |
refute_tac (K true) |
|
16834 | 501 |
(REPEAT o split_tac (#splits (ArithTheoryData.get (Thm.theory_of_thm st)))) |
18394
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
502 |
(* (REPEAT o |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
503 |
(fn i =>(split_tac (#splits (ArithTheoryData.get(Thm.theory_of_thm st))) i) |
fa0674cd6df1
simpset for computation in raw_arith_tac added just as comment, nothing changed!
chaieb
parents:
18328
diff
changeset
|
504 |
THEN (simp_tac comp_ss i))) *) |
14509 | 505 |
((REPEAT_DETERM o etac linorder_neqE) THEN' fast_ex_arith_tac ex) |
506 |
i st; |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
507 |
|
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
508 |
fun presburger_tac i st = |
16834 | 509 |
(case ArithTheoryData.get (Thm.theory_of_thm st) of |
15531 | 510 |
{presburger = SOME tac, ...} => |
16970 | 511 |
(warning "Trying full Presburger arithmetic ..."; tac i st) |
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
512 |
| _ => no_tac st); |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
513 |
|
10516 | 514 |
in |
515 |
||
13877
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
516 |
val simple_arith_tac = FIRST' [fast_arith_tac, |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
517 |
ObjectLogic.atomize_tac THEN' raw_arith_tac true]; |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
518 |
|
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
519 |
val arith_tac = FIRST' [fast_arith_tac, |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
520 |
ObjectLogic.atomize_tac THEN' raw_arith_tac true, |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
521 |
presburger_tac]; |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
522 |
|
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
523 |
val silent_arith_tac = FIRST' [fast_arith_tac, |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
524 |
ObjectLogic.atomize_tac THEN' raw_arith_tac false, |
a6b825ee48d9
Added hook for presburger arithmetic decision procedure.
berghofe
parents:
13517
diff
changeset
|
525 |
presburger_tac]; |
10516 | 526 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
527 |
fun arith_method prems = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
528 |
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
|
529 |
|
10516 | 530 |
end; |
531 |
||
15195 | 532 |
(* antisymmetry: |
15197 | 533 |
combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y |
15195 | 534 |
|
535 |
local |
|
536 |
val antisym = mk_meta_eq order_antisym |
|
537 |
val not_lessD = linorder_not_less RS iffD1 |
|
538 |
fun prp t thm = (#prop(rep_thm thm) = t) |
|
539 |
in |
|
540 |
fun antisym_eq prems thm = |
|
541 |
let |
|
542 |
val r = #prop(rep_thm thm); |
|
543 |
in |
|
544 |
case r of |
|
545 |
Tr $ ((c as Const("op <=",T)) $ s $ t) => |
|
546 |
let val r' = Tr $ (c $ t $ s) |
|
547 |
in |
|
548 |
case Library.find_first (prp r') prems of |
|
15531 | 549 |
NONE => |
16834 | 550 |
let val r' = Tr $ (HOLogic.Not $ (Const("op <",T) $ s $ t)) |
15195 | 551 |
in case Library.find_first (prp r') prems of |
15531 | 552 |
NONE => [] |
553 |
| SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)] |
|
15195 | 554 |
end |
15531 | 555 |
| SOME thm' => [thm' RS (thm RS antisym)] |
15195 | 556 |
end |
557 |
| Tr $ (Const("Not",_) $ (Const("op <",T) $ s $ t)) => |
|
558 |
let val r' = Tr $ (Const("op <=",T) $ s $ t) |
|
559 |
in |
|
560 |
case Library.find_first (prp r') prems of |
|
15531 | 561 |
NONE => |
16834 | 562 |
let val r' = Tr $ (HOLogic.Not $ (Const("op <",T) $ t $ s)) |
15195 | 563 |
in case Library.find_first (prp r') prems of |
15531 | 564 |
NONE => [] |
565 |
| SOME thm' => |
|
15195 | 566 |
[(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)] |
567 |
end |
|
15531 | 568 |
| SOME thm' => [thm' RS ((thm RS not_lessD) RS antisym)] |
15195 | 569 |
end |
570 |
| _ => [] |
|
571 |
end |
|
572 |
handle THM _ => [] |
|
573 |
end; |
|
15197 | 574 |
*) |
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
575 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
576 |
(* theory setup *) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
577 |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
578 |
val arith_setup = |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
579 |
init_lin_arith_data @ |
17875 | 580 |
[fn thy => (Simplifier.change_simpset_of thy (fn ss => ss |
581 |
addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc]) |
|
582 |
addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy), |
|
15221 | 583 |
Method.add_methods |
17875 | 584 |
[("arith", (arith_method o #2) oo Method.syntax Args.bang_facts, |
585 |
"decide linear arithmethic")], |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset
|
586 |
Attrib.add_attributes [("arith_split", |
17875 | 587 |
(Attrib.no_args arith_split_add, |
15221 | 588 |
Attrib.no_args Attrib.undef_local_attribute), |
9893 | 589 |
"declaration of split rules for arithmetic procedure")]]; |