# HG changeset patch
# User haftmann
# Date 1310934248 -7200
# Node ID 8a2f339641c1060251abb8e62776b3587a48aecd
# Parent  6b917e5877d285b8ea346960bcd493cbbe1fb1e0
more on complement

diff -r 6b917e5877d2 -r 8a2f339641c1 NEWS
--- a/NEWS	Sun Jul 17 20:57:56 2011 +0200
+++ b/NEWS	Sun Jul 17 22:24:08 2011 +0200
@@ -71,6 +71,10 @@
   le_SUPI ~> le_SUP_I
   le_SUPI2 ~> le_SUP_I2
   le_INFI ~> le_INF_I
+  INFI_bool_eq ~> INF_bool_eq
+  SUPR_bool_eq ~> SUP_bool_eq
+  INFI_apply ~> INF_apply
+  SUPR_apply ~> SUP_apply
 INCOMPATIBILITY.
 
 * Archimedian_Field.thy:
diff -r 6b917e5877d2 -r 8a2f339641c1 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Sun Jul 17 20:57:56 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 22:24:08 2011 +0200
@@ -349,19 +349,19 @@
  "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   by (auto simp add: SUP_def Sup_bot_conv)
 
-lemma (in complete_lattice) INF_UNIV_range:
+lemma INF_UNIV_range:
   "(\<Sqinter>x. f x) = \<Sqinter>range f"
   by (fact INF_def)
 
-lemma (in complete_lattice) SUP_UNIV_range:
+lemma SUP_UNIV_range:
   "(\<Squnion>x. f x) = \<Squnion>range f"
   by (fact SUP_def)
 
-lemma INF_bool_eq:
+lemma INF_UNIV_bool_expand:
   "(\<Sqinter>b. A b) = A True \<sqinter> A False"
   by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
 
-lemma SUP_bool_eq:
+lemma SUP_UNIV_bool_expand:
   "(\<Squnion>b. A b) = A True \<squnion> A False"
   by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
 
@@ -397,9 +397,45 @@
   shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
   unfolding SUP_def less_Sup_iff by auto
 
+-- "FIXME move"
+
+lemma image_ident [simp]: "(%x. x) ` Y = Y"
+  by blast
+
+lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
+  by blast
+
+class complete_boolean_algebra = boolean_algebra + complete_lattice
+begin
+
+lemma uminus_Inf:
+  "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
+proof (rule antisym)
+  show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)"
+    by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp
+  show "\<Squnion>(uminus ` A) \<le> - \<Sqinter>A"
+    by (rule Sup_least, rule compl_le_swap1, rule Inf_lower) auto
+qed
+
+lemma uminus_Sup:
+  "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
+proof -
+  have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_Inf)
+  then show ?thesis by simp
+qed
+  
+lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
+  by (simp add: INF_def SUP_def uminus_Inf image_image)
+
+lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
+  by (simp add: INF_def SUP_def uminus_Sup image_image)
+
+end
+
+
 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
 
-instantiation bool :: complete_lattice
+instantiation bool :: complete_boolean_algebra
 begin
 
 definition
@@ -413,7 +449,7 @@
 
 end
 
-lemma INFI_bool_eq [simp]:
+lemma INF_bool_eq [simp]:
   "INFI = Ball"
 proof (rule ext)+
   fix A :: "'a set"
@@ -422,7 +458,7 @@
     by (auto simp add: Ball_def INF_def Inf_bool_def)
 qed
 
-lemma SUPR_bool_eq [simp]:
+lemma SUP_bool_eq [simp]:
   "SUPR = Bex"
 proof (rule ext)+
   fix A :: "'a set"
@@ -454,14 +490,16 @@
 
 end
 
-lemma INFI_apply:
+lemma INF_apply:
   "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def Inf_apply)
 
-lemma SUPR_apply:
+lemma SUP_apply:
   "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
 
+instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
+
 
 subsection {* Inter *}
 
@@ -647,7 +685,7 @@
   by (fact INF_top_conv)+
 
 lemma INT_bool_eq: "(\<Inter>b. A b) = A True \<inter> A False"
-  by (fact INF_bool_eq)
+  by (fact INF_UNIV_bool_expand)
 
 lemma INT_anti_mono:
   "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>B. g x)"
@@ -945,11 +983,11 @@
 
 subsection {* Complement *}
 
-lemma Compl_UN [simp]: "- (\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
-  by blast
+lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
+  by (fact uminus_INF)
 
-lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
-  by blast
+lemma Compl_UN [simp]: "- (\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
+  by (fact uminus_SUP)
 
 
 subsection {* Miniscoping and maxiscoping *}
@@ -1047,7 +1085,8 @@
 lemmas (in complete_lattice) le_SUPI = le_SUP_I
 lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
 lemmas (in complete_lattice) le_INFI = le_INF_I
-
+lemmas INFI_apply = INF_apply
+lemmas SUPR_apply = SUP_apply
 
 text {* Finally *}
 
diff -r 6b917e5877d2 -r 8a2f339641c1 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sun Jul 17 20:57:56 2011 +0200
+++ b/src/HOL/Lattices.thy	Sun Jul 17 22:24:08 2011 +0200
@@ -524,7 +524,39 @@
 
 lemma compl_le_compl_iff: (* TODO: declare [simp] ? *)
   "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
-by (auto dest: compl_mono)
+  by (auto dest: compl_mono)
+
+lemma compl_le_swap1:
+  assumes "y \<sqsubseteq> - x" shows "x \<sqsubseteq> -y"
+proof -
+  from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff)
+  then show ?thesis by simp
+qed
+
+lemma compl_le_swap2:
+  assumes "- y \<sqsubseteq> x" shows "- x \<sqsubseteq> y"
+proof -
+  from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff)
+  then show ?thesis by simp
+qed
+
+lemma compl_less_compl_iff: (* TODO: declare [simp] ? *)
+  "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"
+  by (auto simp add: less_le compl_le_compl_iff)
+
+lemma compl_less_swap1:
+  assumes "y \<sqsubset> - x" shows "x \<sqsubset> - y"
+proof -
+  from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff)
+  then show ?thesis by simp
+qed
+
+lemma compl_less_swap2:
+  assumes "- y \<sqsubset> x" shows "- x \<sqsubset> y"
+proof -
+  from assms have "- x \<sqsubset> - (- y)" by (simp only: compl_less_compl_iff)
+  then show ?thesis by simp
+qed
 
 end