1.1 --- a/src/HOL/Complete_Lattice.thy Wed Jul 13 15:50:45 2011 +0200
1.2 +++ b/src/HOL/Complete_Lattice.thy Wed Jul 13 18:36:11 2011 +0200
1.3 @@ -392,13 +392,41 @@
1.4 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
1.5 by (fact Inf_union_distrib)
1.6
1.7 -(*lemma (in complete_lattice) Inf_top_conv [no_atp]:
1.8 - "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"*)
1.9 +lemma (in bounded_lattice_bot) bot_less:
1.10 + -- {* FIXME: tighten classes bot, top to partial orders (uniqueness!), move lemmas there *}
1.11 + "a \<noteq> bot \<longleftrightarrow> bot < a"
1.12 + by (auto simp add: less_le_not_le intro!: antisym)
1.13 +
1.14 +lemma (in bounded_lattice_top) less_top:
1.15 + "a \<noteq> top \<longleftrightarrow> a < top"
1.16 + by (auto simp add: less_le_not_le intro!: antisym)
1.17 +
1.18 +lemma (in complete_lattice) Inf_top_conv [no_atp]:
1.19 + "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
1.20 + "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
1.21 +proof -
1.22 + show "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
1.23 + proof
1.24 + assume "\<forall>x\<in>A. x = \<top>"
1.25 + then have "A = {} \<or> A = {\<top>}" by auto
1.26 + then show "\<Sqinter>A = \<top>" by auto
1.27 + next
1.28 + assume "\<Sqinter>A = \<top>"
1.29 + show "\<forall>x\<in>A. x = \<top>"
1.30 + proof (rule ccontr)
1.31 + assume "\<not> (\<forall>x\<in>A. x = \<top>)"
1.32 + then obtain x where "x \<in> A" and "x \<noteq> \<top>" by blast
1.33 + then obtain B where "A = insert x B" by blast
1.34 + with `\<Sqinter>A = \<top>` `x \<noteq> \<top>` show False by (simp add: Inf_insert)
1.35 + qed
1.36 + qed
1.37 + then show "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)" by auto
1.38 +qed
1.39
1.40 lemma Inter_UNIV_conv [simp,no_atp]:
1.41 "\<Inter>A = UNIV \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
1.42 "UNIV = \<Inter>A \<longleftrightarrow> (\<forall>x\<in>A. x = UNIV)"
1.43 - by blast+
1.44 + by (fact Inf_top_conv)+
1.45
1.46 lemma (in complete_lattice) Inf_anti_mono: "B \<subseteq> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> \<Sqinter>B"
1.47 by (auto intro: Inf_greatest Inf_lower)
1.48 @@ -448,7 +476,7 @@
1.49
1.50 lemma Inter_image_eq [simp]:
1.51 "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
1.52 - by (rule sym) (fact INTER_eq_Inter_image)
1.53 + by (rule sym) (fact INFI_def)
1.54
1.55 lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
1.56 by (unfold INTER_def) blast