src/HOL/Code_Numeral.thy

   "(pcr_integer ===> pcr_integer ===> (\<longleftrightarrow>)) (dvd) (dvd)"
   by (unfold dvd_def) transfer_prover
 
 lemma [transfer_rule]:
   "((\<longleftrightarrow>) ===> pcr_integer) of_bool of_bool"
-  by (unfold of_bool_def [abs_def]) transfer_prover
+  by (unfold of_bool_def) transfer_prover
 
 lemma [transfer_rule]:
   "((=) ===> pcr_integer) int of_nat"
   by (rule transfer_rule_of_nat) transfer_prover+
 

   "((=) ===> pcr_integer) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
   "((=) ===> (=) ===> pcr_integer) Num.sub Num.sub"
-  by (unfold Num.sub_def [abs_def]) transfer_prover
+  by (unfold Num.sub_def) transfer_prover
 
 lemma [transfer_rule]:
   "(pcr_integer ===> (=) ===> pcr_integer) (^) (^)"
-  by (unfold power_def [abs_def]) transfer_prover
+  by (unfold power_def) transfer_prover
 
 end
 
 lemma int_of_integer_of_nat [simp]:
   "int_of_integer (of_nat n) = of_nat n"

 instance
   by standard (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+
 
 end
 
-lemma [transfer_rule]:
-  "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (min :: _ \<Rightarrow> _ \<Rightarrow> int) (min :: _ \<Rightarrow> _ \<Rightarrow> integer)"
-  by (unfold min_def [abs_def]) transfer_prover
-
-lemma [transfer_rule]:
-  "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (max :: _ \<Rightarrow> _ \<Rightarrow> int) (max :: _ \<Rightarrow> _ \<Rightarrow> integer)"
-  by (unfold max_def [abs_def]) transfer_prover
+context
+  includes lifting_syntax
+begin
+
+lemma [transfer_rule]:
+  \<open>(pcr_integer ===> pcr_integer ===> pcr_integer) min min\<close>
+  by (unfold min_def) transfer_prover
+
+lemma [transfer_rule]:
+  \<open>(pcr_integer ===> pcr_integer ===> pcr_integer) max max\<close>
+  by (unfold max_def) transfer_prover
+
+end
 
 lemma int_of_integer_min [simp]:
   "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)"
   by transfer rule
 

     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
     even_mask_div_iff even_mult_exp_div_exp_iff)+
 
 end
 
-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
+context
+  includes lifting_syntax
+begin
+
+lemma [transfer_rule]:
+  \<open>(pcr_integer ===> (=) ===> (\<longleftrightarrow>)) bit bit\<close>
+  by (unfold bit_def) transfer_prover
+
+lemma [transfer_rule]:
+  \<open>((=) ===> pcr_integer ===> pcr_integer) take_bit take_bit\<close>
+  by (unfold take_bit_eq_mod) transfer_prover
+
+end
 
 instance integer :: unique_euclidean_semiring_with_bit_shifts ..
 
 lemma [code]:
   \<open>push_bit n k = k * 2 ^ n\<close>

 
 definition Pos :: "num \<Rightarrow> integer"
 where
   [simp, code_post]: "Pos = numeral"
 
-lemma [transfer_rule]:
-  "rel_fun HOL.eq pcr_integer numeral Pos"
+context
+  includes lifting_syntax
+begin
+
+lemma [transfer_rule]:
+  \<open>((=) ===> pcr_integer) numeral Pos\<close>
   by simp transfer_prover
+
+end
 
 lemma Pos_fold [code_unfold]:
   "numeral Num.One = Pos Num.One"
   "numeral (Num.Bit0 k) = Pos (Num.Bit0 k)"
   "numeral (Num.Bit1 k) = Pos (Num.Bit1 k)"

 
 definition Neg :: "num \<Rightarrow> integer"
 where
   [simp, code_abbrev]: "Neg n = - Pos n"
 
-lemma [transfer_rule]:
-  "rel_fun HOL.eq pcr_integer (\<lambda>n. - numeral n) Neg"
-  by (simp add: Neg_def [abs_def]) transfer_prover
+context
+  includes lifting_syntax
+begin
+
+lemma [transfer_rule]:
+  \<open>((=) ===> pcr_integer) (\<lambda>n. - numeral n) Neg\<close>
+  by (unfold Neg_def) transfer_prover
+
+end
 
 code_datatype "0::integer" Pos Neg
 
   
 text \<open>A further pair of constructors for generated computations\<close>

 
 end
 
 instance natural :: Rings.dvd ..
 
-lemma [transfer_rule]:
-  "rel_fun pcr_natural (rel_fun pcr_natural HOL.iff) Rings.dvd Rings.dvd"
-  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)"
+context
+  includes lifting_syntax
+begin
+
+lemma [transfer_rule]:
+  \<open>(pcr_natural ===> pcr_natural ===> (\<longleftrightarrow>)) (dvd) (dvd)\<close>
+  by (unfold dvd_def) transfer_prover
+
+lemma [transfer_rule]:
+  \<open>((\<longleftrightarrow>) ===> pcr_natural) of_bool of_bool\<close>
+  by (unfold of_bool_def) transfer_prover
+
+lemma [transfer_rule]:
+  \<open>((=) ===> pcr_natural) (\<lambda>n. n) of_nat\<close>
 proof -
   have "rel_fun HOL.eq pcr_natural (of_nat :: nat \<Rightarrow> nat) (of_nat :: nat \<Rightarrow> natural)"
-    by (unfold of_nat_def [abs_def]) transfer_prover
+    by (unfold of_nat_def) transfer_prover
   then show ?thesis by (simp add: id_def)
 qed
 
 lemma [transfer_rule]:
-  "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (numeral :: num \<Rightarrow> natural)"
+  \<open>((=) ===> pcr_natural) numeral numeral\<close>
 proof -
-  have "rel_fun HOL.eq pcr_natural (numeral :: num \<Rightarrow> nat) (\<lambda>n. of_nat (numeral n))"
+  have \<open>((=) ===> pcr_natural) numeral (\<lambda>n. of_nat (numeral n))\<close>
     by transfer_prover
   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
+  \<open>(pcr_natural ===> (=) ===> pcr_natural) (^) (^)\<close>
+  by (unfold power_def) transfer_prover
+
+end
 
 lemma nat_of_natural_of_nat [simp]:
   "nat_of_natural (of_nat n) = n"
   by transfer rule
 

 instance proof
 qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+
 
 end
 
-lemma [transfer_rule]:
-  "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (min :: _ \<Rightarrow> _ \<Rightarrow> nat) (min :: _ \<Rightarrow> _ \<Rightarrow> natural)"
-  by (unfold min_def [abs_def]) transfer_prover
-
-lemma [transfer_rule]:
-  "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (max :: _ \<Rightarrow> _ \<Rightarrow> nat) (max :: _ \<Rightarrow> _ \<Rightarrow> natural)"
-  by (unfold max_def [abs_def]) transfer_prover
+context
+  includes lifting_syntax
+begin
+
+lemma [transfer_rule]:
+  \<open>(pcr_natural ===> pcr_natural ===> pcr_natural) min min\<close>
+  by (unfold min_def) transfer_prover
+
+lemma [transfer_rule]:
+  \<open>(pcr_natural ===> pcr_natural ===> pcr_natural) max max\<close>
+  by (unfold max_def) transfer_prover
+
+end
 
 lemma nat_of_natural_min [simp]:
   "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)"
   by transfer rule
 

     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
     even_mask_div_iff even_mult_exp_div_exp_iff)+
 
 end
 
-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
+context
+  includes lifting_syntax
+begin
+
+lemma [transfer_rule]:
+  \<open>(pcr_natural ===> (=) ===> (\<longleftrightarrow>)) bit bit\<close>
+  by (unfold bit_def) transfer_prover
+
+lemma [transfer_rule]:
+  \<open>((=) ===> pcr_natural ===> pcr_natural) take_bit take_bit\<close>
+  by (unfold take_bit_eq_mod) transfer_prover
+
+end
 
 instance natural :: unique_euclidean_semiring_with_bit_shifts ..
 
 lemma [code]:
   \<open>push_bit n m = m * 2 ^ n\<close>