src/HOL/Code_Numeral.thy
 changeset 68010 3f223b9a0066 parent 67905 fe0f4eeceeb7 child 68028 1f9f973eed2a
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.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.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.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.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.51 @@ -313,6 +333,7 @@
1.52    "integer_of_nat (numeral n) = numeral n"
1.53  by transfer simp
1.55 +
1.56  subsection \<open>Code theorems for target language integers\<close>
1.58  text \<open>Constructors\<close>
1.59 @@ -777,6 +798,10 @@
1.60    unfolding dvd_def by transfer_prover
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.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.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    .