equal
deleted
inserted
replaced
906 |
906 |
907 lemma not_bit_length [simp]: |
907 lemma not_bit_length [simp]: |
908 \<open>\<not> bit w LENGTH('a)\<close> for w :: \<open>'a::len word\<close> |
908 \<open>\<not> bit w LENGTH('a)\<close> for w :: \<open>'a::len word\<close> |
909 by transfer simp |
909 by transfer simp |
910 |
910 |
|
911 lemma finite_bit_word [simp]: |
|
912 \<open>finite {n. bit w n}\<close> |
|
913 for w :: \<open>'a::len word\<close> |
|
914 proof - |
|
915 have \<open>{n. bit w n} \<subseteq> {0..LENGTH('a)}\<close> |
|
916 by (auto dest: bit_imp_le_length) |
|
917 moreover have \<open>finite {0..LENGTH('a)}\<close> |
|
918 by simp |
|
919 ultimately show ?thesis |
|
920 by (rule finite_subset) |
|
921 qed |
|
922 |
911 instantiation word :: (len) semiring_bit_shifts |
923 instantiation word :: (len) semiring_bit_shifts |
912 begin |
924 begin |
913 |
925 |
914 lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> |
926 lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close> |
915 is push_bit |
927 is push_bit |