# HG changeset patch # User haftmann # Date 1524209818 0 # Node ID 3f223b9a006645b955a3900d10e4900a1abbe29a # Parent 72e1d5da30c6fcb2859155626bda3b48b6f4c092 algebraic embeddings for bit operations diff -r 72e1d5da30c6 -r 3f223b9a0066 src/HOL/Code_Numeral.thy --- 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 \ int) (of_nat :: nat \ integer)" + "rel_fun (=) pcr_integer (of_bool :: bool \ int) (of_bool :: bool \ integer)" + by (unfold of_bool_def [abs_def]) transfer_prover + +lemma [transfer_rule]: + "rel_fun (=) pcr_integer (of_nat :: nat \ int) (of_nat :: nat \ integer)" by (rule transfer_rule_of_nat) transfer_prover+ lemma [transfer_rule]: - "rel_fun HOL.eq pcr_integer (\k :: int. k :: int) (of_int :: int \ integer)" + "rel_fun (=) pcr_integer (\k :: int. k :: int) (of_int :: int \ integer)" proof - have "rel_fun HOL.eq pcr_integer (of_int :: int \ int) (of_int :: int \ 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 :: _ \ _ \ int) (Num.sub :: _ \ _ \ integer)" by (unfold Num.sub_def [abs_def]) transfer_prover +lemma [transfer_rule]: + "rel_fun pcr_integer (rel_fun (=) pcr_integer) (power :: _ \ _ \ int) (power :: _ \ _ \ 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 :: _ \ _ \ int) (push_bit :: _ \ _ \ integer)" + by (unfold push_bit_eq_mult [abs_def]) transfer_prover + +lemma [transfer_rule]: + "rel_fun (=) (rel_fun pcr_integer pcr_integer) (take_bit :: _ \ _ \ int) (take_bit :: _ \ _ \ integer)" + by (unfold take_bit_eq_mod [abs_def]) transfer_prover + +lemma [transfer_rule]: + "rel_fun (=) (rel_fun pcr_integer pcr_integer) (drop_bit :: _ \ _ \ int) (drop_bit :: _ \ _ \ 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 \Code theorems for target language integers\ text \Constructors\ @@ -777,6 +798,10 @@ unfolding dvd_def by transfer_prover lemma [transfer_rule]: + "rel_fun (=) pcr_natural (of_bool :: bool \ nat) (of_bool :: bool \ natural)" + by (unfold of_bool_def [abs_def]) transfer_prover + +lemma [transfer_rule]: "rel_fun HOL.eq pcr_natural (\n::nat. n) (of_nat :: nat \ natural)" proof - have "rel_fun HOL.eq pcr_natural (of_nat :: nat \ nat) (of_nat :: nat \ natural)" @@ -792,6 +817,10 @@ then show ?thesis by simp qed +lemma [transfer_rule]: + "rel_fun pcr_natural (rel_fun (=) pcr_natural) (power :: _ \ _ \ nat) (power :: _ \ _ \ 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 :: _ \ _ \ nat) (push_bit :: _ \ _ \ natural)" + by (unfold push_bit_eq_mult [abs_def]) transfer_prover + +lemma [transfer_rule]: + "rel_fun (=) (rel_fun pcr_natural pcr_natural) (take_bit :: _ \ _ \ nat) (take_bit :: _ \ _ \ natural)" + by (unfold take_bit_eq_mod [abs_def]) transfer_prover + +lemma [transfer_rule]: + "rel_fun (=) (rel_fun pcr_natural pcr_natural) (drop_bit :: _ \ _ \ nat) (drop_bit :: _ \ _ \ natural)" + by (unfold drop_bit_eq_div [abs_def]) transfer_prover + lift_definition natural_of_integer :: "integer \ natural" is "nat :: int \ nat" . diff -r 72e1d5da30c6 -r 3f223b9a0066 src/HOL/Parity.thy --- 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 \ 'a \ '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 \ 'a \ '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]: