1477
|
1 |
(* Title: FOLP/ex/nat.thy
|
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
0
|
3 |
Copyright 1992 University of Cambridge
|
|
4 |
*)
|
|
5 |
|
17480
|
6 |
header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
|
|
7 |
|
|
8 |
theory Nat
|
|
9 |
imports FOLP
|
|
10 |
begin
|
|
11 |
|
|
12 |
typedecl nat
|
25991
|
13 |
arities nat :: "term"
|
|
14 |
|
|
15 |
consts
|
|
16 |
0 :: nat ("0")
|
|
17 |
Suc :: "nat => nat"
|
|
18 |
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
|
|
19 |
add :: "[nat, nat] => nat" (infixl "+" 60)
|
0
|
20 |
|
|
21 |
(*Proof terms*)
|
25991
|
22 |
nrec :: "[nat, p, [nat, p] => p] => p"
|
|
23 |
ninj :: "p => p"
|
|
24 |
nneq :: "p => p"
|
|
25 |
rec0 :: "p"
|
|
26 |
recSuc :: "p"
|
17480
|
27 |
|
|
28 |
axioms
|
|
29 |
induct: "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
|
|
30 |
|] ==> nrec(n,b,c):P(n)"
|
0
|
31 |
|
17480
|
32 |
Suc_inject: "p:Suc(m)=Suc(n) ==> ninj(p) : m=n"
|
|
33 |
Suc_neq_0: "p:Suc(m)=0 ==> nneq(p) : R"
|
|
34 |
rec_0: "rec0 : rec(0,a,f) = a"
|
|
35 |
rec_Suc: "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))"
|
25991
|
36 |
|
|
37 |
defs
|
17480
|
38 |
add_def: "m+n == rec(m, n, %x y. Suc(y))"
|
0
|
39 |
|
25991
|
40 |
axioms
|
17480
|
41 |
nrecB0: "b: A ==> nrec(0,b,c) = b : A"
|
|
42 |
nrecBSuc: "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
|
|
43 |
|
25991
|
44 |
|
|
45 |
subsection {* Proofs about the natural numbers *}
|
|
46 |
|
36319
|
47 |
schematic_lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
|
25991
|
48 |
apply (rule_tac n = k in induct)
|
|
49 |
apply (rule notI)
|
|
50 |
apply (erule Suc_neq_0)
|
|
51 |
apply (rule notI)
|
|
52 |
apply (erule notE)
|
|
53 |
apply (erule Suc_inject)
|
|
54 |
done
|
|
55 |
|
36319
|
56 |
schematic_lemma "?p : (k+m)+n = k+(m+n)"
|
25991
|
57 |
apply (rule induct)
|
|
58 |
back
|
|
59 |
back
|
|
60 |
back
|
|
61 |
back
|
|
62 |
back
|
|
63 |
back
|
|
64 |
oops
|
|
65 |
|
36319
|
66 |
schematic_lemma add_0 [simp]: "?p : 0+n = n"
|
25991
|
67 |
apply (unfold add_def)
|
|
68 |
apply (rule rec_0)
|
|
69 |
done
|
|
70 |
|
36319
|
71 |
schematic_lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
|
25991
|
72 |
apply (unfold add_def)
|
|
73 |
apply (rule rec_Suc)
|
|
74 |
done
|
|
75 |
|
|
76 |
|
36319
|
77 |
schematic_lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
|
25991
|
78 |
apply (erule subst)
|
|
79 |
apply (rule refl)
|
|
80 |
done
|
|
81 |
|
36319
|
82 |
schematic_lemma Plus_cong: "[| p : a = x; q: b = y |] ==> ?p : a + b = x + y"
|
25991
|
83 |
apply (erule subst, erule subst, rule refl)
|
|
84 |
done
|
|
85 |
|
|
86 |
lemmas nat_congs = Suc_cong Plus_cong
|
|
87 |
|
|
88 |
ML {*
|
|
89 |
val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}]
|
|
90 |
*}
|
|
91 |
|
36319
|
92 |
schematic_lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
|
25991
|
93 |
apply (rule_tac n = k in induct)
|
|
94 |
apply (tactic {* SIMP_TAC add_ss 1 *})
|
|
95 |
apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
|
|
96 |
done
|
|
97 |
|
36319
|
98 |
schematic_lemma add_0_right: "?p : m+0 = m"
|
25991
|
99 |
apply (rule_tac n = m in induct)
|
|
100 |
apply (tactic {* SIMP_TAC add_ss 1 *})
|
|
101 |
apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
|
|
102 |
done
|
|
103 |
|
36319
|
104 |
schematic_lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
|
25991
|
105 |
apply (rule_tac n = m in induct)
|
|
106 |
apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *})
|
|
107 |
done
|
|
108 |
|
|
109 |
(*mk_typed_congs appears not to work with FOLP's version of subst*)
|
17480
|
110 |
|
0
|
111 |
end
|