refinement of lattice classes
authorhaftmann
Tue Jul 14 15:54:19 2009 +0200 (2009-07-14)
changeset 3206453ca12ff305d
parent 32063 2aab4f2af536
child 32065 9fa18f1c2b2d
refinement of lattice classes
NEWS
src/HOL/Finite_Set.thy
src/HOL/Lattices.thy
src/HOL/OrderedGroup.thy
src/HOL/SEQ.thy
src/HOL/Set.thy
     1.1 --- a/NEWS	Mon Jul 13 08:25:43 2009 +0200
     1.2 +++ b/NEWS	Tue Jul 14 15:54:19 2009 +0200
     1.3 @@ -18,6 +18,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Refinements to lattices classes:
     1.8 +  - added boolean_algebra type class
     1.9 +  - less default intro/elim rules in locale variant, more default
    1.10 +    intro/elim rules in class variant: more uniformity
    1.11 +  - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
    1.12 +  - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
    1.13 +  - renamed ACI to inf_sup_aci
    1.14 +
    1.15  * Class semiring_div requires superclass no_zero_divisors and proof of
    1.16  div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
    1.17  div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
     2.1 --- a/src/HOL/Finite_Set.thy	Mon Jul 13 08:25:43 2009 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Tue Jul 14 15:54:19 2009 +0200
     2.3 @@ -811,7 +811,7 @@
     2.4  by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
     2.5  
     2.6  lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
     2.7 -by (induct pred:finite) auto
     2.8 +by (induct pred: finite) (auto intro: le_infI1)
     2.9  
    2.10  lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
    2.11  proof(induct arbitrary: a pred:finite)
    2.12 @@ -822,7 +822,7 @@
    2.13    proof cases
    2.14      assume "A = {}" thus ?thesis using insert by simp
    2.15    next
    2.16 -    assume "A \<noteq> {}" thus ?thesis using insert by auto
    2.17 +    assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
    2.18    qed
    2.19  qed
    2.20  
     3.1 --- a/src/HOL/Lattices.thy	Mon Jul 13 08:25:43 2009 +0200
     3.2 +++ b/src/HOL/Lattices.thy	Tue Jul 14 15:54:19 2009 +0200
     3.3 @@ -44,38 +44,27 @@
     3.4  context lower_semilattice
     3.5  begin
     3.6  
     3.7 -lemma le_infI1[intro]:
     3.8 -  assumes "a \<sqsubseteq> x"
     3.9 -  shows "a \<sqinter> b \<sqsubseteq> x"
    3.10 -proof (rule order_trans)
    3.11 -  from assms show "a \<sqsubseteq> x" .
    3.12 -  show "a \<sqinter> b \<sqsubseteq> a" by simp 
    3.13 -qed
    3.14 -lemmas (in -) [rule del] = le_infI1
    3.15 +lemma le_infI1:
    3.16 +  "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    3.17 +  by (rule order_trans) auto
    3.18  
    3.19 -lemma le_infI2[intro]:
    3.20 -  assumes "b \<sqsubseteq> x"
    3.21 -  shows "a \<sqinter> b \<sqsubseteq> x"
    3.22 -proof (rule order_trans)
    3.23 -  from assms show "b \<sqsubseteq> x" .
    3.24 -  show "a \<sqinter> b \<sqsubseteq> b" by simp
    3.25 -qed
    3.26 -lemmas (in -) [rule del] = le_infI2
    3.27 +lemma le_infI2:
    3.28 +  "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
    3.29 +  by (rule order_trans) auto
    3.30  
    3.31 -lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    3.32 -by(blast intro: inf_greatest)
    3.33 -lemmas (in -) [rule del] = le_infI
    3.34 +lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
    3.35 +  by (blast intro: inf_greatest)
    3.36  
    3.37 -lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    3.38 -  by (blast intro: order_trans)
    3.39 -lemmas (in -) [rule del] = le_infE
    3.40 +lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    3.41 +  by (blast intro: order_trans le_infI1 le_infI2)
    3.42  
    3.43  lemma le_inf_iff [simp]:
    3.44 -  "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
    3.45 -by blast
    3.46 +  "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
    3.47 +  by (blast intro: le_infI elim: le_infE)
    3.48  
    3.49 -lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
    3.50 -  by (blast intro: antisym dest: eq_iff [THEN iffD1])
    3.51 +lemma le_iff_inf:
    3.52 +  "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
    3.53 +  by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
    3.54  
    3.55  lemma mono_inf:
    3.56    fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice"
    3.57 @@ -87,28 +76,29 @@
    3.58  context upper_semilattice
    3.59  begin
    3.60  
    3.61 -lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    3.62 +lemma le_supI1:
    3.63 +  "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    3.64    by (rule order_trans) auto
    3.65 -lemmas (in -) [rule del] = le_supI1
    3.66  
    3.67 -lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    3.68 +lemma le_supI2:
    3.69 +  "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
    3.70    by (rule order_trans) auto 
    3.71 -lemmas (in -) [rule del] = le_supI2
    3.72  
    3.73 -lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    3.74 +lemma le_supI:
    3.75 +  "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
    3.76    by (blast intro: sup_least)
    3.77 -lemmas (in -) [rule del] = le_supI
    3.78  
    3.79 -lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    3.80 -  by (blast intro: order_trans)
    3.81 -lemmas (in -) [rule del] = le_supE
    3.82 +lemma le_supE:
    3.83 +  "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    3.84 +  by (blast intro: le_supI1 le_supI2 order_trans)
    3.85  
    3.86 -lemma ge_sup_conv[simp]:
    3.87 -  "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
    3.88 -by blast
    3.89 +lemma le_sup_iff [simp]:
    3.90 +  "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    3.91 +  by (blast intro: le_supI elim: le_supE)
    3.92  
    3.93 -lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
    3.94 -  by (blast intro: antisym dest: eq_iff [THEN iffD1])
    3.95 +lemma le_iff_sup:
    3.96 +  "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
    3.97 +  by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
    3.98  
    3.99  lemma mono_sup:
   3.100    fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice"
   3.101 @@ -118,62 +108,61 @@
   3.102  end
   3.103  
   3.104  
   3.105 -subsubsection{* Equational laws *}
   3.106 +subsubsection {* Equational laws *}
   3.107  
   3.108  context lower_semilattice
   3.109  begin
   3.110  
   3.111  lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
   3.112 -  by (blast intro: antisym)
   3.113 +  by (rule antisym) auto
   3.114  
   3.115  lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   3.116 -  by (blast intro: antisym)
   3.117 +  by (rule antisym) (auto intro: le_infI1 le_infI2)
   3.118  
   3.119  lemma inf_idem[simp]: "x \<sqinter> x = x"
   3.120 -  by (blast intro: antisym)
   3.121 +  by (rule antisym) auto
   3.122  
   3.123  lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   3.124 -  by (blast intro: antisym)
   3.125 +  by (rule antisym) (auto intro: le_infI2)
   3.126  
   3.127  lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
   3.128 -  by (blast intro: antisym)
   3.129 +  by (rule antisym) auto
   3.130  
   3.131  lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   3.132 -  by (blast intro: antisym)
   3.133 +  by (rule antisym) auto
   3.134  
   3.135  lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
   3.136 -  by (blast intro: antisym)
   3.137 -
   3.138 -lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem
   3.139 +  by (rule mk_left_commute [of inf]) (fact inf_assoc inf_commute)+
   3.140 +  
   3.141 +lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
   3.142  
   3.143  end
   3.144  
   3.145 -
   3.146  context upper_semilattice
   3.147  begin
   3.148  
   3.149  lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
   3.150 -  by (blast intro: antisym)
   3.151 +  by (rule antisym) auto
   3.152  
   3.153  lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   3.154 -  by (blast intro: antisym)
   3.155 +  by (rule antisym) (auto intro: le_supI1 le_supI2)
   3.156  
   3.157  lemma sup_idem[simp]: "x \<squnion> x = x"
   3.158 -  by (blast intro: antisym)
   3.159 +  by (rule antisym) auto
   3.160  
   3.161  lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   3.162 -  by (blast intro: antisym)
   3.163 +  by (rule antisym) (auto intro: le_supI2)
   3.164  
   3.165  lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
   3.166 -  by (blast intro: antisym)
   3.167 +  by (rule antisym) auto
   3.168  
   3.169  lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
   3.170 -  by (blast intro: antisym)
   3.171 +  by (rule antisym) auto
   3.172  
   3.173  lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
   3.174 -  by (blast intro: antisym)
   3.175 +  by (rule mk_left_commute [of sup]) (fact sup_assoc sup_commute)+
   3.176  
   3.177 -lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem
   3.178 +lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
   3.179  
   3.180  end
   3.181  
   3.182 @@ -191,18 +180,17 @@
   3.183  lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
   3.184    by (blast intro: antisym sup_ge1 sup_least inf_le1)
   3.185  
   3.186 -lemmas ACI = inf_ACI sup_ACI
   3.187 +lemmas inf_sup_aci = inf_aci sup_aci
   3.188  
   3.189  lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
   3.190  
   3.191  text{* Towards distributivity *}
   3.192  
   3.193  lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   3.194 -  by blast
   3.195 +  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
   3.196  
   3.197  lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
   3.198 -  by blast
   3.199 -
   3.200 +  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
   3.201  
   3.202  text{* If you have one of them, you have them all. *}
   3.203  
   3.204 @@ -230,10 +218,6 @@
   3.205    finally show ?thesis .
   3.206  qed
   3.207  
   3.208 -(* seems unused *)
   3.209 -lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z"
   3.210 -by blast
   3.211 -
   3.212  end
   3.213  
   3.214  
   3.215 @@ -247,7 +231,7 @@
   3.216  
   3.217  lemma sup_inf_distrib2:
   3.218   "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   3.219 -by(simp add:ACI sup_inf_distrib1)
   3.220 +by(simp add: inf_sup_aci sup_inf_distrib1)
   3.221  
   3.222  lemma inf_sup_distrib1:
   3.223   "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   3.224 @@ -255,7 +239,7 @@
   3.225  
   3.226  lemma inf_sup_distrib2:
   3.227   "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   3.228 -by(simp add:ACI inf_sup_distrib1)
   3.229 +by(simp add: inf_sup_aci inf_sup_distrib1)
   3.230  
   3.231  lemma dual_distrib_lattice:
   3.232    "distrib_lattice (op \<ge>) (op >) sup inf"
   3.233 @@ -458,10 +442,6 @@
   3.234  lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   3.235    mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
   3.236  
   3.237 -lemmas [rule del] = min_max.le_infI min_max.le_supI
   3.238 -  min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
   3.239 -  min_max.le_infI1 min_max.le_infI2
   3.240 -
   3.241  
   3.242  subsection {* Bool as lattice *}
   3.243  
   3.244 @@ -542,8 +522,6 @@
   3.245  
   3.246  text {* redundant bindings *}
   3.247  
   3.248 -lemmas inf_aci = inf_ACI
   3.249 -lemmas sup_aci = sup_ACI
   3.250  
   3.251  no_notation
   3.252    less_eq  (infix "\<sqsubseteq>" 50) and
     4.1 --- a/src/HOL/OrderedGroup.thy	Mon Jul 13 08:25:43 2009 +0200
     4.2 +++ b/src/HOL/OrderedGroup.thy	Tue Jul 14 15:54:19 2009 +0200
     4.3 @@ -1075,16 +1075,16 @@
     4.4  lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
     4.5  
     4.6  lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
     4.7 -by (simp add: pprt_def le_iff_sup sup_ACI)
     4.8 +by (simp add: pprt_def le_iff_sup sup_aci)
     4.9  
    4.10  lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
    4.11 -by (simp add: nprt_def le_iff_inf inf_ACI)
    4.12 +by (simp add: nprt_def le_iff_inf inf_aci)
    4.13  
    4.14  lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
    4.15 -by (simp add: pprt_def le_iff_sup sup_ACI)
    4.16 +by (simp add: pprt_def le_iff_sup sup_aci)
    4.17  
    4.18  lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
    4.19 -by (simp add: nprt_def le_iff_inf inf_ACI)
    4.20 +by (simp add: nprt_def le_iff_inf inf_aci)
    4.21  
    4.22  lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
    4.23  proof -
    4.24 @@ -1120,7 +1120,7 @@
    4.25    assume "0 <= a + a"
    4.26    hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
    4.27    have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
    4.28 -    by (simp add: add_sup_inf_distribs inf_ACI)
    4.29 +    by (simp add: add_sup_inf_distribs inf_aci)
    4.30    hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
    4.31    hence "inf a 0 = 0" by (simp only: add_right_cancel)
    4.32    then show "0 <= a" by (simp add: le_iff_inf inf_commute)    
    4.33 @@ -1206,10 +1206,10 @@
    4.34  by (simp add: le_iff_inf nprt_def inf_commute)
    4.35  
    4.36  lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
    4.37 -by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
    4.38 +by (simp add: le_iff_sup pprt_def sup_aci sup_assoc [symmetric, of a])
    4.39  
    4.40  lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
    4.41 -by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
    4.42 +by (simp add: le_iff_inf nprt_def inf_aci inf_assoc [symmetric, of a])
    4.43  
    4.44  end
    4.45  
    4.46 @@ -1230,7 +1230,7 @@
    4.47    then have "0 \<le> sup a (- a)" unfolding abs_lattice .
    4.48    then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
    4.49    then show ?thesis
    4.50 -    by (simp add: add_sup_inf_distribs sup_ACI
    4.51 +    by (simp add: add_sup_inf_distribs sup_aci
    4.52        pprt_def nprt_def diff_minus abs_lattice)
    4.53  qed
    4.54  
    4.55 @@ -1254,7 +1254,7 @@
    4.56    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
    4.57    proof -
    4.58      have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
    4.59 -      by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
    4.60 +      by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
    4.61      have a:"a+b <= sup ?m ?n" by (simp)
    4.62      have b:"-a-b <= ?n" by (simp) 
    4.63      have c:"?n <= sup ?m ?n" by (simp)
     5.1 --- a/src/HOL/SEQ.thy	Mon Jul 13 08:25:43 2009 +0200
     5.2 +++ b/src/HOL/SEQ.thy	Tue Jul 14 15:54:19 2009 +0200
     5.3 @@ -113,8 +113,8 @@
     5.4  lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
     5.5  unfolding Bfun_def eventually_sequentially
     5.6  apply (rule iffI)
     5.7 -apply (simp add: Bseq_def, fast)
     5.8 -apply (fast intro: BseqI2')
     5.9 +apply (simp add: Bseq_def)
    5.10 +apply (auto intro: BseqI2')
    5.11  done
    5.12  
    5.13  
    5.14 @@ -762,13 +762,25 @@
    5.15  lemma lemma_NBseq_def:
    5.16       "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
    5.17        (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
    5.18 -apply auto
    5.19 - prefer 2 apply force
    5.20 -apply (cut_tac x = K in reals_Archimedean2, clarify)
    5.21 -apply (rule_tac x = n in exI, clarify)
    5.22 -apply (drule_tac x = na in spec)
    5.23 -apply (auto simp add: real_of_nat_Suc)
    5.24 -done
    5.25 +proof auto
    5.26 +  fix K :: real
    5.27 +  from reals_Archimedean2 obtain n :: nat where "K < real n" ..
    5.28 +  then have "K \<le> real (Suc n)" by auto
    5.29 +  assume "\<forall>m. norm (X m) \<le> K"
    5.30 +  have "\<forall>m. norm (X m) \<le> real (Suc n)"
    5.31 +  proof
    5.32 +    fix m :: 'a
    5.33 +    from `\<forall>m. norm (X m) \<le> K` have "norm (X m) \<le> K" ..
    5.34 +    with `K \<le> real (Suc n)` show "norm (X m) \<le> real (Suc n)" by auto
    5.35 +  qed
    5.36 +  then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
    5.37 +next
    5.38 +  fix N :: nat
    5.39 +  have "real (Suc N) > 0" by (simp add: real_of_nat_Suc)
    5.40 +  moreover assume "\<forall>n. norm (X n) \<le> real (Suc N)"
    5.41 +  ultimately show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" by blast
    5.42 +qed
    5.43 +
    5.44  
    5.45  text{* alternative definition for Bseq *}
    5.46  lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
    5.47 @@ -1105,7 +1117,7 @@
    5.48  lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u"
    5.49  proof (rule reals_complete)
    5.50    obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1"
    5.51 -    using CauchyD [OF X zero_less_one] by fast
    5.52 +    using CauchyD [OF X zero_less_one] by auto
    5.53    hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp
    5.54    show "\<exists>x. x \<in> S"
    5.55    proof
    5.56 @@ -1129,7 +1141,7 @@
    5.57    fix r::real assume "0 < r"
    5.58    hence r: "0 < r/2" by simp
    5.59    obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2"
    5.60 -    using CauchyD [OF X r] by fast
    5.61 +    using CauchyD [OF X r] by auto
    5.62    hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp
    5.63    hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
    5.64      by (simp only: real_norm_def real_abs_diff_less_iff)
     6.1 --- a/src/HOL/Set.thy	Mon Jul 13 08:25:43 2009 +0200
     6.2 +++ b/src/HOL/Set.thy	Tue Jul 14 15:54:19 2009 +0200
     6.3 @@ -2249,10 +2249,10 @@
     6.4    unfolding Inf_Sup by auto
     6.5  
     6.6  lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
     6.7 -  by (auto intro: antisym Inf_greatest Inf_lower)
     6.8 +  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
     6.9  
    6.10  lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    6.11 -  by (auto intro: antisym Sup_least Sup_upper)
    6.12 +  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
    6.13  
    6.14  lemma Inf_singleton [simp]:
    6.15    "\<Sqinter>{a} = a"