src/HOL/Int.thy

--- a/src/HOL/Int.thy	Fri Jul 15 09:18:21 2022 +0200
+++ b/src/HOL/Int.thy	Fri Jul 22 14:39:56 2022 +0200
@@ -53,7 +53,7 @@
 
 lift_definition times_int :: "int \<Rightarrow> int \<Rightarrow> int"
   is "\<lambda>(x, y) (u, v). (x*u + y*v, x*v + y*u)"
-proof (clarsimp)
+proof (unfold intrel_def, clarify)
   fix s t u v w x y z :: nat
   assume "s + v = u + t" and "w + z = y + x"
   then have "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x) =
@@ -140,7 +140,7 @@
   assumes "k \<ge> (0::int)" shows "\<exists>n. k = int n"
 proof -
   have "b \<le> a \<Longrightarrow> \<exists>n::nat. a = n + b" for a b
-    by (rule_tac x="a - b" in exI) simp
+    using exI[of _ "a - b"] by simp
   with assms show ?thesis
     by transfer auto
 qed
@@ -149,7 +149,7 @@
   assumes "k > (0::int)" shows "\<exists>n>0. k = int n"
 proof -
   have "b < a \<Longrightarrow> \<exists>n::nat. n>0 \<and> a = n + b" for a b
-    by (rule_tac x="a - b" in exI) simp
+    using exI[of _ "a - b"] by simp
   with assms show ?thesis
     by transfer auto
 qed
@@ -189,7 +189,14 @@
   for w z :: int
 proof -
   have "\<And>a b c d. a + d < c + b \<Longrightarrow> \<exists>n. c + b = Suc (a + n + d)"
-    by (rule_tac x="c+b - Suc(a+d)" in exI) arith
+  proof -
+    fix a b c d :: nat
+    assume "a + d < c + b"
+    then have "c + b = Suc (a + (c + b - Suc (a + d)) + d) "
+      by arith
+    then show "\<exists>n. c + b = Suc (a + n + d)"
+      by (rule exI)
+  qed
   then show ?thesis
     by transfer auto
 qed
@@ -474,14 +481,20 @@
 
 instance int :: no_top
 proof
-  show "\<And>x::int. \<exists>y. x < y"
-    by (rule_tac x="x + 1" in exI) simp
+  fix x::int
+  have "x < x + 1"
+    by simp
+  then show "\<exists>y. x < y"
+    by (rule exI)
 qed
 
 instance int :: no_bot
 proof
-  show "\<And>x::int. \<exists>y. y < x"
-    by (rule_tac x="x - 1" in exI) simp
+  fix x::int
+  have "x - 1< x"
+    by simp
+  then show "\<exists>y. y < x"
+    by (rule exI)
 qed
 
 
@@ -738,7 +751,14 @@
   assumes "x < 0" shows "\<exists>n. x = - (int (Suc n))"
 proof -
   have "\<And>a b. a < b \<Longrightarrow> \<exists>n. Suc (a + n) = b"
-    by (rule_tac x="b - Suc a" in exI) arith
+  proof -
+    fix a b:: nat
+    assume "a < b"
+    then have "Suc (a + (b - Suc a)) = b"
+      by arith
+    then show "\<exists>n. Suc (a + n) = b"
+      by (rule exI)
+  qed
   with assms show ?thesis
     by transfer auto
 qed
@@ -1148,9 +1168,9 @@
 proof (rule Ints_cases [OF \<open>x \<in> Ints\<close>])
   fix z::int
   assume "x = of_int z"
-    with \<open>x \<noteq> 0\<close> 
+  with \<open>x \<noteq> 0\<close>
   show "1 \<le> \<bar>x\<bar>"
-    apply (auto simp add: abs_if)
+    apply (auto simp: abs_if)
     by (metis diff_0 of_int_1 of_int_le_iff of_int_minus zle_diff1_eq)
 qed
   
@@ -1425,7 +1445,7 @@
   obtain i where "i \<le> n - m" "k = f (m + i)"
     using nat_ivt_aux [of "n - m" "f \<circ> plus m" k] assms by auto
   with assms show ?thesis
-    by (rule_tac x = "m + i" in exI) auto
+    using exI[of _ "m + i"] by auto
 qed
 
 lemma nat0_intermed_int_val: