19 |
19 |
20 val diff_0 = diff_def RS def_nat_rec_0; |
20 val diff_0 = diff_def RS def_nat_rec_0; |
21 |
21 |
22 qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def] |
22 qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def] |
23 "0 - n = 0" |
23 "0 - n = 0" |
24 (fn _ => [nat_ind_tac "n" 1, ALLGOALS(asm_simp_tac nat_ss)]); |
24 (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); |
25 |
25 |
26 (*Must simplify BEFORE the induction!! (Else we get a critical pair) |
26 (*Must simplify BEFORE the induction!! (Else we get a critical pair) |
27 Suc(m) - Suc(n) rewrites to pred(Suc(m) - n) *) |
27 Suc(m) - Suc(n) rewrites to pred(Suc(m) - n) *) |
28 qed_goalw "diff_Suc_Suc" Arith.thy [diff_def, pred_def] |
28 qed_goalw "diff_Suc_Suc" Arith.thy [diff_def, pred_def] |
29 "Suc(m) - Suc(n) = m - n" |
29 "Suc(m) - Suc(n) = m - n" |
30 (fn _ => |
30 (fn _ => |
31 [simp_tac nat_ss 1, nat_ind_tac "n" 1, ALLGOALS(asm_simp_tac nat_ss)]); |
31 [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); |
32 |
32 |
33 (*** Simplification over add, mult, diff ***) |
33 (*** Simplification over add, mult, diff ***) |
34 |
34 |
35 val arith_simps = |
35 Addsimps [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc, diff_0, |
36 [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc, |
36 diff_0_eq_0, diff_Suc_Suc]; |
37 diff_0, diff_0_eq_0, diff_Suc_Suc]; |
37 |
38 |
|
39 val arith_ss = nat_ss addsimps arith_simps; |
|
40 |
38 |
41 (**** Inductive properties of the operators ****) |
39 (**** Inductive properties of the operators ****) |
42 |
40 |
43 (*** Addition ***) |
41 (*** Addition ***) |
44 |
42 |
45 qed_goal "add_0_right" Arith.thy "m + 0 = m" |
43 qed_goal "add_0_right" Arith.thy "m + 0 = m" |
46 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
44 (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); |
47 |
45 |
48 qed_goal "add_Suc_right" Arith.thy "m + Suc(n) = Suc(m+n)" |
46 qed_goal "add_Suc_right" Arith.thy "m + Suc(n) = Suc(m+n)" |
49 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
47 (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); |
50 |
48 |
51 val arith_ss = arith_ss addsimps [add_0_right,add_Suc_right]; |
49 Addsimps [add_0_right,add_Suc_right]; |
52 |
50 |
53 (*Associative law for addition*) |
51 (*Associative law for addition*) |
54 qed_goal "add_assoc" Arith.thy "(m + n) + k = m + ((n + k)::nat)" |
52 qed_goal "add_assoc" Arith.thy "(m + n) + k = m + ((n + k)::nat)" |
55 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
53 (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); |
56 |
54 |
57 (*Commutative law for addition*) |
55 (*Commutative law for addition*) |
58 qed_goal "add_commute" Arith.thy "m + n = n + (m::nat)" |
56 qed_goal "add_commute" Arith.thy "m + n = n + (m::nat)" |
59 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
57 (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); |
60 |
58 |
61 qed_goal "add_left_commute" Arith.thy "x+(y+z)=y+((x+z)::nat)" |
59 qed_goal "add_left_commute" Arith.thy "x+(y+z)=y+((x+z)::nat)" |
62 (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1, |
60 (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1, |
63 rtac (add_commute RS arg_cong) 1]); |
61 rtac (add_commute RS arg_cong) 1]); |
64 |
62 |
65 (*Addition is an AC-operator*) |
63 (*Addition is an AC-operator*) |
66 val add_ac = [add_assoc, add_commute, add_left_commute]; |
64 val add_ac = [add_assoc, add_commute, add_left_commute]; |
67 |
65 |
68 goal Arith.thy "!!k::nat. (k + m = k + n) = (m=n)"; |
66 goal Arith.thy "!!k::nat. (k + m = k + n) = (m=n)"; |
69 by (nat_ind_tac "k" 1); |
67 by (nat_ind_tac "k" 1); |
70 by (simp_tac arith_ss 1); |
68 by (Simp_tac 1); |
71 by (asm_simp_tac arith_ss 1); |
69 by (Asm_simp_tac 1); |
72 qed "add_left_cancel"; |
70 qed "add_left_cancel"; |
73 |
71 |
74 goal Arith.thy "!!k::nat. (m + k = n + k) = (m=n)"; |
72 goal Arith.thy "!!k::nat. (m + k = n + k) = (m=n)"; |
75 by (nat_ind_tac "k" 1); |
73 by (nat_ind_tac "k" 1); |
76 by (simp_tac arith_ss 1); |
74 by (Simp_tac 1); |
77 by (asm_simp_tac arith_ss 1); |
75 by (Asm_simp_tac 1); |
78 qed "add_right_cancel"; |
76 qed "add_right_cancel"; |
79 |
77 |
80 goal Arith.thy "!!k::nat. (k + m <= k + n) = (m<=n)"; |
78 goal Arith.thy "!!k::nat. (k + m <= k + n) = (m<=n)"; |
81 by (nat_ind_tac "k" 1); |
79 by (nat_ind_tac "k" 1); |
82 by (simp_tac arith_ss 1); |
80 by (Simp_tac 1); |
83 by (asm_simp_tac (arith_ss addsimps [Suc_le_mono]) 1); |
81 by (Asm_simp_tac 1); |
84 qed "add_left_cancel_le"; |
82 qed "add_left_cancel_le"; |
85 |
83 |
86 goal Arith.thy "!!k::nat. (k + m < k + n) = (m<n)"; |
84 goal Arith.thy "!!k::nat. (k + m < k + n) = (m<n)"; |
87 by (nat_ind_tac "k" 1); |
85 by (nat_ind_tac "k" 1); |
88 by (simp_tac arith_ss 1); |
86 by (Simp_tac 1); |
89 by (asm_simp_tac arith_ss 1); |
87 by (Asm_simp_tac 1); |
90 qed "add_left_cancel_less"; |
88 qed "add_left_cancel_less"; |
91 |
89 |
92 (*** Multiplication ***) |
90 (*** Multiplication ***) |
93 |
91 |
94 (*right annihilation in product*) |
92 (*right annihilation in product*) |
95 qed_goal "mult_0_right" Arith.thy "m * 0 = 0" |
93 qed_goal "mult_0_right" Arith.thy "m * 0 = 0" |
96 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
94 (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); |
97 |
95 |
98 (*right Sucessor law for multiplication*) |
96 (*right Sucessor law for multiplication*) |
99 qed_goal "mult_Suc_right" Arith.thy "m * Suc(n) = m + (m * n)" |
97 qed_goal "mult_Suc_right" Arith.thy "m * Suc(n) = m + (m * n)" |
100 (fn _ => [nat_ind_tac "m" 1, |
98 (fn _ => [nat_ind_tac "m" 1, |
101 ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]); |
99 ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]); |
102 |
100 |
103 val arith_ss = arith_ss addsimps [mult_0_right,mult_Suc_right]; |
101 Addsimps [mult_0_right,mult_Suc_right]; |
104 |
102 |
105 (*Commutative law for multiplication*) |
103 (*Commutative law for multiplication*) |
106 qed_goal "mult_commute" Arith.thy "m * n = n * (m::nat)" |
104 qed_goal "mult_commute" Arith.thy "m * n = n * (m::nat)" |
107 (fn _ => [nat_ind_tac "m" 1, ALLGOALS (asm_simp_tac arith_ss)]); |
105 (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); |
108 |
106 |
109 (*addition distributes over multiplication*) |
107 (*addition distributes over multiplication*) |
110 qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)" |
108 qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)" |
111 (fn _ => [nat_ind_tac "m" 1, |
109 (fn _ => [nat_ind_tac "m" 1, |
112 ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]); |
110 ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]); |
113 |
111 |
114 qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)" |
112 qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)" |
115 (fn _ => [nat_ind_tac "m" 1, |
113 (fn _ => [nat_ind_tac "m" 1, |
116 ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]); |
114 ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]); |
117 |
115 |
118 val arith_ss = arith_ss addsimps [add_mult_distrib,add_mult_distrib2]; |
116 Addsimps [add_mult_distrib,add_mult_distrib2]; |
119 |
117 |
120 (*Associative law for multiplication*) |
118 (*Associative law for multiplication*) |
121 qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)" |
119 qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)" |
122 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
120 (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); |
123 |
121 |
124 qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)" |
122 qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)" |
125 (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1, |
123 (fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1, |
126 rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]); |
124 rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]); |
127 |
125 |
128 val mult_ac = [mult_assoc,mult_commute,mult_left_commute]; |
126 val mult_ac = [mult_assoc,mult_commute,mult_left_commute]; |
129 |
127 |
130 (*** Difference ***) |
128 (*** Difference ***) |
131 |
129 |
132 qed_goal "diff_self_eq_0" Arith.thy "m - m = 0" |
130 qed_goal "diff_self_eq_0" Arith.thy "m - m = 0" |
133 (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); |
131 (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); |
134 |
132 |
135 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *) |
133 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *) |
136 val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)"; |
134 val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)"; |
137 by (rtac (prem RS rev_mp) 1); |
135 by (rtac (prem RS rev_mp) 1); |
138 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
136 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
139 by (ALLGOALS(asm_simp_tac arith_ss)); |
137 by (ALLGOALS Asm_simp_tac); |
140 qed "add_diff_inverse"; |
138 qed "add_diff_inverse"; |
141 |
139 |
142 |
140 |
143 (*** Remainder ***) |
141 (*** Remainder ***) |
144 |
142 |
145 goal Arith.thy "m - n < Suc(m)"; |
143 goal Arith.thy "m - n < Suc(m)"; |
146 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
144 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
147 by (etac less_SucE 3); |
145 by (etac less_SucE 3); |
148 by (ALLGOALS(asm_simp_tac arith_ss)); |
146 by (ALLGOALS Asm_simp_tac); |
149 qed "diff_less_Suc"; |
147 qed "diff_less_Suc"; |
150 |
148 |
151 goal Arith.thy "!!m::nat. m - n <= m"; |
149 goal Arith.thy "!!m::nat. m - n <= m"; |
152 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); |
150 by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); |
153 by (ALLGOALS (asm_simp_tac arith_ss)); |
151 by (ALLGOALS Asm_simp_tac); |
154 by (etac le_trans 1); |
152 by (etac le_trans 1); |
155 by (simp_tac (HOL_ss addsimps [le_eq_less_or_eq, lessI]) 1); |
153 by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); |
156 qed "diff_le_self"; |
154 qed "diff_le_self"; |
157 |
155 |
158 goal Arith.thy "!!n::nat. (n+m) - n = m"; |
156 goal Arith.thy "!!n::nat. (n+m) - n = m"; |
159 by (nat_ind_tac "n" 1); |
157 by (nat_ind_tac "n" 1); |
160 by (ALLGOALS (asm_simp_tac arith_ss)); |
158 by (ALLGOALS Asm_simp_tac); |
161 qed "diff_add_inverse"; |
159 qed "diff_add_inverse"; |
162 |
160 |
163 goal Arith.thy "!!n::nat. n - (n+m) = 0"; |
161 goal Arith.thy "!!n::nat. n - (n+m) = 0"; |
164 by (nat_ind_tac "n" 1); |
162 by (nat_ind_tac "n" 1); |
165 by (ALLGOALS (asm_simp_tac arith_ss)); |
163 by (ALLGOALS Asm_simp_tac); |
166 qed "diff_add_0"; |
164 qed "diff_add_0"; |
167 |
165 |
168 (*In ordinary notation: if 0<n and n<=m then m-n < m *) |
166 (*In ordinary notation: if 0<n and n<=m then m-n < m *) |
169 goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m"; |
167 goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m"; |
170 by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1); |
168 by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1); |
171 by (fast_tac HOL_cs 1); |
169 by (fast_tac HOL_cs 1); |
172 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
170 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
173 by (ALLGOALS(asm_simp_tac(arith_ss addsimps [diff_less_Suc]))); |
171 by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc]))); |
174 qed "div_termination"; |
172 qed "div_termination"; |
175 |
173 |
176 val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans); |
174 val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans); |
177 |
175 |
178 goalw Nat.thy [less_def] "(m,n) : pred_nat^+ = (m<n)"; |
176 goalw Nat.thy [less_def] "(m,n) : pred_nat^+ = (m<n)"; |
179 by (rtac refl 1); |
177 by (rtac refl 1); |
180 qed "less_eq"; |
178 qed "less_eq"; |
181 |
179 |
182 goal Arith.thy "!!m. m<n ==> m mod n = m"; |
180 goal Arith.thy "!!m. m<n ==> m mod n = m"; |
183 by (rtac (mod_def RS wf_less_trans) 1); |
181 by (rtac (mod_def RS wf_less_trans) 1); |
184 by(asm_simp_tac HOL_ss 1); |
182 by(Asm_simp_tac 1); |
185 qed "mod_less"; |
183 qed "mod_less"; |
186 |
184 |
187 goal Arith.thy "!!m. [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n"; |
185 goal Arith.thy "!!m. [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n"; |
188 by (rtac (mod_def RS wf_less_trans) 1); |
186 by (rtac (mod_def RS wf_less_trans) 1); |
189 by(asm_simp_tac (nat_ss addsimps [div_termination, cut_apply, less_eq]) 1); |
187 by(asm_simp_tac (!simpset addsimps [div_termination, cut_apply, less_eq]) 1); |
190 qed "mod_geq"; |
188 qed "mod_geq"; |
191 |
189 |
192 |
190 |
193 (*** Quotient ***) |
191 (*** Quotient ***) |
194 |
192 |
195 goal Arith.thy "!!m. m<n ==> m div n = 0"; |
193 goal Arith.thy "!!m. m<n ==> m div n = 0"; |
196 by (rtac (div_def RS wf_less_trans) 1); |
194 by (rtac (div_def RS wf_less_trans) 1); |
197 by(asm_simp_tac nat_ss 1); |
195 by(Asm_simp_tac 1); |
198 qed "div_less"; |
196 qed "div_less"; |
199 |
197 |
200 goal Arith.thy "!!M. [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)"; |
198 goal Arith.thy "!!M. [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)"; |
201 by (rtac (div_def RS wf_less_trans) 1); |
199 by (rtac (div_def RS wf_less_trans) 1); |
202 by(asm_simp_tac (nat_ss addsimps [div_termination, cut_apply, less_eq]) 1); |
200 by(asm_simp_tac (!simpset addsimps [div_termination, cut_apply, less_eq]) 1); |
203 qed "div_geq"; |
201 qed "div_geq"; |
204 |
202 |
205 (*Main Result about quotient and remainder.*) |
203 (*Main Result about quotient and remainder.*) |
206 goal Arith.thy "!!m. 0<n ==> (m div n)*n + m mod n = m"; |
204 goal Arith.thy "!!m. 0<n ==> (m div n)*n + m mod n = m"; |
207 by (res_inst_tac [("n","m")] less_induct 1); |
205 by (res_inst_tac [("n","m")] less_induct 1); |
208 by (rename_tac "k" 1); (*Variable name used in line below*) |
206 by (rename_tac "k" 1); (*Variable name used in line below*) |
209 by (case_tac "k<n" 1); |
207 by (case_tac "k<n" 1); |
210 by (ALLGOALS (asm_simp_tac(arith_ss addsimps (add_ac @ |
208 by (ALLGOALS (asm_simp_tac(!simpset addsimps (add_ac @ |
211 [mod_less, mod_geq, div_less, div_geq, |
209 [mod_less, mod_geq, div_less, div_geq, |
212 add_diff_inverse, div_termination])))); |
210 add_diff_inverse, div_termination])))); |
213 qed "mod_div_equality"; |
211 qed "mod_div_equality"; |
214 |
212 |
215 |
213 |
216 (*** More results about difference ***) |
214 (*** More results about difference ***) |
217 |
215 |
218 val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0"; |
216 val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0"; |
219 by (rtac (prem RS rev_mp) 1); |
217 by (rtac (prem RS rev_mp) 1); |
220 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
218 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
221 by (ALLGOALS (asm_simp_tac arith_ss)); |
219 by (ALLGOALS Asm_simp_tac); |
222 qed "less_imp_diff_is_0"; |
220 qed "less_imp_diff_is_0"; |
223 |
221 |
224 val prems = goal Arith.thy "m-n = 0 --> n-m = 0 --> m=n"; |
222 val prems = goal Arith.thy "m-n = 0 --> n-m = 0 --> m=n"; |
225 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
223 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
226 by (REPEAT(simp_tac arith_ss 1 THEN TRY(atac 1))); |
224 by (REPEAT(Simp_tac 1 THEN TRY(atac 1))); |
227 qed "diffs0_imp_equal_lemma"; |
225 qed "diffs0_imp_equal_lemma"; |
228 |
226 |
229 (* [| m-n = 0; n-m = 0 |] ==> m=n *) |
227 (* [| m-n = 0; n-m = 0 |] ==> m=n *) |
230 bind_thm ("diffs0_imp_equal", (diffs0_imp_equal_lemma RS mp RS mp)); |
228 bind_thm ("diffs0_imp_equal", (diffs0_imp_equal_lemma RS mp RS mp)); |
231 |
229 |
232 val [prem] = goal Arith.thy "m<n ==> 0<n-m"; |
230 val [prem] = goal Arith.thy "m<n ==> 0<n-m"; |
233 by (rtac (prem RS rev_mp) 1); |
231 by (rtac (prem RS rev_mp) 1); |
234 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
232 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
235 by (ALLGOALS(asm_simp_tac arith_ss)); |
233 by (ALLGOALS Asm_simp_tac); |
236 qed "less_imp_diff_positive"; |
234 qed "less_imp_diff_positive"; |
237 |
235 |
238 val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)"; |
236 val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)"; |
239 by (rtac (prem RS rev_mp) 1); |
237 by (rtac (prem RS rev_mp) 1); |
240 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
238 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); |
241 by (ALLGOALS(asm_simp_tac arith_ss)); |
239 by (ALLGOALS Asm_simp_tac); |
242 qed "Suc_diff_n"; |
240 qed "Suc_diff_n"; |
243 |
241 |
244 goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc m-n)"; |
242 goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc m-n)"; |
245 by(simp_tac (nat_ss addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n] |
243 by(simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n] |
246 setloop (split_tac [expand_if])) 1); |
244 setloop (split_tac [expand_if])) 1); |
247 qed "if_Suc_diff_n"; |
245 qed "if_Suc_diff_n"; |
248 |
246 |
249 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)"; |
247 goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)"; |
250 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); |
248 by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); |
251 by (ALLGOALS (strip_tac THEN' simp_tac arith_ss THEN' TRY o fast_tac HOL_cs)); |
249 by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o fast_tac HOL_cs)); |
252 qed "zero_induct_lemma"; |
250 qed "zero_induct_lemma"; |
253 |
251 |
254 val prems = goal Arith.thy "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)"; |
252 val prems = goal Arith.thy "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)"; |
255 by (rtac (diff_self_eq_0 RS subst) 1); |
253 by (rtac (diff_self_eq_0 RS subst) 1); |
256 by (rtac (zero_induct_lemma RS mp RS mp) 1); |
254 by (rtac (zero_induct_lemma RS mp RS mp) 1); |
320 by (resolve_tac [le_add1] 1); |
318 by (resolve_tac [le_add1] 1); |
321 qed "less_imp_add_less"; |
319 qed "less_imp_add_less"; |
322 |
320 |
323 goal Arith.thy "m+k<=n --> m<=(n::nat)"; |
321 goal Arith.thy "m+k<=n --> m<=(n::nat)"; |
324 by (nat_ind_tac "k" 1); |
322 by (nat_ind_tac "k" 1); |
325 by (ALLGOALS (asm_simp_tac arith_ss)); |
323 by (ALLGOALS Asm_simp_tac); |
326 by (fast_tac (HOL_cs addDs [Suc_leD]) 1); |
324 by (fast_tac (HOL_cs addDs [Suc_leD]) 1); |
327 val add_leD1_lemma = result(); |
325 val add_leD1_lemma = result(); |
328 bind_thm ("add_leD1", add_leD1_lemma RS mp);; |
326 bind_thm ("add_leD1", add_leD1_lemma RS mp); |
329 |
327 |
330 goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n"; |
328 goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n"; |
331 by (safe_tac (HOL_cs addSDs [less_eq_Suc_add])); |
329 by (safe_tac (HOL_cs addSDs [less_eq_Suc_add])); |
332 by (asm_full_simp_tac |
330 by (asm_full_simp_tac |
333 (HOL_ss addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1); |
331 (!simpset delsimps [add_Suc_right] |
|
332 addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1); |
334 by (eresolve_tac [subst] 1); |
333 by (eresolve_tac [subst] 1); |
335 by (simp_tac (arith_ss addsimps [less_add_Suc1]) 1); |
334 by (simp_tac (!simpset addsimps [less_add_Suc1]) 1); |
336 qed "less_add_eq_less"; |
335 qed "less_add_eq_less"; |
337 |
336 |
338 |
337 |
339 (** Monotonicity of addition (from ZF/Arith) **) |
338 (** Monotonicity of addition (from ZF/Arith) **) |
340 |
339 |
341 (** Monotonicity results **) |
340 (** Monotonicity results **) |
342 |
341 |
343 (*strict, in 1st argument*) |
342 (*strict, in 1st argument*) |
344 goal Arith.thy "!!i j k::nat. i < j ==> i + k < j + k"; |
343 goal Arith.thy "!!i j k::nat. i < j ==> i + k < j + k"; |
345 by (nat_ind_tac "k" 1); |
344 by (nat_ind_tac "k" 1); |
346 by (ALLGOALS (asm_simp_tac arith_ss)); |
345 by (ALLGOALS Asm_simp_tac); |
347 qed "add_less_mono1"; |
346 qed "add_less_mono1"; |
348 |
347 |
349 (*strict, in both arguments*) |
348 (*strict, in both arguments*) |
350 goal Arith.thy "!!i j k::nat. [|i < j; k < l|] ==> i + k < j + l"; |
349 goal Arith.thy "!!i j k::nat. [|i < j; k < l|] ==> i + k < j + l"; |
351 by (rtac (add_less_mono1 RS less_trans) 1); |
350 by (rtac (add_less_mono1 RS less_trans) 1); |
352 by (REPEAT (assume_tac 1)); |
351 by (REPEAT (assume_tac 1)); |
353 by (nat_ind_tac "j" 1); |
352 by (nat_ind_tac "j" 1); |
354 by (ALLGOALS (asm_simp_tac arith_ss)); |
353 by (ALLGOALS Asm_simp_tac); |
355 qed "add_less_mono"; |
354 qed "add_less_mono"; |
356 |
355 |
357 (*A [clumsy] way of lifting < monotonicity to <= monotonicity *) |
356 (*A [clumsy] way of lifting < monotonicity to <= monotonicity *) |
358 val [lt_mono,le] = goal Arith.thy |
357 val [lt_mono,le] = goal Arith.thy |
359 "[| !!i j::nat. i<j ==> f(i) < f(j); \ |
358 "[| !!i j::nat. i<j ==> f(i) < f(j); \ |
360 \ i <= j \ |
359 \ i <= j \ |
361 \ |] ==> f(i) <= (f(j)::nat)"; |
360 \ |] ==> f(i) <= (f(j)::nat)"; |
362 by (cut_facts_tac [le] 1); |
361 by (cut_facts_tac [le] 1); |
363 by (asm_full_simp_tac (HOL_ss addsimps [le_eq_less_or_eq]) 1); |
362 by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); |
364 by (fast_tac (HOL_cs addSIs [lt_mono]) 1); |
363 by (fast_tac (HOL_cs addSIs [lt_mono]) 1); |
365 qed "less_mono_imp_le_mono"; |
364 qed "less_mono_imp_le_mono"; |
366 |
365 |
367 (*non-strict, in 1st argument*) |
366 (*non-strict, in 1st argument*) |
368 goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k"; |
367 goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k"; |