src/HOL/NatArith.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15404 a9a762f586b5
permissions -rw-r--r--
import -> imports
     1 (*  Title:      HOL/NatArith.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel
     4 *)
     5 
     6 header {* More arithmetic on natural numbers *}
     7 
     8 theory NatArith
     9 imports Nat
    10 files "arith_data.ML"
    11 begin
    12 
    13 setup arith_setup
    14 
    15 
    16 lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)"
    17 by (simp add: less_eq reflcl_trancl [symmetric]
    18             del: reflcl_trancl, arith)
    19 
    20 lemma nat_diff_split:
    21     "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
    22     -- {* elimination of @{text -} on @{text nat} *}
    23   by (cases "a<b" rule: case_split)
    24     (auto simp add: diff_is_0_eq [THEN iffD2])
    25 
    26 lemma nat_diff_split_asm:
    27     "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
    28     -- {* elimination of @{text -} on @{text nat} in assumptions *}
    29   by (simp split: nat_diff_split)
    30 
    31 ML {*
    32  val nat_diff_split = thm "nat_diff_split";
    33  val nat_diff_split_asm = thm "nat_diff_split_asm";
    34 *}
    35 (* Careful: arith_tac produces counter examples!
    36 fun add_arith cs = cs addafter ("arith_tac", arith_tac);
    37 TODO: use arith_tac for force_tac in Provers/clasimp.ML *)
    38 
    39 lemmas [arith_split] = nat_diff_split split_min split_max
    40 
    41 end