src/HOL/NatArith.thy
author wenzelm
Fri, 16 Apr 2004 21:00:36 +0200
changeset 14607 099575a938e5
parent 14208 144f45277d5a
child 14981 e73f8140af78
permissions -rw-r--r--
tuned document;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/NatArith.thy
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
13297
wenzelm
parents: 11655
diff changeset
     3
    Author:     Tobias Nipkow and Markus Wenzel
wenzelm
parents: 11655
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm
parents: 11655
diff changeset
     5
*)
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     6
13297
wenzelm
parents: 11655
diff changeset
     7
header {* More arithmetic on natural numbers *}
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     8
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     9
theory NatArith = Nat
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    10
files "arith_data.ML":
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    11
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    12
setup arith_setup
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    13
13297
wenzelm
parents: 11655
diff changeset
    14
11655
923e4d0d36d5 tuned parentheses in relational expressions;
wenzelm
parents: 11454
diff changeset
    15
lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)"
14208
144f45277d5a misc tidying
paulson
parents: 13499
diff changeset
    16
by (simp add: less_eq reflcl_trancl [symmetric]
144f45277d5a misc tidying
paulson
parents: 13499
diff changeset
    17
            del: reflcl_trancl, arith)
11454
7514e5e21cb8 Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents: 11324
diff changeset
    18
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    19
lemma nat_diff_split:
10599
2df753cf86e9 miniscoping of nat_diff_split
paulson
parents: 10214
diff changeset
    20
    "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
13297
wenzelm
parents: 11655
diff changeset
    21
    -- {* elimination of @{text -} on @{text nat} *}
wenzelm
parents: 11655
diff changeset
    22
  by (cases "a<b" rule: case_split)
wenzelm
parents: 11655
diff changeset
    23
    (auto simp add: diff_is_0_eq [THEN iffD2])
11324
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    24
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    25
lemma nat_diff_split_asm:
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    26
    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
13297
wenzelm
parents: 11655
diff changeset
    27
    -- {* elimination of @{text -} on @{text nat} in assumptions *}
11324
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    28
  by (simp split: nat_diff_split)
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    29
11164
03f5dc539fd9 added add_arith (just as hint by now)
oheimb
parents: 10599
diff changeset
    30
ML {*
03f5dc539fd9 added add_arith (just as hint by now)
oheimb
parents: 10599
diff changeset
    31
 val nat_diff_split = thm "nat_diff_split";
11324
82406bd816a5 nat_diff_split_asm, for the assumptions
paulson
parents: 11181
diff changeset
    32
 val nat_diff_split_asm = thm "nat_diff_split_asm";
13499
f95f5818f24f Counter example generation mods.
nipkow
parents: 13297
diff changeset
    33
*}
f95f5818f24f Counter example generation mods.
nipkow
parents: 13297
diff changeset
    34
(* Careful: arith_tac produces counter examples!
11181
d04f57b91166 renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents: 11164
diff changeset
    35
fun add_arith cs = cs addafter ("arith_tac", arith_tac);
14607
099575a938e5 tuned document;
wenzelm
parents: 14208
diff changeset
    36
TODO: use arith_tac for force_tac in Provers/clasimp.ML *)
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    37
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    38
lemmas [arith_split] = nat_diff_split split_min split_max
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    39
11164
03f5dc539fd9 added add_arith (just as hint by now)
oheimb
parents: 10599
diff changeset
    40
14607
099575a938e5 tuned document;
wenzelm
parents: 14208
diff changeset
    41
subsection {* Generic summation indexed over natural numbers *}
13297
wenzelm
parents: 11655
diff changeset
    42
wenzelm
parents: 11655
diff changeset
    43
consts
wenzelm
parents: 11655
diff changeset
    44
  Summation :: "(nat => 'a::{zero, plus}) => nat => 'a"
wenzelm
parents: 11655
diff changeset
    45
primrec
wenzelm
parents: 11655
diff changeset
    46
  "Summation f 0 = 0"
wenzelm
parents: 11655
diff changeset
    47
  "Summation f (Suc n) = Summation f n + f n"
wenzelm
parents: 11655
diff changeset
    48
wenzelm
parents: 11655
diff changeset
    49
syntax
wenzelm
parents: 11655
diff changeset
    50
  "_Summation" :: "idt => nat => 'a => nat"    ("\<Sum>_<_. _" [0, 51, 10] 10)
wenzelm
parents: 11655
diff changeset
    51
translations
wenzelm
parents: 11655
diff changeset
    52
  "\<Sum>i < n. b" == "Summation (\<lambda>i. b) n"
wenzelm
parents: 11655
diff changeset
    53
wenzelm
parents: 11655
diff changeset
    54
theorem Summation_step:
wenzelm
parents: 11655
diff changeset
    55
    "0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)"
wenzelm
parents: 11655
diff changeset
    56
  by (induct n) simp_all
wenzelm
parents: 11655
diff changeset
    57
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    58
end