15 axiomatization |
15 axiomatization |
16 Zero :: nat ("0") and |
16 Zero :: nat ("0") and |
17 Suc :: "nat \<Rightarrow> nat" and |
17 Suc :: "nat \<Rightarrow> nat" and |
18 rec :: "[nat, 'a, [nat,'a] \<Rightarrow> 'a] \<Rightarrow> 'a" |
18 rec :: "[nat, 'a, [nat,'a] \<Rightarrow> 'a] \<Rightarrow> 'a" |
19 where |
19 where |
20 induct: "\<lbrakk>$H |- $E, P(0), $F; |
20 induct: "\<lbrakk>$H \<turnstile> $E, P(0), $F; |
21 \<And>x. $H, P(x) |- $E, P(Suc(x)), $F\<rbrakk> \<Longrightarrow> $H |- $E, P(n), $F" and |
21 \<And>x. $H, P(x) \<turnstile> $E, P(Suc(x)), $F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P(n), $F" and |
22 |
22 |
23 Suc_inject: "|- Suc(m) = Suc(n) \<longrightarrow> m = n" and |
23 Suc_inject: "\<turnstile> Suc(m) = Suc(n) \<longrightarrow> m = n" and |
24 Suc_neq_0: "|- Suc(m) \<noteq> 0" and |
24 Suc_neq_0: "\<turnstile> Suc(m) \<noteq> 0" and |
25 rec_0: "|- rec(0,a,f) = a" and |
25 rec_0: "\<turnstile> rec(0,a,f) = a" and |
26 rec_Suc: "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))" |
26 rec_Suc: "\<turnstile> rec(Suc(m), a, f) = f(m, rec(m,a,f))" |
27 |
27 |
28 definition add :: "[nat, nat] \<Rightarrow> nat" (infixl "+" 60) |
28 definition add :: "[nat, nat] \<Rightarrow> nat" (infixl "+" 60) |
29 where "m + n == rec(m, n, \<lambda>x y. Suc(y))" |
29 where "m + n == rec(m, n, \<lambda>x y. Suc(y))" |
30 |
30 |
31 |
31 |
32 declare Suc_neq_0 [simp] |
32 declare Suc_neq_0 [simp] |
33 |
33 |
34 lemma Suc_inject_rule: "$H, $G, m = n |- $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G |- $E" |
34 lemma Suc_inject_rule: "$H, $G, m = n \<turnstile> $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G \<turnstile> $E" |
35 by (rule L_of_imp [OF Suc_inject]) |
35 by (rule L_of_imp [OF Suc_inject]) |
36 |
36 |
37 lemma Suc_n_not_n: "|- Suc(k) \<noteq> k" |
37 lemma Suc_n_not_n: "\<turnstile> Suc(k) \<noteq> k" |
38 apply (rule_tac n = k in induct) |
38 apply (rule_tac n = k in induct) |
39 apply simp |
39 apply simp |
40 apply (fast add!: Suc_inject_rule) |
40 apply (fast add!: Suc_inject_rule) |
41 done |
41 done |
42 |
42 |
43 lemma add_0: "|- 0 + n = n" |
43 lemma add_0: "\<turnstile> 0 + n = n" |
44 apply (unfold add_def) |
44 apply (unfold add_def) |
45 apply (rule rec_0) |
45 apply (rule rec_0) |
46 done |
46 done |
47 |
47 |
48 lemma add_Suc: "|- Suc(m) + n = Suc(m + n)" |
48 lemma add_Suc: "\<turnstile> Suc(m) + n = Suc(m + n)" |
49 apply (unfold add_def) |
49 apply (unfold add_def) |
50 apply (rule rec_Suc) |
50 apply (rule rec_Suc) |
51 done |
51 done |
52 |
52 |
53 declare add_0 [simp] add_Suc [simp] |
53 declare add_0 [simp] add_Suc [simp] |
54 |
54 |
55 lemma add_assoc: "|- (k + m) + n = k + (m + n)" |
55 lemma add_assoc: "\<turnstile> (k + m) + n = k + (m + n)" |
56 apply (rule_tac n = "k" in induct) |
56 apply (rule_tac n = "k" in induct) |
57 apply simp_all |
57 apply simp_all |
58 done |
58 done |
59 |
59 |
60 lemma add_0_right: "|- m + 0 = m" |
60 lemma add_0_right: "\<turnstile> m + 0 = m" |
61 apply (rule_tac n = "m" in induct) |
61 apply (rule_tac n = "m" in induct) |
62 apply simp_all |
62 apply simp_all |
63 done |
63 done |
64 |
64 |
65 lemma add_Suc_right: "|- m + Suc(n) = Suc(m + n)" |
65 lemma add_Suc_right: "\<turnstile> m + Suc(n) = Suc(m + n)" |
66 apply (rule_tac n = "m" in induct) |
66 apply (rule_tac n = "m" in induct) |
67 apply simp_all |
67 apply simp_all |
68 done |
68 done |
69 |
69 |
70 lemma "(\<And>n. |- f(Suc(n)) = Suc(f(n))) \<Longrightarrow> |- f(i + j) = i + f(j)" |
70 lemma "(\<And>n. \<turnstile> f(Suc(n)) = Suc(f(n))) \<Longrightarrow> \<turnstile> f(i + j) = i + f(j)" |
71 apply (rule_tac n = "i" in induct) |
71 apply (rule_tac n = "i" in induct) |
72 apply simp_all |
72 apply simp_all |
73 done |
73 done |
74 |
74 |
75 end |
75 end |