src/HOL/Complete_Lattice.thy
 changeset 41971 a54e8e95fe96 parent 41082 9ff94e7cc3b3 child 42284 326f57825e1a
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.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.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.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.59 @@ -146,15 +166,27 @@
1.60  context complete_lattice
1.61  begin
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.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.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.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)