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