src/HOL/Orderings.thy
changeset 43816 05ab37be94ed
parent 43814 58791b75cf1f
child 43853 020ddc6a9508
     1.1 --- a/src/HOL/Orderings.thy	Wed Jul 13 23:41:13 2011 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Wed Jul 13 23:49:56 2011 +0200
     1.3 @@ -1088,6 +1088,10 @@
     1.4    assumes bot_least [simp]: "bot \<le> x"
     1.5  begin
     1.6  
     1.7 +lemma bot_unique:
     1.8 +  "a \<le> bot \<longleftrightarrow> a = bot"
     1.9 +  by (auto simp add: intro: antisym)
    1.10 +
    1.11  lemma bot_less:
    1.12    "a \<noteq> bot \<longleftrightarrow> bot < a"
    1.13    by (auto simp add: less_le_not_le intro!: antisym)
    1.14 @@ -1099,6 +1103,10 @@
    1.15    assumes top_greatest [simp]: "x \<le> top"
    1.16  begin
    1.17  
    1.18 +lemma top_unique:
    1.19 +  "top \<le> a \<longleftrightarrow> a = top"
    1.20 +  by (auto simp add: intro: antisym)
    1.21 +
    1.22  lemma less_top:
    1.23    "a \<noteq> top \<longleftrightarrow> a < top"
    1.24    by (auto simp add: less_le_not_le intro!: antisym)