3525 (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)))" |
3525 (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)))" |
3526 apply (unfold word_split_bin') |
3526 apply (unfold word_split_bin') |
3527 apply safe |
3527 apply safe |
3528 defer |
3528 defer |
3529 apply (clarsimp split: prod.splits) |
3529 apply (clarsimp split: prod.splits) |
|
3530 apply (metis bintrunc_eq_take_bit of_bl_drop' ucast_bl ucast_def word_size word_size_bl word_ubin.Abs_norm) |
3530 apply hypsubst_thin |
3531 apply hypsubst_thin |
3531 apply (drule word_ubin.norm_Rep [THEN ssubst]) |
3532 apply (drule word_ubin.norm_Rep [THEN ssubst]) |
3532 apply (drule split_bintrunc) |
|
3533 apply (simp add: of_bl_def bl2bin_drop word_size |
3533 apply (simp add: of_bl_def bl2bin_drop word_size |
3534 word_ubin.norm_eq_iff [symmetric] min_def del: word_ubin.norm_Rep) |
3534 word_ubin.norm_eq_iff [symmetric] min_def del: word_ubin.norm_Rep) |
3535 apply (clarsimp split: prod.splits) |
3535 apply (clarsimp split: prod.splits) |
3536 apply (frule split_uint_lem [THEN conjunct1]) |
|
3537 apply (unfold word_size) |
|
3538 apply (cases "LENGTH('a) \<ge> LENGTH('b)") |
3536 apply (cases "LENGTH('a) \<ge> LENGTH('b)") |
3539 defer |
3537 apply (simp_all add: not_le) |
3540 apply simp |
3538 defer |
|
3539 apply (simp add: drop_bit_eq_div lt2p_lem) |
3541 apply (simp add : of_bl_def to_bl_def) |
3540 apply (simp add : of_bl_def to_bl_def) |
3542 apply (subst bin_split_take1 [symmetric]) |
3541 apply (subst bin_to_bl_drop_bit [symmetric]) |
3543 prefer 2 |
3542 apply (subst diff_add) |
3544 apply assumption |
3543 apply (simp_all add: bintrunc_eq_take_bit take_bit_drop_bit) |
3545 apply simp |
3544 apply (simp add: take_bit_eq_mod) |
3546 apply (erule thin_rl) |
|
3547 apply (erule arg_cong [THEN trans]) |
|
3548 apply (simp add : word_ubin.norm_eq_iff [symmetric]) |
|
3549 done |
3545 done |
3550 |
3546 |
3551 lemma word_split_bl: "std = size c - size b \<Longrightarrow> |
3547 lemma word_split_bl: "std = size c - size b \<Longrightarrow> |
3552 (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow> |
3548 (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow> |
3553 word_split c = (a, b)" |
3549 word_split c = (a, b)" |
3577 b !! n = (n < size b \<and> c !! n) \<and> |
3573 b !! n = (n < size b \<and> c !! n) \<and> |
3578 a !! m = (m < size a \<and> c !! (m + size b)))" |
3574 a !! m = (m < size a \<and> c !! (m + size b)))" |
3579 apply (unfold word_split_bin' test_bit_bin) |
3575 apply (unfold word_split_bin' test_bit_bin) |
3580 apply (clarify) |
3576 apply (clarify) |
3581 apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits) |
3577 apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits) |
3582 apply (drule bin_nth_split) |
3578 apply (auto simp add: bin_nth_iff bit_take_bit_iff bit_drop_bit_eq ac_simps bin_nth_uint_imp) |
3583 apply safe |
|
3584 apply (simp_all add: add.commute) |
|
3585 apply (erule bin_nth_uint_imp)+ |
|
3586 done |
3579 done |
3587 |
3580 |
3588 lemma test_bit_split: |
3581 lemma test_bit_split: |
3589 "word_split c = (a, b) \<Longrightarrow> |
3582 "word_split c = (a, b) \<Longrightarrow> |
3590 (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and> |
3583 (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and> |