src/HOL/NatArith.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 14607 099575a938e5
child 15041 a6b1f0cef7b3
permissions -rw-r--r--
Merged in license change from Isabelle2004
nipkow@10214
     1
(*  Title:      HOL/NatArith.thy
nipkow@10214
     2
    ID:         $Id$
wenzelm@13297
     3
    Author:     Tobias Nipkow and Markus Wenzel
wenzelm@13297
     4
*)
nipkow@10214
     5
wenzelm@13297
     6
header {* More arithmetic on natural numbers *}
nipkow@10214
     7
nipkow@10214
     8
theory NatArith = Nat
nipkow@10214
     9
files "arith_data.ML":
nipkow@10214
    10
nipkow@10214
    11
setup arith_setup
nipkow@10214
    12
wenzelm@13297
    13
wenzelm@11655
    14
lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)"
paulson@14208
    15
by (simp add: less_eq reflcl_trancl [symmetric]
paulson@14208
    16
            del: reflcl_trancl, arith)
paulson@11454
    17
nipkow@10214
    18
lemma nat_diff_split:
paulson@10599
    19
    "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
wenzelm@13297
    20
    -- {* elimination of @{text -} on @{text nat} *}
wenzelm@13297
    21
  by (cases "a<b" rule: case_split)
wenzelm@13297
    22
    (auto simp add: diff_is_0_eq [THEN iffD2])
paulson@11324
    23
paulson@11324
    24
lemma nat_diff_split_asm:
paulson@11324
    25
    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
wenzelm@13297
    26
    -- {* elimination of @{text -} on @{text nat} in assumptions *}
paulson@11324
    27
  by (simp split: nat_diff_split)
nipkow@10214
    28
oheimb@11164
    29
ML {*
oheimb@11164
    30
 val nat_diff_split = thm "nat_diff_split";
paulson@11324
    31
 val nat_diff_split_asm = thm "nat_diff_split_asm";
nipkow@13499
    32
*}
nipkow@13499
    33
(* Careful: arith_tac produces counter examples!
oheimb@11181
    34
fun add_arith cs = cs addafter ("arith_tac", arith_tac);
wenzelm@14607
    35
TODO: use arith_tac for force_tac in Provers/clasimp.ML *)
nipkow@10214
    36
nipkow@10214
    37
lemmas [arith_split] = nat_diff_split split_min split_max
nipkow@10214
    38
oheimb@11164
    39
wenzelm@14607
    40
subsection {* Generic summation indexed over natural numbers *}
wenzelm@13297
    41
wenzelm@13297
    42
consts
wenzelm@13297
    43
  Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
wenzelm@13297
    44
primrec
wenzelm@13297
    45
  "Summation f 0 = 0"
wenzelm@13297
    46
  "Summation f (Suc n) = Summation f n + f n"
wenzelm@13297
    47
wenzelm@13297
    48
syntax
wenzelm@13297
    49
  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
wenzelm@13297
    50
translations
wenzelm@13297
    51
  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
wenzelm@13297
    52
wenzelm@13297
    53
theorem Summation_step:
wenzelm@13297
    54
    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
wenzelm@13297
    55
  by (induct n) simp_all
wenzelm@13297
    56
nipkow@10214
    57
end