more on complement
authorhaftmann
Sun Jul 17 22:24:08 2011 +0200 (2011-07-17)
changeset 438738a2f339641c1
parent 43872 6b917e5877d2
child 43874 74f1f2dd8f52
more on complement
NEWS
src/HOL/Complete_Lattice.thy
src/HOL/Lattices.thy
     1.1 --- a/NEWS	Sun Jul 17 20:57:56 2011 +0200
     1.2 +++ b/NEWS	Sun Jul 17 22:24:08 2011 +0200
     1.3 @@ -71,6 +71,10 @@
     1.4    le_SUPI ~> le_SUP_I
     1.5    le_SUPI2 ~> le_SUP_I2
     1.6    le_INFI ~> le_INF_I
     1.7 +  INFI_bool_eq ~> INF_bool_eq
     1.8 +  SUPR_bool_eq ~> SUP_bool_eq
     1.9 +  INFI_apply ~> INF_apply
    1.10 +  SUPR_apply ~> SUP_apply
    1.11  INCOMPATIBILITY.
    1.12  
    1.13  * Archimedian_Field.thy:
     2.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 17 20:57:56 2011 +0200
     2.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 22:24:08 2011 +0200
     2.3 @@ -349,19 +349,19 @@
     2.4   "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
     2.5    by (auto simp add: SUP_def Sup_bot_conv)
     2.6  
     2.7 -lemma (in complete_lattice) INF_UNIV_range:
     2.8 +lemma INF_UNIV_range:
     2.9    "(\<Sqinter>x. f x) = \<Sqinter>range f"
    2.10    by (fact INF_def)
    2.11  
    2.12 -lemma (in complete_lattice) SUP_UNIV_range:
    2.13 +lemma SUP_UNIV_range:
    2.14    "(\<Squnion>x. f x) = \<Squnion>range f"
    2.15    by (fact SUP_def)
    2.16  
    2.17 -lemma INF_bool_eq:
    2.18 +lemma INF_UNIV_bool_expand:
    2.19    "(\<Sqinter>b. A b) = A True \<sqinter> A False"
    2.20    by (simp add: UNIV_bool INF_empty INF_insert inf_commute)
    2.21  
    2.22 -lemma SUP_bool_eq:
    2.23 +lemma SUP_UNIV_bool_expand:
    2.24    "(\<Squnion>b. A b) = A True \<squnion> A False"
    2.25    by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
    2.26  
    2.27 @@ -397,9 +397,45 @@
    2.28    shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
    2.29    unfolding SUP_def less_Sup_iff by auto
    2.30  
    2.31 +-- "FIXME move"
    2.32 +
    2.33 +lemma image_ident [simp]: "(%x. x) ` Y = Y"
    2.34 +  by blast
    2.35 +
    2.36 +lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
    2.37 +  by blast
    2.38 +
    2.39 +class complete_boolean_algebra = boolean_algebra + complete_lattice
    2.40 +begin
    2.41 +
    2.42 +lemma uminus_Inf:
    2.43 +  "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
    2.44 +proof (rule antisym)
    2.45 +  show "- \<Sqinter>A \<le> \<Squnion>(uminus ` A)"
    2.46 +    by (rule compl_le_swap2, rule Inf_greatest, rule compl_le_swap2, rule Sup_upper) simp
    2.47 +  show "\<Squnion>(uminus ` A) \<le> - \<Sqinter>A"
    2.48 +    by (rule Sup_least, rule compl_le_swap1, rule Inf_lower) auto
    2.49 +qed
    2.50 +
    2.51 +lemma uminus_Sup:
    2.52 +  "- (\<Squnion>A) = \<Sqinter>(uminus ` A)"
    2.53 +proof -
    2.54 +  have "\<Squnion>A = - \<Sqinter>(uminus ` A)" by (simp add: image_image uminus_Inf)
    2.55 +  then show ?thesis by simp
    2.56 +qed
    2.57 +  
    2.58 +lemma uminus_INF: "- (\<Sqinter>x\<in>A. B x) = (\<Squnion>x\<in>A. - B x)"
    2.59 +  by (simp add: INF_def SUP_def uminus_Inf image_image)
    2.60 +
    2.61 +lemma uminus_SUP: "- (\<Squnion>x\<in>A. B x) = (\<Sqinter>x\<in>A. - B x)"
    2.62 +  by (simp add: INF_def SUP_def uminus_Sup image_image)
    2.63 +
    2.64 +end
    2.65 +
    2.66 +
    2.67  subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
    2.68  
    2.69 -instantiation bool :: complete_lattice
    2.70 +instantiation bool :: complete_boolean_algebra
    2.71  begin
    2.72  
    2.73  definition
    2.74 @@ -413,7 +449,7 @@
    2.75  
    2.76  end
    2.77  
    2.78 -lemma INFI_bool_eq [simp]:
    2.79 +lemma INF_bool_eq [simp]:
    2.80    "INFI = Ball"
    2.81  proof (rule ext)+
    2.82    fix A :: "'a set"
    2.83 @@ -422,7 +458,7 @@
    2.84      by (auto simp add: Ball_def INF_def Inf_bool_def)
    2.85  qed
    2.86  
    2.87 -lemma SUPR_bool_eq [simp]:
    2.88 +lemma SUP_bool_eq [simp]:
    2.89    "SUPR = Bex"
    2.90  proof (rule ext)+
    2.91    fix A :: "'a set"
    2.92 @@ -454,14 +490,16 @@
    2.93  
    2.94  end
    2.95  
    2.96 -lemma INFI_apply:
    2.97 +lemma INF_apply:
    2.98    "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
    2.99    by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def Inf_apply)
   2.100  
   2.101 -lemma SUPR_apply:
   2.102 +lemma SUP_apply:
   2.103    "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   2.104    by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
   2.105  
   2.106 +instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
   2.107 +
   2.108  
   2.109  subsection {* Inter *}
   2.110  
   2.111 @@ -647,7 +685,7 @@
   2.112    by (fact INF_top_conv)+
   2.113  
   2.114  lemma INT_bool_eq: "(\<Inter>b. A b) = A True \<inter> A False"
   2.115 -  by (fact INF_bool_eq)
   2.116 +  by (fact INF_UNIV_bool_expand)
   2.117  
   2.118  lemma INT_anti_mono:
   2.119    "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)"
   2.120 @@ -945,11 +983,11 @@
   2.121  
   2.122  subsection {* Complement *}
   2.123  
   2.124 -lemma Compl_UN [simp]: "- (\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
   2.125 -  by blast
   2.126 +lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
   2.127 +  by (fact uminus_INF)
   2.128  
   2.129 -lemma Compl_INT [simp]: "- (\<Inter>x\<in>A. B x) = (\<Union>x\<in>A. -B x)"
   2.130 -  by blast
   2.131 +lemma Compl_UN [simp]: "- (\<Union>x\<in>A. B x) = (\<Inter>x\<in>A. -B x)"
   2.132 +  by (fact uminus_SUP)
   2.133  
   2.134  
   2.135  subsection {* Miniscoping and maxiscoping *}
   2.136 @@ -1047,7 +1085,8 @@
   2.137  lemmas (in complete_lattice) le_SUPI = le_SUP_I
   2.138  lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
   2.139  lemmas (in complete_lattice) le_INFI = le_INF_I
   2.140 -
   2.141 +lemmas INFI_apply = INF_apply
   2.142 +lemmas SUPR_apply = SUP_apply
   2.143  
   2.144  text {* Finally *}
   2.145  
     3.1 --- a/src/HOL/Lattices.thy	Sun Jul 17 20:57:56 2011 +0200
     3.2 +++ b/src/HOL/Lattices.thy	Sun Jul 17 22:24:08 2011 +0200
     3.3 @@ -524,7 +524,39 @@
     3.4  
     3.5  lemma compl_le_compl_iff: (* TODO: declare [simp] ? *)
     3.6    "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
     3.7 -by (auto dest: compl_mono)
     3.8 +  by (auto dest: compl_mono)
     3.9 +
    3.10 +lemma compl_le_swap1:
    3.11 +  assumes "y \<sqsubseteq> - x" shows "x \<sqsubseteq> -y"
    3.12 +proof -
    3.13 +  from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff)
    3.14 +  then show ?thesis by simp
    3.15 +qed
    3.16 +
    3.17 +lemma compl_le_swap2:
    3.18 +  assumes "- y \<sqsubseteq> x" shows "- x \<sqsubseteq> y"
    3.19 +proof -
    3.20 +  from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff)
    3.21 +  then show ?thesis by simp
    3.22 +qed
    3.23 +
    3.24 +lemma compl_less_compl_iff: (* TODO: declare [simp] ? *)
    3.25 +  "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"
    3.26 +  by (auto simp add: less_le compl_le_compl_iff)
    3.27 +
    3.28 +lemma compl_less_swap1:
    3.29 +  assumes "y \<sqsubset> - x" shows "x \<sqsubset> - y"
    3.30 +proof -
    3.31 +  from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff)
    3.32 +  then show ?thesis by simp
    3.33 +qed
    3.34 +
    3.35 +lemma compl_less_swap2:
    3.36 +  assumes "- y \<sqsubset> x" shows "- x \<sqsubset> y"
    3.37 +proof -
    3.38 +  from assms have "- x \<sqsubset> - (- y)" by (simp only: compl_less_compl_iff)
    3.39 +  then show ?thesis by simp
    3.40 +qed
    3.41  
    3.42  end
    3.43