1.1 --- a/src/HOL/Complete_Lattice.thy	Tue Jul 12 23:22:22 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Wed Jul 13 07:26:31 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