tune simpset for Complete_Lattices
authornoschinl
Tue Sep 13 16:21:48 2011 +0200 (2011-09-13)
changeset 449186a80fbc4e72c
parent 44917 8df4c332cb1c
child 44919 482f1807976e
tune simpset for Complete_Lattices
src/HOL/Big_Operators.thy
src/HOL/Complete_Lattices.thy
src/HOL/Induct/Sexp.thy
src/HOL/Lattices.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Kleene_Algebra.thy
src/HOL/Main.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/UNITY/ProgressSets.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Tue Sep 13 13:17:52 2011 +0200
     1.2 +++ b/src/HOL/Big_Operators.thy	Tue Sep 13 16:21:48 2011 +0200
     1.3 @@ -1433,11 +1433,10 @@
     1.4  proof -
     1.5    interpret ab_semigroup_idem_mult inf
     1.6      by (rule ab_semigroup_idem_mult_inf)
     1.7 -  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
     1.8 +  from `A \<noteq> {}` obtain b B where "A = {b} \<union> B" by auto
     1.9    moreover with `finite A` have "finite B" by simp
    1.10 -  ultimately show ?thesis  
    1.11 -  by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
    1.12 -    (simp add: Inf_fold_inf)
    1.13 +  ultimately show ?thesis
    1.14 +    by (simp add: Inf_fin_def fold1_eq_fold_idem inf_Inf_fold_inf [symmetric])
    1.15  qed
    1.16  
    1.17  lemma Sup_fin_Sup:
    1.18 @@ -1446,11 +1445,10 @@
    1.19  proof -
    1.20    interpret ab_semigroup_idem_mult sup
    1.21      by (rule ab_semigroup_idem_mult_sup)
    1.22 -  from `A \<noteq> {}` obtain b B where "A = insert b B" by auto
    1.23 +  from `A \<noteq> {}` obtain b B where "A = {b} \<union> B" by auto
    1.24    moreover with `finite A` have "finite B" by simp
    1.25    ultimately show ?thesis  
    1.26    by (simp add: Sup_fin_def fold1_eq_fold_idem sup_Sup_fold_sup [symmetric])
    1.27 -    (simp add: Sup_fold_sup)
    1.28  qed
    1.29  
    1.30  end
     2.1 --- a/src/HOL/Complete_Lattices.thy	Tue Sep 13 13:17:52 2011 +0200
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Sep 13 16:21:48 2011 +0200
     2.3 @@ -126,16 +126,16 @@
     2.4  lemma SUP_upper2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
     2.5    using SUP_upper [of i A f] by auto
     2.6  
     2.7 -lemma le_Inf_iff (*[simp]*): "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
     2.8 +lemma le_Inf_iff: "b \<sqsubseteq> \<Sqinter>A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
     2.9    by (auto intro: Inf_greatest dest: Inf_lower)
    2.10  
    2.11 -lemma le_INF_iff (*[simp]*): "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
    2.12 +lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<sqsubseteq> f i)"
    2.13    by (auto simp add: INF_def le_Inf_iff)
    2.14  
    2.15 -lemma Sup_le_iff (*[simp]*): "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
    2.16 +lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
    2.17    by (auto intro: Sup_least dest: Sup_upper)
    2.18  
    2.19 -lemma SUP_le_iff (*[simp]*): "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
    2.20 +lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
    2.21    by (auto simp add: SUP_def Sup_le_iff)
    2.22  
    2.23  lemma Inf_empty [simp]:
    2.24 @@ -160,22 +160,22 @@
    2.25    "\<Squnion>UNIV = \<top>"
    2.26    by (auto intro!: antisym Sup_upper)
    2.27  
    2.28 -lemma Inf_insert (*[simp]*): "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    2.29 +lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
    2.30    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
    2.31  
    2.32  lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
    2.33    by (simp add: INF_def Inf_insert)
    2.34  
    2.35 -lemma Sup_insert (*[simp]*): "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    2.36 +lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    2.37    by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
    2.38  
    2.39  lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
    2.40    by (simp add: SUP_def Sup_insert)
    2.41  
    2.42 -lemma INF_image (*[simp]*): "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
    2.43 +lemma INF_image [simp]: "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
    2.44    by (simp add: INF_def image_image)
    2.45  
    2.46 -lemma SUP_image (*[simp]*): "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))"
    2.47 +lemma SUP_image [simp]: "(\<Squnion>x\<in>f`A. g x) = (\<Squnion>x\<in>A. g (f x))"
    2.48    by (simp add: SUP_def image_image)
    2.49  
    2.50  lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<sqsubseteq> a}"
    2.51 @@ -210,7 +210,7 @@
    2.52  
    2.53  lemma INF_mono:
    2.54    "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<sqsubseteq> (\<Sqinter>n\<in>B. g n)"
    2.55 -  by (force intro!: Inf_mono simp: INF_def)
    2.56 +  unfolding INF_def by (rule Inf_mono) fast
    2.57  
    2.58  lemma Sup_mono:
    2.59    assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
    2.60 @@ -224,7 +224,7 @@
    2.61  
    2.62  lemma SUP_mono:
    2.63    "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<sqsubseteq> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<sqsubseteq> (\<Squnion>n\<in>B. g n)"
    2.64 -  by (force intro!: Sup_mono simp: SUP_def)
    2.65 +  unfolding SUP_def by (rule Sup_mono) fast
    2.66  
    2.67  lemma INF_superset_mono:
    2.68    "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
    2.69 @@ -278,11 +278,14 @@
    2.70  lemma INF_inf_distrib: "(\<Sqinter>a\<in>A. f a) \<sqinter> (\<Sqinter>a\<in>A. g a) = (\<Sqinter>a\<in>A. f a \<sqinter> g a)"
    2.71    by (rule antisym) (rule INF_greatest, auto intro: le_infI1 le_infI2 INF_lower INF_mono)
    2.72  
    2.73 -lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)"
    2.74 -  by (rule antisym) (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono,
    2.75 -    rule SUP_least, auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
    2.76 +lemma SUP_sup_distrib: "(\<Squnion>a\<in>A. f a) \<squnion> (\<Squnion>a\<in>A. g a) = (\<Squnion>a\<in>A. f a \<squnion> g a)" (is "?L = ?R")
    2.77 +proof (rule antisym)
    2.78 +  show "?L \<le> ?R" by (auto intro: le_supI1 le_supI2 SUP_upper SUP_mono)
    2.79 +next
    2.80 +  show "?R \<le> ?L" by (rule SUP_least) (auto intro: le_supI1 le_supI2 SUP_upper)
    2.81 +qed
    2.82  
    2.83 -lemma Inf_top_conv (*[simp]*) [no_atp]:
    2.84 +lemma Inf_top_conv [simp, no_atp]:
    2.85    "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
    2.86    "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
    2.87  proof -
    2.88 @@ -304,12 +307,12 @@
    2.89    then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
    2.90  qed
    2.91  
    2.92 -lemma INF_top_conv (*[simp]*):
    2.93 +lemma INF_top_conv [simp]:
    2.94   "(\<Sqinter>x\<in>A. B x) = \<top> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
    2.95   "\<top> = (\<Sqinter>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<top>)"
    2.96    by (auto simp add: INF_def Inf_top_conv)
    2.97  
    2.98 -lemma Sup_bot_conv (*[simp]*) [no_atp]:
    2.99 +lemma Sup_bot_conv [simp, no_atp]:
   2.100    "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
   2.101    "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
   2.102  proof -
   2.103 @@ -318,7 +321,7 @@
   2.104    from dual.Inf_top_conv show ?P and ?Q by simp_all
   2.105  qed
   2.106  
   2.107 -lemma SUP_bot_conv (*[simp]*):
   2.108 +lemma SUP_bot_conv [simp]:
   2.109   "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   2.110   "\<bottom> = (\<Squnion>x\<in>A. B x) \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   2.111    by (auto simp add: SUP_def Sup_bot_conv)
   2.112 @@ -329,10 +332,10 @@
   2.113  lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
   2.114    by (auto intro: antisym SUP_upper SUP_least)
   2.115  
   2.116 -lemma INF_top (*[simp]*): "(\<Sqinter>x\<in>A. \<top>) = \<top>"
   2.117 +lemma INF_top [simp]: "(\<Sqinter>x\<in>A. \<top>) = \<top>"
   2.118    by (cases "A = {}") (simp_all add: INF_empty)
   2.119  
   2.120 -lemma SUP_bot (*[simp]*): "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
   2.121 +lemma SUP_bot [simp]: "(\<Squnion>x\<in>A. \<bottom>) = \<bottom>"
   2.122    by (cases "A = {}") (simp_all add: SUP_empty)
   2.123  
   2.124  lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)"
   2.125 @@ -492,23 +495,23 @@
   2.126    "class.complete_linorder Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   2.127    by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
   2.128  
   2.129 -lemma Inf_less_iff (*[simp]*):
   2.130 +lemma Inf_less_iff:
   2.131    "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
   2.132    unfolding not_le [symmetric] le_Inf_iff by auto
   2.133  
   2.134 -lemma INF_less_iff (*[simp]*):
   2.135 +lemma INF_less_iff:
   2.136    "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
   2.137    unfolding INF_def Inf_less_iff by auto
   2.138  
   2.139 -lemma less_Sup_iff (*[simp]*):
   2.140 +lemma less_Sup_iff:
   2.141    "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
   2.142    unfolding not_le [symmetric] Sup_le_iff by auto
   2.143  
   2.144 -lemma less_SUP_iff (*[simp]*):
   2.145 +lemma less_SUP_iff:
   2.146    "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   2.147    unfolding SUP_def less_Sup_iff by auto
   2.148  
   2.149 -lemma Sup_eq_top_iff (*[simp]*):
   2.150 +lemma Sup_eq_top_iff [simp]:
   2.151    "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
   2.152  proof
   2.153    assume *: "\<Squnion>A = \<top>"
   2.154 @@ -530,11 +533,11 @@
   2.155    qed
   2.156  qed
   2.157  
   2.158 -lemma SUP_eq_top_iff (*[simp]*):
   2.159 +lemma SUP_eq_top_iff [simp]:
   2.160    "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
   2.161    unfolding SUP_def Sup_eq_top_iff by auto
   2.162  
   2.163 -lemma Inf_eq_bot_iff (*[simp]*):
   2.164 +lemma Inf_eq_bot_iff [simp]:
   2.165    "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
   2.166  proof -
   2.167    interpret dual: complete_linorder Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
   2.168 @@ -542,7 +545,7 @@
   2.169    from dual.Sup_eq_top_iff show ?thesis .
   2.170  qed
   2.171  
   2.172 -lemma INF_eq_bot_iff (*[simp]*):
   2.173 +lemma INF_eq_bot_iff [simp]:
   2.174    "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
   2.175    unfolding INF_def Inf_eq_bot_iff by auto
   2.176  
     3.1 --- a/src/HOL/Induct/Sexp.thy	Tue Sep 13 13:17:52 2011 +0200
     3.2 +++ b/src/HOL/Induct/Sexp.thy	Tue Sep 13 16:21:48 2011 +0200
     3.3 @@ -73,7 +73,7 @@
     3.4  (** Introduction rules for 'pred_sexp' **)
     3.5  
     3.6  lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp"
     3.7 -by (simp add: pred_sexp_def, blast)
     3.8 +  by (simp add: pred_sexp_def) blast
     3.9  
    3.10  (* (a,b) \<in> pred_sexp^+ ==> a \<in> sexp *)
    3.11  lemmas trancl_pred_sexpD1 = 
     4.1 --- a/src/HOL/Lattices.thy	Tue Sep 13 13:17:52 2011 +0200
     4.2 +++ b/src/HOL/Lattices.thy	Tue Sep 13 16:21:48 2011 +0200
     4.3 @@ -180,10 +180,10 @@
     4.4  lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
     4.5    by (fact inf.left_commute)
     4.6  
     4.7 -lemma inf_idem (*[simp]*): "x \<sqinter> x = x"
     4.8 +lemma inf_idem [simp]: "x \<sqinter> x = x"
     4.9    by (fact inf.idem)
    4.10  
    4.11 -lemma inf_left_idem (*[simp]*): "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    4.12 +lemma inf_left_idem [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    4.13    by (fact inf.left_idem)
    4.14  
    4.15  lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
    4.16 @@ -219,10 +219,10 @@
    4.17  lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
    4.18    by (fact sup.left_commute)
    4.19  
    4.20 -lemma sup_idem (*[simp]*): "x \<squnion> x = x"
    4.21 +lemma sup_idem [simp]: "x \<squnion> x = x"
    4.22    by (fact sup.idem)
    4.23  
    4.24 -lemma sup_left_idem (*[simp]*): "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    4.25 +lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    4.26    by (fact sup.left_idem)
    4.27  
    4.28  lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
    4.29 @@ -243,10 +243,10 @@
    4.30    by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
    4.31      (unfold_locales, auto)
    4.32  
    4.33 -lemma inf_sup_absorb (*[simp]*): "x \<sqinter> (x \<squnion> y) = x"
    4.34 +lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x"
    4.35    by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
    4.36  
    4.37 -lemma sup_inf_absorb (*[simp]*): "x \<squnion> (x \<sqinter> y) = x"
    4.38 +lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x"
    4.39    by (blast intro: antisym sup_ge1 sup_least inf_le1)
    4.40  
    4.41  lemmas inf_sup_aci = inf_aci sup_aci
    4.42 @@ -267,8 +267,9 @@
    4.43  assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    4.44  shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    4.45  proof-
    4.46 -  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
    4.47 -  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
    4.48 +  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by simp
    4.49 +  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))"
    4.50 +    by (simp add: D inf_commute sup_assoc del: sup_inf_absorb)
    4.51    also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
    4.52      by(simp add:inf_sup_absorb inf_commute)
    4.53    also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
    4.54 @@ -279,8 +280,9 @@
    4.55  assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    4.56  shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    4.57  proof-
    4.58 -  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
    4.59 -  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
    4.60 +  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by simp
    4.61 +  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))"
    4.62 +    by (simp add: D sup_commute inf_assoc del: inf_sup_absorb)
    4.63    also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
    4.64      by(simp add:sup_inf_absorb sup_commute)
    4.65    also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
    4.66 @@ -439,11 +441,11 @@
    4.67    by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    4.68      (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
    4.69  
    4.70 -lemma compl_inf_bot (*[simp]*):
    4.71 +lemma compl_inf_bot [simp]:
    4.72    "- x \<sqinter> x = \<bottom>"
    4.73    by (simp add: inf_commute inf_compl_bot)
    4.74  
    4.75 -lemma compl_sup_top (*[simp]*):
    4.76 +lemma compl_sup_top [simp]:
    4.77    "- x \<squnion> x = \<top>"
    4.78    by (simp add: sup_commute sup_compl_top)
    4.79  
    4.80 @@ -525,7 +527,7 @@
    4.81    then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
    4.82  qed
    4.83  
    4.84 -lemma compl_le_compl_iff (*[simp]*):
    4.85 +lemma compl_le_compl_iff [simp]:
    4.86    "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
    4.87    by (auto dest: compl_mono)
    4.88  
     5.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Sep 13 13:17:52 2011 +0200
     5.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Sep 13 16:21:48 2011 +0200
     5.3 @@ -1506,7 +1506,8 @@
     5.4        proof cases
     5.5          assume "\<forall>i. f i = 0"
     5.6          moreover then have "range f = {0}" by auto
     5.7 -        ultimately show "c * SUPR UNIV f \<le> y" using * by (auto simp: SUPR_def)
     5.8 +        ultimately show "c * SUPR UNIV f \<le> y" using *
     5.9 +          by (auto simp: SUPR_def min_max.sup_absorb1)
    5.10        next
    5.11          assume "\<not> (\<forall>i. f i = 0)"
    5.12          then obtain i where "f i \<noteq> 0" by auto
    5.13 @@ -1568,7 +1569,8 @@
    5.14          hence "0 < r" using `0 < e` by auto
    5.15          then obtain n ::nat where *: "1 / real n < r" "0 < n"
    5.16            using ex_inverse_of_nat_less by (auto simp: real_eq_of_nat inverse_eq_divide)
    5.17 -        have "Sup A \<le> f n + 1 / ereal (real n)" using f[THEN spec, of n] by auto
    5.18 +        have "Sup A \<le> f n + 1 / ereal (real n)" using f[THEN spec, of n]
    5.19 +          by auto
    5.20          also have "1 / ereal (real n) \<le> e" using real * by (auto simp: one_ereal_def )
    5.21          with bound have "f n + 1 / ereal (real n) \<le> y + e" by (rule add_mono) simp
    5.22          finally show "Sup A \<le> y + e" .
    5.23 @@ -1625,7 +1627,7 @@
    5.24    then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
    5.25    show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
    5.26    proof (cases a)
    5.27 -    case PInf with `A \<noteq> {}` show ?thesis by (auto simp: image_constant)
    5.28 +    case PInf with `A \<noteq> {}` show ?thesis by (auto simp: image_constant min_max.sup_absorb1)
    5.29    next
    5.30      case (real r)
    5.31      then have **: "op + (- a) ` op + a ` A = A"
     6.1 --- a/src/HOL/Library/Kleene_Algebra.thy	Tue Sep 13 13:17:52 2011 +0200
     6.2 +++ b/src/HOL/Library/Kleene_Algebra.thy	Tue Sep 13 16:21:48 2011 +0200
     6.3 @@ -377,19 +377,18 @@
     6.4    have [simp]: "1 \<le> star a"
     6.5      unfolding star_cont[of 1 a 1, simplified] 
     6.6      by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I])
     6.7 -  
     6.8 -  show "1 + a * star a \<le> star a"
     6.9 -    apply (rule plus_leI, simp)
    6.10 -    apply (simp add:star_cont[of a a 1, simplified])
    6.11 -    apply (simp add:star_cont[of 1 a 1, simplified])
    6.12 -    apply (subst power_Suc[symmetric])
    6.13 -    by (intro SUP_leI le_SUPI UNIV_I)
    6.14 +
    6.15 +  have "a * star a \<le> star a"
    6.16 +    using star_cont[of a a 1] star_cont[of 1 a 1]
    6.17 +    by (auto simp add: power_Suc[symmetric] simp del: power_Suc
    6.18 +      intro: SUP_leI le_SUPI)
    6.19  
    6.20 -  show "1 + star a * a \<le> star a" 
    6.21 -    apply (rule plus_leI, simp)
    6.22 -    apply (simp add:star_cont[of 1 a a, simplified])
    6.23 -    apply (simp add:star_cont[of 1 a 1, simplified])
    6.24 -    by (auto intro: SUP_leI le_SUPI simp add: power_Suc[symmetric] power_commutes simp del: power_Suc)
    6.25 +  then show "1 + a * star a \<le> star a"
    6.26 +    by simp
    6.27 +
    6.28 +  then show "1 + star a * a \<le> star a"
    6.29 +    using star_cont[of a a 1] star_cont[of 1 a a]
    6.30 +    by (simp add: power_commutes)
    6.31  
    6.32    show "a * x \<le> x \<Longrightarrow> star a * x \<le> x"
    6.33    proof -
     7.1 --- a/src/HOL/Main.thy	Tue Sep 13 13:17:52 2011 +0200
     7.2 +++ b/src/HOL/Main.thy	Tue Sep 13 16:21:48 2011 +0200
     7.3 @@ -11,17 +11,4 @@
     7.4  
     7.5  text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
     7.6  
     7.7 -text {* Compatibility layer -- to be dropped *}
     7.8 -
     7.9 -lemma Inf_bool_def:
    7.10 -  "Inf A \<longleftrightarrow> (\<forall>x\<in>A. x)"
    7.11 -  by (auto intro: bool_induct)
    7.12 -
    7.13 -lemma Sup_bool_def:
    7.14 -  "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    7.15 -  by auto
    7.16 -
    7.17 -declare Complete_Lattices.Inf_bool_def [simp del]
    7.18 -declare Complete_Lattices.Sup_bool_def [simp del]
    7.19 -
    7.20  end
     8.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Sep 13 13:17:52 2011 +0200
     8.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Sep 13 16:21:48 2011 +0200
     8.3 @@ -101,7 +101,7 @@
     8.4      then show False using MInf by auto
     8.5    next
     8.6      case PInf then have "S={\<infinity>}" by (metis Inf_eq_PInfty assms(2))
     8.7 -    then show False using `Inf S ~: S` by simp
     8.8 +    then show False using `Inf S ~: S` by (simp add: top_ereal_def)
     8.9    next
    8.10      case (real r) then have fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" by simp
    8.11      from ereal_open_cont_interval[OF a this] guess e . note e = this
    8.12 @@ -143,7 +143,8 @@
    8.13      from ereal_open_cont_interval[OF assms(1) * fin] guess e . note e = this
    8.14      then obtain b where b_def: "Inf S-e<b & b<Inf S"
    8.15        using fin ereal_between[of "Inf S" e] ereal_dense[of "Inf S-e"] by auto
    8.16 -    hence "b: {Inf S-e <..< Inf S+e}" using e fin ereal_between[of "Inf S" e] by auto
    8.17 +    hence "b: {Inf S-e <..< Inf S+e}" using e fin ereal_between[of "Inf S" e]
    8.18 +      by auto
    8.19      hence "b:S" using e by auto
    8.20      hence False using b_def by (metis complete_lattice_class.Inf_lower leD)
    8.21    } ultimately show False by auto
    8.22 @@ -247,7 +248,7 @@
    8.23      show "eventually (\<lambda>x. a * X x \<in> S) net"
    8.24        by (rule eventually_mono[OF _ *]) auto
    8.25    qed
    8.26 -qed (auto intro: tendsto_const)
    8.27 +qed auto
    8.28  
    8.29  lemma ereal_lim_uminus:
    8.30    fixes X :: "'a \<Rightarrow> ereal" shows "((\<lambda>i. - X i) ---> -L) net \<longleftrightarrow> (X ---> L) net"
    8.31 @@ -306,7 +307,7 @@
    8.32      assume S: "S = {Inf S<..}"
    8.33      then have "Inf S < l" using `l \<in> S` by auto
    8.34      then have "eventually (\<lambda>x. Inf S < f x) net" using ev by auto
    8.35 -    then show "eventually (\<lambda>x. f x \<in> S) net"  by (subst S) auto
    8.36 +    then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto
    8.37    qed auto
    8.38  next
    8.39    fix l y assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "y < l"
     9.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Sep 13 13:17:52 2011 +0200
     9.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Sep 13 16:21:48 2011 +0200
     9.3 @@ -613,7 +613,7 @@
     9.4    assumes posf: "positive M f"
     9.5    shows "increasing \<lparr> space = space M, sets = Pow (space M) \<rparr>
     9.6                      (\<lambda>x. Inf (measure_set M f x))"
     9.7 -apply (auto simp add: increasing_def)
     9.8 +apply (clarsimp simp add: increasing_def)
     9.9  apply (rule complete_lattice_class.Inf_greatest)
    9.10  apply (rule complete_lattice_class.Inf_lower)
    9.11  apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast)
    10.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Sep 13 13:17:52 2011 +0200
    10.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Sep 13 16:21:48 2011 +0200
    10.3 @@ -411,7 +411,9 @@
    10.4    also have "\<dots> = ?y"
    10.5    proof (rule antisym)
    10.6      show "(SUP i. integral\<^isup>P M (?g i)) \<le> ?y"
    10.7 -      using g_in_G by (auto intro!: exI Sup_mono simp: SUPR_def)
    10.8 +      using g_in_G
    10.9 +      using [[simp_trace]]
   10.10 +      by (auto intro!: exI Sup_mono simp: SUPR_def)
   10.11      show "?y \<le> (SUP i. integral\<^isup>P M (?g i))" unfolding y_eq
   10.12        by (auto intro!: SUP_mono positive_integral_mono Max_ge)
   10.13    qed
    11.1 --- a/src/HOL/UNITY/ProgressSets.thy	Tue Sep 13 13:17:52 2011 +0200
    11.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Tue Sep 13 16:21:48 2011 +0200
    11.3 @@ -77,7 +77,7 @@
    11.4  by (simp add: cl_def, blast)
    11.5  
    11.6  lemma subset_cl: "r \<subseteq> cl L r"
    11.7 -by (simp add: cl_def, blast)
    11.8 +by (simp add: cl_def le_Inf_iff)
    11.9  
   11.10  text{*A reformulation of @{thm subset_cl}*}
   11.11  lemma clI: "x \<in> r ==> x \<in> cl L r"