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
webertj@23193
     1
(*  Title:  HOL/ex/Arith_Examples.thy
webertj@23193
     2
    Author: Tjark Weber
webertj@23193
     3
*)
webertj@23193
     4
wenzelm@23218
     5
header {* Arithmetic *}
webertj@23193
     6
haftmann@31066
     7
theory Arith_Examples
haftmann@31066
     8
imports Main
haftmann@31066
     9
begin
webertj@23193
    10
webertj@23193
    11
text {*
wenzelm@23218
    12
  The @{text arith} method is used frequently throughout the Isabelle
webertj@23193
    13
  distribution.  This file merely contains some additional tests and special
webertj@23193
    14
  corner cases.  Some rather technical remarks:
webertj@23193
    15
haftmann@31101
    16
  @{ML Lin_Arith.simple_tac} is a very basic version of the tactic.  It performs no
webertj@23193
    17
  meta-to-object-logic conversion, and only some splitting of operators.
haftmann@31101
    18
  @{ML Lin_Arith.tac} performs meta-to-object-logic conversion, full
wenzelm@23218
    19
  splitting of operators, and NNF normalization of the goal.  The @{text arith}
wenzelm@23218
    20
  method combines them both, and tries other methods (e.g.~@{text presburger})
webertj@23193
    21
  as well.  This is the one that you should use in your proofs!
webertj@23193
    22
wenzelm@24093
    23
  An @{text arith}-based simproc is available as well (see @{ML
haftmann@31101
    24
  Lin_Arith.simproc}), which---for performance
haftmann@31101
    25
  reasons---however does even less splitting than @{ML Lin_Arith.simple_tac}
wenzelm@24093
    26
  at the moment (namely inequalities only).  (On the other hand, it
haftmann@31101
    27
  does take apart conjunctions, which @{ML Lin_Arith.simple_tac} currently
wenzelm@24093
    28
  does not do.)
webertj@23193
    29
*}
webertj@23193
    30
webertj@23193
    31
wenzelm@23218
    32
subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
haftmann@35267
    33
           @{term minus}, @{term nat}, @{term Divides.mod},
webertj@23193
    34
           @{term Divides.div} *}
webertj@23193
    35
webertj@23193
    36
lemma "(i::nat) <= max i j"
haftmann@31066
    37
  by linarith
webertj@23193
    38
webertj@23193
    39
lemma "(i::int) <= max i j"
haftmann@31066
    40
  by linarith
webertj@23193
    41
webertj@23193
    42
lemma "min i j <= (i::nat)"
haftmann@31066
    43
  by linarith
webertj@23193
    44
webertj@23193
    45
lemma "min i j <= (i::int)"
haftmann@31066
    46
  by linarith
webertj@23193
    47
webertj@23193
    48
lemma "min (i::nat) j <= max i j"
haftmann@31066
    49
  by linarith
webertj@23193
    50
webertj@23193
    51
lemma "min (i::int) j <= max i j"
haftmann@31066
    52
  by linarith
webertj@23193
    53
webertj@23208
    54
lemma "min (i::nat) j + max i j = i + j"
haftmann@31066
    55
  by linarith
webertj@23208
    56
webertj@23208
    57
lemma "min (i::int) j + max i j = i + j"
haftmann@31066
    58
  by linarith
webertj@23208
    59
webertj@23193
    60
lemma "(i::nat) < j ==> min i j < max i j"
haftmann@31066
    61
  by linarith
webertj@23193
    62
webertj@23193
    63
lemma "(i::int) < j ==> min i j < max i j"
haftmann@31066
    64
  by linarith
webertj@23193
    65
webertj@23193
    66
lemma "(0::int) <= abs i"
haftmann@31066
    67
  by linarith
webertj@23193
    68
webertj@23193
    69
lemma "(i::int) <= abs i"
haftmann@31066
    70
  by linarith
webertj@23193
    71
webertj@23193
    72
lemma "abs (abs (i::int)) = abs i"
haftmann@31066
    73
  by linarith
webertj@23193
    74
webertj@23193
    75
text {* Also testing subgoals with bound variables. *}
webertj@23193
    76
webertj@23193
    77
lemma "!!x. (x::nat) <= y ==> x - y = 0"
haftmann@31066
    78
  by linarith
webertj@23193
    79
webertj@23193
    80
lemma "!!x. (x::nat) - y = 0 ==> x <= y"
haftmann@31066
    81
  by linarith
webertj@23193
    82
webertj@23193
    83
lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
haftmann@31066
    84
  by linarith
webertj@23193
    85
webertj@23193
    86
lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
haftmann@31066
    87
  by linarith
webertj@23193
    88
webertj@23193
    89
lemma "[| (x::nat) < y; d < 1 |] ==> x - y - x = d - x"
haftmann@31066
    90
  by linarith
webertj@23193
    91
webertj@23193
    92
lemma "(x::int) < y ==> x - y < 0"
haftmann@31066
    93
  by linarith
webertj@23193
    94
webertj@23193
    95
lemma "nat (i + j) <= nat i + nat j"
haftmann@31066
    96
  by linarith
webertj@23193
    97
webertj@23193
    98
lemma "i < j ==> nat (i - j) = 0"
haftmann@31066
    99
  by linarith
webertj@23193
   100
webertj@23193
   101
lemma "(i::nat) mod 0 = i"
webertj@23198
   102
  (* FIXME: need to replace 0 by its numeral representation *)
webertj@23198
   103
  apply (subst nat_numeral_0_eq_0 [symmetric])
haftmann@31066
   104
  by linarith
webertj@23198
   105
webertj@23198
   106
lemma "(i::nat) mod 1 = 0"
webertj@23198
   107
  (* FIXME: need to replace 1 by its numeral representation *)
webertj@23198
   108
  apply (subst nat_numeral_1_eq_1 [symmetric])
haftmann@31066
   109
  by linarith
webertj@23193
   110
webertj@23198
   111
lemma "(i::nat) mod 42 <= 41"
haftmann@31066
   112
  by linarith
webertj@23198
   113
webertj@23198
   114
lemma "(i::int) mod 0 = i"
webertj@23198
   115
  (* FIXME: need to replace 0 by its numeral representation *)
webertj@23198
   116
  apply (subst numeral_0_eq_0 [symmetric])
haftmann@31066
   117
  by linarith
webertj@23198
   118
webertj@23198
   119
lemma "(i::int) mod 1 = 0"
webertj@23198
   120
  (* FIXME: need to replace 1 by its numeral representation *)
webertj@23198
   121
  apply (subst numeral_1_eq_1 [symmetric])
webertj@23198
   122
  (* FIXME: arith does not know about iszero *)
wenzelm@35230
   123
  apply (tactic {* Lin_Arith.pre_tac @{simpset} 1 *})
webertj@23193
   124
oops
webertj@23193
   125
webertj@23198
   126
lemma "(i::int) mod 42 <= 41"
webertj@23198
   127
  (* FIXME: arith does not know about iszero *)
wenzelm@35230
   128
  apply (tactic {* Lin_Arith.pre_tac @{simpset} 1 *})
webertj@23193
   129
oops
webertj@23193
   130
webertj@24328
   131
lemma "-(i::int) * 1 = 0 ==> i = 0"
haftmann@31066
   132
  by linarith
webertj@24328
   133
webertj@24328
   134
lemma "[| (0::int) < abs i; abs i * 1 < abs i * j |] ==> 1 < abs i * j"
haftmann@31066
   135
  by linarith
webertj@24328
   136
wenzelm@23218
   137
wenzelm@23218
   138
subsection {* Meta-Logic *}
webertj@23193
   139
webertj@23193
   140
lemma "x < Suc y == x <= y"
haftmann@31066
   141
  by linarith
webertj@23193
   142
webertj@23193
   143
lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
haftmann@31066
   144
  by linarith
webertj@23193
   145
wenzelm@23218
   146
wenzelm@23218
   147
subsection {* Various Other Examples *}
webertj@23193
   148
webertj@23198
   149
lemma "(x < Suc y) = (x <= y)"
haftmann@31066
   150
  by linarith
webertj@23198
   151
webertj@23193
   152
lemma "[| (x::nat) < y; y < z |] ==> x < z"
haftmann@31066
   153
  by linarith
webertj@23193
   154
webertj@23193
   155
lemma "(x::nat) < y & y < z ==> x < z"
haftmann@31066
   156
  by linarith
webertj@23193
   157
webertj@23208
   158
text {* This example involves no arithmetic at all, but is solved by
webertj@23208
   159
  preprocessing (i.e. NNF normalization) alone. *}
webertj@23208
   160
webertj@23208
   161
lemma "(P::bool) = Q ==> Q = P"
haftmann@31066
   162
  by linarith
webertj@23208
   163
webertj@23208
   164
lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
haftmann@31066
   165
  by linarith
webertj@23208
   166
webertj@23208
   167
lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
haftmann@31066
   168
  by linarith
webertj@23208
   169
webertj@23193
   170
lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
haftmann@31066
   171
  by linarith
webertj@23193
   172
webertj@23193
   173
lemma "[| (x::nat) > y; y > z; z > x |] ==> False"
haftmann@31066
   174
  by linarith
webertj@23193
   175
webertj@23193
   176
lemma "(x::nat) - 5 > y ==> y < x"
haftmann@31066
   177
  by linarith
webertj@23193
   178
webertj@23193
   179
lemma "(x::nat) ~= 0 ==> 0 < x"
haftmann@31066
   180
  by linarith
webertj@23193
   181
webertj@23193
   182
lemma "[| (x::nat) ~= y; x <= y |] ==> x < y"
haftmann@31066
   183
  by linarith
webertj@23193
   184
webertj@23196
   185
lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
haftmann@31066
   186
  by linarith
webertj@23193
   187
webertj@23193
   188
lemma "(x - y) - (x::nat) = (x - x) - y"
haftmann@31066
   189
  by linarith
webertj@23193
   190
webertj@23193
   191
lemma "[| (a::nat) < b; c < d |] ==> (a - b) = (c - d)"
haftmann@31066
   192
  by linarith
webertj@23193
   193
webertj@23193
   194
lemma "((a::nat) - (b - (c - (d - e)))) = (a - (b - (c - (d - e))))"
haftmann@31066
   195
  by linarith
webertj@23193
   196
webertj@23198
   197
lemma "(n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) |
webertj@23198
   198
  (n = n' & n' < m) | (n = m & m < n') |
webertj@23198
   199
  (n' < m & m < n) | (n' < m & m = n) |
webertj@23198
   200
  (n' < n & n < m) | (n' = n & n < m) | (n' = m & m < n) |
webertj@23198
   201
  (m < n & n < n') | (m < n & n' = n) | (m < n' & n' < n) |
webertj@23198
   202
  (m = n & n < n') | (m = n' & n' < n) |
webertj@23198
   203
  (n' = m & m = (n::nat))"
webertj@23198
   204
(* FIXME: this should work in principle, but is extremely slow because     *)
webertj@23198
   205
(*        preprocessing negates the goal and tries to compute its negation *)
webertj@23198
   206
(*        normal form, which creates lots of separate cases for this       *)
webertj@23198
   207
(*        disjunction of conjunctions                                      *)
haftmann@31101
   208
(* by (tactic {* Lin_Arith.tac 1 *}) *)
webertj@23198
   209
oops
webertj@23198
   210
webertj@23198
   211
lemma "2 * (x::nat) ~= 1"
webertj@23208
   212
(* FIXME: this is beyond the scope of the decision procedure at the moment, *)
webertj@23208
   213
(*        because its negation is satisfiable in the rationals?             *)
haftmann@31101
   214
(* by (tactic {* Lin_Arith.simple_tac 1 *}) *)
webertj@23198
   215
oops
webertj@23198
   216
webertj@23198
   217
text {* Constants. *}
webertj@23198
   218
webertj@23198
   219
lemma "(0::nat) < 1"
haftmann@31066
   220
  by linarith
webertj@23198
   221
webertj@23198
   222
lemma "(0::int) < 1"
haftmann@31066
   223
  by linarith
webertj@23198
   224
webertj@23198
   225
lemma "(47::nat) + 11 < 08 * 15"
haftmann@31066
   226
  by linarith
webertj@23198
   227
webertj@23198
   228
lemma "(47::int) + 11 < 08 * 15"
haftmann@31066
   229
  by linarith
webertj@23198
   230
webertj@23193
   231
text {* Splitting of inequalities of different type. *}
webertj@23193
   232
webertj@23193
   233
lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
webertj@23193
   234
  a + b <= nat (max (abs i) (abs j))"
haftmann@31066
   235
  by linarith
webertj@23193
   236
webertj@23198
   237
text {* Again, but different order. *}
webertj@23198
   238
webertj@23193
   239
lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
webertj@23193
   240
  a + b <= nat (max (abs i) (abs j))"
haftmann@31066
   241
  by linarith
webertj@23193
   242
webertj@23193
   243
end