src/HOL/Orderings.thy
changeset 41082 9ff94e7cc3b3
parent 41080 294956ff285b
child 42284 326f57825e1a
     1.1 --- a/src/HOL/Orderings.thy	Wed Dec 08 14:52:23 2010 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Wed Dec 08 15:05:46 2010 +0100
     1.3 @@ -1082,14 +1082,14 @@
     1.4  
     1.5  subsection {* Top and bottom elements *}
     1.6  
     1.7 +class bot = preorder +
     1.8 +  fixes bot :: 'a
     1.9 +  assumes bot_least [simp]: "bot \<le> x"
    1.10 +
    1.11  class top = preorder +
    1.12    fixes top :: 'a
    1.13    assumes top_greatest [simp]: "x \<le> top"
    1.14  
    1.15 -class bot = preorder +
    1.16 -  fixes bot :: 'a
    1.17 -  assumes bot_least [simp]: "bot \<le> x"
    1.18 -
    1.19  
    1.20  subsection {* Dense orders *}
    1.21  
    1.22 @@ -1204,7 +1204,7 @@
    1.23  
    1.24  subsection {* Order on bool *}
    1.25  
    1.26 -instantiation bool :: "{order, top, bot}"
    1.27 +instantiation bool :: "{order, bot, top}"
    1.28  begin
    1.29  
    1.30  definition
    1.31 @@ -1214,10 +1214,10 @@
    1.32    [simp]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
    1.33  
    1.34  definition
    1.35 -  [simp]: "top \<longleftrightarrow> True"
    1.36 +  [simp]: "bot \<longleftrightarrow> False"
    1.37  
    1.38  definition
    1.39 -  [simp]: "bot \<longleftrightarrow> False"
    1.40 +  [simp]: "top \<longleftrightarrow> True"
    1.41  
    1.42  instance proof
    1.43  qed auto
    1.44 @@ -1272,6 +1272,21 @@
    1.45  instance "fun" :: (type, order) order proof
    1.46  qed (auto simp add: le_fun_def intro: antisym ext)
    1.47  
    1.48 +instantiation "fun" :: (type, bot) bot
    1.49 +begin
    1.50 +
    1.51 +definition
    1.52 +  "bot = (\<lambda>x. bot)"
    1.53 +
    1.54 +lemma bot_apply:
    1.55 +  "bot x = bot"
    1.56 +  by (simp add: bot_fun_def)
    1.57 +
    1.58 +instance proof
    1.59 +qed (simp add: le_fun_def bot_apply)
    1.60 +
    1.61 +end
    1.62 +
    1.63  instantiation "fun" :: (type, top) top
    1.64  begin
    1.65  
    1.66 @@ -1288,21 +1303,6 @@
    1.67  
    1.68  end
    1.69  
    1.70 -instantiation "fun" :: (type, bot) bot
    1.71 -begin
    1.72 -
    1.73 -definition
    1.74 -  "bot = (\<lambda>x. bot)"
    1.75 -
    1.76 -lemma bot_apply:
    1.77 -  "bot x = bot"
    1.78 -  by (simp add: bot_fun_def)
    1.79 -
    1.80 -instance proof
    1.81 -qed (simp add: le_fun_def bot_apply)
    1.82 -
    1.83 -end
    1.84 -
    1.85  lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
    1.86    unfolding le_fun_def by simp
    1.87