src/HOL/ex/Arith_Examples.thy
author webertj
Sat Jun 02 00:09:02 2007 +0200 (2007-06-02)
changeset 23196 fabf2e8a7ba4
parent 23193 1f2d94b6a8ef
child 23198 174b5f2ec7c1
permissions -rw-r--r--
tracing disabled
     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 "(i::nat) < j ==> min i j < max i j"
    56   by (tactic {* fast_arith_tac 1 *})
    57 
    58 lemma "(i::int) < j ==> min i j < max i j"
    59   by (tactic {* fast_arith_tac 1 *})
    60 
    61 lemma "(0::int) <= abs i"
    62   by (tactic {* fast_arith_tac 1 *})
    63 
    64 lemma "(i::int) <= abs i"
    65   by (tactic {* fast_arith_tac 1 *})
    66 
    67 lemma "abs (abs (i::int)) = abs i"
    68   by (tactic {* fast_arith_tac 1 *})
    69 
    70 text {* Also testing subgoals with bound variables. *}
    71 
    72 lemma "!!x. (x::nat) <= y ==> x - y = 0"
    73   by (tactic {* fast_arith_tac 1 *})
    74 
    75 lemma "!!x. (x::nat) - y = 0 ==> x <= y"
    76   by (tactic {* fast_arith_tac 1 *})
    77 
    78 lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
    79   by (tactic {* simple_arith_tac 1 *})
    80 
    81 lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
    82   by (tactic {* fast_arith_tac 1 *})
    83 
    84 lemma "[| (x::nat) < y; d < 1 |] ==> x - y - x = d - x"
    85   by (tactic {* fast_arith_tac 1 *})
    86 
    87 lemma "(x::int) < y ==> x - y < 0"
    88   by (tactic {* fast_arith_tac 1 *})
    89 
    90 lemma "nat (i + j) <= nat i + nat j"
    91   by (tactic {* fast_arith_tac 1 *})
    92 
    93 lemma "i < j ==> nat (i - j) = 0"
    94   by (tactic {* fast_arith_tac 1 *})
    95 
    96 lemma "(i::nat) mod 0 = i"
    97 oops
    98 
    99 lemma "(i::nat) mod (Suc 0) = 0"
   100 oops
   101 
   102 lemma "(i::nat) div 0 = 0"
   103 oops
   104 
   105 lemma "(i::nat) mod (number_of (1::int)) = 0"
   106 oops
   107 
   108 section {* Meta-Logic *}
   109 
   110 lemma "x < Suc y == x <= y"
   111   by (tactic {* simple_arith_tac 1 *})
   112 
   113 lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
   114   by (tactic {* simple_arith_tac 1 *})
   115 
   116 section {* Various Other Examples *}
   117 
   118 lemma "[| (x::nat) < y; y < z |] ==> x < z"
   119   by (tactic {* fast_arith_tac 1 *})
   120 
   121 lemma "(x::nat) < y & y < z ==> x < z"
   122   by (tactic {* simple_arith_tac 1 *})
   123 
   124 lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
   125   by (tactic {* fast_arith_tac 1 *})
   126 
   127 lemma "[| (x::nat) > y; y > z; z > x |] ==> False"
   128   by (tactic {* fast_arith_tac 1 *})
   129 
   130 lemma "(x::nat) - 5 > y ==> y < x"
   131   by (tactic {* fast_arith_tac 1 *})
   132 
   133 lemma "(x::nat) ~= 0 ==> 0 < x"
   134   by (tactic {* fast_arith_tac 1 *})
   135 
   136 lemma "[| (x::nat) ~= y; x <= y |] ==> x < y"
   137   by (tactic {* fast_arith_tac 1 *})
   138 
   139 lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
   140   by (tactic {* simple_arith_tac 1 *})
   141 
   142 lemma "(x - y) - (x::nat) = (x - x) - y"
   143   by (tactic {* fast_arith_tac 1 *})
   144 
   145 lemma "[| (a::nat) < b; c < d |] ==> (a - b) = (c - d)"
   146   by (tactic {* fast_arith_tac 1 *})
   147 
   148 lemma "((a::nat) - (b - (c - (d - e)))) = (a - (b - (c - (d - e))))"
   149   by (tactic {* fast_arith_tac 1 *})
   150 
   151 text {* Splitting of inequalities of different type. *}
   152 
   153 lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
   154   a + b <= nat (max (abs i) (abs j))"
   155   by (tactic {* fast_arith_tac 1 *})
   156 
   157 lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
   158   a + b <= nat (max (abs i) (abs j))"
   159   by (tactic {* fast_arith_tac 1 *})
   160 
   161 (*
   162 ML {* reset trace_arith; *}
   163 *)
   164 
   165 end