# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1522073656 -7200
# Node ID 655aa11359dc49974c2337880c7f4c15117227e3
# Parent  99eaa5cedbb74e6d12214a579ccff6583a4a2b99
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)

diff -r 99eaa5cedbb7 -r 655aa11359dc src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Mon Mar 26 16:12:55 2018 +0200
+++ b/src/HOL/Enum.thy	Mon Mar 26 16:14:16 2018 +0200
@@ -795,18 +795,29 @@
 proof
   fix x A
   show "x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x"
-    by (cut_tac A = A and a = x in Inf_finite_insert, simp add: insert_absorb inf.absorb_iff2)
+    by (metis Set.set_insert abel_semigroup.commute local.Inf_finite_insert local.inf.abel_semigroup_axioms local.inf.left_idem local.inf.orderI)
   show "x \<in> A \<Longrightarrow> x \<le> \<Squnion>A"
-    by (cut_tac A = A and a = x in Sup_finite_insert, simp add: insert_absorb sup.absorb_iff2)
+    by (metis Set.set_insert insert_absorb2 local.Sup_finite_insert local.sup.absorb_iff2)
 next
   fix A z
-  show "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
-    apply (cut_tac F = A and P = "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> z \<le> x) \<longrightarrow> z \<le> \<Sqinter>A" in finite_induct, simp_all add: Inf_finite_empty Inf_finite_insert)
-    by(cut_tac A = UNIV and a = z in Sup_finite_insert, simp add: insert_UNIV local.sup.absorb_iff2)
+  have "\<Squnion> UNIV = z \<squnion> \<Squnion>UNIV"
+    by (subst Sup_finite_insert [symmetric], simp add: insert_UNIV)
+  from this have [simp]: "z \<le> \<Squnion>UNIV"
+    using local.le_iff_sup by auto
+  have "(\<forall> x. x \<in> A \<longrightarrow> z \<le> x) \<longrightarrow> z \<le> \<Sqinter>A"
+    apply (rule finite_induct [of A "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> z \<le> x) \<longrightarrow> z \<le> \<Sqinter>A"])
+    by (simp_all add: Inf_finite_empty Inf_finite_insert)
+  from this show "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
+    by simp
 
-  show " (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
-    apply (cut_tac F = A and  P = "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> x \<le> z) \<longrightarrow> \<Squnion>A \<le> z" in finite_induct, simp_all add: Sup_finite_empty Sup_finite_insert)
-    by(cut_tac A = UNIV and a = z in Inf_finite_insert, simp add: insert_UNIV local.inf.absorb_iff2)
+  have "\<Sqinter> UNIV = z \<sqinter> \<Sqinter>UNIV"
+    by (subst Inf_finite_insert [symmetric], simp add: insert_UNIV)
+  from this have [simp]: "\<Sqinter>UNIV \<le> z"
+    by (simp add: local.inf.absorb_iff2)
+  have "(\<forall> x. x \<in> A \<longrightarrow> x \<le> z) \<longrightarrow> \<Squnion>A \<le> z"
+    by (rule finite_induct [of A "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> x \<le> z) \<longrightarrow> \<Squnion>A \<le> z" ], simp_all add: Sup_finite_empty Sup_finite_insert)
+  from this show " (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
+    by blast
 next
   show "\<Sqinter>{} = \<top>"
     by (simp add: Inf_finite_empty top_finite_def)
@@ -818,40 +829,38 @@
 class finite_distrib_lattice = finite_lattice + distrib_lattice 
 begin
 lemma finite_inf_Sup: "a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}"
-proof (cut_tac F = A and P = "\<lambda> A . a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}" in finite_induct, simp_all)
+proof (rule finite_induct [of A "\<lambda> A . a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}"], simp_all)
   fix x::"'a"
   fix F
   assume "x \<notin> F"
-  assume A: "a \<sqinter> \<Squnion>F = \<Squnion>{a \<sqinter> b |b. b \<in> F}"
-
+  assume [simp]: "a \<sqinter> \<Squnion>F = \<Squnion>{a \<sqinter> b |b. b \<in> F}"
   have [simp]: " insert (a \<sqinter> x) {a \<sqinter> b |b. b \<in> F} = {a \<sqinter> b |b. b = x \<or> b \<in> F}"
-    by auto
-
+    by blast
   have "a \<sqinter> (x \<squnion> \<Squnion>F) = a \<sqinter> x \<squnion> a \<sqinter> \<Squnion>F"
     by (simp add: inf_sup_distrib1)
   also have "... = a \<sqinter> x \<squnion> \<Squnion>{a \<sqinter> b |b. b \<in> F}"
-    by (simp add: A)
+    by simp
   also have "... = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}"
     by (unfold Sup_insert[THEN sym], simp)
-
   finally show "a \<sqinter> (x \<squnion> \<Squnion>F) = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}"
     by simp
 qed
 
 lemma finite_Inf_Sup: "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
-proof (cut_tac F = A and P = "\<lambda> A .INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf" in finite_induct, simp_all add: finite_UnionD)
+proof (rule  finite_induct [of A "\<lambda> A .INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"], simp_all add: finite_UnionD)
   fix x::"'a set"
   fix F
   assume "x \<notin> F"
-  have [simp]: "{\<Squnion>x \<sqinter> b |b . b \<in> Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} } = {\<Squnion>x \<sqinter> (Inf (f ` F)) |f  .  (\<forall>Y\<in>F. f Y \<in> Y)}"
-    by auto
-  have [simp]:" \<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> \<exists>fa. insert b (f ` (F \<inter> {Y. Y \<noteq> x})) = insert (fa x) (fa ` F) \<and> fa x \<in> x \<and> (\<forall>Y\<in>F. fa Y \<in> Y)"
-     apply (rule_tac x = "(\<lambda> Y . (if Y = x then b else f Y))" in exI)
+  have [simp]: "{\<Squnion>x \<sqinter> b |b . b \<in> Inf ` {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} } = {\<Squnion>x \<sqinter> (Inf (f ` F)) |f  . (\<forall>Y\<in>F. f Y \<in> Y)}"
     by auto
-  have [simp]: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> (\<Sqinter>x\<in>F. f x) \<sqinter> b \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
-    apply (rule_tac i = "(\<lambda> Y . (if Y = x then b else f Y)) ` ({x} \<union> F)" in SUP_upper2, simp)
-    apply (subst inf_commute)
-    by (simp add: INF_greatest Inf_lower inf.coboundedI2)
+  define fa where "fa = (\<lambda> (b::'a) f Y . (if Y = x then b else f Y))"
+  have "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> insert b (f ` (F \<inter> {Y. Y \<noteq> x})) = insert (fa b f x) (fa b f ` F) \<and> fa b f x \<in> x \<and> (\<forall>Y\<in>F. fa b f Y \<in> Y)"
+    by (auto simp add: fa_def)
+  from this have B: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> fa b f ` ({x} \<union> F) \<in> {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)}"
+    by blast
+  have [simp]: "\<And>f b. \<forall>Y\<in>F. f Y \<in> Y \<Longrightarrow> b \<in> x \<Longrightarrow> b \<sqinter> (\<Sqinter>x\<in>F. f x)  \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
+    using B apply (rule SUP_upper2, simp_all)
+    by (simp_all add: INF_greatest Inf_lower inf.coboundedI2 fa_def)
 
   assume "INFIMUM F Sup \<le> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf"
 
@@ -866,7 +875,8 @@
     by (simp add: finite_inf_Sup)
 
   also have "... \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
-    by (rule Sup_least, clarsimp, rule Sup_least, clarsimp)
+    apply (rule Sup_least, clarsimp)+
+    by (subst inf_commute, simp)
 
   finally show "\<Squnion>x \<sqinter> INFIMUM F Sup \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
     by simp
diff -r 99eaa5cedbb7 -r 655aa11359dc src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Mon Mar 26 16:12:55 2018 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Mon Mar 26 16:14:16 2018 +0200
@@ -815,7 +815,7 @@
     using Inf_lower2 Sup_upper by auto
 next
   show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup \<le> SUPREMUM A Inf"
-  proof (simp add:  Inf_Sup, rule_tac SUP_least, simp, safe)
+  proof (simp add:  Inf_Sup, rule SUP_least, simp, safe)
     fix f
     assume "\<forall>Y. (\<exists>f. Y = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<longrightarrow> f Y \<in> Y"
     from this have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y) \<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z"
@@ -828,7 +828,7 @@
       have B: "... \<le> SUPREMUM A Inf"
         by (simp add: SUP_upper)
       from A and B show ?thesis
-        by (drule_tac order_trans, simp_all)
+        by simp
     next
       case False
       from this have X: "\<And> Z . Z \<in> A \<Longrightarrow> \<exists> x . x \<in> Z \<and> \<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> x"
@@ -842,8 +842,9 @@
         by blast
       from E and D have W: "\<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> F Z"
         by simp
-      from C have "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> f (F ` A)"
-        by (rule_tac INF_lower, blast)
+      have "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> f (F ` A)"
+        apply (rule INF_lower)
+        using C by blast
       from this and W and Y show ?thesis
         by simp
     qed
@@ -859,12 +860,13 @@
 lemma sup_Inf: "a \<squnion> Inf B = (INF b:B. a \<squnion> b)"
 proof (rule antisym)
   show "a \<squnion> Inf B \<le> (INF b:B. a \<squnion> b)"
-    using Inf_lower sup.mono by (rule_tac INF_greatest, fastforce)
+    apply (rule INF_greatest)
+    using Inf_lower sup.mono by fastforce
 next
   have "(INF b:B. a \<squnion> b) \<le> INFIMUM {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B} Sup"
     by (rule INF_greatest, auto simp add: INF_lower)
-  also have "... = a \<squnion> Inf B"
-    by (cut_tac A = "{{a}, B}" in Sup_Inf, simp)
+  also have "... = SUPREMUM {{a}, B} Inf"
+    by (unfold Sup_Inf, simp)
   finally show "(INF b:B. a \<squnion> b) \<le> a \<squnion> Inf B"
     by simp
 qed
@@ -879,7 +881,7 @@
     by (rule SUP_least, rule INF_greatest, rule SUP_upper2, simp_all, rule INF_lower2, simp, blast)
 next
   have "(INF y. SUP x. ((P x y))) \<le> Inf (Sup ` {{P x y | x . True} | y . True })" (is "?A \<le> ?B")
-  proof (rule_tac INF_greatest, clarsimp)
+  proof (rule INF_greatest, clarsimp)
     fix y
     have "?A \<le> (SUP x. P x y)"
       by (rule INF_lower, simp)
@@ -889,7 +891,7 @@
       by simp
   qed
   also have "... \<le>  (SUP x. INF y. P (x y) y)"
-  proof (subst  Inf_Sup, rule_tac SUP_least, clarsimp)
+  proof (subst Inf_Sup, rule SUP_least, clarsimp)
     fix f
     assume A: "\<forall>Y. (\<exists>y. Y = {uu. \<exists>x. uu = P x y}) \<longrightarrow> f Y \<in> Y"
       
@@ -897,9 +899,10 @@
     proof (rule INF_greatest, clarsimp)
       fix y
         have "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> f {uu. \<exists>x. uu = P x y}"
-          by (rule_tac INF_lower, blast)
+          by (rule INF_lower, blast)
         also have "... \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y"
-          using A by (rule_tac someI2_ex, auto)
+          apply (rule someI2_ex)
+          using A by auto
         finally show "(INF x:{uu. \<exists>y. uu = {uu. \<exists>x. uu = P x y}}. f x) \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y"
           by simp
       qed
@@ -914,8 +917,12 @@
 
 lemma INF_SUP_set: "(INF x:A. SUP a:x. (g a)) = (SUP x:{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. INF a:x. g a)"
 proof (rule antisym)
+  have [simp]: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> (\<Sqinter>x\<in>A. g (f x)) \<le> g (f xa)"
+    by (rule INF_lower2, blast+)
+  have B: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> f xa \<in> xa"
+    by blast
   have A: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> (\<Sqinter>x\<in>A. g (f x)) \<le> SUPREMUM xa g"
-    by (rule_tac i = "(f xa)" in SUP_upper2, simp, rule_tac i = "xa" in INF_lower2, simp_all)
+    by (rule SUP_upper2, rule B, simp_all, simp)
   show "(\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)"
     apply (rule SUP_least, simp, safe, rule INF_greatest, simp)
     by (rule A)
@@ -924,22 +931,38 @@
   proof (cases "{} \<in> A")
     case True
     then show ?thesis 
-      by (rule_tac i = "{}" in INF_lower2, simp_all)
+      by (rule INF_lower2, simp_all)
   next
     case False
     have [simp]: "\<And>x xa xb. xb \<in> A \<Longrightarrow> x xb \<in> xb \<Longrightarrow> (\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> g (x xb)"
-      by (rule_tac i = xb in INF_lower2, simp_all)
+      by (rule INF_lower2, auto)
     have [simp]: " \<And>x xa y. y \<in> A \<Longrightarrow> x y \<notin> y \<Longrightarrow> (\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> g (SOME x. x \<in> y)"
-      by (rule_tac i = y in INF_lower2, simp_all)
+      by (rule INF_lower2, auto)
     have [simp]: "\<And>x. (\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
-      apply (rule_tac i = "(\<lambda> y . if x y \<in> y then x y else (SOME x . x \<in>y)) ` A" in SUP_upper2, simp)
-       apply (rule_tac x = "(\<lambda> y . if x y \<in> y then x y else (SOME x . x \<in>y))" in exI, simp)
-      using False some_in_eq apply auto[1]
-      by (rule INF_greatest, auto)
-    have "\<And>x. (\<Sqinter>x\<in>A. \<Squnion>x\<in>x. g x) \<le> (\<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
-      apply (case_tac "x \<in> A")
-       apply (rule INF_lower2, simp)
-      by (rule SUP_least, rule SUP_upper2, auto)
+    proof -
+      fix x
+      define F where "F = (\<lambda> (y::'b set) . if x y \<in> y then x y else (SOME x . x \<in>y))"
+      have B: "(\<forall>Y\<in>A. F Y \<in> Y)"
+        using False some_in_eq F_def by auto
+      have A: "F ` A \<in> {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
+        using B by blast
+      show "(\<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x\<in>x. g x)"
+        using A apply (rule SUP_upper2)
+        by (simp add: F_def, rule INF_greatest, auto)
+    qed
+
+    {fix x
+      have "(\<Sqinter>x\<in>A. \<Squnion>x\<in>x. g x) \<le> (\<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
+      proof (cases "x \<in> A")
+        case True
+        then show ?thesis
+          apply (rule INF_lower2, simp_all)
+          by (rule SUP_least, rule SUP_upper2, auto)
+      next
+        case False
+        then show ?thesis by simp
+      qed
+    }
     from this have "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Sqinter>x. \<Squnion>xa. if x \<in> A then if xa \<in> x then g xa else \<bottom> else \<top>)"
       by (rule INF_greatest)
     also have "... = (\<Squnion>x. \<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>)"
@@ -1020,10 +1043,14 @@
   from this have B: " (\<forall>xa \<in> F ` A. x \<in> xa)"
     apply (safe, simp add: F_def)
     by (rule someI2_ex, auto)
-    
+
+  have C: "(\<forall>Y\<in>A. F Y \<in> Y)"
+    apply (simp  add: F_def, safe)
+    apply (rule someI2_ex)
+    using A by auto
+
   have "(\<exists>f. F ` A  = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y))"
-    apply (rule_tac x = "F" in exI, simp add: F_def, safe)
-    using A by (rule_tac someI2_ex, auto)
+    using C by blast
     
   from B and this show "\<exists>X. (\<exists>f. X = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>xa\<in>X. x \<in> xa)"
     by auto
@@ -1063,10 +1090,13 @@
       define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> z < k)"
         
       have D: "\<And> Y . Y \<in> A \<Longrightarrow> z < F Y"
-        using B by (simp add: F_def, rule_tac someI2_ex, auto)
+        using B apply (simp add: F_def)
+        by (rule someI2_ex, auto)
+
     
       have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
-        using B by (simp add: F_def, rule_tac someI2_ex, auto)
+        using B apply (simp add: F_def)
+        by (rule someI2_ex, auto)
     
       have "z \<le> Inf (F ` A)"
         by (simp add: D local.INF_greatest local.order.strict_implies_order)
@@ -1093,10 +1123,12 @@
       define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < k)"
         
       have D: "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < F Y"
-        using B by (simp add: F_def, rule_tac someI2_ex, auto)
+        using B apply (simp add: F_def)
+        by (rule someI2_ex, auto)
     
       have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
-        using B by (simp add: F_def, rule_tac someI2_ex, auto)
+        using B apply (simp add: F_def)
+        by (rule someI2_ex, auto)
           
       have "\<And> Y . Y \<in> A \<Longrightarrow> INFIMUM A Sup \<le> F Y"
         using D False local.leI by blast
@@ -1112,7 +1144,7 @@
         by simp
         
       from C and this show ?thesis
-        using local.not_less by blast
+        using not_less by blast
     qed
   qed
 end
diff -r 99eaa5cedbb7 -r 655aa11359dc src/HOL/Library/Option_ord.thy
--- a/src/HOL/Library/Option_ord.thy	Mon Mar 26 16:12:55 2018 +0200
+++ b/src/HOL/Library/Option_ord.thy	Mon Mar 26 16:14:16 2018 +0200
@@ -287,7 +287,7 @@
 proof (cases "{} \<in> A")
   case True
   then show ?thesis
-    by (rule_tac i = "{}" in INF_lower2, simp_all)
+    by (rule INF_lower2, simp_all)
 next
   case False
   from this have X: "{} \<notin> A"
@@ -296,37 +296,41 @@
   proof (cases "{None} \<in> A")
     case True
     then show ?thesis
-      by (rule_tac i = "{None}" in INF_lower2, simp_all)
+      by (rule INF_lower2, simp_all)
   next
     case False
-    have "\<And> y . y\<in>A \<Longrightarrow> Sup (y - {None}) = Sup y"
-      by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq)
-   
+
+    {fix y
+      assume A: "y \<in> A"
+      have "Sup (y - {None}) = Sup y"
+        by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq)
+      from A and this have "(\<exists>z. y - {None} = z - {None} \<and> z \<in> A) \<and> \<Squnion>y = \<Squnion>(y - {None})"
+        by auto
+    }
     from this have A: "Sup ` A = (Sup ` {y - {None} | y. y\<in>A})"
-      apply (simp add: image_def, simp, safe)
-       apply (rule_tac x = "xa - {None}" in exI, simp, blast)
-      by blast
+      by (auto simp add: image_def)
 
     have [simp]: "\<And>y. y \<in> A \<Longrightarrow> \<exists>ya. {ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x} 
           = {y. \<exists>x\<in>ya - {None}. y = the x} \<and> ya \<in> A"
-      by (rule_tac x = "y" in exI, auto)
+      by (rule exI, auto)
 
     have [simp]: "\<And>y. y \<in> A \<Longrightarrow>
          (\<exists>ya. y - {None} = ya - {None} \<and> ya \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x} 
           = \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"
-      apply safe
-       apply blast
-      apply (rule_tac f = Sup in arg_cong)
-      by auto
-
-    have C: "(\<lambda>x.  (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A} =  (Sup ` {the ` (y - {None}) |y. y \<in> A})"
-      apply (simp add: image_def Option.these_def, safe)
-       apply (rule_tac x = "{ya. \<exists>x. x \<in> y - {None} \<and> (\<exists>y. x = Some y) \<and> ya = the x}" in exI, simp)
-      by (rule_tac x = "y -{None}" in exI, simp)
+      apply (safe, blast)
+      by (rule arg_cong [of _ _ Sup], auto)
+    {fix y
+      assume [simp]: "y \<in> A"
+      have "\<exists>x. (\<exists>y. x = {ya. \<exists>x\<in>y - {None}. ya = the x} \<and> y \<in> A) \<and> \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x} = \<Squnion>x"
+      and "\<exists>x. (\<exists>y. x = y - {None} \<and> y \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x} = \<Squnion>{y. \<exists>xa. xa \<in> x \<and> (\<exists>y. xa = Some y) \<and> y = the xa}"
+         apply (rule exI [of _ "{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"], simp)
+        by (rule exI [of _ "y - {None}"], simp)
+    }
+    from this have C: "(\<lambda>x.  (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A} =  (Sup ` {the ` (y - {None}) |y. y \<in> A})"
+      by (simp add: image_def Option.these_def, safe, simp_all)
   
     have D: "\<forall> f . \<exists>Y\<in>A. f Y \<notin> Y \<Longrightarrow> False"
-      apply (drule_tac x = "\<lambda> Y . SOME x . x \<in> Y" in spec, safe)
-      by (simp add: X some_in_eq)
+      by (drule spec [of _ "\<lambda> Y . SOME x . x \<in> Y"], simp add: X some_in_eq)
   
     define F where "F = (\<lambda> Y . SOME x::'a option . x \<in> (Y - {None}))"
   
@@ -341,12 +345,13 @@
           less_eq_option_Some singletonI)
       
     from this have "Inf (F ` A) \<noteq> None"
-      by (case_tac "\<Sqinter>x\<in>A. F x", simp_all)
-  
+      by (cases "\<Sqinter>x\<in>A. F x", simp_all)
+
+    from this have "Inf (F ` A) \<noteq> None \<and> Inf (F ` A) \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
+      using F by auto
+
     from this have "\<exists> x . x \<noteq> None \<and> x \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
-      apply (rule_tac x = "Inf (F ` A)" in exI, simp add: image_def, safe)
-      apply (rule_tac x = "F `  A" in exI, safe)
-      using F by auto
+      by blast
   
     from this have E:" Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None} \<Longrightarrow> False"
       by blast
@@ -358,36 +363,59 @@
     have B: "Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}) 
         = ((\<lambda>x. (\<Squnion> Option.these x)) ` {y - {None} |y. y \<in> A})"
       by (metis image_image these_image_Some_eq)
+    {
+      fix f
+      assume A: "\<And> Y . (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<Longrightarrow> f Y \<in> Y"
 
-    have [simp]: "\<And>f. \<forall>Y. (\<exists>y. Y = {ya. \<exists>x\<in>y - {None}. ya = the x} \<and> y \<in> A) \<longrightarrow> f Y \<in> Y \<Longrightarrow>
-         \<exists>x. (\<exists>f. x = {y. \<exists>x\<in>A. y = f x} \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x})) = \<Sqinter>x"
-      apply (rule_tac x = "{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) | x . x\<in> A}" in exI, safe)
-       apply (rule_tac x = "(\<lambda> Y . Some (f (the ` (Y - {None})))) " in exI, safe)
-         apply (rule_tac x = xa in bexI, simp add: image_def, simp)
-        apply (rule_tac x = xa in exI, simp add: image_def)
-       apply(drule_tac x = "(the ` (Y - {None}))" in spec)
-       apply (simp add: image_def,safe, simp)
-      using option.collapse apply fastforce
-      by (simp add: Setcompr_eq_image)
+      have "\<And>xa. xa \<in> A \<Longrightarrow> f {y. \<exists>a\<in>xa - {None}. y = the a} = f (the ` (xa - {None}))"
+        by  (simp add: image_def)
+      from this have [simp]: "\<And>xa. xa \<in> A \<Longrightarrow> \<exists>x\<in>A. f {y. \<exists>a\<in>xa - {None}. y = the a} = f (the ` (x - {None}))"
+        by blast
+      have "\<And>xa. xa \<in> A \<Longrightarrow> f (the ` (xa - {None})) = f {y. \<exists>a \<in> xa - {None}. y = the a} \<and> xa \<in> A"
+        by (simp add: image_def)
+      from this have [simp]: "\<And>xa. xa \<in> A \<Longrightarrow> \<exists>x. f (the ` (xa - {None})) = f {y. \<exists>a\<in>x - {None}. y = the a} \<and> x \<in> A"
+        by blast
 
-    have [simp]: "\<And>f. \<forall>Y. (\<exists>y. Y = {ya. \<exists>x\<in>y - {None}. ya = the x} \<and> y \<in> A) \<longrightarrow> f Y \<in> Y 
-        \<Longrightarrow> \<exists>y. (\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x})) = Some y"
-      by (metis (no_types) Some_INF)
+      {
+        fix Y
+        have "Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y"
+          using A [of "the ` (Y - {None})"] apply (simp add: image_def)
+          using option.collapse by fastforce
+      }
+      from this have [simp]: "\<And> Y . Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y"
+        by blast
+      have [simp]: "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x})) = \<Sqinter>{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) |x. x \<in> A}"
+        by (simp add: Setcompr_eq_image)
+      
+      have [simp]: "\<exists>x. (\<exists>f. x = {y. \<exists>x\<in>A. y = f x} \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> \<Sqinter>{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) |x. x \<in> A} = \<Sqinter>x"
+        apply (rule exI [of _ "{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) | x . x\<in> A}"], safe)
+        by (rule exI [of _ "(\<lambda> Y . Some (f (the ` (Y - {None})))) "], safe, simp_all)
 
-    have [simp]: "\<And> f.
-         (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None}))))"
-      apply (simp add: Inf_option_def, safe)
-      apply (rule Inf_greatest, simp add: image_def Option.these_def, safe)
-      apply (rule_tac i = " {y. \<exists>x\<in>xb - {None}. y = the x}" in INF_lower2)
-       apply simp_all
+      {
+        fix xb
+        have "xb \<in> A \<Longrightarrow> (\<Sqinter>x\<in>{{ya. \<exists>x\<in>y - {None}. ya = the x} |y. y \<in> A}. f x) \<le> f {y. \<exists>x\<in>xb - {None}. y = the x}"
+          apply (rule INF_lower2 [of "{y. \<exists>x\<in>xb - {None}. y = the x}"])
+          by blast+
+      }
+      from this have [simp]: "(\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None}))))"
+        apply (simp add: Inf_option_def image_def Option.these_def)
+        by (rule Inf_greatest, clarsimp)
+
+      have [simp]: "the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None})))) \<in> Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+        apply (simp add:  Option.these_def image_def)
+        apply (rule exI [of _ "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x}))"], simp)
+        by (simp add: Inf_option_def)
+
+      have "(\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
+        by (rule Sup_upper2 [of "the (Inf ((\<lambda> Y . Some (f (the ` (Y - {None})) )) ` A))"], simp_all)
+    }
+    from this have X: "\<And> f . \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y \<Longrightarrow>
+      (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
       by blast
+    
 
-    have X: "\<And> f . \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y
-      \<Longrightarrow> (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> \<Squnion>Option.these (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
-      apply (rule_tac u = "the (Inf ((\<lambda> Y . Some (f (the ` (Y - {None})) )) ` A))" in Sup_upper2)
-       apply (simp add:  Option.these_def image_def)
-       apply (rule_tac x = "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x}))" in exI, simp)
-      by simp
+    have [simp]: "\<And> x . x\<in>{y - {None} |y. y \<in> A} \<Longrightarrow>  x \<noteq> {} \<and> x \<noteq> {None}"
+      using F by fastforce
 
     have "(Inf (Sup `A)) = (Inf (Sup ` {y - {None} | y. y\<in>A}))"
       by (subst A, simp)
@@ -396,7 +424,6 @@
       by (simp add: Sup_option_def)
 
     also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. Some (\<Squnion>Option.these x))"
-      apply (subgoal_tac "\<And> x . x\<in>{y - {None} |y. y \<in> A} \<Longrightarrow>  x \<noteq> {} \<and> x \<noteq> {None}", simp)
       using G by fastforce
   
     also have "... = Some (\<Sqinter>Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))"
@@ -412,12 +439,18 @@
       by (simp add: Inf_Sup)
   
     also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
-      apply (simp add: less_eq_option_def)
-      apply (case_tac "\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x", simp_all)
-      apply (rule Sup_least, safe)
-      apply (simp add: Sup_option_def)
-      apply (case_tac "(\<forall>f. \<exists>Y\<in>A. f Y \<notin> Y) \<or> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None}", simp_all)
-      by (drule X, simp)
+    proof (cases "SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
+      case None
+      then show ?thesis by (simp add: less_eq_option_def)
+    next
+      case (Some a)
+      then show ?thesis
+        apply simp
+        apply (rule Sup_least, safe)
+        apply (simp add: Sup_option_def)
+        apply (cases "(\<forall>f. \<exists>Y\<in>A. f Y \<notin> Y) \<or> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None}", simp_all)
+        by (drule X, simp)
+    qed
     finally show ?thesis by simp
   qed
 qed
diff -r 99eaa5cedbb7 -r 655aa11359dc src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Mar 26 16:12:55 2018 +0200
+++ b/src/HOL/Predicate.thy	Mon Mar 26 16:14:16 2018 +0200
@@ -110,9 +110,10 @@
     define F where "F = (\<lambda> x . SOME f . f \<in> x \<and> eval f w)"
     have [simp]: "(\<forall>f\<in> (F ` A). eval f w)"
       by (metis (no_types, lifting) A F_def image_iff some_eq_ex)
-    show "\<exists>x. (\<exists>f. x = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>f\<in>x. eval f w)"
-      apply (rule_tac x = "F ` A" in exI, simp)
-      using A by (metis (no_types, lifting) F_def someI)+
+    have "(\<exists>f. F ` A = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>f\<in>(F ` A). eval f w)"
+      using A by (simp, metis (no_types, lifting) F_def someI)+
+    from this show "\<exists>x. (\<exists>f. x = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<and> (\<forall>f\<in>x. eval f w)"
+      by (rule exI [of _ "F ` A"])
   qed
 qed (auto intro!: pred_eqI)