algebraic embeddings for bit operations
authorhaftmann
Fri Apr 20 07:36:58 2018 +0000 (14 months ago)
changeset 680103f223b9a0066
parent 68009 72e1d5da30c6
child 68011 fb6469cdf094
algebraic embeddings for bit operations
src/HOL/Code_Numeral.thy
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Apr 19 21:54:46 2018 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Apr 20 07:36:58 2018 +0000
     1.3 @@ -82,11 +82,15 @@
     1.4    unfolding dvd_def by transfer_prover
     1.5  
     1.6  lemma [transfer_rule]:
     1.7 -  "rel_fun HOL.eq pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
     1.8 +  "rel_fun (=) pcr_integer (of_bool :: bool \<Rightarrow> int) (of_bool :: bool \<Rightarrow> integer)"
     1.9 +  by (unfold of_bool_def [abs_def]) transfer_prover
    1.10 +
    1.11 +lemma [transfer_rule]:
    1.12 +  "rel_fun (=) pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
    1.13    by (rule transfer_rule_of_nat) transfer_prover+
    1.14  
    1.15  lemma [transfer_rule]:
    1.16 -  "rel_fun HOL.eq pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
    1.17 +  "rel_fun (=) pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
    1.18  proof -
    1.19    have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
    1.20      by (rule transfer_rule_of_int) transfer_prover+
    1.21 @@ -101,6 +105,10 @@
    1.22    "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    1.23    by (unfold Num.sub_def [abs_def]) transfer_prover
    1.24  
    1.25 +lemma [transfer_rule]:
    1.26 +  "rel_fun pcr_integer (rel_fun (=) pcr_integer) (power :: _ \<Rightarrow> _ \<Rightarrow> int) (power :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    1.27 +  by (unfold power_def [abs_def]) transfer_prover
    1.28 +
    1.29  lemma int_of_integer_of_nat [simp]:
    1.30    "int_of_integer (of_nat n) = of_nat n"
    1.31    by transfer rule
    1.32 @@ -265,6 +273,18 @@
    1.33  instance integer :: ring_parity
    1.34    by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def)
    1.35  
    1.36 +lemma [transfer_rule]:
    1.37 +  "rel_fun (=) (rel_fun pcr_integer pcr_integer) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    1.38 +  by (unfold push_bit_eq_mult [abs_def]) transfer_prover
    1.39 +
    1.40 +lemma [transfer_rule]:
    1.41 +  "rel_fun (=) (rel_fun pcr_integer pcr_integer) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    1.42 +  by (unfold take_bit_eq_mod [abs_def]) transfer_prover
    1.43 +
    1.44 +lemma [transfer_rule]:
    1.45 +  "rel_fun (=) (rel_fun pcr_integer pcr_integer) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"
    1.46 +  by (unfold drop_bit_eq_div [abs_def]) transfer_prover
    1.47 +
    1.48  instantiation integer :: unique_euclidean_semiring_numeral
    1.49  begin
    1.50  
    1.51 @@ -313,6 +333,7 @@
    1.52    "integer_of_nat (numeral n) = numeral n"
    1.53  by transfer simp
    1.54  
    1.55 +
    1.56  subsection \<open>Code theorems for target language integers\<close>
    1.57  
    1.58  text \<open>Constructors\<close>
    1.59 @@ -777,6 +798,10 @@
    1.60    unfolding dvd_def by transfer_prover
    1.61  
    1.62  lemma [transfer_rule]:
    1.63 +  "rel_fun (=) pcr_natural (of_bool :: bool \<Rightarrow> nat) (of_bool :: bool \<Rightarrow> natural)"
    1.64 +  by (unfold of_bool_def [abs_def]) transfer_prover
    1.65 +
    1.66 +lemma [transfer_rule]:
    1.67    "rel_fun HOL.eq pcr_natural (\<lambda>n::nat. n) (of_nat :: nat \<Rightarrow> natural)"
    1.68  proof -
    1.69    have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
    1.70 @@ -792,6 +817,10 @@
    1.71    then show ?thesis by simp
    1.72  qed
    1.73  
    1.74 +lemma [transfer_rule]:
    1.75 +  "rel_fun pcr_natural (rel_fun (=) pcr_natural) (power :: _ \<Rightarrow> _ \<Rightarrow> nat) (power :: _ \<Rightarrow> _ \<Rightarrow> natural)"
    1.76 +  by (unfold power_def [abs_def]) transfer_prover
    1.77 +
    1.78  lemma nat_of_natural_of_nat [simp]:
    1.79    "nat_of_natural (of_nat n) = n"
    1.80    by transfer rule
    1.81 @@ -895,6 +924,18 @@
    1.82  instance natural :: semiring_parity
    1.83    by (standard; transfer) simp_all
    1.84  
    1.85 +lemma [transfer_rule]:
    1.86 +  "rel_fun (=) (rel_fun pcr_natural pcr_natural) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (push_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"
    1.87 +  by (unfold push_bit_eq_mult [abs_def]) transfer_prover
    1.88 +
    1.89 +lemma [transfer_rule]:
    1.90 +  "rel_fun (=) (rel_fun pcr_natural pcr_natural) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"
    1.91 +  by (unfold take_bit_eq_mod [abs_def]) transfer_prover
    1.92 +
    1.93 +lemma [transfer_rule]:
    1.94 +  "rel_fun (=) (rel_fun pcr_natural pcr_natural) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (drop_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"
    1.95 +  by (unfold drop_bit_eq_div [abs_def]) transfer_prover
    1.96 +
    1.97  lift_definition natural_of_integer :: "integer \<Rightarrow> natural"
    1.98    is "nat :: int \<Rightarrow> nat"
    1.99    .
     2.1 --- a/src/HOL/Parity.thy	Thu Apr 19 21:54:46 2018 +0200
     2.2 +++ b/src/HOL/Parity.thy	Fri Apr 20 07:36:58 2018 +0000
     2.3 @@ -689,10 +689,10 @@
     2.4    where push_bit_eq_mult: "push_bit n a = a * 2 ^ n"
     2.5   
     2.6  definition take_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
     2.7 -  where take_bit_eq_mod: "take_bit n a = a mod of_nat (2 ^ n)"
     2.8 +  where take_bit_eq_mod: "take_bit n a = a mod 2 ^ n"
     2.9  
    2.10  definition drop_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
    2.11 -  where drop_bit_eq_div: "drop_bit n a = a div of_nat (2 ^ n)"
    2.12 +  where drop_bit_eq_div: "drop_bit n a = a div 2 ^ n"
    2.13  
    2.14  lemma bit_ident:
    2.15    "push_bit n (drop_bit n a) + take_bit n a = a"
    2.16 @@ -807,6 +807,10 @@
    2.17    "push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))"
    2.18    by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric]) (simp add: ac_simps)
    2.19  
    2.20 +lemma push_bit_of_nat:
    2.21 +  "push_bit n (of_nat m) = of_nat (push_bit n m)"
    2.22 +  by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult)
    2.23 +
    2.24  lemma take_bit_0 [simp]:
    2.25    "take_bit 0 a = 0"
    2.26    by (simp add: take_bit_eq_mod)
    2.27 @@ -858,6 +862,10 @@
    2.28    by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] take_bit_Suc
    2.29      ac_simps even_add even_mult_iff div_mult_self1 [OF numeral_neq_zero]) (simp add: ac_simps)
    2.30  
    2.31 +lemma take_bit_of_nat:
    2.32 +  "take_bit n (of_nat m) = of_nat (take_bit n m)"
    2.33 +  by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"])
    2.34 +
    2.35  lemma drop_bit_0 [simp]:
    2.36    "drop_bit 0 = id"
    2.37    by (simp add: fun_eq_iff drop_bit_eq_div)
    2.38 @@ -907,6 +915,10 @@
    2.39    by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] drop_bit_Suc
    2.40      div_mult_self4 [OF numeral_neq_zero]) simp
    2.41  
    2.42 +lemma drop_bit_of_nat:
    2.43 +  "drop_bit n (of_nat m) = of_nat (drop_bit n m)"
    2.44 +	by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"])
    2.45 +
    2.46  end
    2.47  
    2.48  lemma push_bit_of_Suc_0 [simp]: