equal
deleted
inserted
replaced
739 [symmetric, folded word_number_of_def, standard] |
739 [symmetric, folded word_number_of_def, standard] |
740 lemmas sbintr_num = word_sbin.norm_eq_iff |
740 lemmas sbintr_num = word_sbin.norm_eq_iff |
741 [symmetric, folded word_number_of_def, standard] |
741 [symmetric, folded word_number_of_def, standard] |
742 |
742 |
743 lemmas num_of_bintr = word_ubin.Abs_norm [folded word_number_of_def, standard] |
743 lemmas num_of_bintr = word_ubin.Abs_norm [folded word_number_of_def, standard] |
744 lemmas num_of_sbintr = word_sbin.Abs_norm [folded word_number_of_def, standard]; |
744 lemmas num_of_sbintr = word_sbin.Abs_norm [folded word_number_of_def, standard] |
745 |
745 |
746 (* don't add these to simpset, since may want bintrunc n w to be simplified; |
746 (* don't add these to simpset, since may want bintrunc n w to be simplified; |
747 may want these in reverse, but loop as simp rules, so use following *) |
747 may want these in reverse, but loop as simp rules, so use following *) |
748 |
748 |
749 lemma num_of_bintr': |
749 lemma num_of_bintr': |
1350 lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y" |
1350 lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y" |
1351 unfolding dvd_def udvd_nat_alt by force |
1351 unfolding dvd_def udvd_nat_alt by force |
1352 |
1352 |
1353 lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard] |
1353 lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard] |
1354 |
1354 |
1355 lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1"; |
1355 lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1" |
1356 unfolding word_arith_wis |
1356 unfolding word_arith_wis |
1357 by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc) |
1357 by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc) |
1358 |
1358 |
1359 lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one] |
1359 lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one] |
1360 |
1360 |
1659 apply (unfold udvd_def) |
1659 apply (unfold udvd_def) |
1660 apply clarify |
1660 apply clarify |
1661 apply (erule (2) udvd_decr0) |
1661 apply (erule (2) udvd_decr0) |
1662 done |
1662 done |
1663 |
1663 |
1664 ML {* Delsimprocs Numeral_Simprocs.cancel_factors *} |
1664 ML {* Delsimprocs [@{simproc linordered_ring_less_cancel_factor}] *} |
1665 |
1665 |
1666 lemma udvd_incr2_K: |
1666 lemma udvd_incr2_K: |
1667 "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow> |
1667 "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow> |
1668 0 < K \<Longrightarrow> p <= p + K & p + K <= a + s" |
1668 0 < K \<Longrightarrow> p <= p + K & p + K <= a + s" |
1669 apply (unfold udvd_def) |
1669 apply (unfold udvd_def) |
1677 apply (drule less_le_mult) |
1677 apply (drule less_le_mult) |
1678 apply arith |
1678 apply arith |
1679 apply simp |
1679 apply simp |
1680 done |
1680 done |
1681 |
1681 |
1682 ML {* Addsimprocs Numeral_Simprocs.cancel_factors *} |
1682 ML {* Addsimprocs [@{simproc linordered_ring_less_cancel_factor}] *} |
1683 |
1683 |
1684 (* links with rbl operations *) |
1684 (* links with rbl operations *) |
1685 lemma word_succ_rbl: |
1685 lemma word_succ_rbl: |
1686 "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))" |
1686 "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))" |
1687 apply (unfold word_succ_def) |
1687 apply (unfold word_succ_def) |