1060 done |
1060 done |
1061 |
1061 |
1062 lemma bin_rsplit_aux_len_le [rule_format] : |
1062 lemma bin_rsplit_aux_len_le [rule_format] : |
1063 "\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow> |
1063 "\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow> |
1064 length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n" |
1064 length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n" |
1065 apply (induct n nw w bs rule: bin_rsplit_aux.induct) |
1065 proof - |
1066 apply (subst bin_rsplit_aux.simps) |
1066 { fix i j j' k k' m :: nat and R |
1067 apply (simp add: lrlem Let_def split: prod.split) |
1067 assume d: "(i::nat) \<le> j \<or> m < j'" |
1068 done |
1068 assume R1: "i * k \<le> j * k \<Longrightarrow> R" |
|
1069 assume R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R" |
|
1070 have "R" using d |
|
1071 apply safe |
|
1072 apply (rule R1, erule mult_le_mono1) |
|
1073 apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]]) |
|
1074 done |
|
1075 } note A = this |
|
1076 { fix sc m n lb :: nat |
|
1077 have "(0::nat) < sc \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n \<longleftrightarrow> sc + lb * n \<le> m * n" |
|
1078 apply safe |
|
1079 apply arith |
|
1080 apply (case_tac "sc >= n") |
|
1081 apply arith |
|
1082 apply (insert linorder_le_less_linear [of m lb]) |
|
1083 apply (erule_tac k2=n and k'2=n in A) |
|
1084 apply arith |
|
1085 apply simp |
|
1086 done |
|
1087 } note B = this |
|
1088 show ?thesis |
|
1089 apply (induct n nw w bs rule: bin_rsplit_aux.induct) |
|
1090 apply (subst bin_rsplit_aux.simps) |
|
1091 apply (simp add: B Let_def split: prod.split) |
|
1092 done |
|
1093 qed |
1069 |
1094 |
1070 lemma bin_rsplit_len_le: |
1095 lemma bin_rsplit_len_le: |
1071 "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)" |
1096 "n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)" |
1072 unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le) |
1097 unfolding bin_rsplit_def by (clarsimp simp add : bin_rsplit_aux_len_le) |
1073 |
1098 |