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.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    .