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