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