1.1 --- a/NEWS	Wed Jul 20 16:15:33 2011 +0200
     1.2 +++ b/NEWS	Wed Jul 20 22:14:39 2011 +0200
     1.3 @@ -63,15 +63,16 @@
     1.4  * Classes bot and top require underlying partial order rather than preorder:
     1.5  uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
     1.6  
     1.7 -* Class 'complete_lattice': generalized a couple of lemmas from sets;
     1.8 -generalized theorems INF_cong and SUP_cong.  More consistent and less
     1.9 -misunderstandable names:
    1.10 +* Class complete_lattice: generalized a couple of lemmas from sets;
    1.11 +generalized theorems INF_cong and SUP_cong.  New type classes for complete
    1.12 +boolean algebras and complete linear orderes.  Lemmas Inf_less_iff,
    1.13 +less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
    1.14 +More consistent and less misunderstandable names:
    1.15    INFI_def ~> INF_def
    1.16    SUPR_def ~> SUP_def
    1.17    le_SUPI ~> le_SUP_I
    1.18    le_SUPI2 ~> le_SUP_I2
    1.19    le_INFI ~> le_INF_I
    1.20 -  INF_subset ~> INF_superset_mono
    1.21    INFI_bool_eq ~> INF_bool_eq
    1.22    SUPR_bool_eq ~> SUP_bool_eq
    1.23    INFI_apply ~> INF_apply

     2.1 --- a/src/HOL/Complete_Lattice.thy	Wed Jul 20 16:15:33 2011 +0200
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Wed Jul 20 22:14:39 2011 +0200
     2.3 @@ -292,12 +292,13 @@
     2.4    by (force intro!: Sup_mono simp: SUP_def)
     2.5  
     2.6  lemma INF_superset_mono:
     2.7 -  "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
     2.8 -  by (rule INF_mono) auto
     2.9 +  "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.10 +  -- {* The last inclusion is POSITIVE! *}
    2.11 +  by (blast intro: INF_mono dest: subsetD)
    2.12  
    2.13  lemma SUP_subset_mono:
    2.14 -  "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
    2.15 -  by (rule SUP_mono) auto
    2.16 +  "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
    2.17 +  by (blast intro: SUP_mono dest: subsetD)
    2.18  
    2.19  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.20    by (iprover intro: INF_leI le_INF_I order_trans antisym)
    2.21 @@ -371,38 +372,8 @@
    2.22    "(\<Squnion>b. A b) = A True \<squnion> A False"
    2.23    by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
    2.24  
    2.25 -lemma INF_mono':
    2.26 -  "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.27 -  -- {* The last inclusion is POSITIVE! *}
    2.28 -  by (rule INF_mono) auto
    2.29 -
    2.30 -lemma SUP_mono':
    2.31 -  "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
    2.32 -  -- {* The last inclusion is POSITIVE! *}
    2.33 -  by (blast intro: SUP_mono dest: subsetD)
    2.34 -
    2.35  end
    2.36  
    2.37 -lemma Inf_less_iff:
    2.38 -  fixes a :: "'a\<Colon>{complete_lattice,linorder}"
    2.39 -  shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
    2.40 -  unfolding not_le [symmetric] le_Inf_iff by auto
    2.41 -
    2.42 -lemma less_Sup_iff:
    2.43 -  fixes a :: "'a\<Colon>{complete_lattice,linorder}"
    2.44 -  shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
    2.45 -  unfolding not_le [symmetric] Sup_le_iff by auto
    2.46 -
    2.47 -lemma INF_less_iff:
    2.48 -  fixes a :: "'a::{complete_lattice,linorder}"
    2.49 -  shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
    2.50 -  unfolding INF_def Inf_less_iff by auto
    2.51 -
    2.52 -lemma less_SUP_iff:
    2.53 -  fixes a :: "'a::{complete_lattice,linorder}"
    2.54 -  shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
    2.55 -  unfolding SUP_def less_Sup_iff by auto
    2.56 -
    2.57  class complete_boolean_algebra = boolean_algebra + complete_lattice
    2.58  begin
    2.59  
    2.60 @@ -430,6 +401,27 @@
    2.61  
    2.62  end
    2.63  
    2.64 +class complete_linorder = linorder + complete_lattice
    2.65 +begin
    2.66 +
    2.67 +lemma Inf_less_iff:
    2.68 +  "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
    2.69 +  unfolding not_le [symmetric] le_Inf_iff by auto
    2.70 +
    2.71 +lemma less_Sup_iff:
    2.72 +  "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
    2.73 +  unfolding not_le [symmetric] Sup_le_iff by auto
    2.74 +
    2.75 +lemma INF_less_iff:
    2.76 +  "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
    2.77 +  unfolding INF_def Inf_less_iff by auto
    2.78 +
    2.79 +lemma less_SUP_iff:
    2.80 +  "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
    2.81 +  unfolding SUP_def less_Sup_iff by auto
    2.82 +
    2.83 +end
    2.84 +
    2.85  
    2.86  subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
    2.87  
    2.88 @@ -688,7 +680,7 @@
    2.89  lemma INT_anti_mono:
    2.90    "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
    2.91    -- {* The last inclusion is POSITIVE! *}
    2.92 -  by (fact INF_mono')
    2.93 +  by (fact INF_superset_mono)
    2.94  
    2.95  lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
    2.96    by blast
    2.97 @@ -922,7 +914,7 @@
    2.98  lemma UN_mono:
    2.99    "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow>
   2.100      (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
   2.101 -  by (fact SUP_mono')
   2.102 +  by (fact SUP_subset_mono)
   2.103  
   2.104  lemma vimage_Union: "f -` (\<Union>A) = (\<Union>X\<in>A. f -` X)"
   2.105    by blast
   2.106 @@ -1083,7 +1075,11 @@
   2.107  lemmas (in complete_lattice) le_SUPI = le_SUP_I
   2.108  lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
   2.109  lemmas (in complete_lattice) le_INFI = le_INF_I
   2.110 -lemmas (in complete_lattice) INF_subset = INF_superset_mono 
   2.111 +
   2.112 +lemma (in complete_lattice) INF_subset:
   2.113 +  "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
   2.114 +  by (rule INF_superset_mono) auto
   2.115 +
   2.116  lemmas INFI_apply = INF_apply
   2.117  lemmas SUPR_apply = SUP_apply
   2.118