src/HOL/ex/Arith_Examples.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 44654 d80fe56788a5 child 46597 7fc239ebece2 permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
1 (*  Title:  HOL/ex/Arith_Examples.thy
2     Author: Tjark Weber
3 *)
5 header {* Arithmetic *}
7 theory Arith_Examples
8 imports Main
9 begin
11 text {*
12   The @{text arith} method is used frequently throughout the Isabelle
13   distribution.  This file merely contains some additional tests and special
14   corner cases.  Some rather technical remarks:
16   @{ML Lin_Arith.simple_tac} is a very basic version of the tactic.  It performs no
17   meta-to-object-logic conversion, and only some splitting of operators.
18   @{ML Lin_Arith.tac} performs meta-to-object-logic conversion, full
19   splitting of operators, and NNF normalization of the goal.  The @{text arith}
20   method combines them both, and tries other methods (e.g.~@{text presburger})
21   as well.  This is the one that you should use in your proofs!
23   An @{text arith}-based simproc is available as well (see @{ML
24   Lin_Arith.simproc}), which---for performance
25   reasons---however does even less splitting than @{ML Lin_Arith.simple_tac}
26   at the moment (namely inequalities only).  (On the other hand, it
27   does take apart conjunctions, which @{ML Lin_Arith.simple_tac} currently
28   does not do.)
29 *}
32 subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
33            @{term minus}, @{term nat}, @{term Divides.mod},
34            @{term Divides.div} *}
36 lemma "(i::nat) <= max i j"
37   by linarith
39 lemma "(i::int) <= max i j"
40   by linarith
42 lemma "min i j <= (i::nat)"
43   by linarith
45 lemma "min i j <= (i::int)"
46   by linarith
48 lemma "min (i::nat) j <= max i j"
49   by linarith
51 lemma "min (i::int) j <= max i j"
52   by linarith
54 lemma "min (i::nat) j + max i j = i + j"
55   by linarith
57 lemma "min (i::int) j + max i j = i + j"
58   by linarith
60 lemma "(i::nat) < j ==> min i j < max i j"
61   by linarith
63 lemma "(i::int) < j ==> min i j < max i j"
64   by linarith
66 lemma "(0::int) <= abs i"
67   by linarith
69 lemma "(i::int) <= abs i"
70   by linarith
72 lemma "abs (abs (i::int)) = abs i"
73   by linarith
75 text {* Also testing subgoals with bound variables. *}
77 lemma "!!x. (x::nat) <= y ==> x - y = 0"
78   by linarith
80 lemma "!!x. (x::nat) - y = 0 ==> x <= y"
81   by linarith
83 lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
84   by linarith
86 lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
87   by linarith
89 lemma "[| (x::nat) < y; d < 1 |] ==> x - y - x = d - x"
90   by linarith
92 lemma "(x::int) < y ==> x - y < 0"
93   by linarith
95 lemma "nat (i + j) <= nat i + nat j"
96   by linarith
98 lemma "i < j ==> nat (i - j) = 0"
99   by linarith
101 lemma "(i::nat) mod 0 = i"
102   (* FIXME: need to replace 0 by its numeral representation *)
103   apply (subst nat_numeral_0_eq_0 [symmetric])
104   by linarith
106 lemma "(i::nat) mod 1 = 0"
107   (* FIXME: need to replace 1 by its numeral representation *)
108   apply (subst nat_numeral_1_eq_1 [symmetric])
109   by linarith
111 lemma "(i::nat) mod 42 <= 41"
112   by linarith
114 lemma "(i::int) mod 0 = i"
115   (* FIXME: need to replace 0 by its numeral representation *)
116   apply (subst numeral_0_eq_0 [symmetric])
117   by linarith
119 lemma "(i::int) mod 1 = 0"
120   (* FIXME: need to replace 1 by its numeral representation *)
121   apply (subst numeral_1_eq_1 [symmetric])
122   (* FIXME: arith does not know about iszero *)
123   apply (tactic {* Lin_Arith.pre_tac @{simpset} 1 *})
124 oops
126 lemma "(i::int) mod 42 <= 41"
127   (* FIXME: arith does not know about iszero *)
128   apply (tactic {* Lin_Arith.pre_tac @{simpset} 1 *})
129 oops
131 lemma "-(i::int) * 1 = 0 ==> i = 0"
132   by linarith
134 lemma "[| (0::int) < abs i; abs i * 1 < abs i * j |] ==> 1 < abs i * j"
135   by linarith
138 subsection {* Meta-Logic *}
140 lemma "x < Suc y == x <= y"
141   by linarith
143 lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
144   by linarith
147 subsection {* Various Other Examples *}
149 lemma "(x < Suc y) = (x <= y)"
150   by linarith
152 lemma "[| (x::nat) < y; y < z |] ==> x < z"
153   by linarith
155 lemma "(x::nat) < y & y < z ==> x < z"
156   by linarith
158 text {* This example involves no arithmetic at all, but is solved by
159   preprocessing (i.e. NNF normalization) alone. *}
161 lemma "(P::bool) = Q ==> Q = P"
162   by linarith
164 lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
165   by linarith
167 lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
168   by linarith
170 lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
171   by linarith
173 lemma "[| (x::nat) > y; y > z; z > x |] ==> False"
174   by linarith
176 lemma "(x::nat) - 5 > y ==> y < x"
177   by linarith
179 lemma "(x::nat) ~= 0 ==> 0 < x"
180   by linarith
182 lemma "[| (x::nat) ~= y; x <= y |] ==> x < y"
183   by linarith
185 lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
186   by linarith
188 lemma "(x - y) - (x::nat) = (x - x) - y"
189   by linarith
191 lemma "[| (a::nat) < b; c < d |] ==> (a - b) = (c - d)"
192   by linarith
194 lemma "((a::nat) - (b - (c - (d - e)))) = (a - (b - (c - (d - e))))"
195   by linarith
197 lemma "(n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) |
198   (n = n' & n' < m) | (n = m & m < n') |
199   (n' < m & m < n) | (n' < m & m = n) |
200   (n' < n & n < m) | (n' = n & n < m) | (n' = m & m < n) |
201   (m < n & n < n') | (m < n & n' = n) | (m < n' & n' < n) |
202   (m = n & n < n') | (m = n' & n' < n) |
203   (n' = m & m = (n::nat))"
204 (* FIXME: this should work in principle, but is extremely slow because     *)
205 (*        preprocessing negates the goal and tries to compute its negation *)
206 (*        normal form, which creates lots of separate cases for this       *)
207 (*        disjunction of conjunctions                                      *)
208 (* by (tactic {* Lin_Arith.tac 1 *}) *)
209 oops
211 lemma "2 * (x::nat) ~= 1"
212 (* FIXME: this is beyond the scope of the decision procedure at the moment, *)
213 (*        because its negation is satisfiable in the rationals?             *)
214 (* by (tactic {* Lin_Arith.simple_tac 1 *}) *)
215 oops
217 text {* Constants. *}
219 lemma "(0::nat) < 1"
220   by linarith
222 lemma "(0::int) < 1"
223   by linarith
225 lemma "(47::nat) + 11 < 08 * 15"
226   by linarith
228 lemma "(47::int) + 11 < 08 * 15"
229   by linarith
231 text {* Splitting of inequalities of different type. *}
233 lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
234   a + b <= nat (max (abs i) (abs j))"
235   by linarith
237 text {* Again, but different order. *}
239 lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
240   a + b <= nat (max (abs i) (abs j))"
241   by linarith
243 end