author  haftmann 
Mon, 11 May 2009 15:57:29 +0200  
changeset 31101  26c7bb764a38 
parent 31100  6a2e67fe4488 
child 34974  18b41bba42b5 
permissions  rwrr 
23193  1 
(* Title: HOL/ex/Arith_Examples.thy 
2 
Author: Tjark Weber 

3 
*) 

4 

23218  5 
header {* Arithmetic *} 
23193  6 

31066  7 
theory Arith_Examples 
8 
imports Main 

9 
begin 

23193  10 

11 
text {* 

23218  12 
The @{text arith} method is used frequently throughout the Isabelle 
23193  13 
distribution. This file merely contains some additional tests and special 
14 
corner cases. Some rather technical remarks: 

15 

31101
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
31100
diff
changeset

16 
@{ML Lin_Arith.simple_tac} is a very basic version of the tactic. It performs no 
23193  17 
metatoobjectlogic conversion, and only some splitting of operators. 
31101
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
31100
diff
changeset

18 
@{ML Lin_Arith.tac} performs metatoobjectlogic conversion, full 
23218  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}) 

23193  21 
as well. This is the one that you should use in your proofs! 
22 

24093  23 
An @{text arith}based simproc is available as well (see @{ML 
31101
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
31100
diff
changeset

24 
Lin_Arith.simproc}), whichfor performance 
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
31100
diff
changeset

25 
reasonshowever does even less splitting than @{ML Lin_Arith.simple_tac} 
24093  26 
at the moment (namely inequalities only). (On the other hand, it 
31101
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
31100
diff
changeset

27 
does take apart conjunctions, which @{ML Lin_Arith.simple_tac} currently 
24093  28 
does not do.) 
23193  29 
*} 
30 

23196  31 
(* 
31082  32 
ML {* set Lin_Arith.trace; *} 
23196  33 
*) 
23193  34 

23218  35 
subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs}, 
23193  36 
@{term HOL.minus}, @{term nat}, @{term Divides.mod}, 
37 
@{term Divides.div} *} 

38 

39 
lemma "(i::nat) <= max i j" 

31066  40 
by linarith 
23193  41 

42 
lemma "(i::int) <= max i j" 

31066  43 
by linarith 
23193  44 

45 
lemma "min i j <= (i::nat)" 

31066  46 
by linarith 
23193  47 

48 
lemma "min i j <= (i::int)" 

31066  49 
by linarith 
23193  50 

51 
lemma "min (i::nat) j <= max i j" 

31066  52 
by linarith 
23193  53 

54 
lemma "min (i::int) j <= max i j" 

31066  55 
by linarith 
23193  56 

23208  57 
lemma "min (i::nat) j + max i j = i + j" 
31066  58 
by linarith 
23208  59 

60 
lemma "min (i::int) j + max i j = i + j" 

31066  61 
by linarith 
23208  62 

23193  63 
lemma "(i::nat) < j ==> min i j < max i j" 
31066  64 
by linarith 
23193  65 

66 
lemma "(i::int) < j ==> min i j < max i j" 

31066  67 
by linarith 
23193  68 

69 
lemma "(0::int) <= abs i" 

31066  70 
by linarith 
23193  71 

72 
lemma "(i::int) <= abs i" 

31066  73 
by linarith 
23193  74 

75 
lemma "abs (abs (i::int)) = abs i" 

31066  76 
by linarith 
23193  77 

78 
text {* Also testing subgoals with bound variables. *} 

79 

80 
lemma "!!x. (x::nat) <= y ==> x  y = 0" 

31066  81 
by linarith 
23193  82 

83 
lemma "!!x. (x::nat)  y = 0 ==> x <= y" 

31066  84 
by linarith 
23193  85 

86 
lemma "!!x. ((x::nat) <= y) = (x  y = 0)" 

31066  87 
by linarith 
23193  88 

89 
lemma "[ (x::nat) < y; d < 1 ] ==> x  y = d" 

31066  90 
by linarith 
23193  91 

92 
lemma "[ (x::nat) < y; d < 1 ] ==> x  y  x = d  x" 

31066  93 
by linarith 
23193  94 

95 
lemma "(x::int) < y ==> x  y < 0" 

31066  96 
by linarith 
23193  97 

98 
lemma "nat (i + j) <= nat i + nat j" 

31066  99 
by linarith 
23193  100 

101 
lemma "i < j ==> nat (i  j) = 0" 

31066  102 
by linarith 
23193  103 

104 
lemma "(i::nat) mod 0 = i" 

23198  105 
(* FIXME: need to replace 0 by its numeral representation *) 
106 
apply (subst nat_numeral_0_eq_0 [symmetric]) 

31066  107 
by linarith 
23198  108 

109 
lemma "(i::nat) mod 1 = 0" 

110 
(* FIXME: need to replace 1 by its numeral representation *) 

111 
apply (subst nat_numeral_1_eq_1 [symmetric]) 

31066  112 
by linarith 
23193  113 

23198  114 
lemma "(i::nat) mod 42 <= 41" 
31066  115 
by linarith 
23198  116 

117 
lemma "(i::int) mod 0 = i" 

118 
(* FIXME: need to replace 0 by its numeral representation *) 

119 
apply (subst numeral_0_eq_0 [symmetric]) 

31066  120 
by linarith 
23198  121 

122 
lemma "(i::int) mod 1 = 0" 

123 
(* FIXME: need to replace 1 by its numeral representation *) 

124 
apply (subst numeral_1_eq_1 [symmetric]) 

125 
(* FIXME: arith does not know about iszero *) 

31100  126 
apply (tactic {* Lin_Arith.pre_tac @{context} 1 *}) 
23193  127 
oops 
128 

23198  129 
lemma "(i::int) mod 42 <= 41" 
130 
(* FIXME: arith does not know about iszero *) 

31100  131 
apply (tactic {* Lin_Arith.pre_tac @{context} 1 *}) 
23193  132 
oops 
133 

24328
83afe527504d
fixed a bug in demult: a in (a * b) is no longer treated as atomic
webertj
parents:
24093
diff
changeset

134 
lemma "(i::int) * 1 = 0 ==> i = 0" 
31066  135 
by linarith 
24328
83afe527504d
fixed a bug in demult: a in (a * b) is no longer treated as atomic
webertj
parents:
24093
diff
changeset

136 

83afe527504d
fixed a bug in demult: a in (a * b) is no longer treated as atomic
webertj
parents:
24093
diff
changeset

137 
lemma "[ (0::int) < abs i; abs i * 1 < abs i * j ] ==> 1 < abs i * j" 
31066  138 
by linarith 
24328
83afe527504d
fixed a bug in demult: a in (a * b) is no longer treated as atomic
webertj
parents:
24093
diff
changeset

139 

23218  140 

141 
subsection {* MetaLogic *} 

23193  142 

143 
lemma "x < Suc y == x <= y" 

31066  144 
by linarith 
23193  145 

146 
lemma "((x::nat) == z ==> x ~= y) ==> x ~= y  z ~= y" 

31066  147 
by linarith 
23193  148 

23218  149 

150 
subsection {* Various Other Examples *} 

23193  151 

23198  152 
lemma "(x < Suc y) = (x <= y)" 
31066  153 
by linarith 
23198  154 

23193  155 
lemma "[ (x::nat) < y; y < z ] ==> x < z" 
31066  156 
by linarith 
23193  157 

158 
lemma "(x::nat) < y & y < z ==> x < z" 

31066  159 
by linarith 
23193  160 

23208  161 
text {* This example involves no arithmetic at all, but is solved by 
162 
preprocessing (i.e. NNF normalization) alone. *} 

163 

164 
lemma "(P::bool) = Q ==> Q = P" 

31066  165 
by linarith 
23208  166 

167 
lemma "[ P = (x = 0); (~P) = (y = 0) ] ==> min (x::nat) y = 0" 

31066  168 
by linarith 
23208  169 

170 
lemma "[ P = (x = 0); (~P) = (y = 0) ] ==> max (x::nat) y = x + y" 

31066  171 
by linarith 
23208  172 

23193  173 
lemma "[ (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b ] ==> False" 
31066  174 
by linarith 
23193  175 

176 
lemma "[ (x::nat) > y; y > z; z > x ] ==> False" 

31066  177 
by linarith 
23193  178 

179 
lemma "(x::nat)  5 > y ==> y < x" 

31066  180 
by linarith 
23193  181 

182 
lemma "(x::nat) ~= 0 ==> 0 < x" 

31066  183 
by linarith 
23193  184 

185 
lemma "[ (x::nat) ~= y; x <= y ] ==> x < y" 

31066  186 
by linarith 
23193  187 

23196  188 
lemma "[ (x::nat) < y; P (x  y) ] ==> P 0" 
31066  189 
by linarith 
23193  190 

191 
lemma "(x  y)  (x::nat) = (x  x)  y" 

31066  192 
by linarith 
23193  193 

194 
lemma "[ (a::nat) < b; c < d ] ==> (a  b) = (c  d)" 

31066  195 
by linarith 
23193  196 

197 
lemma "((a::nat)  (b  (c  (d  e)))) = (a  (b  (c  (d  e))))" 

31066  198 
by linarith 
23193  199 

23198  200 
lemma "(n < m & m < n')  (n < m & m = n')  (n < n' & n' < m)  
201 
(n = n' & n' < m)  (n = m & m < n')  

202 
(n' < m & m < n)  (n' < m & m = n)  

203 
(n' < n & n < m)  (n' = n & n < m)  (n' = m & m < n)  

204 
(m < n & n < n')  (m < n & n' = n)  (m < n' & n' < n)  

205 
(m = n & n < n')  (m = n' & n' < n)  

206 
(n' = m & m = (n::nat))" 

207 
(* FIXME: this should work in principle, but is extremely slow because *) 

208 
(* preprocessing negates the goal and tries to compute its negation *) 

209 
(* normal form, which creates lots of separate cases for this *) 

210 
(* disjunction of conjunctions *) 

31101
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
31100
diff
changeset

211 
(* by (tactic {* Lin_Arith.tac 1 *}) *) 
23198  212 
oops 
213 

214 
lemma "2 * (x::nat) ~= 1" 

23208  215 
(* FIXME: this is beyond the scope of the decision procedure at the moment, *) 
216 
(* because its negation is satisfiable in the rationals? *) 

31101
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
31100
diff
changeset

217 
(* by (tactic {* Lin_Arith.simple_tac 1 *}) *) 
23198  218 
oops 
219 

220 
text {* Constants. *} 

221 

222 
lemma "(0::nat) < 1" 

31066  223 
by linarith 
23198  224 

225 
lemma "(0::int) < 1" 

31066  226 
by linarith 
23198  227 

228 
lemma "(47::nat) + 11 < 08 * 15" 

31066  229 
by linarith 
23198  230 

231 
lemma "(47::int) + 11 < 08 * 15" 

31066  232 
by linarith 
23198  233 

23193  234 
text {* Splitting of inequalities of different type. *} 
235 

236 
lemma "[ (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 ] ==> 

237 
a + b <= nat (max (abs i) (abs j))" 

31066  238 
by linarith 
23193  239 

23198  240 
text {* Again, but different order. *} 
241 

23193  242 
lemma "[ (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 ] ==> 
243 
a + b <= nat (max (abs i) (abs j))" 

31066  244 
by linarith 
23193  245 

23196  246 
(* 
31082  247 
ML {* reset Lin_Arith.trace; *} 
23196  248 
*) 
23193  249 

250 
end 