1.1 --- a/src/HOL/Complete_Lattice.thy	Mon Mar 14 14:37:35 2011 +0100
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Mon Mar 14 14:37:36 2011 +0100
     1.3 @@ -89,25 +89,45 @@
     1.4    by (auto intro: Sup_least dest: Sup_upper)
     1.5  
     1.6  lemma Inf_mono:
     1.7 -  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<le> b"
     1.8 -  shows "Inf A \<le> Inf B"
     1.9 +  assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
    1.10 +  shows "Inf A \<sqsubseteq> Inf B"
    1.11  proof (rule Inf_greatest)
    1.12    fix b assume "b \<in> B"
    1.13 -  with assms obtain a where "a \<in> A" and "a \<le> b" by blast
    1.14 -  from `a \<in> A` have "Inf A \<le> a" by (rule Inf_lower)
    1.15 -  with `a \<le> b` show "Inf A \<le> b" by auto
    1.16 +  with assms obtain a where "a \<in> A" and "a \<sqsubseteq> b" by blast
    1.17 +  from `a \<in> A` have "Inf A \<sqsubseteq> a" by (rule Inf_lower)
    1.18 +  with `a \<sqsubseteq> b` show "Inf A \<sqsubseteq> b" by auto
    1.19  qed
    1.20  
    1.21  lemma Sup_mono:
    1.22 -  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
    1.23 -  shows "Sup A \<le> Sup B"
    1.24 +  assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
    1.25 +  shows "Sup A \<sqsubseteq> Sup B"
    1.26  proof (rule Sup_least)
    1.27    fix a assume "a \<in> A"
    1.28 -  with assms obtain b where "b \<in> B" and "a \<le> b" by blast
    1.29 -  from `b \<in> B` have "b \<le> Sup B" by (rule Sup_upper)
    1.30 -  with `a \<le> b` show "a \<le> Sup B" by auto
    1.31 +  with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast
    1.32 +  from `b \<in> B` have "b \<sqsubseteq> Sup B" by (rule Sup_upper)
    1.33 +  with `a \<sqsubseteq> b` show "a \<sqsubseteq> Sup B" by auto
    1.34  qed
    1.35  
    1.36 +lemma top_le:
    1.37 +  "top \<sqsubseteq> x \<Longrightarrow> x = top"
    1.38 +  by (rule antisym) auto
    1.39 +
    1.40 +lemma le_bot:
    1.41 +  "x \<sqsubseteq> bot \<Longrightarrow> x = bot"
    1.42 +  by (rule antisym) auto
    1.43 +
    1.44 +lemma not_less_bot[simp]: "\<not> (x \<sqsubset> bot)"
    1.45 +  using bot_least[of x] by (auto simp: le_less)
    1.46 +
    1.47 +lemma not_top_less[simp]: "\<not> (top \<sqsubset> x)"
    1.48 +  using top_greatest[of x] by (auto simp: le_less)
    1.49 +
    1.50 +lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> Sup A"
    1.51 +  using Sup_upper[of u A] by auto
    1.52 +
    1.53 +lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> Inf A \<sqsubseteq> v"
    1.54 +  using Inf_lower[of u A] by auto
    1.55 +
    1.56  definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.57    "INFI A f = \<Sqinter> (f ` A)"
    1.58  
    1.59 @@ -146,15 +166,27 @@
    1.60  context complete_lattice
    1.61  begin
    1.62  
    1.63 +lemma SUP_cong: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> SUPR A f = SUPR A g"
    1.64 +  by (simp add: SUPR_def cong: image_cong)
    1.65 +
    1.66 +lemma INF_cong: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> INFI A f = INFI A g"
    1.67 +  by (simp add: INFI_def cong: image_cong)
    1.68 +
    1.69  lemma le_SUPI: "i : A \<Longrightarrow> M i \<sqsubseteq> (SUP i:A. M i)"
    1.70    by (auto simp add: SUPR_def intro: Sup_upper)
    1.71  
    1.72 +lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> M i \<Longrightarrow> u \<sqsubseteq> (SUP i:A. M i)"
    1.73 +  using le_SUPI[of i A M] by auto
    1.74 +
    1.75  lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (SUP i:A. M i) \<sqsubseteq> u"
    1.76    by (auto simp add: SUPR_def intro: Sup_least)
    1.77  
    1.78  lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> M i"
    1.79    by (auto simp add: INFI_def intro: Inf_lower)
    1.80  
    1.81 +lemma INF_leI2: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> u \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> u"
    1.82 +  using INF_leI[of i A M] by auto
    1.83 +
    1.84  lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (INF i:A. M i)"
    1.85    by (auto simp add: INFI_def intro: Inf_greatest)
    1.86