147 |
147 |
148 lemma partition_lb_lt: "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)" |
148 lemma partition_lb_lt: "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)" |
149 apply (rule_tac t = a in partition_lhs [THEN subst], assumption) |
149 apply (rule_tac t = a in partition_lhs [THEN subst], assumption) |
150 apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear) |
150 apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear) |
151 apply (frule partition [THEN iffD1], safe) |
151 apply (frule partition [THEN iffD1], safe) |
152 using neq0_conv |
|
153 apply (blast intro: partition_lt less_le_trans) |
152 apply (blast intro: partition_lt less_le_trans) |
154 apply (rotate_tac 3) |
153 apply (rotate_tac 3) |
155 apply (drule_tac x = "Suc n" in spec) |
154 apply (drule_tac x = "Suc n" in spec) |
156 apply (erule impE) |
155 apply (erule impE) |
157 apply (erule less_imp_le) |
156 apply (erule less_imp_le) |
158 apply (frule partition_rhs, simp only: neq0_conv) |
157 apply (frule partition_rhs) |
159 apply (drule partition_gt, assumption) |
158 apply (drule partition_gt[of _ _ _ 0], arith) |
160 apply (simp (no_asm_simp)) |
159 apply (simp (no_asm_simp)) |
161 done |
160 done |
162 |
161 |
163 lemma partition_ub: "partition(a,b) D ==> D(r) \<le> b" |
162 lemma partition_ub: "partition(a,b) D ==> D(r) \<le> b" |
164 apply (frule partition [THEN iffD1]) |
163 apply (frule partition [THEN iffD1]) |