# HG changeset patch
# User haftmann
# Date 1310305535 -7200
# Node ID fac11b64713c54d6caba05f34b9d84feafb4e598
# Parent  3316e6831801a7e2c7eb9e62e34adb9c03c3817a
tuned proofs and notation

diff -r 3316e6831801 -r fac11b64713c src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sun Jul 10 14:26:07 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sun Jul 10 15:45:35 2011 +0200
@@ -85,47 +85,47 @@
 lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
   by (auto intro: Inf_greatest dest: Inf_lower)
 
-lemma Sup_le_iff: "Sup A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
+lemma Sup_le_iff: "\<Squnion>A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
   by (auto intro: Sup_least dest: Sup_upper)
 
 lemma Inf_mono:
   assumes "\<And>b. b \<in> B \<Longrightarrow> \<exists>a\<in>A. a \<sqsubseteq> b"
-  shows "Inf A \<sqsubseteq> Inf B"
+  shows "\<Sqinter>A \<sqsubseteq> \<Sqinter>B"
 proof (rule Inf_greatest)
   fix b assume "b \<in> B"
   with assms obtain a where "a \<in> A" and "a \<sqsubseteq> b" by blast
-  from `a \<in> A` have "Inf A \<sqsubseteq> a" by (rule Inf_lower)
-  with `a \<sqsubseteq> b` show "Inf A \<sqsubseteq> b" by auto
+  from `a \<in> A` have "\<Sqinter>A \<sqsubseteq> a" by (rule Inf_lower)
+  with `a \<sqsubseteq> b` show "\<Sqinter>A \<sqsubseteq> b" by auto
 qed
 
 lemma Sup_mono:
   assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<sqsubseteq> b"
-  shows "Sup A \<sqsubseteq> Sup B"
+  shows "\<Squnion>A \<sqsubseteq> \<Squnion>B"
 proof (rule Sup_least)
   fix a assume "a \<in> A"
   with assms obtain b where "b \<in> B" and "a \<sqsubseteq> b" by blast
-  from `b \<in> B` have "b \<sqsubseteq> Sup B" by (rule Sup_upper)
-  with `a \<sqsubseteq> b` show "a \<sqsubseteq> Sup B" by auto
+  from `b \<in> B` have "b \<sqsubseteq> \<Squnion>B" by (rule Sup_upper)
+  with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto
 qed
 
 lemma top_le:
-  "top \<sqsubseteq> x \<Longrightarrow> x = top"
+  "\<top> \<sqsubseteq> x \<Longrightarrow> x = \<top>"
   by (rule antisym) auto
 
 lemma le_bot:
-  "x \<sqsubseteq> bot \<Longrightarrow> x = bot"
+  "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
   by (rule antisym) auto
 
-lemma not_less_bot[simp]: "\<not> (x \<sqsubset> bot)"
+lemma not_less_bot[simp]: "\<not> (x \<sqsubset> \<bottom>)"
   using bot_least[of x] by (auto simp: le_less)
 
-lemma not_top_less[simp]: "\<not> (top \<sqsubset> x)"
+lemma not_top_less[simp]: "\<not> (\<top> \<sqsubset> x)"
   using top_greatest[of x] by (auto simp: le_less)
 
-lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> Sup A"
+lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
   using Sup_upper[of u A] by auto
 
-lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> Inf A \<sqsubseteq> v"
+lemma Inf_lower2: "u \<in> A \<Longrightarrow> u \<sqsubseteq> v \<Longrightarrow> \<Sqinter>A \<sqsubseteq> v"
   using Inf_lower[of u A] by auto
 
 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
@@ -172,22 +172,22 @@
 lemma INF_cong: "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> INFI A f = INFI A g"
   by (simp add: INFI_def cong: image_cong)
 
-lemma le_SUPI: "i : A \<Longrightarrow> M i \<sqsubseteq> (SUP i:A. M i)"
+lemma le_SUPI: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
   by (auto simp add: SUPR_def intro: Sup_upper)
 
-lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> M i \<Longrightarrow> u \<sqsubseteq> (SUP i:A. M i)"
+lemma le_SUPI2: "i \<in> A \<Longrightarrow> u \<sqsubseteq> M i \<Longrightarrow> u \<sqsubseteq> (\<Squnion>i\<in>A. M i)"
   using le_SUPI[of i A M] by auto
 
-lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (SUP i:A. M i) \<sqsubseteq> u"
+lemma SUP_leI: "(\<And>i. i \<in> A \<Longrightarrow> M i \<sqsubseteq> u) \<Longrightarrow> (\<Squnion>i\<in>A. M i) \<sqsubseteq> u"
   by (auto simp add: SUPR_def intro: Sup_least)
 
-lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> M i"
+lemma INF_leI: "i \<in> A \<Longrightarrow> (\<Sqinter>i\<in>A. M i) \<sqsubseteq> M i"
   by (auto simp add: INFI_def intro: Inf_lower)
 
-lemma INF_leI2: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> u \<Longrightarrow> (INF i:A. M i) \<sqsubseteq> u"
+lemma INF_leI2: "i \<in> A \<Longrightarrow> M i \<sqsubseteq> u \<Longrightarrow> (\<Sqinter>i\<in>A. M i) \<sqsubseteq> u"
   using INF_leI[of i A M] by auto
 
-lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (INF i:A. M i)"
+lemma le_INFI: "(\<And>i. i \<in> A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (\<Sqinter>i\<in>A. M i)"
   by (auto simp add: INFI_def intro: Inf_greatest)
 
 lemma SUP_le_iff: "(SUP i:A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
@@ -328,27 +328,27 @@
     by (simp add: Inf_fun_def Inf_bool_def) (simp add: mem_def)
 qed
 
-lemma Inter_iff [simp,no_atp]: "(A : Inter C) = (ALL X:C. A:X)"
+lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
   by (unfold Inter_eq) blast
 
-lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C"
+lemma InterI [intro!]: "(\<And>X. X \<in> C \<Longrightarrow> A \<in> X) \<Longrightarrow> A \<in> \<Inter>C"
   by (simp add: Inter_eq)
 
 text {*
   \medskip A ``destruct'' rule -- every @{term X} in @{term C}
-  contains @{term A} as an element, but @{prop "A:X"} can hold when
-  @{prop "X:C"} does not!  This rule is analogous to @{text spec}.
+  contains @{term A} as an element, but @{prop "A \<in> X"} can hold when
+  @{prop "X \<in> C"} does not!  This rule is analogous to @{text spec}.
 *}
 
-lemma InterD [elim, Pure.elim]: "A : Inter C ==> X:C ==> A:X"
+lemma InterD [elim, Pure.elim]: "A \<in> \<Inter>C \<Longrightarrow> X \<in> C \<Longrightarrow> A \<in> X"
   by auto
 
-lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R"
+lemma InterE [elim]: "A \<in> \<Inter>C \<Longrightarrow> (X \<notin> C \<Longrightarrow> R) \<Longrightarrow> (A \<in> X \<Longrightarrow> R) \<Longrightarrow> R"
   -- {* ``Classical'' elimination rule -- does not require proving
-    @{prop "X:C"}. *}
+    @{prop "X \<in> C"}. *}
   by (unfold Inter_eq) blast
 
-lemma Inter_lower: "B \<in> A ==> Inter A \<subseteq> B"
+lemma Inter_lower: "B \<in> A \<Longrightarrow> \<Inter>A \<subseteq> B"
   by (fact Inf_lower)
 
 lemma (in complete_lattice) Inf_less_eq:
@@ -380,18 +380,23 @@
 lemma Inter_insert [simp]: "\<Inter>(insert a B) = a \<inter> \<Inter>B"
   by (fact Inf_insert)
 
+lemma (in complete_lattice) Inf_inter_less: "\<Sqinter>A \<squnion> \<Sqinter>B \<sqsubseteq> \<Sqinter>(A \<inter> B)"
+  by (auto intro: Inf_greatest Inf_lower)
+
 lemma Inter_Un_subset: "\<Inter>A \<union> \<Inter>B \<subseteq> \<Inter>(A \<inter> B)"
-  by blast
+  by (fact Inf_inter_less)
+
+(*lemma (in complete_lattice) Inf_union_distrib: "\<Sqinter>(A \<union> B) = \<Sqinter>A \<sqinter> \<Sqinter>B"*)
 
 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   by blast
 
 lemma Inter_UNIV_conv [simp,no_atp]:
-  "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
-  "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
+  "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
+  "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
   by blast+
 
-lemma Inter_anti_mono: "B \<subseteq> A ==> \<Inter>A \<subseteq> \<Inter>B"
+lemma Inter_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Inter>A \<subseteq> \<Inter>B"
   by blast