moved lemmas bot_less and less_top to classes bot and top respectively
authorhaftmann
Wed Jul 13 19:43:12 2011 +0200 (2011-07-13)
changeset 4381458791b75cf1f
parent 43813 07f0650146f2
child 43815 4f6e2965d821
moved lemmas bot_less and less_top to classes bot and top respectively
src/HOL/Complete_Lattice.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Complete_Lattice.thy	Wed Jul 13 19:40:18 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Wed Jul 13 19:43:12 2011 +0200
     1.3 @@ -392,15 +392,6 @@
     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 bounded_lattice_bot) bot_less:
     1.8 -  -- {* FIXME: tighten classes bot, top to partial orders (uniqueness!), move lemmas there *}
     1.9 -  "a \<noteq> bot \<longleftrightarrow> bot < a"
    1.10 -  by (auto simp add: less_le_not_le intro!: antisym)
    1.11 -
    1.12 -lemma (in bounded_lattice_top) less_top:
    1.13 -  "a \<noteq> top \<longleftrightarrow> a < top"
    1.14 -  by (auto simp add: less_le_not_le intro!: antisym)
    1.15 -
    1.16  lemma (in complete_lattice) Inf_top_conv [no_atp]:
    1.17    "\<Sqinter>A = \<top> \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
    1.18    "\<top> = \<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<top>)"
     2.1 --- a/src/HOL/Orderings.thy	Wed Jul 13 19:40:18 2011 +0200
     2.2 +++ b/src/HOL/Orderings.thy	Wed Jul 13 19:43:12 2011 +0200
     2.3 @@ -1086,10 +1086,24 @@
     2.4  class bot = order +
     2.5    fixes bot :: 'a
     2.6    assumes bot_least [simp]: "bot \<le> x"
     2.7 +begin
     2.8 +
     2.9 +lemma bot_less:
    2.10 +  "a \<noteq> bot \<longleftrightarrow> bot < a"
    2.11 +  by (auto simp add: less_le_not_le intro!: antisym)
    2.12 +
    2.13 +end
    2.14  
    2.15  class top = order +
    2.16    fixes top :: 'a
    2.17    assumes top_greatest [simp]: "x \<le> top"
    2.18 +begin
    2.19 +
    2.20 +lemma less_top:
    2.21 +  "a \<noteq> top \<longleftrightarrow> a < top"
    2.22 +  by (auto simp add: less_le_not_le intro!: antisym)
    2.23 +
    2.24 +end
    2.25  
    2.26  
    2.27  subsection {* Dense orders *}