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