src/FOL/ex/Natural_Numbers.thy
author wenzelm
Fri, 05 Oct 2001 21:42:10 +0200
changeset 11696 233362cfecc7
parent 11679 afdbee613f58
child 11726 2b2a45abe876
permissions -rw-r--r--
induct: case names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11673
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
     1
(*  Title:      FOL/ex/Natural_Numbers.thy
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Munich
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
     4
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
     5
Theory of the natural numbers: Peano's axioms, primitive recursion.
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
     6
(Modernized version of Larry Paulson's theory "Nat".)
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
     7
*)
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
     8
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
     9
theory Natural_Numbers = FOL:
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    10
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    11
typedecl nat
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    12
arities nat :: "term"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    13
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    14
consts
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    15
  Zero :: nat    ("0")
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    16
  Suc :: "nat => nat"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    17
  rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    18
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    19
axioms
11696
233362cfecc7 induct: case names;
wenzelm
parents: 11679
diff changeset
    20
  induct [case_names Zero Suc, induct type: nat]:
11679
afdbee613f58 unsymbolized;
wenzelm
parents: 11673
diff changeset
    21
    "P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)"
11673
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    22
  Suc_inject: "Suc(m) = Suc(n) ==> m = n"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    23
  Suc_neq_0: "Suc(m) = 0 ==> R"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    24
  rec_0: "rec(0, a, f) = a"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    25
  rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    26
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    27
lemma Suc_n_not_n: "Suc(k) \<noteq> k"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    28
proof (induct k)
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    29
  show "Suc(0) \<noteq> 0"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    30
  proof
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    31
    assume "Suc(0) = 0"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    32
    thus False by (rule Suc_neq_0)
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    33
  qed
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    34
  fix n assume hyp: "Suc(n) \<noteq> n"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    35
  show "Suc(Suc(n)) \<noteq> Suc(n)"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    36
  proof
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    37
    assume "Suc(Suc(n)) = Suc(n)"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    38
    hence "Suc(n) = n" by (rule Suc_inject)
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    39
    with hyp show False by contradiction
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    40
  qed
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    41
qed
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    42
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    43
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    44
constdefs
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    45
  add :: "[nat, nat] => nat"    (infixl "+" 60)
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    46
  "m + n == rec(m, n, \<lambda>x y. Suc(y))"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    47
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    48
lemma add_0 [simp]: "0 + n = n"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    49
  by (unfold add_def) (rule rec_0)
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    50
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    51
lemma add_Suc [simp]: "Suc(m) + n = Suc(m + n)"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    52
  by (unfold add_def) (rule rec_Suc)
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    53
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    54
lemma add_assoc: "(k + m) + n = k + (m + n)"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    55
  by (induct k) simp_all
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    56
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    57
lemma add_0_right: "m + 0 = m"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    58
  by (induct m) simp_all
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    59
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    60
lemma add_Suc_right: "m + Suc(n) = Suc(m + n)"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    61
  by (induct m) simp_all
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    62
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    63
lemma "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i + j) = i + f(j)"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    64
proof -
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    65
  assume a: "!!n. f(Suc(n)) = Suc(f(n))"
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    66
  show ?thesis by (induct i) (simp, simp add: a)  (* FIXME tune *)
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    67
qed
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    68
79e5536af6c4 Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff changeset
    69
end