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)