equal
deleted
inserted
replaced
100 |
100 |
101 |
101 |
102 subsection{*Uniqueness and Monotonicity of Quotients and Remainders*} |
102 subsection{*Uniqueness and Monotonicity of Quotients and Remainders*} |
103 |
103 |
104 lemma unique_quotient_lemma: |
104 lemma unique_quotient_lemma: |
105 "[| b*q' + r' \<le> b*q + r; 0 \<le> r'; 0 < b; r < b |] |
105 "[| b*q' + r' \<le> b*q + r; 0 \<le> r'; r' < b; r < b |] |
106 ==> q' \<le> (q::int)" |
106 ==> q' \<le> (q::int)" |
107 apply (subgoal_tac "r' + b * (q'-q) \<le> r") |
107 apply (subgoal_tac "r' + b * (q'-q) \<le> r") |
108 prefer 2 apply (simp add: right_diff_distrib) |
108 prefer 2 apply (simp add: right_diff_distrib) |
109 apply (subgoal_tac "0 < b * (1 + q - q') ") |
109 apply (subgoal_tac "0 < b * (1 + q - q') ") |
110 apply (erule_tac [2] order_le_less_trans) |
110 apply (erule_tac [2] order_le_less_trans) |
113 prefer 2 apply (simp add: right_diff_distrib right_distrib) |
113 prefer 2 apply (simp add: right_diff_distrib right_distrib) |
114 apply (simp add: mult_less_cancel_left) |
114 apply (simp add: mult_less_cancel_left) |
115 done |
115 done |
116 |
116 |
117 lemma unique_quotient_lemma_neg: |
117 lemma unique_quotient_lemma_neg: |
118 "[| b*q' + r' \<le> b*q + r; r \<le> 0; b < 0; b < r' |] |
118 "[| b*q' + r' \<le> b*q + r; r \<le> 0; b < r; b < r' |] |
119 ==> q \<le> (q'::int)" |
119 ==> q \<le> (q'::int)" |
120 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma, |
120 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma, |
121 auto) |
121 auto) |
122 |
122 |
123 lemma unique_quotient: |
123 lemma unique_quotient: |