src/HOL/Complete_Lattice.thy
changeset 43854 f1d23df1adde
parent 43853 020ddc6a9508
child 43865 db18f4d0cc7d
     1.1 --- a/src/HOL/Complete_Lattice.thy	Sat Jul 16 22:04:02 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sat Jul 16 22:28:35 2011 +0200
     1.3 @@ -208,6 +208,12 @@
     1.4  lemma SUP_commute: "(\<Squnion>i\<in>A. \<Squnion>j\<in>B. f i j) = (\<Squnion>j\<in>B. \<Squnion>i\<in>A. f i j)"
     1.5    by (iprover intro: SUP_leI le_SUPI order_trans antisym)
     1.6  
     1.7 +lemma INFI_insert: "(\<Sqinter>x\<in>insert a A. B x) = B a \<sqinter> INFI A B"
     1.8 +  by (simp add: INFI_def Inf_insert)
     1.9 +
    1.10 +lemma SUPR_insert: "(\<Squnion>x\<in>insert a A. B x) = B a \<squnion> SUPR A B"
    1.11 +  by (simp add: SUPR_def Sup_insert)
    1.12 +
    1.13  end
    1.14  
    1.15  lemma Inf_less_iff:
    1.16 @@ -468,9 +474,13 @@
    1.17    -- {* "Classical" elimination -- by the Excluded Middle on @{prop "a\<in>A"}. *}
    1.18    by (unfold INTER_def) blast
    1.19  
    1.20 +lemma (in complete_lattice) INFI_cong:
    1.21 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Sqinter>x\<in>A. C x) = (\<Sqinter>x\<in>B. D x)"
    1.22 +  by (simp add: INFI_def image_def)
    1.23 +
    1.24  lemma INT_cong [cong]:
    1.25 -    "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Inter>x\<in>A. C x) = (\<Inter>x\<in>B. D x)"
    1.26 -  by (simp add: INTER_def)
    1.27 +  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> (\<Inter>x\<in>A. C x) = (\<Inter>x\<in>B. D x)"
    1.28 +  by (fact INFI_cong)
    1.29  
    1.30  lemma Collect_ball_eq: "{x. \<forall>y\<in>A. P x y} = (\<Inter>y\<in>A. {x. P x y})"
    1.31    by blast
    1.32 @@ -484,17 +494,31 @@
    1.33  lemma INT_greatest: "(\<And>x. x \<in> A \<Longrightarrow> C \<subseteq> B x) \<Longrightarrow> C \<subseteq> (\<Inter>x\<in>A. B x)"
    1.34    by (fact le_INFI)
    1.35  
    1.36 +lemma (in complete_lattice) INFI_empty:
    1.37 +  "(\<Sqinter>x\<in>{}. B x) = \<top>"
    1.38 +  by (simp add: INFI_def)
    1.39 +
    1.40  lemma INT_empty [simp]: "(\<Inter>x\<in>{}. B x) = UNIV"
    1.41 -  by blast
    1.42 +  by (fact INFI_empty)
    1.43 +
    1.44 +lemma (in complete_lattice) INFI_absorb:
    1.45 +  assumes "k \<in> I"
    1.46 +  shows "A k \<sqinter> (\<Sqinter>i\<in>I. A i) = (\<Sqinter>i\<in>I. A i)"
    1.47 +proof -
    1.48 +  from assms obtain J where "I = insert k J" by blast
    1.49 +  then show ?thesis by (simp add: INFI_insert)
    1.50 +qed
    1.51  
    1.52  lemma INT_absorb: "k \<in> I \<Longrightarrow> A k \<inter> (\<Inter>i\<in>I. A i) = (\<Inter>i\<in>I. A i)"
    1.53 -  by blast
    1.54 +  by (fact INFI_absorb)
    1.55  
    1.56 -lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
    1.57 +lemma INT_subset_iff: "B \<subseteq> (\<Inter>i\<in>I. A i) \<longleftrightarrow> (\<forall>i\<in>I. B \<subseteq> A i)"
    1.58    by (fact le_INF_iff)
    1.59  
    1.60  lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
    1.61 -  by blast
    1.62 +  by (fact INFI_insert)
    1.63 +
    1.64 +-- {* continue generalization from here *}
    1.65  
    1.66  lemma INT_Un: "(\<Inter>i \<in> A \<union> B. M i) = (\<Inter>i \<in> A. M i) \<inter> (\<Inter>i\<in>B. M i)"
    1.67    by blast
    1.68 @@ -510,10 +534,10 @@
    1.69    -- {* Look: it has an \emph{existential} quantifier *}
    1.70    by blast
    1.71  
    1.72 -lemma INTER_UNIV_conv[simp]:
    1.73 +lemma INTER_UNIV_conv [simp]:
    1.74   "(UNIV = (\<Inter>x\<in>A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
    1.75   "((\<Inter>x\<in>A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
    1.76 -by blast+
    1.77 +  by blast+
    1.78  
    1.79  lemma INT_bool_eq: "(\<Inter>b. A b) = (A True \<inter> A False)"
    1.80    by (auto intro: bool_induct)