equal
deleted
inserted
replaced
607 apply safe |
607 apply safe |
608 apply (case_tac m) |
608 apply (case_tac m) |
609 apply (auto simp: Bit_B0_2t [symmetric]) |
609 apply (auto simp: Bit_B0_2t [symmetric]) |
610 done |
610 done |
611 |
611 |
612 (*for use when simplifying with bin_nth_Bit*) |
612 \<comment> \<open>for use when simplifying with \<open>bin_nth_Bit\<close>\<close> |
613 lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)" |
613 lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)" |
614 by auto |
614 by auto |
615 |
615 |
616 lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT True" |
616 lemma power_BIT: "2 ^ (Suc n) - 1 = (2 ^ n - 1) BIT True" |
617 by (induct n) (simp_all add: Bit_B1) |
617 by (induct n) (simp_all add: Bit_B1) |