author  haftmann 
Tue, 10 Jul 2007 17:30:50 +0200  
changeset 23709  fd31da8f752a 
parent 16417  9bc16273c2d4 
child 25989  3267d0694d93 
permissions  rwrr 
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 

12371  6 
header {* Natural numbers *} 
7 

16417  8 
theory Natural_Numbers imports FOL begin 
11673
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

9 

12371  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 

11673
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

15 
typedecl nat 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

16 
arities nat :: "term" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

17 

79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

18 
consts 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

19 
Zero :: nat ("0") 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

20 
Suc :: "nat => nat" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

21 
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

22 

79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

23 
axioms 
11789  24 
induct [case_names 0 Suc, induct type: nat]: 
11679  25 
"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

26 
Suc_inject: "Suc(m) = Suc(n) ==> m = n" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

27 
Suc_neq_0: "Suc(m) = 0 ==> R" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

28 
rec_0: "rec(0, a, f) = a" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

29 
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

30 

79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

31 
lemma Suc_n_not_n: "Suc(k) \<noteq> k" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

32 
proof (induct k) 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

33 
show "Suc(0) \<noteq> 0" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

34 
proof 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

35 
assume "Suc(0) = 0" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

36 
thus False by (rule Suc_neq_0) 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

37 
qed 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

38 
fix n assume hyp: "Suc(n) \<noteq> n" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

39 
show "Suc(Suc(n)) \<noteq> Suc(n)" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

40 
proof 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

41 
assume "Suc(Suc(n)) = Suc(n)" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

42 
hence "Suc(n) = n" by (rule Suc_inject) 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

43 
with hyp show False by contradiction 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

44 
qed 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

45 
qed 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

46 

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 
constdefs 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

49 
add :: "[nat, nat] => nat" (infixl "+" 60) 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

50 
"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

51 

79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

52 
lemma add_0 [simp]: "0 + n = n" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

53 
by (unfold add_def) (rule rec_0) 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

54 

79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

55 
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

56 
by (unfold add_def) (rule rec_Suc) 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

57 

79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

58 
lemma add_assoc: "(k + m) + n = k + (m + n)" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

59 
by (induct k) simp_all 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

60 

79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

61 
lemma add_0_right: "m + 0 = m" 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

62 
by (induct m) simp_all 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

63 

79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

64 
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

65 
by (induct m) simp_all 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

66 

79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

67 
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

68 
proof  
11726  69 
assume "!!n. f(Suc(n)) = Suc(f(n))" 
70 
thus ?thesis by (induct i) simp_all 

11673
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

71 
qed 
79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

72 

79e5536af6c4
Theory of the natural numbers: Peano's axioms, primitive recursion.
wenzelm
parents:
diff
changeset

73 
end 