1097 apply clarsimp |
1097 apply clarsimp |
1098 apply (clarsimp simp add: bin_split_cat rsplit_aux_alts) |
1098 apply (clarsimp simp add: bin_split_cat rsplit_aux_alts) |
1099 done |
1099 done |
1100 |
1100 |
1101 lemma bin_rsplit_aux_len_le [rule_format] : |
1101 lemma bin_rsplit_aux_len_le [rule_format] : |
1102 "ALL ws m. n > 0 --> ws = bin_rsplit_aux (n, bs, nw, w) --> |
1102 "ALL ws m. n \<noteq> 0 --> ws = bin_rsplit_aux (n, bs, nw, w) --> |
1103 (length ws <= m) = (nw + length bs * n <= m * n)" |
1103 (length ws <= m) = (nw + length bs * n <= m * n)" |
1104 apply (rule_tac u=n and v=bs and w=nw and x=w in bin_rsplit_aux.induct) |
1104 apply (rule_tac u=n and v=bs and w=nw and x=w in bin_rsplit_aux.induct) |
1105 apply (subst bin_rsplit_aux.simps) |
1105 apply (subst bin_rsplit_aux.simps) |
1106 apply (clarsimp simp: Let_def neq0_conv split: ls_splits ) |
1106 apply (simp add:lrlem Let_def split: ls_splits ) |
1107 apply (erule lrlem) |
|
1108 done |
1107 done |
1109 |
1108 |
1110 lemma bin_rsplit_len_le: |
1109 lemma bin_rsplit_len_le: |
1111 "n > 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)" |
1110 "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)" |
1112 unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le) |
1111 unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le) |
1113 |
1112 |
1114 lemma bin_rsplit_aux_len [rule_format] : |
1113 lemma bin_rsplit_aux_len [rule_format] : |
1115 "0 < n --> length (bin_rsplit_aux (n, cs, nw, w)) = |
1114 "n\<noteq>0 --> length (bin_rsplit_aux (n, cs, nw, w)) = |
1116 (nw + n - 1) div n + length cs" |
1115 (nw + n - 1) div n + length cs" |
1117 apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct) |
1116 apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct) |
1118 apply (subst bin_rsplit_aux.simps) |
1117 apply (subst bin_rsplit_aux.simps) |
1119 apply (clarsimp simp: Let_def split: ls_splits) |
1118 apply (clarsimp simp: Let_def split: ls_splits) |
1120 apply (erule thin_rl) |
1119 apply (erule thin_rl) |
1124 apply (case_tac m, clarsimp) |
1123 apply (case_tac m, clarsimp) |
1125 apply (simp add: div_add_self2) |
1124 apply (simp add: div_add_self2) |
1126 done |
1125 done |
1127 |
1126 |
1128 lemma bin_rsplit_len: |
1127 lemma bin_rsplit_len: |
1129 "0 < n ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n" |
1128 "n\<noteq>0 ==> length (bin_rsplit n (nw, w)) = (nw + n - 1) div n" |
1130 unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len) |
1129 unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len) |
1131 |
1130 |
1132 lemma bin_rsplit_aux_len_indep [rule_format] : |
1131 lemma bin_rsplit_aux_len_indep [rule_format] : |
1133 "0 < n ==> (ALL v bs. length bs = length cs --> |
1132 "n\<noteq>0 ==> (ALL v bs. length bs = length cs --> |
1134 length (bin_rsplit_aux (n, bs, nw, v)) = |
1133 length (bin_rsplit_aux (n, bs, nw, v)) = |
1135 length (bin_rsplit_aux (n, cs, nw, w)))" |
1134 length (bin_rsplit_aux (n, cs, nw, w)))" |
1136 apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct) |
1135 apply (rule_tac u=n and v=cs and w=nw and x=w in bin_rsplit_aux.induct) |
1137 apply clarsimp |
1136 apply clarsimp |
1138 apply (simp (no_asm_simp) add: bin_rsplit_aux_simp_alt Let_def |
1137 apply (simp (no_asm_simp) add: bin_rsplit_aux_simp_alt Let_def |
1146 apply (rule_tac x="ba # bs" in exI) |
1145 apply (rule_tac x="ba # bs" in exI) |
1147 apply auto |
1146 apply auto |
1148 done |
1147 done |
1149 |
1148 |
1150 lemma bin_rsplit_len_indep: |
1149 lemma bin_rsplit_len_indep: |
1151 "0 < n ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))" |
1150 "n\<noteq>0 ==> length (bin_rsplit n (nw, v)) = length (bin_rsplit n (nw, w))" |
1152 apply (unfold bin_rsplit_def) |
1151 apply (unfold bin_rsplit_def) |
1153 apply (erule bin_rsplit_aux_len_indep) |
1152 apply (erule bin_rsplit_aux_len_indep) |
1154 apply (rule refl) |
1153 apply (rule refl) |
1155 done |
1154 done |
1156 |
1155 |