src/FOL/ex/Natural_Numbers.thy
author wenzelm
Wed Dec 05 03:06:05 2001 +0100 (2001-12-05)
changeset 12371 80ca9058db95
parent 11789 da81334357ba
child 14981 e73f8140af78
permissions -rw-r--r--
tuned;
     1 (*  Title:      FOL/ex/Natural_Numbers.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Munich
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 
     7 header {* Natural numbers *}
     8 
     9 theory Natural_Numbers = FOL:
    10 
    11 text {*
    12   Theory of the natural numbers: Peano's axioms, primitive recursion.
    13   (Modernized version of Larry Paulson's theory "Nat".)  \medskip
    14 *}
    15 
    16 typedecl nat
    17 arities nat :: "term"
    18 
    19 consts
    20   Zero :: nat    ("0")
    21   Suc :: "nat => nat"
    22   rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
    23 
    24 axioms
    25   induct [case_names 0 Suc, induct type: nat]:
    26     "P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)"
    27   Suc_inject: "Suc(m) = Suc(n) ==> m = n"
    28   Suc_neq_0: "Suc(m) = 0 ==> R"
    29   rec_0: "rec(0, a, f) = a"
    30   rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
    31 
    32 lemma Suc_n_not_n: "Suc(k) \<noteq> k"
    33 proof (induct k)
    34   show "Suc(0) \<noteq> 0"
    35   proof
    36     assume "Suc(0) = 0"
    37     thus False by (rule Suc_neq_0)
    38   qed
    39   fix n assume hyp: "Suc(n) \<noteq> n"
    40   show "Suc(Suc(n)) \<noteq> Suc(n)"
    41   proof
    42     assume "Suc(Suc(n)) = Suc(n)"
    43     hence "Suc(n) = n" by (rule Suc_inject)
    44     with hyp show False by contradiction
    45   qed
    46 qed
    47 
    48 
    49 constdefs
    50   add :: "[nat, nat] => nat"    (infixl "+" 60)
    51   "m + n == rec(m, n, \<lambda>x y. Suc(y))"
    52 
    53 lemma add_0 [simp]: "0 + n = n"
    54   by (unfold add_def) (rule rec_0)
    55 
    56 lemma add_Suc [simp]: "Suc(m) + n = Suc(m + n)"
    57   by (unfold add_def) (rule rec_Suc)
    58 
    59 lemma add_assoc: "(k + m) + n = k + (m + n)"
    60   by (induct k) simp_all
    61 
    62 lemma add_0_right: "m + 0 = m"
    63   by (induct m) simp_all
    64 
    65 lemma add_Suc_right: "m + Suc(n) = Suc(m + n)"
    66   by (induct m) simp_all
    67 
    68 lemma "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i + j) = i + f(j)"
    69 proof -
    70   assume "!!n. f(Suc(n)) = Suc(f(n))"
    71   thus ?thesis by (induct i) simp_all
    72 qed
    73 
    74 end