1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 17 20:23:39 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 20:29:54 2011 +0200
     1.3 @@ -224,38 +224,75 @@
     1.4  lemma INF_empty: "(\<Sqinter>x\<in>{}. f x) = \<top>"
     1.5    by (simp add: INFI_def)
     1.6  
     1.7 +lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
     1.8 +  by (simp add: SUPR_def)
     1.9 +
    1.10  lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
    1.11    by (simp add: INFI_def Inf_insert)
    1.12  
    1.13 +lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
    1.14 +  by (simp add: SUPR_def Sup_insert)
    1.15 +
    1.16  lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> f i"
    1.17    by (auto simp add: INFI_def intro: Inf_lower)
    1.18  
    1.19 +lemma le_SUPI: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
    1.20 +  by (auto simp add: SUPR_def intro: Sup_upper)
    1.21 +
    1.22  lemma INF_leI2: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. f i) \<sqsubseteq> u"
    1.23    using INF_leI [of i A f] by auto
    1.24  
    1.25 +lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
    1.26 +  using le_SUPI [of i A f] by auto
    1.27 +
    1.28  lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> f i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. f i)"
    1.29    by (auto simp add: INFI_def intro: Inf_greatest)
    1.30  
    1.31 +lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
    1.32 +  by (auto simp add: SUPR_def intro: Sup_least)
    1.33 +
    1.34  lemma le_INF_iff: "u \<sqsubseteq> (\<Sqinter>i\<in>A. f i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> f i)"
    1.35    by (auto simp add: INFI_def le_Inf_iff)
    1.36  
    1.37 +lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. f i \<sqsubseteq> u)"
    1.38 +  by (auto simp add: SUPR_def Sup_le_iff)
    1.39 +
    1.40  lemma INF_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Sqinter>i\<in>A. f) = f"
    1.41    by (auto intro: antisym INF_leI le_INFI)
    1.42  
    1.43 +lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
    1.44 +  by (auto intro: antisym SUP_leI le_SUPI)
    1.45 +
    1.46  lemma INF_cong:
    1.47    "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Sqinter>x\<in>A. C x) = (\<Sqinter>x\<in>B. D x)"
    1.48    by (simp add: INFI_def image_def)
    1.49  
    1.50 +lemma SUP_cong:
    1.51 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Squnion>x\<in>A. C x) = (\<Squnion>x\<in>B. D x)"
    1.52 +  by (simp add: SUPR_def image_def)
    1.53 +
    1.54  lemma INF_mono:
    1.55    "(\<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)"
    1.56    by (force intro!: Inf_mono simp: INFI_def)
    1.57  
    1.58 -lemma INF_subset:  "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
    1.59 +lemma SUP_mono:
    1.60 +  "(\<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)"
    1.61 +  by (force intro!: Sup_mono simp: SUPR_def)
    1.62 +
    1.63 +lemma INF_subset:
    1.64 +  "A \<subseteq> B \<Longrightarrow> INFI B f \<sqsubseteq> INFI A f"
    1.65    by (intro INF_mono) auto
    1.66  
    1.67 +lemma SUP_subset:
    1.68 +  "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
    1.69 +  by (intro SUP_mono) auto
    1.70 +
    1.71  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)"
    1.72    by (iprover intro: INF_leI le_INFI order_trans antisym)
    1.73  
    1.74 +lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)"
    1.75 +  by (iprover intro: SUP_leI le_SUPI order_trans antisym)
    1.76 +
    1.77  lemma (in complete_lattice) INFI_empty:
    1.78    "(\<Sqinter>x\<in>{}. B x) = \<top>"
    1.79    by (simp add: INFI_def)
    1.80 @@ -298,41 +335,6 @@
    1.81    -- {* The last inclusion is POSITIVE! *}
    1.82    by (blast intro: INF_mono dest: subsetD)
    1.83  
    1.84 -lemma SUP_cong:
    1.85 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Squnion>x\<in>A. C x) = (\<Squnion>x\<in>B. D x)"
    1.86 -  by (simp add: SUPR_def image_def)
    1.87 -
    1.88 -lemma le_SUPI: "i \<in> A \<Longrightarrow> f i \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
    1.89 -  by (auto simp add: SUPR_def intro: Sup_upper)
    1.90 -
    1.91 -lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> f i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. f i)"
    1.92 -  using le_SUPI [of i A f] by auto
    1.93 -
    1.94 -lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> f i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. f i) \<sqsubseteq> u"
    1.95 -  by (auto simp add: SUPR_def intro: Sup_least)
    1.96 -
    1.97 -lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. f i \<sqsubseteq> u)"
    1.98 -  unfolding SUPR_def by (auto simp add: Sup_le_iff)
    1.99 -
   1.100 -lemma SUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (\<Squnion>i\<in>A. f) = f"
   1.101 -  by (auto intro: antisym SUP_leI le_SUPI)
   1.102 -
   1.103 -lemma SUP_mono:
   1.104 -  "(\<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)"
   1.105 -  by (force intro!: Sup_mono simp: SUPR_def)
   1.106 -
   1.107 -lemma SUP_subset:  "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
   1.108 -  by (intro SUP_mono) auto
   1.109 -
   1.110 -lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)"
   1.111 -  by (iprover intro: SUP_leI le_SUPI order_trans antisym)
   1.112 -
   1.113 -lemma SUP_empty: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
   1.114 -  by (simp add: SUPR_def)
   1.115 -
   1.116 -lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
   1.117 -  by (simp add: SUPR_def Sup_insert)
   1.118 -
   1.119  end
   1.120  
   1.121  lemma Inf_less_iff: