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