src/FOL/ex/Natural_Numbers.thy
changeset 11673 79e5536af6c4
child 11679 afdbee613f58
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/FOL/ex/Natural_Numbers.thy	Thu Oct 04 15:25:31 2001 +0200
     1.3 @@ -0,0 +1,69 @@
     1.4 +(*  Title:      FOL/ex/Natural_Numbers.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Munich
     1.7 +
     1.8 +Theory of the natural numbers: Peano's axioms, primitive recursion.
     1.9 +(Modernized version of Larry Paulson's theory "Nat".)
    1.10 +*)
    1.11 +
    1.12 +theory Natural_Numbers = FOL:
    1.13 +
    1.14 +typedecl nat
    1.15 +arities nat :: "term"
    1.16 +
    1.17 +consts
    1.18 +  Zero :: nat    ("0")
    1.19 +  Suc :: "nat => nat"
    1.20 +  rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
    1.21 +
    1.22 +axioms
    1.23 +  induct [induct type: nat]:
    1.24 +    "P(0) \<Longrightarrow> (!!x. P(x) ==> P(Suc(x))) ==> P(n)"
    1.25 +  Suc_inject: "Suc(m) = Suc(n) ==> m = n"
    1.26 +  Suc_neq_0: "Suc(m) = 0 ==> R"
    1.27 +  rec_0: "rec(0, a, f) = a"
    1.28 +  rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
    1.29 +
    1.30 +lemma Suc_n_not_n: "Suc(k) \<noteq> k"
    1.31 +proof (induct k)
    1.32 +  show "Suc(0) \<noteq> 0"
    1.33 +  proof
    1.34 +    assume "Suc(0) = 0"
    1.35 +    thus False by (rule Suc_neq_0)
    1.36 +  qed
    1.37 +  fix n assume hyp: "Suc(n) \<noteq> n"
    1.38 +  show "Suc(Suc(n)) \<noteq> Suc(n)"
    1.39 +  proof
    1.40 +    assume "Suc(Suc(n)) = Suc(n)"
    1.41 +    hence "Suc(n) = n" by (rule Suc_inject)
    1.42 +    with hyp show False by contradiction
    1.43 +  qed
    1.44 +qed
    1.45 +
    1.46 +
    1.47 +constdefs
    1.48 +  add :: "[nat, nat] => nat"    (infixl "+" 60)
    1.49 +  "m + n == rec(m, n, \<lambda>x y. Suc(y))"
    1.50 +
    1.51 +lemma add_0 [simp]: "0 + n = n"
    1.52 +  by (unfold add_def) (rule rec_0)
    1.53 +
    1.54 +lemma add_Suc [simp]: "Suc(m) + n = Suc(m + n)"
    1.55 +  by (unfold add_def) (rule rec_Suc)
    1.56 +
    1.57 +lemma add_assoc: "(k + m) + n = k + (m + n)"
    1.58 +  by (induct k) simp_all
    1.59 +
    1.60 +lemma add_0_right: "m + 0 = m"
    1.61 +  by (induct m) simp_all
    1.62 +
    1.63 +lemma add_Suc_right: "m + Suc(n) = Suc(m + n)"
    1.64 +  by (induct m) simp_all
    1.65 +
    1.66 +lemma "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i + j) = i + f(j)"
    1.67 +proof -
    1.68 +  assume a: "!!n. f(Suc(n)) = Suc(f(n))"
    1.69 +  show ?thesis by (induct i) (simp, simp add: a)  (* FIXME tune *)
    1.70 +qed
    1.71 +
    1.72 +end