1.1 --- a/src/HOL/Complete_Lattice.thy	Sat Jul 16 21:53:50 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sat Jul 16 22:04:02 2011 +0200
     1.3 @@ -108,20 +108,6 @@
     1.4    with `a \<sqsubseteq> b` show "a \<sqsubseteq> \<Squnion>B" by auto
     1.5  qed
     1.6  
     1.7 -lemma top_le:
     1.8 -  "\<top> \<sqsubseteq> x \<Longrightarrow> x = \<top>"
     1.9 -  by (rule antisym) auto
    1.10 -
    1.11 -lemma le_bot:
    1.12 -  "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
    1.13 -  by (rule antisym) auto
    1.14 -
    1.15 -lemma not_less_bot [simp]: "\<not> (x \<sqsubset> \<bottom>)"
    1.16 -  using bot_least [of x] by (auto simp: le_less)
    1.17 -
    1.18 -lemma not_top_less [simp]: "\<not> (\<top> \<sqsubset> x)"
    1.19 -  using top_greatest [of x] by (auto simp: le_less)
    1.20 -
    1.21  lemma Sup_upper2: "u \<in> A \<Longrightarrow> v \<sqsubseteq> u \<Longrightarrow> v \<sqsubseteq> \<Squnion>A"
    1.22    using Sup_upper[of u A] by auto
    1.23  

     2.1 --- a/src/HOL/Orderings.thy	Sat Jul 16 21:53:50 2011 +0200
     2.2 +++ b/src/HOL/Orderings.thy	Sat Jul 16 22:04:02 2011 +0200
     2.3 @@ -1084,35 +1084,54 @@
     2.4  subsection {* (Unique) top and bottom elements *}
     2.5  
     2.6  class bot = order +
     2.7 -  fixes bot :: 'a
     2.8 -  assumes bot_least [simp]: "bot \<le> x"
     2.9 +  fixes bot :: 'a ("\<bottom>")
    2.10 +  assumes bot_least [simp]: "\<bottom> \<le> a"
    2.11  begin
    2.12  
    2.13 +lemma le_bot:
    2.14 +  "a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
    2.15 +  by (auto intro: antisym)
    2.16 +
    2.17  lemma bot_unique:
    2.18 -  "a \<le> bot \<longleftrightarrow> a = bot"
    2.19 -  by (auto simp add: intro: antisym)
    2.20 +  "a \<le> \<bottom> \<longleftrightarrow> a = \<bottom>"
    2.21 +  by (auto intro: antisym)
    2.22 +
    2.23 +lemma not_less_bot [simp]:
    2.24 +  "\<not> (a < \<bottom>)"
    2.25 +  using bot_least [of a] by (auto simp: le_less)
    2.26  
    2.27  lemma bot_less:
    2.28 -  "a \<noteq> bot \<longleftrightarrow> bot < a"
    2.29 +  "a \<noteq> \<bottom> \<longleftrightarrow> \<bottom> < a"
    2.30    by (auto simp add: less_le_not_le intro!: antisym)
    2.31  
    2.32  end
    2.33  
    2.34  class top = order +
    2.35 -  fixes top :: 'a
    2.36 -  assumes top_greatest [simp]: "x \<le> top"
    2.37 +  fixes top :: 'a ("\<top>")
    2.38 +  assumes top_greatest [simp]: "a \<le> \<top>"
    2.39  begin
    2.40  
    2.41 +lemma top_le:
    2.42 +  "\<top> \<le> a \<Longrightarrow> a = \<top>"
    2.43 +  by (rule antisym) auto
    2.44 +
    2.45  lemma top_unique:
    2.46 -  "top \<le> a \<longleftrightarrow> a = top"
    2.47 -  by (auto simp add: intro: antisym)
    2.48 +  "\<top> \<le> a \<longleftrightarrow> a = \<top>"
    2.49 +  by (auto intro: antisym)
    2.50 +
    2.51 +lemma not_top_less [simp]: "\<not> (\<top> < a)"
    2.52 +  using top_greatest [of a] by (auto simp: le_less)
    2.53  
    2.54  lemma less_top:
    2.55 -  "a \<noteq> top \<longleftrightarrow> a < top"
    2.56 +  "a \<noteq> \<top> \<longleftrightarrow> a < \<top>"
    2.57    by (auto simp add: less_le_not_le intro!: antisym)
    2.58  
    2.59  end
    2.60  
    2.61 +no_notation
    2.62 +  bot ("\<bottom>") and
    2.63 +  top ("\<top>")
    2.64 +
    2.65  
    2.66  subsection {* Dense orders *}
    2.67