src/HOL/Orderings.thy
changeset 43853 020ddc6a9508
parent 43816 05ab37be94ed
child 44025 ec2a7901217b
     1.1 --- a/src/HOL/Orderings.thy	Sat Jul 16 21:53:50 2011 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Sat Jul 16 22:04:02 2011 +0200
     1.3 @@ -1084,35 +1084,54 @@
     1.4  subsection {* (Unique) top and bottom elements *}
     1.5  
     1.6  class bot = order +
     1.7 -  fixes bot :: 'a
     1.8 -  assumes bot_least [simp]: "bot \<le> x"
     1.9 +  fixes bot :: 'a ("\<bottom>")
    1.10 +  assumes bot_least [simp]: "\<bottom> \<le> a"
    1.11  begin
    1.12  
    1.13 +lemma le_bot:
    1.14 +  "a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
    1.15 +  by (auto intro: antisym)
    1.16 +
    1.17  lemma bot_unique:
    1.18 -  "a \<le> bot \<longleftrightarrow> a = bot"
    1.19 -  by (auto simp add: intro: antisym)
    1.20 +  "a \<le> \<bottom> \<longleftrightarrow> a = \<bottom>"
    1.21 +  by (auto intro: antisym)
    1.22 +
    1.23 +lemma not_less_bot [simp]:
    1.24 +  "\<not> (a < \<bottom>)"
    1.25 +  using bot_least [of a] by (auto simp: le_less)
    1.26  
    1.27  lemma bot_less:
    1.28 -  "a \<noteq> bot \<longleftrightarrow> bot < a"
    1.29 +  "a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a"
    1.30    by (auto simp add: less_le_not_le intro!: antisym)
    1.31  
    1.32  end
    1.33  
    1.34  class top = order +
    1.35 -  fixes top :: 'a
    1.36 -  assumes top_greatest [simp]: "x \<le> top"
    1.37 +  fixes top :: 'a ("\<top>")
    1.38 +  assumes top_greatest [simp]: "a \<le> \<top>"
    1.39  begin
    1.40  
    1.41 +lemma top_le:
    1.42 +  "\<top> \<le> a \<Longrightarrow> a = \<top>"
    1.43 +  by (rule antisym) auto
    1.44 +
    1.45  lemma top_unique:
    1.46 -  "top \<le> a \<longleftrightarrow> a = top"
    1.47 -  by (auto simp add: intro: antisym)
    1.48 +  "\<top> \<le> a \<longleftrightarrow> a = \<top>"
    1.49 +  by (auto intro: antisym)
    1.50 +
    1.51 +lemma not_top_less [simp]: "\<not> (\<top> < a)"
    1.52 +  using top_greatest [of a] by (auto simp: le_less)
    1.53  
    1.54  lemma less_top:
    1.55 -  "a \<noteq> top \<longleftrightarrow> a < top"
    1.56 +  "a \<noteq> \<top> \<longleftrightarrow> a < \<top>"
    1.57    by (auto simp add: less_le_not_le intro!: antisym)
    1.58  
    1.59  end
    1.60  
    1.61 +no_notation
    1.62 +  bot ("\<bottom>") and
    1.63 +  top ("\<top>")
    1.64 +
    1.65  
    1.66  subsection {* Dense orders *}
    1.67