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 |- $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G |- $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) ~= k" |
37 lemma Suc_n_not_n: "|- Suc(k) ~= k" |
38 apply (rule_tac n = k in induct) |
38 apply (rule_tac n = k in induct) |
39 apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms Suc_neq_0}) 1 *}) |
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: "|- 0+n = n" |
44 apply (unfold add_def) |
44 apply (unfold add_def) |
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: "|- (k+m)+n = k+(m+n)" |
56 apply (rule_tac n = "k" in induct) |
56 apply (rule_tac n = "k" in induct) |
57 apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *}) |
57 apply simp_all |
58 apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *}) |
|
59 done |
58 done |
60 |
59 |
61 lemma add_0_right: "|- m+0 = m" |
60 lemma add_0_right: "|- m+0 = m" |
62 apply (rule_tac n = "m" in induct) |
61 apply (rule_tac n = "m" in induct) |
63 apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *}) |
62 apply simp_all |
64 apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *}) |
|
65 done |
63 done |
66 |
64 |
67 lemma add_Suc_right: "|- m+Suc(n) = Suc(m+n)" |
65 lemma add_Suc_right: "|- m+Suc(n) = Suc(m+n)" |
68 apply (rule_tac n = "m" in induct) |
66 apply (rule_tac n = "m" in induct) |
69 apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *}) |
67 apply simp_all |
70 apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *}) |
|
71 done |
68 done |
72 |
69 |
73 lemma "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)" |
70 lemma "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)" |
74 apply (rule_tac n = "i" in induct) |
71 apply (rule_tac n = "i" in induct) |
75 apply (tactic {* simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_0}) 1 *}) |
72 apply simp_all |
76 apply (tactic {* asm_simp_tac (put_simpset LK_ss @{context} addsimps @{thms add_Suc}) 1 *}) |
|
77 done |
73 done |
78 |
74 |
79 end |
75 end |