# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1586120659 -3600
# Node ID 34ff9ca387c0b8e41a05aaae374f62dbf9fbd276
# Parent  105d2d42a66064f32a1dc89eb7e24546cd2e461f
fixed more nasty proofs

diff -r 105d2d42a660 -r 34ff9ca387c0 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Apr 05 17:12:37 2020 +0100
+++ b/src/HOL/Rings.thy	Sun Apr 05 22:04:19 2020 +0100
@@ -1975,31 +1975,39 @@
 lemma mult_pos_neg2: "0 < a \<Longrightarrow> b < 0 \<Longrightarrow> b * a < 0"
   by (drule mult_strict_right_mono [of b 0]) auto
 
-lemma zero_less_mult_pos: "0 < a * b \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
-  apply (cases "b \<le> 0")
-   apply (auto simp add: le_less not_less)
-  apply (drule_tac mult_pos_neg [of a b])
-   apply (auto dest: less_not_sym)
-  done
-
-lemma zero_less_mult_pos2: "0 < b * a \<Longrightarrow> 0 < a \<Longrightarrow> 0 < b"
-  apply (cases "b \<le> 0")
-   apply (auto simp add: le_less not_less)
-  apply (drule_tac mult_pos_neg2 [of a b])
-   apply (auto dest: less_not_sym)
-  done
+lemma zero_less_mult_pos: 
+  assumes "0 < a * b" "0 < a" shows "0 < b"
+proof (cases "b \<le> 0")
+  case True
+  then show ?thesis
+    using assms by (auto simp: le_less dest: less_not_sym mult_pos_neg [of a b])
+qed (auto simp add: le_less not_less)
+
+
+lemma zero_less_mult_pos2: 
+  assumes "0 < b * a" "0 < a" shows "0 < b"
+proof (cases "b \<le> 0")
+  case True
+  then show ?thesis
+    using assms by (auto simp: le_less dest: less_not_sym mult_pos_neg2 [of a b])
+qed (auto simp add: le_less not_less)
 
 text \<open>Strict monotonicity in both arguments\<close>
 lemma mult_strict_mono:
-  assumes "a < b" and "c < d" and "0 < b" and "0 \<le> c"
+  assumes "a < b" "c < d" "0 < b" "0 \<le> c"
   shows "a * c < b * d"
-  using assms
-  apply (cases "c = 0")
-   apply simp
-  apply (erule mult_strict_right_mono [THEN less_trans])
-   apply (auto simp add: le_less)
-  apply (erule (1) mult_strict_left_mono)
-  done
+proof (cases "c = 0")
+  case True
+  with assms show ?thesis
+    by simp
+next
+  case False
+  with assms have "a*c < b*c"
+    by (simp add: mult_strict_right_mono [OF \<open>a < b\<close>])
+  also have "\<dots> < b*d"
+    by (simp add: assms mult_strict_left_mono)
+  finally show ?thesis .
+qed
 
 text \<open>This weaker variant has more natural premises\<close>
 lemma mult_strict_mono':
@@ -2010,24 +2018,24 @@
 lemma mult_less_le_imp_less:
   assumes "a < b" and "c \<le> d" and "0 \<le> a" and "0 < c"
   shows "a * c < b * d"
-  using assms
-  apply (subgoal_tac "a * c < b * c")
-   apply (erule less_le_trans)
-   apply (erule mult_left_mono)
-   apply simp
-  apply (erule (1) mult_strict_right_mono)
-  done
+proof -
+  have "a * c < b * c"
+    by (simp add: assms mult_strict_right_mono)
+  also have "... \<le> b * d"
+    by (intro mult_left_mono) (use assms in auto)
+  finally show ?thesis .
+qed
 
 lemma mult_le_less_imp_less:
   assumes "a \<le> b" and "c < d" and "0 < a" and "0 \<le> c"
   shows "a * c < b * d"
-  using assms
-  apply (subgoal_tac "a * c \<le> b * c")
-   apply (erule le_less_trans)
-   apply (erule mult_strict_left_mono)
-   apply simp
-  apply (erule (1) mult_right_mono)
-  done
+proof -
+  have "a * c \<le> b * c"
+    by (simp add: assms mult_right_mono)
+  also have "... < b * d"
+    by (intro mult_strict_left_mono) (use assms in auto)
+  finally show ?thesis .
+qed
 
 end
 
@@ -2114,14 +2122,10 @@
   by (simp add: algebra_simps)
 
 lemma mult_left_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c * a \<le> c * b"
-  apply (drule mult_left_mono [of _ _ "- c"])
-  apply simp_all
-  done
+  by (auto dest: mult_left_mono [of _ _ "- c"])
 
 lemma mult_right_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a * c \<le> b * c"
-  apply (drule mult_right_mono [of _ _ "- c"])
-  apply simp_all
-  done
+  by (auto dest: mult_right_mono [of _ _ "- c"])
 
 lemma mult_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a * b"
   using mult_right_mono_neg [of a 0 b] by simp
diff -r 105d2d42a660 -r 34ff9ca387c0 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Sun Apr 05 17:12:37 2020 +0100
+++ b/src/HOL/Transfer.thy	Sun Apr 05 22:04:19 2020 +0100
@@ -162,31 +162,33 @@
 using assms by(auto simp add: right_total_def)
 
 lemma right_total_alt_def2:
-  "right_total R \<longleftrightarrow> ((R ===> (\<longrightarrow>)) ===> (\<longrightarrow>)) All All"
-  unfolding right_total_def rel_fun_def
-  apply (rule iffI, fast)
-  apply (rule allI)
-  apply (drule_tac x="\<lambda>x. True" in spec)
-  apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec)
-  apply fast
-  done
+  "right_total R \<longleftrightarrow> ((R ===> (\<longrightarrow>)) ===> (\<longrightarrow>)) All All" (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    unfolding right_total_def rel_fun_def by blast
+next
+  assume \<section>: ?rhs
+  show ?lhs
+    using \<section> [unfolded rel_fun_def, rule_format, of "\<lambda>x. True" "\<lambda>y. \<exists>x. R x y"]
+    unfolding right_total_def by blast
+qed
 
 lemma right_unique_alt_def2:
   "right_unique R \<longleftrightarrow> (R ===> R ===> (\<longrightarrow>)) (=) (=)"
   unfolding right_unique_def rel_fun_def by auto
 
 lemma bi_total_alt_def2:
-  "bi_total R \<longleftrightarrow> ((R ===> (=)) ===> (=)) All All"
-  unfolding bi_total_def rel_fun_def
-  apply (rule iffI, fast)
-  apply safe
-  apply (drule_tac x="\<lambda>x. \<exists>y. R x y" in spec)
-  apply (drule_tac x="\<lambda>y. True" in spec)
-  apply fast
-  apply (drule_tac x="\<lambda>x. True" in spec)
-  apply (drule_tac x="\<lambda>y. \<exists>x. R x y" in spec)
-  apply fast
-  done
+  "bi_total R \<longleftrightarrow> ((R ===> (=)) ===> (=)) All All" (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    unfolding bi_total_def rel_fun_def by blast
+next
+  assume \<section>: ?rhs
+  show ?lhs
+    using \<section> [unfolded rel_fun_def, rule_format, of "\<lambda>x. \<exists>y. R x y" "\<lambda>y. True"]
+    using \<section> [unfolded rel_fun_def, rule_format, of "\<lambda>x. True" "\<lambda>y. \<exists>x. R x y"]
+    by (auto simp: bi_total_def)
+qed
 
 lemma bi_unique_alt_def2:
   "bi_unique R \<longleftrightarrow> (R ===> R ===> (=)) (=) (=)"
@@ -194,19 +196,19 @@
 
 lemma [simp]:
   shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
-  and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
-by(auto simp add: left_unique_def right_unique_def)
+    and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
+  by(auto simp add: left_unique_def right_unique_def)
 
 lemma [simp]:
   shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
-  and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
-by(simp_all add: left_total_def right_total_def)
+    and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
+  by(simp_all add: left_total_def right_total_def)
 
 lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
-by(auto simp add: bi_unique_def)
+  by(auto simp add: bi_unique_def)
 
 lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
-by(auto simp add: bi_total_def)
+  by(auto simp add: bi_total_def)
 
 lemma right_unique_alt_def: "right_unique R = (conversep R OO R \<le> (=))" unfolding right_unique_def by blast
 lemma left_unique_alt_def: "left_unique R = (R OO (conversep R) \<le> (=))" unfolding left_unique_def by blast
@@ -230,21 +232,21 @@
 
 
 lemma is_equality_lemma: "(\<And>R. is_equality R \<Longrightarrow> PROP (P R)) \<equiv> PROP (P (=))"
-  apply (unfold is_equality_def)
-  apply (rule equal_intr_rule)
-   apply (drule meta_spec)
-   apply (erule meta_mp)
-   apply (rule refl)
-  apply simp
-  done
+  unfolding is_equality_def
+proof (rule equal_intr_rule)
+  show "(\<And>R. R = (=) \<Longrightarrow> PROP P R) \<Longrightarrow> PROP P (=)"
+    apply (drule meta_spec)
+    apply (erule meta_mp [OF _ refl])
+    done
+qed simp
 
 lemma Domainp_lemma: "(\<And>R. Domainp T = R \<Longrightarrow> PROP (P R)) \<equiv> PROP (P (Domainp T))"
-  apply (rule equal_intr_rule)
-   apply (drule meta_spec)
-   apply (erule meta_mp)
-   apply (rule refl)
-  apply simp
-  done
+proof (rule equal_intr_rule)
+  show "(\<And>R. Domainp T = R \<Longrightarrow> PROP P R) \<Longrightarrow> PROP P (Domainp T)"
+    apply (drule meta_spec)
+    apply (erule meta_mp [OF _ refl])
+    done
+qed simp
 
 ML_file \<open>Tools/Transfer/transfer.ML\<close>
 declare refl [transfer_rule]
@@ -266,14 +268,21 @@
 
 lemma Domainp_pred_fun_eq[relator_domain]:
   assumes "left_unique T"
-  shows "Domainp (T ===> S) = pred_fun (Domainp T) (Domainp S)"
-  using assms unfolding rel_fun_def Domainp_iff[abs_def] left_unique_def fun_eq_iff pred_fun_def
-  apply safe
-   apply blast
-  apply (subst all_comm)
-  apply (rule choice)
-  apply blast
-  done
+  shows "Domainp (T ===> S) = pred_fun (Domainp T) (Domainp S)"   (is "?lhs = ?rhs")
+proof (intro ext iffI)
+  fix x
+  assume "?lhs x"
+  then show "?rhs x"
+    using assms unfolding rel_fun_def pred_fun_def by blast
+next
+  fix x
+  assume "?rhs x"
+  then have "\<exists>g. \<forall>y xa. T xa y \<longrightarrow> S (x xa) (g y)"
+    using assms unfolding Domainp_iff left_unique_def  pred_fun_def
+    by (intro choice) blast
+  then show "?lhs x"
+    by blast
+qed
 
 text \<open>Properties are preserved by relation composition.\<close>
 
@@ -295,10 +304,10 @@
   unfolding right_unique_def OO_def by fast
 
 lemma left_total_OO: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
-unfolding left_total_def OO_def by fast
+  unfolding left_total_def OO_def by fast
 
 lemma left_unique_OO: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
-unfolding left_unique_def OO_def by blast
+  unfolding left_unique_def OO_def by blast
 
 
 subsection \<open>Properties of relators\<close>
@@ -322,18 +331,22 @@
   unfolding bi_unique_def by simp
 
 lemma left_total_fun[transfer_rule]:
-  "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
-  unfolding left_total_def rel_fun_def
-  apply (rule allI, rename_tac f)
-  apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
-  apply clarify
-  apply (subgoal_tac "(THE x. A x y) = x", simp)
-  apply (rule someI_ex)
-  apply (simp)
-  apply (rule the_equality)
-  apply assumption
-  apply (simp add: left_unique_def)
-  done
+  assumes "left_unique A" "left_total B"
+  shows "left_total (A ===> B)"
+  unfolding left_total_def 
+proof
+  fix f
+  show "Ex ((A ===> B) f)"
+    unfolding rel_fun_def
+  proof (intro exI strip)
+    fix x y
+    assume A: "A x y"
+    have "(THE x. A x y) = x"
+      using A assms by (simp add: left_unique_def the_equality)
+    then show "B (f x) (SOME z. B (f (THE x. A x y)) z)"
+      using assms by (force simp: left_total_def intro: someI_ex)
+  qed
+qed
 
 lemma left_unique_fun[transfer_rule]:
   "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
@@ -341,18 +354,22 @@
   by (clarify, rule ext, fast)
 
 lemma right_total_fun [transfer_rule]:
-  "\<lbrakk>right_unique A; right_total B\<rbrakk> \<Longrightarrow> right_total (A ===> B)"
-  unfolding right_total_def rel_fun_def
-  apply (rule allI, rename_tac g)
-  apply (rule_tac x="\<lambda>x. SOME z. B z (g (THE y. A x y))" in exI)
-  apply clarify
-  apply (subgoal_tac "(THE y. A x y) = y", simp)
-  apply (rule someI_ex)
-  apply (simp)
-  apply (rule the_equality)
-  apply assumption
-  apply (simp add: right_unique_def)
-  done
+  assumes "right_unique A" "right_total B"
+  shows "right_total (A ===> B)"
+  unfolding right_total_def 
+proof
+  fix g
+  show "\<exists>x. (A ===> B) x g"
+    unfolding rel_fun_def
+  proof (intro exI strip)
+    fix x y
+    assume A: "A x y"
+    have "(THE y. A x y) = y"
+      using A assms by (simp add: right_unique_def the_equality)
+    then show "B (SOME z. B z (g (THE y. A x y))) (g y)"
+      using assms by (force simp: right_total_def intro: someI_ex)
+  qed
+qed
 
 lemma right_unique_fun [transfer_rule]:
   "\<lbrakk>right_total A; right_unique B\<rbrakk> \<Longrightarrow> right_unique (A ===> B)"
@@ -435,8 +452,8 @@
   assumes "right_total B"
   assumes "bi_unique A"
   shows "((A ===> B ===> (=)) ===> implies) left_unique left_unique"
-using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
-by metis
+  using assms unfolding left_unique_def right_total_def bi_unique_def rel_fun_def
+  by metis
 
 lemma eq_transfer [transfer_rule]:
   assumes "bi_unique A"
@@ -446,14 +463,14 @@
 lemma right_total_Ex_transfer[transfer_rule]:
   assumes "right_total A"
   shows "((A ===> (=)) ===> (=)) (Bex (Collect (Domainp A))) Ex"
-using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def]
-by fast
+  using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff
+  by fast
 
 lemma right_total_All_transfer[transfer_rule]:
   assumes "right_total A"
   shows "((A ===> (=)) ===> (=)) (Ball (Collect (Domainp A))) All"
-using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def]
-by fast
+  using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff
+  by fast
 
 context
   includes lifting_syntax
@@ -480,7 +497,7 @@
 lemma Ex1_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A" "bi_total A"
   shows "((A ===> (=)) ===> (=)) Ex1 Ex1"
-unfolding Ex1_def[abs_def] by transfer_prover
+unfolding Ex1_def by transfer_prover
 
 declare If_transfer [transfer_rule]
 
@@ -498,7 +515,7 @@
 lemma fun_upd_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"
   shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
-  unfolding fun_upd_def [abs_def] by transfer_prover
+  unfolding fun_upd_def  by transfer_prover
 
 lemma case_nat_transfer [transfer_rule]:
   "(A ===> ((=) ===> A) ===> (=) ===> A) case_nat case_nat"
@@ -517,18 +534,18 @@
   assumes [transfer_rule]: "(A ===> A ===> (=)) (\<le>) (\<le>)"
   assumes [transfer_rule]: "(B ===> B ===> (=)) (\<le>) (\<le>)"
   shows "((A ===> B) ===> (=)) mono mono"
-unfolding mono_def[abs_def] by transfer_prover
+unfolding mono_def by transfer_prover
 
 lemma right_total_relcompp_transfer[transfer_rule]:
   assumes [transfer_rule]: "right_total B"
   shows "((A ===> B ===> (=)) ===> (B ===> C ===> (=)) ===> A ===> C ===> (=))
     (\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) (OO)"
-unfolding OO_def[abs_def] by transfer_prover
+unfolding OO_def by transfer_prover
 
 lemma relcompp_transfer[transfer_rule]:
   assumes [transfer_rule]: "bi_total B"
   shows "((A ===> B ===> (=)) ===> (B ===> C ===> (=)) ===> A ===> C ===> (=)) (OO) (OO)"
-unfolding OO_def[abs_def] by transfer_prover
+unfolding OO_def by transfer_prover
 
 lemma right_total_Domainp_transfer[transfer_rule]:
   assumes [transfer_rule]: "right_total B"
@@ -538,7 +555,7 @@
 lemma Domainp_transfer[transfer_rule]:
   assumes [transfer_rule]: "bi_total B"
   shows "((A ===> B ===> (=)) ===> A ===> (=)) Domainp Domainp"
-unfolding Domainp_iff[abs_def] by transfer_prover
+unfolding Domainp_iff by transfer_prover
 
 lemma reflp_transfer[transfer_rule]:
   "bi_total A \<Longrightarrow> ((A ===> A ===> (=)) ===> (=)) reflp reflp"
@@ -546,38 +563,38 @@
   "right_total A \<Longrightarrow> ((A ===> A ===> (=)) ===> implies) reflp reflp"
   "bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
   "bi_total A \<Longrightarrow> ((A ===> A ===> (=)) ===> rev_implies) reflp reflp"
-unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
+unfolding reflp_def rev_implies_def bi_total_def right_total_def rel_fun_def
 by fast+
 
 lemma right_unique_transfer [transfer_rule]:
   "\<lbrakk> right_total A; right_total B; bi_unique B \<rbrakk>
   \<Longrightarrow> ((A ===> B ===> (=)) ===> implies) right_unique right_unique"
-unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
+unfolding right_unique_def right_total_def bi_unique_def rel_fun_def
 by metis
 
 lemma left_total_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_total A" "bi_total B"
   shows "((A ===> B ===> (=)) ===> (=)) left_total left_total"
-unfolding left_total_def[abs_def] by transfer_prover
+unfolding left_total_def by transfer_prover
 
 lemma right_total_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_total A" "bi_total B"
   shows "((A ===> B ===> (=)) ===> (=)) right_total right_total"
-unfolding right_total_def[abs_def] by transfer_prover
+unfolding right_total_def by transfer_prover
 
 lemma left_unique_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A" "bi_total A" "bi_total B"
   shows "((A ===> B ===> (=)) ===> (=)) left_unique left_unique"
-unfolding left_unique_def[abs_def] by transfer_prover
+unfolding left_unique_def by transfer_prover
 
 lemma prod_pred_parametric [transfer_rule]:
   "((A ===> (=)) ===> (B ===> (=)) ===> rel_prod A B ===> (=)) pred_prod pred_prod"
-unfolding prod.pred_set[abs_def] Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps 
+unfolding prod.pred_set Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps 
 by simp transfer_prover
 
 lemma apfst_parametric [transfer_rule]:
   "((A ===> B) ===> rel_prod A C ===> rel_prod B C) apfst apfst"
-unfolding apfst_def[abs_def] by transfer_prover
+unfolding apfst_def by transfer_prover
 
 lemma rel_fun_eq_eq_onp: "((=) ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
 unfolding eq_onp_def rel_fun_def by auto
@@ -589,7 +606,7 @@
 lemma eq_onp_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"
   shows "((A ===> (=)) ===> A ===> A ===> (=)) eq_onp eq_onp"
-unfolding eq_onp_def[abs_def] by transfer_prover
+unfolding eq_onp_def by transfer_prover
 
 lemma rtranclp_parametric [transfer_rule]:
   assumes "bi_unique A" "bi_total A"
@@ -633,11 +650,11 @@
 lemma right_unique_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_total A" "bi_unique B" "bi_total B"
   shows "((A ===> B ===> (=)) ===> (=)) right_unique right_unique"
-unfolding right_unique_def[abs_def] by transfer_prover
+  unfolding right_unique_def by transfer_prover
 
 lemma map_fun_parametric [transfer_rule]:
   "((A ===> B) ===> (C ===> D) ===> (B ===> C) ===> A ===> D) map_fun map_fun"
-unfolding map_fun_def[abs_def] by transfer_prover
+  unfolding map_fun_def by transfer_prover
 
 end
 
@@ -652,14 +669,14 @@
   \<open>((\<longleftrightarrow>) ===> (\<cong>)) of_bool of_bool\<close>
     if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
     for R :: \<open>'a::zero_neq_one \<Rightarrow> 'b::zero_neq_one \<Rightarrow> bool\<close>  (infix \<open>\<cong>\<close> 50)
-  by (unfold of_bool_def [abs_def]) transfer_prover
+  unfolding of_bool_def by transfer_prover
 
 lemma transfer_rule_of_nat:
   "((=) ===> (\<cong>)) of_nat of_nat"
     if [transfer_rule]: \<open>0 \<cong> 0\<close> \<open>1 \<cong> 1\<close>
     \<open>((\<cong>) ===> (\<cong>) ===> (\<cong>)) (+) (+)\<close>
   for R :: \<open>'a::semiring_1 \<Rightarrow> 'b::semiring_1 \<Rightarrow> bool\<close>  (infix \<open>\<cong>\<close> 50)
-  by (unfold of_nat_def [abs_def]) transfer_prover
+  unfolding of_nat_def by transfer_prover
 
 end