equal
deleted
inserted
replaced
15 \<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)) |
15 \<Longrightarrow> (\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)) |
16 \<Longrightarrow> P a\<close> |
16 \<Longrightarrow> P a\<close> |
17 assumes half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close> |
17 assumes half_div_exp_eq: \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close> |
18 and even_double_div_exp_iff: \<open>2 ^ Suc n \<noteq> 0 \<Longrightarrow> even (2 * a div 2 ^ Suc n) \<longleftrightarrow> even (a div 2 ^ n)\<close> |
18 and even_double_div_exp_iff: \<open>2 ^ Suc n \<noteq> 0 \<Longrightarrow> even (2 * a div 2 ^ Suc n) \<longleftrightarrow> even (a div 2 ^ n)\<close> |
19 and even_decr_exp_div_exp_iff: \<open>2 ^ n \<noteq> 0 \<Longrightarrow> even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close> |
19 and even_decr_exp_div_exp_iff: \<open>2 ^ n \<noteq> 0 \<Longrightarrow> even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> m \<le> n\<close> |
20 and even_mod_exp_diff_exp_iff: \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close> |
20 and even_mod_exp_div_exp_iff: \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close> |
21 fixes bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close> |
21 fixes bit :: \<open>'a \<Rightarrow> nat \<Rightarrow> bool\<close> |
22 assumes bit_iff_odd: \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close> |
22 assumes bit_iff_odd: \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close> |
23 begin |
23 begin |
24 |
24 |
25 text \<open> |
25 text \<open> |
78 \<open>bit a n \<longleftrightarrow> odd a\<close> |
78 \<open>bit a n \<longleftrightarrow> odd a\<close> |
79 by (induction n) (simp_all add: stable bit_Suc bit_0) |
79 by (induction n) (simp_all add: stable bit_Suc bit_0) |
80 |
80 |
81 end |
81 end |
82 |
82 |
83 lemma bit_iff_idd_imp_stable: |
83 lemma bit_iff_odd_imp_stable: |
84 \<open>a div 2 = a\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> odd a\<close> |
84 \<open>a div 2 = a\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> odd a\<close> |
85 using that proof (induction a rule: bit_induct) |
85 using that proof (induction a rule: bit_induct) |
86 case (stable a) |
86 case (stable a) |
87 then show ?case |
87 then show ?case |
88 by simp |
88 by simp |
180 then show ?thesis proof (induction a arbitrary: b rule: bit_induct) |
180 then show ?thesis proof (induction a arbitrary: b rule: bit_induct) |
181 case (stable a) |
181 case (stable a) |
182 from stable(2) [of 0] have **: \<open>even b \<longleftrightarrow> even a\<close> |
182 from stable(2) [of 0] have **: \<open>even b \<longleftrightarrow> even a\<close> |
183 by (simp add: bit_0) |
183 by (simp add: bit_0) |
184 have \<open>b div 2 = b\<close> |
184 have \<open>b div 2 = b\<close> |
185 proof (rule bit_iff_idd_imp_stable) |
185 proof (rule bit_iff_odd_imp_stable) |
186 fix n |
186 fix n |
187 from stable have *: \<open>bit b n \<longleftrightarrow> bit a n\<close> |
187 from stable have *: \<open>bit b n \<longleftrightarrow> bit a n\<close> |
188 by simp |
188 by simp |
189 also have \<open>bit a n \<longleftrightarrow> odd a\<close> |
189 also have \<open>bit a n \<longleftrightarrow> odd a\<close> |
190 using stable by (simp add: stable_imp_bit_iff_odd) |
190 using stable by (simp add: stable_imp_bit_iff_odd) |
868 "take_bit 0 a = 0" |
868 "take_bit 0 a = 0" |
869 by (simp add: take_bit_eq_mod) |
869 by (simp add: take_bit_eq_mod) |
870 |
870 |
871 lemma bit_take_bit_iff [bit_simps]: |
871 lemma bit_take_bit_iff [bit_simps]: |
872 \<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close> |
872 \<open>bit (take_bit m a) n \<longleftrightarrow> n < m \<and> bit a n\<close> |
873 by (simp add: take_bit_eq_mod bit_iff_odd even_mod_exp_diff_exp_iff not_le) |
873 by (simp add: take_bit_eq_mod bit_iff_odd even_mod_exp_div_exp_iff not_le) |
874 |
874 |
875 lemma take_bit_Suc: |
875 lemma take_bit_Suc: |
876 \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2\<close> (is \<open>?lhs = ?rhs\<close>) |
876 \<open>take_bit (Suc n) a = take_bit n (a div 2) * 2 + a mod 2\<close> (is \<open>?lhs = ?rhs\<close>) |
877 proof (rule bit_eqI) |
877 proof (rule bit_eqI) |
878 fix m |
878 fix m |