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