equal
deleted
inserted
replaced
56 way as for the concrete version. The original proof scripts may be |
56 way as for the concrete version. The original proof scripts may be |
57 re-used with some trivial changes only (mostly adding some type |
57 re-used with some trivial changes only (mostly adding some type |
58 constraints). |
58 constraints). |
59 *} |
59 *} |
60 |
60 |
|
61 (*<*) |
|
62 lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)" |
|
63 apply (rule_tac n = k in induct) |
|
64 apply (rule notI) |
|
65 apply (erule Suc_neq_0) |
|
66 apply (rule notI) |
|
67 apply (erule notE) |
|
68 apply (erule Suc_inject) |
|
69 done |
|
70 |
|
71 lemma "(k+m)+n = k+(m+n)" |
|
72 apply (rule induct) |
|
73 back |
|
74 back |
|
75 back |
|
76 back |
|
77 back |
|
78 back |
|
79 oops |
|
80 |
|
81 lemma add_0 [simp]: "\<zero>+n = n" |
|
82 apply (unfold add_def) |
|
83 apply (rule rec_0) |
|
84 done |
|
85 |
|
86 lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)" |
|
87 apply (unfold add_def) |
|
88 apply (rule rec_Suc) |
|
89 done |
|
90 |
|
91 lemma add_assoc: "(k+m)+n = k+(m+n)" |
|
92 apply (rule_tac n = k in induct) |
|
93 apply simp |
|
94 apply simp |
|
95 done |
|
96 |
|
97 lemma add_0_right: "m+\<zero> = m" |
|
98 apply (rule_tac n = m in induct) |
|
99 apply simp |
|
100 apply simp |
|
101 done |
|
102 |
|
103 lemma add_Suc_right: "m+Suc(n) = Suc(m+n)" |
|
104 apply (rule_tac n = m in induct) |
|
105 apply simp_all |
|
106 done |
|
107 |
|
108 lemma |
|
109 assumes prem: "!!n. f(Suc(n)) = Suc(f(n))" |
|
110 shows "f(i+j) = i+f(j)" |
|
111 apply (rule_tac n = i in induct) |
|
112 apply simp |
|
113 apply (simp add: prem) |
|
114 done |
|
115 (*>*) |
|
116 |
61 end |
117 end |