algebraic embeddings for bit operations

--- a/src/HOL/Code_Numeral.thy	Thu Apr 19 21:54:46 2018 +0200
+++ b/src/HOL/Code_Numeral.thy	Fri Apr 20 07:36:58 2018 +0000
@@ -82,11 +82,15 @@
   unfolding dvd_def by transfer_prover
 
 lemma [transfer_rule]:
-  "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
+  "rel_fun (=) pcr_integer (of_bool :: bool \<Rightarrow> int) (of_bool :: bool \<Rightarrow> integer)"
+  by (unfold of_bool_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+  "rel_fun (=) pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
   by (rule transfer_rule_of_nat) transfer_prover+
 
 lemma [transfer_rule]:
-  "rel_fun HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
+  "rel_fun (=) pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
 proof -
   have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
     by (rule transfer_rule_of_int) transfer_prover+
@@ -101,6 +105,10 @@
   "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
   by (unfold Num.sub_def [abs_def]) transfer_prover
 
+lemma [transfer_rule]:
+  "rel_fun pcr_integer (rel_fun (=) pcr_integer) (power :: _ \<Rightarrow> _ \<Rightarrow> int) (power :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  by (unfold power_def [abs_def]) transfer_prover
+
 lemma int_of_integer_of_nat [simp]:
   "int_of_integer (of_nat n) = of_nat n"
   by transfer rule
@@ -265,6 +273,18 @@
 instance integer :: ring_parity
   by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def)
 
+lemma [transfer_rule]:
+  "rel_fun (=) (rel_fun pcr_integer pcr_integer) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  by (unfold push_bit_eq_mult [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+  "rel_fun (=) (rel_fun pcr_integer pcr_integer) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  by (unfold take_bit_eq_mod [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+  "rel_fun (=) (rel_fun pcr_integer pcr_integer) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  by (unfold drop_bit_eq_div [abs_def]) transfer_prover
+
 instantiation integer :: unique_euclidean_semiring_numeral
 begin
 
@@ -313,6 +333,7 @@
   "integer_of_nat (numeral n) = numeral n"
 by transfer simp
 
+
 subsection \<open>Code theorems for target language integers\<close>
 
 text \<open>Constructors\<close>
@@ -777,6 +798,10 @@
   unfolding dvd_def by transfer_prover
 
 lemma [transfer_rule]:
+  "rel_fun (=) pcr_natural (of_bool :: bool \<Rightarrow> nat) (of_bool :: bool \<Rightarrow> natural)"
+  by (unfold of_bool_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
   "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
 proof -
   have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
@@ -792,6 +817,10 @@
   then show ?thesis by simp
 qed
 
+lemma [transfer_rule]:
+  "rel_fun pcr_natural (rel_fun (=) pcr_natural) (power :: _ \<Rightarrow> _ \<Rightarrow> nat) (power :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+  by (unfold power_def [abs_def]) transfer_prover
+
 lemma nat_of_natural_of_nat [simp]:
   "nat_of_natural (of_nat n) = n"
   by transfer rule
@@ -895,6 +924,18 @@
 instance natural :: semiring_parity
   by (standard; transfer) simp_all
 
+lemma [transfer_rule]:
+  "rel_fun (=) (rel_fun pcr_natural pcr_natural) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+  by (unfold push_bit_eq_mult [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+  "rel_fun (=) (rel_fun pcr_natural pcr_natural) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+  by (unfold take_bit_eq_mod [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+  "rel_fun (=) (rel_fun pcr_natural pcr_natural) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"
+  by (unfold drop_bit_eq_div [abs_def]) transfer_prover
+
 lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
   is "nat :: int \<Rightarrow> nat"
   .

--- a/src/HOL/Parity.thy	Thu Apr 19 21:54:46 2018 +0200
+++ b/src/HOL/Parity.thy	Fri Apr 20 07:36:58 2018 +0000
@@ -689,10 +689,10 @@
   where push_bit_eq_mult: "push_bit n a = a * 2 ^ n"
  
 definition take_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
-  where take_bit_eq_mod: "take_bit n a = a mod of_nat (2 ^ n)"
+  where take_bit_eq_mod: "take_bit n a = a mod 2 ^ n"
 
 definition drop_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
-  where drop_bit_eq_div: "drop_bit n a = a div of_nat (2 ^ n)"
+  where drop_bit_eq_div: "drop_bit n a = a div 2 ^ n"
 
 lemma bit_ident:
   "push_bit n (drop_bit n a) + take_bit n a = a"
@@ -807,6 +807,10 @@
   "push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))"
   by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric]) (simp add: ac_simps)
 
+lemma push_bit_of_nat:
+  "push_bit n (of_nat m) = of_nat (push_bit n m)"
+  by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult)
+
 lemma take_bit_0 [simp]:
   "take_bit 0 a = 0"
   by (simp add: take_bit_eq_mod)
@@ -858,6 +862,10 @@
   by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] take_bit_Suc
     ac_simps even_add even_mult_iff div_mult_self1 [OF numeral_neq_zero]) (simp add: ac_simps)
 
+lemma take_bit_of_nat:
+  "take_bit n (of_nat m) = of_nat (take_bit n m)"
+  by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"])
+
 lemma drop_bit_0 [simp]:
   "drop_bit 0 = id"
   by (simp add: fun_eq_iff drop_bit_eq_div)
@@ -907,6 +915,10 @@
   by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] drop_bit_Suc
     div_mult_self4 [OF numeral_neq_zero]) simp
 
+lemma drop_bit_of_nat:
+  "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
+	by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
+
 end
 
 lemma push_bit_of_Suc_0 [simp]: