refinement of lattice classes

--- a/NEWS	Mon Jul 13 08:25:43 2009 +0200
+++ b/NEWS	Tue Jul 14 15:54:19 2009 +0200
@@ -18,6 +18,14 @@
 
 *** HOL ***
 
+* Refinements to lattices classes:
+  - added boolean_algebra type class
+  - less default intro/elim rules in locale variant, more default
+    intro/elim rules in class variant: more uniformity
+  - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
+  - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
+  - renamed ACI to inf_sup_aci
+
 * Class semiring_div requires superclass no_zero_divisors and proof of
 div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
 div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been

--- a/src/HOL/Finite_Set.thy	Mon Jul 13 08:25:43 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Jul 14 15:54:19 2009 +0200
@@ -811,7 +811,7 @@
 by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
 
 lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
-by (induct pred:finite) auto
+by (induct pred: finite) (auto intro: le_infI1)
 
 lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
 proof(induct arbitrary: a pred:finite)
@@ -822,7 +822,7 @@
   proof cases
     assume "A = {}" thus ?thesis using insert by simp
   next
-    assume "A \<noteq> {}" thus ?thesis using insert by auto
+    assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
   qed
 qed
 

--- a/src/HOL/Lattices.thy	Mon Jul 13 08:25:43 2009 +0200
+++ b/src/HOL/Lattices.thy	Tue Jul 14 15:54:19 2009 +0200
@@ -44,38 +44,27 @@
 context lower_semilattice
 begin
 
-lemma le_infI1[intro]:
-  assumes "a \<sqsubseteq> x"
-  shows "a \<sqinter> b \<sqsubseteq> x"
-proof (rule order_trans)
-  from assms show "a \<sqsubseteq> x" .
-  show "a \<sqinter> b \<sqsubseteq> a" by simp 
-qed
-lemmas (in -) [rule del] = le_infI1
+lemma le_infI1:
+  "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+  by (rule order_trans) auto
 
-lemma le_infI2[intro]:
-  assumes "b \<sqsubseteq> x"
-  shows "a \<sqinter> b \<sqsubseteq> x"
-proof (rule order_trans)
-  from assms show "b \<sqsubseteq> x" .
-  show "a \<sqinter> b \<sqsubseteq> b" by simp
-qed
-lemmas (in -) [rule del] = le_infI2
+lemma le_infI2:
+  "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+  by (rule order_trans) auto
 
-lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
-by(blast intro: inf_greatest)
-lemmas (in -) [rule del] = le_infI
+lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
+  by (blast intro: inf_greatest)
 
-lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
-  by (blast intro: order_trans)
-lemmas (in -) [rule del] = le_infE
+lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
+  by (blast intro: order_trans le_infI1 le_infI2)
 
 lemma le_inf_iff [simp]:
-  "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
-by blast
+  "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
+  by (blast intro: le_infI elim: le_infE)
 
-lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
-  by (blast intro: antisym dest: eq_iff [THEN iffD1])
+lemma le_iff_inf:
+  "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
+  by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
 
 lemma mono_inf:
   fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice"
@@ -87,28 +76,29 @@
 context upper_semilattice
 begin
 
-lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI1:
+  "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   by (rule order_trans) auto
-lemmas (in -) [rule del] = le_supI1
 
-lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI2:
+  "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   by (rule order_trans) auto 
-lemmas (in -) [rule del] = le_supI2
 
-lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
+lemma le_supI:
+  "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
   by (blast intro: sup_least)
-lemmas (in -) [rule del] = le_supI
 
-lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
-  by (blast intro: order_trans)
-lemmas (in -) [rule del] = le_supE
+lemma le_supE:
+  "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
+  by (blast intro: le_supI1 le_supI2 order_trans)
 
-lemma ge_sup_conv[simp]:
-  "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
-by blast
+lemma le_sup_iff [simp]:
+  "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
+  by (blast intro: le_supI elim: le_supE)
 
-lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
-  by (blast intro: antisym dest: eq_iff [THEN iffD1])
+lemma le_iff_sup:
+  "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
+  by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
 
 lemma mono_sup:
   fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice"
@@ -118,62 +108,61 @@
 end
 
 
-subsubsection{* Equational laws *}
+subsubsection {* Equational laws *}
 
 context lower_semilattice
 begin
 
 lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
-  by (blast intro: antisym)
+  by (rule antisym) (auto intro: le_infI1 le_infI2)
 
 lemma inf_idem[simp]: "x \<sqinter> x = x"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
-  by (blast intro: antisym)
+  by (rule antisym) (auto intro: le_infI2)
 
 lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
-  by (blast intro: antisym)
-
-lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem
+  by (rule mk_left_commute [of inf]) (fact inf_assoc inf_commute)+
+  
+lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
 
 end
 
-
 context upper_semilattice
 begin
 
 lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
-  by (blast intro: antisym)
+  by (rule antisym) (auto intro: le_supI1 le_supI2)
 
 lemma sup_idem[simp]: "x \<squnion> x = x"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
-  by (blast intro: antisym)
+  by (rule antisym) (auto intro: le_supI2)
 
 lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
-  by (blast intro: antisym)
+  by (rule antisym) auto
 
 lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
-  by (blast intro: antisym)
+  by (rule mk_left_commute [of sup]) (fact sup_assoc sup_commute)+
 
-lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem
+lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
 
 end
 
@@ -191,18 +180,17 @@
 lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
   by (blast intro: antisym sup_ge1 sup_least inf_le1)
 
-lemmas ACI = inf_ACI sup_ACI
+lemmas inf_sup_aci = inf_aci sup_aci
 
 lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
 
 text{* Towards distributivity *}
 
 lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
-  by blast
+  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
 
 lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
-  by blast
-
+  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
 
 text{* If you have one of them, you have them all. *}
 
@@ -230,10 +218,6 @@
   finally show ?thesis .
 qed
 
-(* seems unused *)
-lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z"
-by blast
-
 end
 
 
@@ -247,7 +231,7 @@
 
 lemma sup_inf_distrib2:
  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
-by(simp add:ACI sup_inf_distrib1)
+by(simp add: inf_sup_aci sup_inf_distrib1)
 
 lemma inf_sup_distrib1:
  "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
@@ -255,7 +239,7 @@
 
 lemma inf_sup_distrib2:
  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
-by(simp add:ACI inf_sup_distrib1)
+by(simp add: inf_sup_aci inf_sup_distrib1)
 
 lemma dual_distrib_lattice:
   "distrib_lattice (op \<ge>) (op >) sup inf"
@@ -458,10 +442,6 @@
 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
 
-lemmas [rule del] = min_max.le_infI min_max.le_supI
-  min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
-  min_max.le_infI1 min_max.le_infI2
-
 
 subsection {* Bool as lattice *}
 
@@ -542,8 +522,6 @@
 
 text {* redundant bindings *}
 
-lemmas inf_aci = inf_ACI
-lemmas sup_aci = sup_ACI
 
 no_notation
   less_eq  (infix "\<sqsubseteq>" 50) and

--- a/src/HOL/OrderedGroup.thy	Mon Jul 13 08:25:43 2009 +0200
+++ b/src/HOL/OrderedGroup.thy	Tue Jul 14 15:54:19 2009 +0200
@@ -1075,16 +1075,16 @@
 lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
 
 lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
-by (simp add: pprt_def le_iff_sup sup_ACI)
+by (simp add: pprt_def le_iff_sup sup_aci)
 
 lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
-by (simp add: nprt_def le_iff_inf inf_ACI)
+by (simp add: nprt_def le_iff_inf inf_aci)
 
 lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
-by (simp add: pprt_def le_iff_sup sup_ACI)
+by (simp add: pprt_def le_iff_sup sup_aci)
 
 lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
-by (simp add: nprt_def le_iff_inf inf_ACI)
+by (simp add: nprt_def le_iff_inf inf_aci)
 
 lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
 proof -
@@ -1120,7 +1120,7 @@
   assume "0 <= a + a"
   hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
   have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
-    by (simp add: add_sup_inf_distribs inf_ACI)
+    by (simp add: add_sup_inf_distribs inf_aci)
   hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
   hence "inf a 0 = 0" by (simp only: add_right_cancel)
   then show "0 <= a" by (simp add: le_iff_inf inf_commute)    
@@ -1206,10 +1206,10 @@
 by (simp add: le_iff_inf nprt_def inf_commute)
 
 lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
-by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
+by (simp add: le_iff_sup pprt_def sup_aci sup_assoc [symmetric, of a])
 
 lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
-by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
+by (simp add: le_iff_inf nprt_def inf_aci inf_assoc [symmetric, of a])
 
 end
 
@@ -1230,7 +1230,7 @@
   then have "0 \<le> sup a (- a)" unfolding abs_lattice .
   then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
   then show ?thesis
-    by (simp add: add_sup_inf_distribs sup_ACI
+    by (simp add: add_sup_inf_distribs sup_aci
       pprt_def nprt_def diff_minus abs_lattice)
 qed
 
@@ -1254,7 +1254,7 @@
   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   proof -
     have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
-      by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
+      by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
     have a:"a+b <= sup ?m ?n" by (simp)
     have b:"-a-b <= ?n" by (simp) 
     have c:"?n <= sup ?m ?n" by (simp)

--- a/src/HOL/SEQ.thy	Mon Jul 13 08:25:43 2009 +0200
+++ b/src/HOL/SEQ.thy	Tue Jul 14 15:54:19 2009 +0200
@@ -113,8 +113,8 @@
 lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
 unfolding Bfun_def eventually_sequentially
 apply (rule iffI)
-apply (simp add: Bseq_def, fast)
-apply (fast intro: BseqI2')
+apply (simp add: Bseq_def)
+apply (auto intro: BseqI2')
 done
 
 
@@ -762,13 +762,25 @@
 lemma lemma_NBseq_def:
      "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
       (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
-apply auto
- prefer 2 apply force
-apply (cut_tac x = K in reals_Archimedean2, clarify)
-apply (rule_tac x = n in exI, clarify)
-apply (drule_tac x = na in spec)
-apply (auto simp add: real_of_nat_Suc)
-done
+proof auto
+  fix K :: real
+  from reals_Archimedean2 obtain n :: nat where "K < real n" ..
+  then have "K \<le> real (Suc n)" by auto
+  assume "\<forall>m. norm (X m) \<le> K"
+  have "\<forall>m. norm (X m) \<le> real (Suc n)"
+  proof
+    fix m :: 'a
+    from `\<forall>m. norm (X m) \<le> K` have "norm (X m) \<le> K" ..
+    with `K \<le> real (Suc n)` show "norm (X m) \<le> real (Suc n)" by auto
+  qed
+  then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
+next
+  fix N :: nat
+  have "real (Suc N) > 0" by (simp add: real_of_nat_Suc)
+  moreover assume "\<forall>n. norm (X n) \<le> real (Suc N)"
+  ultimately show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" by blast
+qed
+
 
 text{* alternative definition for Bseq *}
 lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
@@ -1105,7 +1117,7 @@
 lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u"
 proof (rule reals_complete)
   obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1"
-    using CauchyD [OF X zero_less_one] by fast
+    using CauchyD [OF X zero_less_one] by auto
   hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp
   show "\<exists>x. x \<in> S"
   proof
@@ -1129,7 +1141,7 @@
   fix r::real assume "0 < r"
   hence r: "0 < r/2" by simp
   obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2"
-    using CauchyD [OF X r] by fast
+    using CauchyD [OF X r] by auto
   hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp
   hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
     by (simp only: real_norm_def real_abs_diff_less_iff)

--- a/src/HOL/Set.thy	Mon Jul 13 08:25:43 2009 +0200
+++ b/src/HOL/Set.thy	Tue Jul 14 15:54:19 2009 +0200
@@ -2249,10 +2249,10 @@
   unfolding Inf_Sup by auto
 
 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
-  by (auto intro: antisym Inf_greatest Inf_lower)
+  by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
 
 lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
-  by (auto intro: antisym Sup_least Sup_upper)
+  by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
 
 lemma Inf_singleton [simp]:
   "\<Sqinter>{a} = a"