equal
deleted
inserted
replaced
115 lemma bin_to_bl_aux_Bit1_minus_simp [simp]: |
115 lemma bin_to_bl_aux_Bit1_minus_simp [simp]: |
116 "0 < n \<Longrightarrow> |
116 "0 < n \<Longrightarrow> |
117 bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)" |
117 bin_to_bl_aux n (numeral (Num.Bit1 w)) bl = bin_to_bl_aux (n - 1) (numeral w) (True # bl)" |
118 by (cases n) auto |
118 by (cases n) auto |
119 |
119 |
120 text \<open>Link between bin and bool list.\<close> |
120 text \<open>Link between \<open>bin\<close> and \<open>bool list\<close>.\<close> |
121 |
121 |
122 lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)" |
122 lemma bl_to_bin_aux_append: "bl_to_bin_aux (bs @ cs) w = bl_to_bin_aux cs (bl_to_bin_aux bs w)" |
123 by (induct bs arbitrary: w) auto |
123 by (induct bs arbitrary: w) auto |
124 |
124 |
125 lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)" |
125 lemma bin_to_bl_aux_append: "bin_to_bl_aux n w bs @ cs = bin_to_bl_aux n w (bs @ cs)" |
236 lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)" |
236 lemma bl_sbin_sign: "hd (bin_to_bl (Suc n) w) = (bin_sign (sbintrunc n w) = -1)" |
237 unfolding bin_to_bl_def by (rule bl_sbin_sign_aux) |
237 unfolding bin_to_bl_def by (rule bl_sbin_sign_aux) |
238 |
238 |
239 lemma bin_nth_of_bl_aux: |
239 lemma bin_nth_of_bl_aux: |
240 "bin_nth (bl_to_bin_aux bl w) n = |
240 "bin_nth (bl_to_bin_aux bl w) n = |
241 (n < size bl \<and> rev bl ! n | n \<ge> length bl \<and> bin_nth w (n - size bl))" |
241 (n < size bl \<and> rev bl ! n \<or> n \<ge> length bl \<and> bin_nth w (n - size bl))" |
242 apply (induct bl arbitrary: w) |
242 apply (induct bl arbitrary: w) |
243 apply clarsimp |
243 apply clarsimp |
244 apply clarsimp |
244 apply clarsimp |
245 apply (cut_tac x=n and y="size bl" in linorder_less_linear) |
245 apply (cut_tac x=n and y="size bl" in linorder_less_linear) |
246 apply (erule disjE, simp add: nth_append)+ |
246 apply (erule disjE, simp add: nth_append)+ |
296 lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)" |
296 lemma bl_to_bin_lt2p_drop: "bl_to_bin bs < 2 ^ length (dropWhile Not bs)" |
297 proof (induct bs) |
297 proof (induct bs) |
298 case Nil |
298 case Nil |
299 then show ?case by simp |
299 then show ?case by simp |
300 next |
300 next |
301 case (Cons b bs) with bl_to_bin_lt2p_aux[where w=1] |
301 case (Cons b bs) |
302 show ?case unfolding bl_to_bin_def by simp |
302 with bl_to_bin_lt2p_aux[where w=1] show ?case |
|
303 by (simp add: bl_to_bin_def) |
303 qed |
304 qed |
304 |
305 |
305 lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs" |
306 lemma bl_to_bin_lt2p: "bl_to_bin bs < 2 ^ length bs" |
306 by (metis bin_bl_bin bintr_lt2p bl_bin_bl) |
307 by (metis bin_bl_bin bintr_lt2p bl_bin_bl) |
307 |
308 |
507 by (induct m arbitrary: l n) (auto split: list.split) |
508 by (induct m arbitrary: l n) (auto split: list.split) |
508 |
509 |
509 lemma length_takefill [simp]: "length (takefill fill n l) = n" |
510 lemma length_takefill [simp]: "length (takefill fill n l) = n" |
510 by (simp add: takefill_alt) |
511 by (simp add: takefill_alt) |
511 |
512 |
512 lemma take_takefill': "\<And>w n. n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w" |
513 lemma take_takefill': "n = k + m \<Longrightarrow> take k (takefill fill n w) = takefill fill k w" |
513 by (induct k) (auto split: list.split) |
514 by (induct k arbitrary: w n) (auto split: list.split) |
514 |
515 |
515 lemma drop_takefill: "\<And>w. drop k (takefill fill (m + k) w) = takefill fill m (drop k w)" |
516 lemma drop_takefill: "drop k (takefill fill (m + k) w) = takefill fill m (drop k w)" |
516 by (induct k) (auto split: list.split) |
517 by (induct k arbitrary: w) (auto split: list.split) |
517 |
518 |
518 lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l" |
519 lemma takefill_le [simp]: "m \<le> n \<Longrightarrow> takefill x m (takefill x n l) = takefill x m l" |
519 by (auto simp: le_iff_add takefill_le') |
520 by (auto simp: le_iff_add takefill_le') |
520 |
521 |
521 lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w" |
522 lemma take_takefill [simp]: "m \<le> n \<Longrightarrow> take m (takefill fill n w) = takefill fill m w" |
713 apply (case_tac blb, clarsimp) |
714 apply (case_tac blb, clarsimp) |
714 apply (clarsimp simp: Let_def) |
715 apply (clarsimp simp: Let_def) |
715 done |
716 done |
716 |
717 |
717 lemma rbl_add_take2: |
718 lemma rbl_add_take2: |
718 "length blb >= length bla ==> rbl_add bla (take (length bla) blb) = rbl_add bla blb" |
719 "length blb \<ge> length bla \<Longrightarrow> rbl_add bla (take (length bla) blb) = rbl_add bla blb" |
719 apply (induct bla arbitrary: blb) |
720 apply (induct bla arbitrary: blb) |
720 apply simp |
721 apply simp |
721 apply clarsimp |
722 apply clarsimp |
722 apply (case_tac blb, clarsimp) |
723 apply (case_tac blb, clarsimp) |
723 apply (clarsimp simp: Let_def) |
724 apply (clarsimp simp: Let_def) |
1021 proof (cases "m = 0") |
1022 proof (cases "m = 0") |
1022 case True |
1023 case True |
1023 with \<open>length bs = length cs\<close> show ?thesis by simp |
1024 with \<open>length bs = length cs\<close> show ?thesis by simp |
1024 next |
1025 next |
1025 case False |
1026 case False |
1026 from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow> |
1027 from "1.hyps" \<open>m \<noteq> 0\<close> \<open>n \<noteq> 0\<close> |
|
1028 have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow> |
1027 length (bin_rsplit_aux n (m - n) v bs) = |
1029 length (bin_rsplit_aux n (m - n) v bs) = |
1028 length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))" |
1030 length (bin_rsplit_aux n (m - n) (fst (bin_split n w)) (snd (bin_split n w) # cs))" |
1029 by auto |
1031 by auto |
1030 from \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close> show ?thesis |
1032 from \<open>length bs = length cs\<close> \<open>n \<noteq> 0\<close> show ?thesis |
1031 by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len split: prod.split) |
1033 by (auto simp add: bin_rsplit_aux_simp_alt Let_def bin_rsplit_len split: prod.split) |