Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
authorManuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (17 months ago)
changeset 67951655aa11359dc
parent 67950 99eaa5cedbb7
child 67952 120c96286336
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
src/HOL/Enum.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/Option_ord.thy
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Enum.thy	Mon Mar 26 16:12:55 2018 +0200
     1.2 +++ b/src/HOL/Enum.thy	Mon Mar 26 16:14:16 2018 +0200
     1.3 @@ -795,18 +795,29 @@
     1.4  proof
     1.5    fix x A
     1.6    show "x \<in> A \<Longrightarrow> \<Sqinter>A \<le> x"
     1.7 -    by (cut_tac A = A and a = x in Inf_finite_insert, simp add: insert_absorb inf.absorb_iff2)
     1.8 +    by (metis Set.set_insert abel_semigroup.commute local.Inf_finite_insert local.inf.abel_semigroup_axioms local.inf.left_idem local.inf.orderI)
     1.9    show "x \<in> A \<Longrightarrow> x \<le> \<Squnion>A"
    1.10 -    by (cut_tac A = A and a = x in Sup_finite_insert, simp add: insert_absorb sup.absorb_iff2)
    1.11 +    by (metis Set.set_insert insert_absorb2 local.Sup_finite_insert local.sup.absorb_iff2)
    1.12  next
    1.13    fix A z
    1.14 -  show "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
    1.15 -    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)
    1.16 -    by(cut_tac A = UNIV and a = z in Sup_finite_insert, simp add: insert_UNIV local.sup.absorb_iff2)
    1.17 +  have "\<Squnion> UNIV = z \<squnion> \<Squnion>UNIV"
    1.18 +    by (subst Sup_finite_insert [symmetric], simp add: insert_UNIV)
    1.19 +  from this have [simp]: "z \<le> \<Squnion>UNIV"
    1.20 +    using local.le_iff_sup by auto
    1.21 +  have "(\<forall> x. x \<in> A \<longrightarrow> z \<le> x) \<longrightarrow> z \<le> \<Sqinter>A"
    1.22 +    apply (rule finite_induct [of A "\<lambda> A . (\<forall> x. x \<in> A \<longrightarrow> z \<le> x) \<longrightarrow> z \<le> \<Sqinter>A"])
    1.23 +    by (simp_all add: Inf_finite_empty Inf_finite_insert)
    1.24 +  from this show "(\<And>x. x \<in> A \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> \<Sqinter>A"
    1.25 +    by simp
    1.26  
    1.27 -  show " (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
    1.28 -    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)
    1.29 -    by(cut_tac A = UNIV and a = z in Inf_finite_insert, simp add: insert_UNIV local.inf.absorb_iff2)
    1.30 +  have "\<Sqinter> UNIV = z \<sqinter> \<Sqinter>UNIV"
    1.31 +    by (subst Inf_finite_insert [symmetric], simp add: insert_UNIV)
    1.32 +  from this have [simp]: "\<Sqinter>UNIV \<le> z"
    1.33 +    by (simp add: local.inf.absorb_iff2)
    1.34 +  have "(\<forall> x. x \<in> A \<longrightarrow> x \<le> z) \<longrightarrow> \<Squnion>A \<le> z"
    1.35 +    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)
    1.36 +  from this show " (\<And>x. x \<in> A \<Longrightarrow> x \<le> z) \<Longrightarrow> \<Squnion>A \<le> z"
    1.37 +    by blast
    1.38  next
    1.39    show "\<Sqinter>{} = \<top>"
    1.40      by (simp add: Inf_finite_empty top_finite_def)
    1.41 @@ -818,40 +829,38 @@
    1.42  class finite_distrib_lattice = finite_lattice + distrib_lattice 
    1.43  begin
    1.44  lemma finite_inf_Sup: "a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}"
    1.45 -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)
    1.46 +proof (rule finite_induct [of A "\<lambda> A . a \<sqinter> (Sup A) = Sup {a \<sqinter> b | b . b \<in> A}"], simp_all)
    1.47    fix x::"'a"
    1.48    fix F
    1.49    assume "x \<notin> F"
    1.50 -  assume A: "a \<sqinter> \<Squnion>F = \<Squnion>{a \<sqinter> b |b. b \<in> F}"
    1.51 -
    1.52 +  assume [simp]: "a \<sqinter> \<Squnion>F = \<Squnion>{a \<sqinter> b |b. b \<in> F}"
    1.53    have [simp]: " insert (a \<sqinter> x) {a \<sqinter> b |b. b \<in> F} = {a \<sqinter> b |b. b = x \<or> b \<in> F}"
    1.54 -    by auto
    1.55 -
    1.56 +    by blast
    1.57    have "a \<sqinter> (x \<squnion> \<Squnion>F) = a \<sqinter> x \<squnion> a \<sqinter> \<Squnion>F"
    1.58      by (simp add: inf_sup_distrib1)
    1.59    also have "... = a \<sqinter> x \<squnion> \<Squnion>{a \<sqinter> b |b. b \<in> F}"
    1.60 -    by (simp add: A)
    1.61 +    by simp
    1.62    also have "... = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}"
    1.63      by (unfold Sup_insert[THEN sym], simp)
    1.64 -
    1.65    finally show "a \<sqinter> (x \<squnion> \<Squnion>F) = \<Squnion>{a \<sqinter> b |b. b = x \<or> b \<in> F}"
    1.66      by simp
    1.67  qed
    1.68  
    1.69  lemma finite_Inf_Sup: "INFIMUM A Sup \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
    1.70 -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)
    1.71 +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)
    1.72    fix x::"'a set"
    1.73    fix F
    1.74    assume "x \<notin> F"
    1.75 -  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)}"
    1.76 -    by auto
    1.77 -  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)"
    1.78 -     apply (rule_tac x = "(\<lambda> Y . (if Y = x then b else f Y))" in exI)
    1.79 +  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)}"
    1.80      by auto
    1.81 -  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"
    1.82 -    apply (rule_tac i = "(\<lambda> Y . (if Y = x then b else f Y)) ` ({x} \<union> F)" in SUP_upper2, simp)
    1.83 -    apply (subst inf_commute)
    1.84 -    by (simp add: INF_greatest Inf_lower inf.coboundedI2)
    1.85 +  define fa where "fa = (\<lambda> (b::'a) f Y . (if Y = x then b else f Y))"
    1.86 +  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)"
    1.87 +    by (auto simp add: fa_def)
    1.88 +  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)}"
    1.89 +    by blast
    1.90 +  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"
    1.91 +    using B apply (rule SUP_upper2, simp_all)
    1.92 +    by (simp_all add: INF_greatest Inf_lower inf.coboundedI2 fa_def)
    1.93  
    1.94    assume "INFIMUM F Sup \<le> SUPREMUM {f ` F |f. \<forall>Y\<in>F. f Y \<in> Y} Inf"
    1.95  
    1.96 @@ -866,7 +875,8 @@
    1.97      by (simp add: finite_inf_Sup)
    1.98  
    1.99    also have "... \<le> SUPREMUM {insert (f x) (f ` F) |f. f x \<in> x \<and> (\<forall>Y\<in>F. f Y \<in> Y)} Inf"
   1.100 -    by (rule Sup_least, clarsimp, rule Sup_least, clarsimp)
   1.101 +    apply (rule Sup_least, clarsimp)+
   1.102 +    by (subst inf_commute, simp)
   1.103  
   1.104    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"
   1.105      by simp
     2.1 --- a/src/HOL/Hilbert_Choice.thy	Mon Mar 26 16:12:55 2018 +0200
     2.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Mar 26 16:14:16 2018 +0200
     2.3 @@ -815,7 +815,7 @@
     2.4      using Inf_lower2 Sup_upper by auto
     2.5  next
     2.6    show "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Sup \<le> SUPREMUM A Inf"
     2.7 -  proof (simp add:  Inf_Sup, rule_tac SUP_least, simp, safe)
     2.8 +  proof (simp add:  Inf_Sup, rule SUP_least, simp, safe)
     2.9      fix f
    2.10      assume "\<forall>Y. (\<exists>f. Y = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y)) \<longrightarrow> f Y \<in> Y"
    2.11      from this have B: "\<And> F . (\<forall> Y \<in> A . F Y \<in> Y) \<Longrightarrow> \<exists> Z \<in> A . f (F ` A) = F Z"
    2.12 @@ -828,7 +828,7 @@
    2.13        have B: "... \<le> SUPREMUM A Inf"
    2.14          by (simp add: SUP_upper)
    2.15        from A and B show ?thesis
    2.16 -        by (drule_tac order_trans, simp_all)
    2.17 +        by simp
    2.18      next
    2.19        case False
    2.20        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"
    2.21 @@ -842,8 +842,9 @@
    2.22          by blast
    2.23        from E and D have W: "\<not> INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> F Z"
    2.24          by simp
    2.25 -      from C have "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> f (F ` A)"
    2.26 -        by (rule_tac INF_lower, blast)
    2.27 +      have "INFIMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} f \<le> f (F ` A)"
    2.28 +        apply (rule INF_lower)
    2.29 +        using C by blast
    2.30        from this and W and Y show ?thesis
    2.31          by simp
    2.32      qed
    2.33 @@ -859,12 +860,13 @@
    2.34  lemma sup_Inf: "a \<squnion> Inf B = (INF b:B. a \<squnion> b)"
    2.35  proof (rule antisym)
    2.36    show "a \<squnion> Inf B \<le> (INF b:B. a \<squnion> b)"
    2.37 -    using Inf_lower sup.mono by (rule_tac INF_greatest, fastforce)
    2.38 +    apply (rule INF_greatest)
    2.39 +    using Inf_lower sup.mono by fastforce
    2.40  next
    2.41    have "(INF b:B. a \<squnion> b) \<le> INFIMUM {{f {a}, f B} |f. f {a} = a \<and> f B \<in> B} Sup"
    2.42      by (rule INF_greatest, auto simp add: INF_lower)
    2.43 -  also have "... = a \<squnion> Inf B"
    2.44 -    by (cut_tac A = "{{a}, B}" in Sup_Inf, simp)
    2.45 +  also have "... = SUPREMUM {{a}, B} Inf"
    2.46 +    by (unfold Sup_Inf, simp)
    2.47    finally show "(INF b:B. a \<squnion> b) \<le> a \<squnion> Inf B"
    2.48      by simp
    2.49  qed
    2.50 @@ -879,7 +881,7 @@
    2.51      by (rule SUP_least, rule INF_greatest, rule SUP_upper2, simp_all, rule INF_lower2, simp, blast)
    2.52  next
    2.53    have "(INF y. SUP x. ((P x y))) \<le> Inf (Sup ` {{P x y | x . True} | y . True })" (is "?A \<le> ?B")
    2.54 -  proof (rule_tac INF_greatest, clarsimp)
    2.55 +  proof (rule INF_greatest, clarsimp)
    2.56      fix y
    2.57      have "?A \<le> (SUP x. P x y)"
    2.58        by (rule INF_lower, simp)
    2.59 @@ -889,7 +891,7 @@
    2.60        by simp
    2.61    qed
    2.62    also have "... \<le>  (SUP x. INF y. P (x y) y)"
    2.63 -  proof (subst  Inf_Sup, rule_tac SUP_least, clarsimp)
    2.64 +  proof (subst Inf_Sup, rule SUP_least, clarsimp)
    2.65      fix f
    2.66      assume A: "\<forall>Y. (\<exists>y. Y = {uu. \<exists>x. uu = P x y}) \<longrightarrow> f Y \<in> Y"
    2.67        
    2.68 @@ -897,9 +899,10 @@
    2.69      proof (rule INF_greatest, clarsimp)
    2.70        fix y
    2.71          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}"
    2.72 -          by (rule_tac INF_lower, blast)
    2.73 +          by (rule INF_lower, blast)
    2.74          also have "... \<le> P (SOME x. f {uu . \<exists>x. uu = P x y} = P x y) y"
    2.75 -          using A by (rule_tac someI2_ex, auto)
    2.76 +          apply (rule someI2_ex)
    2.77 +          using A by auto
    2.78          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"
    2.79            by simp
    2.80        qed
    2.81 @@ -914,8 +917,12 @@
    2.82  
    2.83  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)"
    2.84  proof (rule antisym)
    2.85 +  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)"
    2.86 +    by (rule INF_lower2, blast+)
    2.87 +  have B: "\<And>f xa. \<forall>Y\<in>A. f Y \<in> Y \<Longrightarrow> xa \<in> A \<Longrightarrow> f xa \<in> xa"
    2.88 +    by blast
    2.89    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"
    2.90 -    by (rule_tac i = "(f xa)" in SUP_upper2, simp, rule_tac i = "xa" in INF_lower2, simp_all)
    2.91 +    by (rule SUP_upper2, rule B, simp_all, simp)
    2.92    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)"
    2.93      apply (rule SUP_least, simp, safe, rule INF_greatest, simp)
    2.94      by (rule A)
    2.95 @@ -924,22 +931,38 @@
    2.96    proof (cases "{} \<in> A")
    2.97      case True
    2.98      then show ?thesis 
    2.99 -      by (rule_tac i = "{}" in INF_lower2, simp_all)
   2.100 +      by (rule INF_lower2, simp_all)
   2.101    next
   2.102      case False
   2.103      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)"
   2.104 -      by (rule_tac i = xb in INF_lower2, simp_all)
   2.105 +      by (rule INF_lower2, auto)
   2.106      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)"
   2.107 -      by (rule_tac i = y in INF_lower2, simp_all)
   2.108 +      by (rule INF_lower2, auto)
   2.109      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)"
   2.110 -      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)
   2.111 -       apply (rule_tac x = "(\<lambda> y . if x y \<in> y then x y else (SOME x . x \<in>y))" in exI, simp)
   2.112 -      using False some_in_eq apply auto[1]
   2.113 -      by (rule INF_greatest, auto)
   2.114 -    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>)"
   2.115 -      apply (case_tac "x \<in> A")
   2.116 -       apply (rule INF_lower2, simp)
   2.117 -      by (rule SUP_least, rule SUP_upper2, auto)
   2.118 +    proof -
   2.119 +      fix x
   2.120 +      define F where "F = (\<lambda> (y::'b set) . if x y \<in> y then x y else (SOME x . x \<in>y))"
   2.121 +      have B: "(\<forall>Y\<in>A. F Y \<in> Y)"
   2.122 +        using False some_in_eq F_def by auto
   2.123 +      have A: "F ` A \<in> {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
   2.124 +        using B by blast
   2.125 +      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)"
   2.126 +        using A apply (rule SUP_upper2)
   2.127 +        by (simp add: F_def, rule INF_greatest, auto)
   2.128 +    qed
   2.129 +
   2.130 +    {fix x
   2.131 +      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>)"
   2.132 +      proof (cases "x \<in> A")
   2.133 +        case True
   2.134 +        then show ?thesis
   2.135 +          apply (rule INF_lower2, simp_all)
   2.136 +          by (rule SUP_least, rule SUP_upper2, auto)
   2.137 +      next
   2.138 +        case False
   2.139 +        then show ?thesis by simp
   2.140 +      qed
   2.141 +    }
   2.142      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>)"
   2.143        by (rule INF_greatest)
   2.144      also have "... = (\<Squnion>x. \<Sqinter>xa. if xa \<in> A then if x xa \<in> xa then g (x xa) else \<bottom> else \<top>)"
   2.145 @@ -1020,10 +1043,14 @@
   2.146    from this have B: " (\<forall>xa \<in> F ` A. x \<in> xa)"
   2.147      apply (safe, simp add: F_def)
   2.148      by (rule someI2_ex, auto)
   2.149 -    
   2.150 +
   2.151 +  have C: "(\<forall>Y\<in>A. F Y \<in> Y)"
   2.152 +    apply (simp  add: F_def, safe)
   2.153 +    apply (rule someI2_ex)
   2.154 +    using A by auto
   2.155 +
   2.156    have "(\<exists>f. F ` A  = f ` A \<and> (\<forall>Y\<in>A. f Y \<in> Y))"
   2.157 -    apply (rule_tac x = "F" in exI, simp add: F_def, safe)
   2.158 -    using A by (rule_tac someI2_ex, auto)
   2.159 +    using C by blast
   2.160      
   2.161    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)"
   2.162      by auto
   2.163 @@ -1063,10 +1090,13 @@
   2.164        define F where "F = (\<lambda> Y . SOME k . k \<in> Y \<and> z < k)"
   2.165          
   2.166        have D: "\<And> Y . Y \<in> A \<Longrightarrow> z < F Y"
   2.167 -        using B by (simp add: F_def, rule_tac someI2_ex, auto)
   2.168 +        using B apply (simp add: F_def)
   2.169 +        by (rule someI2_ex, auto)
   2.170 +
   2.171      
   2.172        have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
   2.173 -        using B by (simp add: F_def, rule_tac someI2_ex, auto)
   2.174 +        using B apply (simp add: F_def)
   2.175 +        by (rule someI2_ex, auto)
   2.176      
   2.177        have "z \<le> Inf (F ` A)"
   2.178          by (simp add: D local.INF_greatest local.order.strict_implies_order)
   2.179 @@ -1093,10 +1123,12 @@
   2.180        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)"
   2.181          
   2.182        have D: "\<And> Y . Y \<in> A \<Longrightarrow> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf < F Y"
   2.183 -        using B by (simp add: F_def, rule_tac someI2_ex, auto)
   2.184 +        using B apply (simp add: F_def)
   2.185 +        by (rule someI2_ex, auto)
   2.186      
   2.187        have E: "\<And> Y . Y \<in> A \<Longrightarrow> F Y \<in> Y"
   2.188 -        using B by (simp add: F_def, rule_tac someI2_ex, auto)
   2.189 +        using B apply (simp add: F_def)
   2.190 +        by (rule someI2_ex, auto)
   2.191            
   2.192        have "\<And> Y . Y \<in> A \<Longrightarrow> INFIMUM A Sup \<le> F Y"
   2.193          using D False local.leI by blast
   2.194 @@ -1112,7 +1144,7 @@
   2.195          by simp
   2.196          
   2.197        from C and this show ?thesis
   2.198 -        using local.not_less by blast
   2.199 +        using not_less by blast
   2.200      qed
   2.201    qed
   2.202  end
     3.1 --- a/src/HOL/Library/Option_ord.thy	Mon Mar 26 16:12:55 2018 +0200
     3.2 +++ b/src/HOL/Library/Option_ord.thy	Mon Mar 26 16:14:16 2018 +0200
     3.3 @@ -287,7 +287,7 @@
     3.4  proof (cases "{} \<in> A")
     3.5    case True
     3.6    then show ?thesis
     3.7 -    by (rule_tac i = "{}" in INF_lower2, simp_all)
     3.8 +    by (rule INF_lower2, simp_all)
     3.9  next
    3.10    case False
    3.11    from this have X: "{} \<notin> A"
    3.12 @@ -296,37 +296,41 @@
    3.13    proof (cases "{None} \<in> A")
    3.14      case True
    3.15      then show ?thesis
    3.16 -      by (rule_tac i = "{None}" in INF_lower2, simp_all)
    3.17 +      by (rule INF_lower2, simp_all)
    3.18    next
    3.19      case False
    3.20 -    have "\<And> y . y\<in>A \<Longrightarrow> Sup (y - {None}) = Sup y"
    3.21 -      by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq)
    3.22 -   
    3.23 +
    3.24 +    {fix y
    3.25 +      assume A: "y \<in> A"
    3.26 +      have "Sup (y - {None}) = Sup y"
    3.27 +        by (metis (no_types, lifting) Sup_option_def insert_Diff_single these_insert_None these_not_empty_eq)
    3.28 +      from A and this have "(\<exists>z. y - {None} = z - {None} \<and> z \<in> A) \<and> \<Squnion>y = \<Squnion>(y - {None})"
    3.29 +        by auto
    3.30 +    }
    3.31      from this have A: "Sup ` A = (Sup ` {y - {None} | y. y\<in>A})"
    3.32 -      apply (simp add: image_def, simp, safe)
    3.33 -       apply (rule_tac x = "xa - {None}" in exI, simp, blast)
    3.34 -      by blast
    3.35 +      by (auto simp add: image_def)
    3.36  
    3.37      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} 
    3.38            = {y. \<exists>x\<in>ya - {None}. y = the x} \<and> ya \<in> A"
    3.39 -      by (rule_tac x = "y" in exI, auto)
    3.40 +      by (rule exI, auto)
    3.41  
    3.42      have [simp]: "\<And>y. y \<in> A \<Longrightarrow>
    3.43           (\<exists>ya. y - {None} = ya - {None} \<and> ya \<in> A) \<and> \<Squnion>{ya. \<exists>x\<in>y - {None}. ya = the x} 
    3.44            = \<Squnion>{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"
    3.45 -      apply safe
    3.46 -       apply blast
    3.47 -      apply (rule_tac f = Sup in arg_cong)
    3.48 -      by auto
    3.49 -
    3.50 -    have C: "(\<lambda>x.  (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A} =  (Sup ` {the ` (y - {None}) |y. y \<in> A})"
    3.51 -      apply (simp add: image_def Option.these_def, safe)
    3.52 -       apply (rule_tac x = "{ya. \<exists>x. x \<in> y - {None} \<and> (\<exists>y. x = Some y) \<and> ya = the x}" in exI, simp)
    3.53 -      by (rule_tac x = "y -{None}" in exI, simp)
    3.54 +      apply (safe, blast)
    3.55 +      by (rule arg_cong [of _ _ Sup], auto)
    3.56 +    {fix y
    3.57 +      assume [simp]: "y \<in> A"
    3.58 +      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"
    3.59 +      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}"
    3.60 +         apply (rule exI [of _ "{ya. \<exists>x. x \<in> y \<and> (\<exists>y. x = Some y) \<and> ya = the x}"], simp)
    3.61 +        by (rule exI [of _ "y - {None}"], simp)
    3.62 +    }
    3.63 +    from this have C: "(\<lambda>x.  (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A} =  (Sup ` {the ` (y - {None}) |y. y \<in> A})"
    3.64 +      by (simp add: image_def Option.these_def, safe, simp_all)
    3.65    
    3.66      have D: "\<forall> f . \<exists>Y\<in>A. f Y \<notin> Y \<Longrightarrow> False"
    3.67 -      apply (drule_tac x = "\<lambda> Y . SOME x . x \<in> Y" in spec, safe)
    3.68 -      by (simp add: X some_in_eq)
    3.69 +      by (drule spec [of _ "\<lambda> Y . SOME x . x \<in> Y"], simp add: X some_in_eq)
    3.70    
    3.71      define F where "F = (\<lambda> Y . SOME x::'a option . x \<in> (Y - {None}))"
    3.72    
    3.73 @@ -341,12 +345,13 @@
    3.74            less_eq_option_Some singletonI)
    3.75        
    3.76      from this have "Inf (F ` A) \<noteq> None"
    3.77 -      by (case_tac "\<Sqinter>x\<in>A. F x", simp_all)
    3.78 -  
    3.79 +      by (cases "\<Sqinter>x\<in>A. F x", simp_all)
    3.80 +
    3.81 +    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}"
    3.82 +      using F by auto
    3.83 +
    3.84      from this have "\<exists> x . x \<noteq> None \<and> x \<in> Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}"
    3.85 -      apply (rule_tac x = "Inf (F ` A)" in exI, simp add: image_def, safe)
    3.86 -      apply (rule_tac x = "F `  A" in exI, safe)
    3.87 -      using F by auto
    3.88 +      by blast
    3.89    
    3.90      from this have E:" Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} = {None} \<Longrightarrow> False"
    3.91        by blast
    3.92 @@ -358,36 +363,59 @@
    3.93      have B: "Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}) 
    3.94          = ((\<lambda>x. (\<Squnion> Option.these x)) ` {y - {None} |y. y \<in> A})"
    3.95        by (metis image_image these_image_Some_eq)
    3.96 +    {
    3.97 +      fix f
    3.98 +      assume A: "\<And> Y . (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<Longrightarrow> f Y \<in> Y"
    3.99  
   3.100 -    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>
   3.101 -         \<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"
   3.102 -      apply (rule_tac x = "{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) | x . x\<in> A}" in exI, safe)
   3.103 -       apply (rule_tac x = "(\<lambda> Y . Some (f (the ` (Y - {None})))) " in exI, safe)
   3.104 -         apply (rule_tac x = xa in bexI, simp add: image_def, simp)
   3.105 -        apply (rule_tac x = xa in exI, simp add: image_def)
   3.106 -       apply(drule_tac x = "(the ` (Y - {None}))" in spec)
   3.107 -       apply (simp add: image_def,safe, simp)
   3.108 -      using option.collapse apply fastforce
   3.109 -      by (simp add: Setcompr_eq_image)
   3.110 +      have "\<And>xa. xa \<in> A \<Longrightarrow> f {y. \<exists>a\<in>xa - {None}. y = the a} = f (the ` (xa - {None}))"
   3.111 +        by  (simp add: image_def)
   3.112 +      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}))"
   3.113 +        by blast
   3.114 +      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"
   3.115 +        by (simp add: image_def)
   3.116 +      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"
   3.117 +        by blast
   3.118  
   3.119 -    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 
   3.120 -        \<Longrightarrow> \<exists>y. (\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x})) = Some y"
   3.121 -      by (metis (no_types) Some_INF)
   3.122 +      {
   3.123 +        fix Y
   3.124 +        have "Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y"
   3.125 +          using A [of "the ` (Y - {None})"] apply (simp add: image_def)
   3.126 +          using option.collapse by fastforce
   3.127 +      }
   3.128 +      from this have [simp]: "\<And> Y . Y \<in> A \<Longrightarrow> Some (f (the ` (Y - {None}))) \<in> Y"
   3.129 +        by blast
   3.130 +      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}"
   3.131 +        by (simp add: Setcompr_eq_image)
   3.132 +      
   3.133 +      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"
   3.134 +        apply (rule exI [of _ "{Some (f {y. \<exists>a\<in>x - {None}. y = the a}) | x . x\<in> A}"], safe)
   3.135 +        by (rule exI [of _ "(\<lambda> Y . Some (f (the ` (Y - {None})))) "], safe, simp_all)
   3.136  
   3.137 -    have [simp]: "\<And> f.
   3.138 -         (\<Sqinter>x\<in>{the ` (y - {None}) |y. y \<in> A}. f x) \<le> the (\<Sqinter>Y\<in>A. Some (f (the ` (Y - {None}))))"
   3.139 -      apply (simp add: Inf_option_def, safe)
   3.140 -      apply (rule Inf_greatest, simp add: image_def Option.these_def, safe)
   3.141 -      apply (rule_tac i = " {y. \<exists>x\<in>xb - {None}. y = the x}" in INF_lower2)
   3.142 -       apply simp_all
   3.143 +      {
   3.144 +        fix xb
   3.145 +        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}"
   3.146 +          apply (rule INF_lower2 [of "{y. \<exists>x\<in>xb - {None}. y = the x}"])
   3.147 +          by blast+
   3.148 +      }
   3.149 +      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}))))"
   3.150 +        apply (simp add: Inf_option_def image_def Option.these_def)
   3.151 +        by (rule Inf_greatest, clarsimp)
   3.152 +
   3.153 +      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})"
   3.154 +        apply (simp add:  Option.these_def image_def)
   3.155 +        apply (rule exI [of _ "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x}))"], simp)
   3.156 +        by (simp add: Inf_option_def)
   3.157 +
   3.158 +      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})"
   3.159 +        by (rule Sup_upper2 [of "the (Inf ((\<lambda> Y . Some (f (the ` (Y - {None})) )) ` A))"], simp_all)
   3.160 +    }
   3.161 +    from this have X: "\<And> f . \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y \<Longrightarrow>
   3.162 +      (\<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})"
   3.163        by blast
   3.164 +    
   3.165  
   3.166 -    have X: "\<And> f . \<forall>Y. (\<exists>y. Y = the ` (y - {None}) \<and> y \<in> A) \<longrightarrow> f Y \<in> Y
   3.167 -      \<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})"
   3.168 -      apply (rule_tac u = "the (Inf ((\<lambda> Y . Some (f (the ` (Y - {None})) )) ` A))" in Sup_upper2)
   3.169 -       apply (simp add:  Option.these_def image_def)
   3.170 -       apply (rule_tac x = "(\<Sqinter>x\<in>A. Some (f {y. \<exists>x\<in>x - {None}. y = the x}))" in exI, simp)
   3.171 -      by simp
   3.172 +    have [simp]: "\<And> x . x\<in>{y - {None} |y. y \<in> A} \<Longrightarrow>  x \<noteq> {} \<and> x \<noteq> {None}"
   3.173 +      using F by fastforce
   3.174  
   3.175      have "(Inf (Sup `A)) = (Inf (Sup ` {y - {None} | y. y\<in>A}))"
   3.176        by (subst A, simp)
   3.177 @@ -396,7 +424,6 @@
   3.178        by (simp add: Sup_option_def)
   3.179  
   3.180      also have "... = (\<Sqinter>x\<in>{y - {None} |y. y \<in> A}. Some (\<Squnion>Option.these x))"
   3.181 -      apply (subgoal_tac "\<And> x . x\<in>{y - {None} |y. y \<in> A} \<Longrightarrow>  x \<noteq> {} \<and> x \<noteq> {None}", simp)
   3.182        using G by fastforce
   3.183    
   3.184      also have "... = Some (\<Sqinter>Option.these ((\<lambda>x. Some (\<Squnion>Option.these x)) ` {y - {None} |y. y \<in> A}))"
   3.185 @@ -412,12 +439,18 @@
   3.186        by (simp add: Inf_Sup)
   3.187    
   3.188      also have "... \<le> SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf"
   3.189 -      apply (simp add: less_eq_option_def)
   3.190 -      apply (case_tac "\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>x", simp_all)
   3.191 -      apply (rule Sup_least, safe)
   3.192 -      apply (simp add: Sup_option_def)
   3.193 -      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)
   3.194 -      by (drule X, simp)
   3.195 +    proof (cases "SUPREMUM {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y} Inf")
   3.196 +      case None
   3.197 +      then show ?thesis by (simp add: less_eq_option_def)
   3.198 +    next
   3.199 +      case (Some a)
   3.200 +      then show ?thesis
   3.201 +        apply simp
   3.202 +        apply (rule Sup_least, safe)
   3.203 +        apply (simp add: Sup_option_def)
   3.204 +        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)
   3.205 +        by (drule X, simp)
   3.206 +    qed
   3.207      finally show ?thesis by simp
   3.208    qed
   3.209  qed
     4.1 --- a/src/HOL/Predicate.thy	Mon Mar 26 16:12:55 2018 +0200
     4.2 +++ b/src/HOL/Predicate.thy	Mon Mar 26 16:14:16 2018 +0200
     4.3 @@ -110,9 +110,10 @@
     4.4      define F where "F = (\<lambda> x . SOME f . f \<in> x \<and> eval f w)"
     4.5      have [simp]: "(\<forall>f\<in> (F ` A). eval f w)"
     4.6        by (metis (no_types, lifting) A F_def image_iff some_eq_ex)
     4.7 -    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)"
     4.8 -      apply (rule_tac x = "F ` A" in exI, simp)
     4.9 -      using A by (metis (no_types, lifting) F_def someI)+
    4.10 +    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)"
    4.11 +      using A by (simp, metis (no_types, lifting) F_def someI)+
    4.12 +    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)"
    4.13 +      by (rule exI [of _ "F ` A"])
    4.14    qed
    4.15  qed (auto intro!: pred_eqI)
    4.16