equal
deleted
inserted
replaced
346 |
346 |
347 lift_definition take_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close> |
347 lift_definition take_bit_integer :: \<open>nat \<Rightarrow> integer \<Rightarrow> integer\<close> |
348 is take_bit . |
348 is take_bit . |
349 |
349 |
350 instance by (standard; transfer) |
350 instance by (standard; transfer) |
351 (fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod |
351 (fact bit_eq_rec bit_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod |
352 bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2 |
352 bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2 |
353 exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq |
353 exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq |
354 even_mask_div_iff even_mult_exp_div_exp_iff |
354 even_mask_div_iff even_mult_exp_div_exp_iff |
355 and_rec or_rec xor_rec mask_eq_exp_minus_1 |
355 and_rec or_rec xor_rec mask_eq_exp_minus_1 |
356 set_bit_def unset_bit_0 unset_bit_Suc flip_bit_def not_eq_complement)+ |
356 set_bit_def unset_bit_0 unset_bit_Suc flip_bit_def not_eq_complement)+ |
1105 |
1105 |
1106 lift_definition take_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close> |
1106 lift_definition take_bit_natural :: \<open>nat \<Rightarrow> natural \<Rightarrow> natural\<close> |
1107 is take_bit . |
1107 is take_bit . |
1108 |
1108 |
1109 instance by (standard; transfer) |
1109 instance by (standard; transfer) |
1110 (fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod |
1110 (fact bit_eq_rec bit_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod |
1111 bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2 |
1111 bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2 |
1112 exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq |
1112 exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq |
1113 even_mask_div_iff even_mult_exp_div_exp_iff and_rec or_rec xor_rec |
1113 even_mask_div_iff even_mult_exp_div_exp_iff and_rec or_rec xor_rec |
1114 mask_eq_exp_minus_1 set_bit_def unset_bit_0 unset_bit_Suc flip_bit_def)+ |
1114 mask_eq_exp_minus_1 set_bit_def unset_bit_0 unset_bit_Suc flip_bit_def)+ |
1115 |
1115 |