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