equal
deleted
inserted
replaced
95 Addsimps [mod_mult_self_is_0]; |
95 Addsimps [mod_mult_self_is_0]; |
96 |
96 |
97 (*** Quotient ***) |
97 (*** Quotient ***) |
98 |
98 |
99 Goal "(%m. m div n) = wfrec (trancl pred_nat) \ |
99 Goal "(%m. m div n) = wfrec (trancl pred_nat) \ |
100 \ (%f j. if j<n then 0 else Suc (f (j-n)))"; |
100 \ (%f j. if j<n then 0 else Suc (f (j-n)))"; |
101 by (simp_tac (simpset() addsimps [div_def]) 1); |
101 by (simp_tac (simpset() addsimps [div_def]) 1); |
102 qed "div_eq"; |
102 qed "div_eq"; |
103 |
103 |
104 Goal "m<n ==> m div n = 0"; |
104 Goal "m<n ==> m div n = 0"; |
105 by (rtac (div_eq RS wf_less_trans) 1); |
105 by (rtac (div_eq RS wf_less_trans) 1); |
114 (*Avoids the ugly ~m<n above*) |
114 (*Avoids the ugly ~m<n above*) |
115 Goal "[| 0<n; n<=m |] ==> m div n = Suc((m-n) div n)"; |
115 Goal "[| 0<n; n<=m |] ==> m div n = Suc((m-n) div n)"; |
116 by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1); |
116 by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1); |
117 qed "le_div_geq"; |
117 qed "le_div_geq"; |
118 |
118 |
119 (*NOT suitable for rewriting: loops*) |
|
120 Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"; |
119 Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))"; |
121 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1); |
120 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1); |
122 qed "div_if"; |
121 qed "div_if"; |
123 |
122 |
124 (*Main Result about quotient and remainder.*) |
123 (*Main Result about quotient and remainder.*) |
304 (*Restore the default*) |
303 (*Restore the default*) |
305 Delrules [less_SucE]; |
304 Delrules [less_SucE]; |
306 |
305 |
307 (*** More division laws ***) |
306 (*** More division laws ***) |
308 |
307 |
309 Goal "0<n ==> m*n div n = m"; |
308 Goal "0<n ==> (m*n) div n = m"; |
310 by (cut_inst_tac [("m", "m*n")] mod_div_equality 1); |
309 by (cut_inst_tac [("m", "m*n")] mod_div_equality 1); |
311 by (assume_tac 1); |
310 by (assume_tac 1); |
312 by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1); |
311 by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1); |
313 qed "div_mult_self_is_m"; |
312 qed "div_mult_self_is_m"; |
314 Addsimps [div_mult_self_is_m]; |
313 Addsimps [div_mult_self_is_m]; |