src/HOL/ex/Arith_Examples.thy
author webertj
Fri Jun 01 23:21:40 2007 +0200 (2007-06-01)
changeset 23193 1f2d94b6a8ef
child 23196 fabf2e8a7ba4
permissions -rw-r--r--
some tests for arith added
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
webertj@23193
    15
  {\tt 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.
webertj@23193
    17
  {\tt 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
webertj@23193
    22
  An {\tt arith}-based simproc is available as well (see {\tt
webertj@23193
    23
  Fast_Arith.lin_arith_prover}), which---for performance reasons---however
webertj@23193
    24
  does even less splitting than {\tt fast_arith_tac} at the moment (namely
webertj@23193
    25
  inequalities only).  (On the other hand, it does take apart conjunctions,
webertj@23193
    26
  which {\tt fast_arith_tac} currently does not do.)
webertj@23193
    27
*}
webertj@23193
    28
webertj@23193
    29
ML {* set trace_arith; *}
webertj@23193
    30
webertj@23193
    31
section {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
webertj@23193
    32
           @{term HOL.minus}, @{term nat}, @{term Divides.mod},
webertj@23193
    33
           @{term Divides.div} *}
webertj@23193
    34
webertj@23193
    35
lemma "(i::nat) <= max i j"
webertj@23193
    36
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    37
webertj@23193
    38
lemma "(i::int) <= max i j"
webertj@23193
    39
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    40
webertj@23193
    41
lemma "min i j <= (i::nat)"
webertj@23193
    42
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    43
webertj@23193
    44
lemma "min i j <= (i::int)"
webertj@23193
    45
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    46
webertj@23193
    47
lemma "min (i::nat) j <= max i j"
webertj@23193
    48
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    49
webertj@23193
    50
lemma "min (i::int) j <= max i j"
webertj@23193
    51
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    52
webertj@23193
    53
lemma "(i::nat) < j ==> min i j < max i j"
webertj@23193
    54
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    55
webertj@23193
    56
lemma "(i::int) < j ==> min i j < max i j"
webertj@23193
    57
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    58
webertj@23193
    59
lemma "(0::int) <= abs i"
webertj@23193
    60
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    61
webertj@23193
    62
lemma "(i::int) <= abs i"
webertj@23193
    63
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    64
webertj@23193
    65
lemma "abs (abs (i::int)) = abs i"
webertj@23193
    66
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    67
webertj@23193
    68
text {* Also testing subgoals with bound variables. *}
webertj@23193
    69
webertj@23193
    70
lemma "!!x. (x::nat) <= y ==> x - y = 0"
webertj@23193
    71
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    72
webertj@23193
    73
lemma "!!x. (x::nat) - y = 0 ==> x <= y"
webertj@23193
    74
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    75
webertj@23193
    76
lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
webertj@23193
    77
  by (tactic {* simple_arith_tac 1 *})
webertj@23193
    78
webertj@23193
    79
lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
webertj@23193
    80
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    81
webertj@23193
    82
lemma "[| (x::nat) < y; d < 1 |] ==> x - y - x = d - x"
webertj@23193
    83
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    84
webertj@23193
    85
lemma "(x::int) < y ==> x - y < 0"
webertj@23193
    86
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    87
webertj@23193
    88
lemma "nat (i + j) <= nat i + nat j"
webertj@23193
    89
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    90
webertj@23193
    91
lemma "i < j ==> nat (i - j) = 0"
webertj@23193
    92
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
    93
webertj@23193
    94
lemma "(i::nat) mod 0 = i"
webertj@23193
    95
oops
webertj@23193
    96
webertj@23193
    97
lemma "(i::nat) mod (Suc 0) = 0"
webertj@23193
    98
oops
webertj@23193
    99
webertj@23193
   100
lemma "(i::nat) div 0 = 0"
webertj@23193
   101
oops
webertj@23193
   102
webertj@23193
   103
ML {* (#splits (ArithTheoryData.get (the_context ()))); *}
webertj@23193
   104
webertj@23193
   105
lemma "(i::nat) mod (number_of (1::int)) = 0"
webertj@23193
   106
oops
webertj@23193
   107
webertj@23193
   108
section {* Meta-Logic *}
webertj@23193
   109
webertj@23193
   110
lemma "x < Suc y == x <= y"
webertj@23193
   111
  by (tactic {* simple_arith_tac 1 *})
webertj@23193
   112
webertj@23193
   113
lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
webertj@23193
   114
  by (tactic {* simple_arith_tac 1 *})
webertj@23193
   115
webertj@23193
   116
section {* Other Examples *}
webertj@23193
   117
webertj@23193
   118
lemma "[| (x::nat) < y; y < z |] ==> x < z"
webertj@23193
   119
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
   120
webertj@23193
   121
lemma "(x::nat) < y & y < z ==> x < z"
webertj@23193
   122
  by (tactic {* simple_arith_tac 1 *})
webertj@23193
   123
webertj@23193
   124
lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
webertj@23193
   125
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
   126
webertj@23193
   127
lemma "[| (x::nat) > y; y > z; z > x |] ==> False"
webertj@23193
   128
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
   129
webertj@23193
   130
lemma "(x::nat) - 5 > y ==> y < x"
webertj@23193
   131
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
   132
webertj@23193
   133
lemma "(x::nat) ~= 0 ==> 0 < x"
webertj@23193
   134
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
   135
webertj@23193
   136
lemma "[| (x::nat) ~= y; x <= y |] ==> x < y"
webertj@23193
   137
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
   138
webertj@23193
   139
lemma "(x::nat) < y \<longrightarrow> P (x - y) \<longrightarrow> P 0"
webertj@23193
   140
  by (tactic {* simple_arith_tac 1 *})
webertj@23193
   141
webertj@23193
   142
lemma "(x - y) - (x::nat) = (x - x) - y"
webertj@23193
   143
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
   144
webertj@23193
   145
lemma "[| (a::nat) < b; c < d |] ==> (a - b) = (c - d)"
webertj@23193
   146
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
   147
webertj@23193
   148
lemma "((a::nat) - (b - (c - (d - e)))) = (a - (b - (c - (d - e))))"
webertj@23193
   149
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
   150
webertj@23193
   151
text {* Splitting of inequalities of different type. *}
webertj@23193
   152
webertj@23193
   153
lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
webertj@23193
   154
  a + b <= nat (max (abs i) (abs j))"
webertj@23193
   155
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
   156
webertj@23193
   157
lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
webertj@23193
   158
  a + b <= nat (max (abs i) (abs j))"
webertj@23193
   159
  by (tactic {* fast_arith_tac 1 *})
webertj@23193
   160
webertj@23193
   161
ML {* reset trace_arith; *}
webertj@23193
   162
webertj@23193
   163
end