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