src/HOL/Orderings.thy
changeset 28685 275122631271
parent 28562 4e74209f113e
child 28823 dcbef866c9e2
     1.1 --- a/src/HOL/Orderings.thy	Fri Oct 24 17:48:36 2008 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Oct 24 17:48:37 2008 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 - (*  Title:      HOL/Orderings.thy
     1.5 +(*  Title:      HOL/Orderings.thy
     1.6      ID:         $Id$
     1.7      Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
     1.8  *)
     1.9 @@ -962,112 +962,6 @@
    1.10    leave out the "(xtrans)" above.
    1.11  *)
    1.12  
    1.13 -subsection {* Order on bool *}
    1.14 -
    1.15 -instantiation bool :: order
    1.16 -begin
    1.17 -
    1.18 -definition
    1.19 -  le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
    1.20 -
    1.21 -definition
    1.22 -  less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
    1.23 -
    1.24 -instance
    1.25 -  by intro_classes (auto simp add: le_bool_def less_bool_def)
    1.26 -
    1.27 -end
    1.28 -
    1.29 -lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
    1.30 -by (simp add: le_bool_def)
    1.31 -
    1.32 -lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
    1.33 -by (simp add: le_bool_def)
    1.34 -
    1.35 -lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
    1.36 -by (simp add: le_bool_def)
    1.37 -
    1.38 -lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    1.39 -by (simp add: le_bool_def)
    1.40 -
    1.41 -lemma [code]:
    1.42 -  "False \<le> b \<longleftrightarrow> True"
    1.43 -  "True \<le> b \<longleftrightarrow> b"
    1.44 -  "False < b \<longleftrightarrow> b"
    1.45 -  "True < b \<longleftrightarrow> False"
    1.46 -  unfolding le_bool_def less_bool_def by simp_all
    1.47 -
    1.48 -
    1.49 -subsection {* Order on functions *}
    1.50 -
    1.51 -instantiation "fun" :: (type, ord) ord
    1.52 -begin
    1.53 -
    1.54 -definition
    1.55 -  le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
    1.56 -
    1.57 -definition
    1.58 -  less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
    1.59 -
    1.60 -instance ..
    1.61 -
    1.62 -end
    1.63 -
    1.64 -instance "fun" :: (type, order) order
    1.65 -  by default
    1.66 -    (auto simp add: le_fun_def less_fun_def
    1.67 -       intro: order_trans order_antisym intro!: ext)
    1.68 -
    1.69 -lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
    1.70 -  unfolding le_fun_def by simp
    1.71 -
    1.72 -lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
    1.73 -  unfolding le_fun_def by simp
    1.74 -
    1.75 -lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
    1.76 -  unfolding le_fun_def by simp
    1.77 -
    1.78 -text {*
    1.79 -  Handy introduction and elimination rules for @{text "\<le>"}
    1.80 -  on unary and binary predicates
    1.81 -*}
    1.82 -
    1.83 -lemma predicate1I:
    1.84 -  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    1.85 -  shows "P \<le> Q"
    1.86 -  apply (rule le_funI)
    1.87 -  apply (rule le_boolI)
    1.88 -  apply (rule PQ)
    1.89 -  apply assumption
    1.90 -  done
    1.91 -
    1.92 -lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    1.93 -  apply (erule le_funE)
    1.94 -  apply (erule le_boolE)
    1.95 -  apply assumption+
    1.96 -  done
    1.97 -
    1.98 -lemma predicate2I [Pure.intro!, intro!]:
    1.99 -  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
   1.100 -  shows "P \<le> Q"
   1.101 -  apply (rule le_funI)+
   1.102 -  apply (rule le_boolI)
   1.103 -  apply (rule PQ)
   1.104 -  apply assumption
   1.105 -  done
   1.106 -
   1.107 -lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   1.108 -  apply (erule le_funE)+
   1.109 -  apply (erule le_boolE)
   1.110 -  apply assumption+
   1.111 -  done
   1.112 -
   1.113 -lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
   1.114 -  by (rule predicate1D)
   1.115 -
   1.116 -lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
   1.117 -  by (rule predicate2D)
   1.118 -
   1.119  
   1.120  subsection {* Monotonicity, least value operator and min/max *}
   1.121  
   1.122 @@ -1123,6 +1017,17 @@
   1.123  done
   1.124  
   1.125  
   1.126 +subsection {* Top and bottom elements *}
   1.127 +
   1.128 +class top = preorder +
   1.129 +  fixes top :: 'a
   1.130 +  assumes top_greatest [simp]: "x \<le> top"
   1.131 +
   1.132 +class bot = preorder +
   1.133 +  fixes bot :: 'a
   1.134 +  assumes bot_least [simp]: "bot \<le> x"
   1.135 +
   1.136 +
   1.137  subsection {* Dense orders *}
   1.138  
   1.139  class dense_linear_order = linorder + 
   1.140 @@ -1189,4 +1094,141 @@
   1.141  
   1.142  end  
   1.143  
   1.144 +
   1.145 +subsection {* Order on bool *}
   1.146 +
   1.147 +instantiation bool :: "{order, top, bot}"
   1.148 +begin
   1.149 +
   1.150 +definition
   1.151 +  le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
   1.152 +
   1.153 +definition
   1.154 +  less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
   1.155 +
   1.156 +definition
   1.157 +  top_bool_eq: "top = True"
   1.158 +
   1.159 +definition
   1.160 +  bot_bool_eq: "bot = False"
   1.161 +
   1.162 +instance proof
   1.163 +qed (auto simp add: le_bool_def less_bool_def top_bool_eq bot_bool_eq)
   1.164 +
   1.165  end
   1.166 +
   1.167 +lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
   1.168 +by (simp add: le_bool_def)
   1.169 +
   1.170 +lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
   1.171 +by (simp add: le_bool_def)
   1.172 +
   1.173 +lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   1.174 +by (simp add: le_bool_def)
   1.175 +
   1.176 +lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
   1.177 +by (simp add: le_bool_def)
   1.178 +
   1.179 +lemma [code]:
   1.180 +  "False \<le> b \<longleftrightarrow> True"
   1.181 +  "True \<le> b \<longleftrightarrow> b"
   1.182 +  "False < b \<longleftrightarrow> b"
   1.183 +  "True < b \<longleftrightarrow> False"
   1.184 +  unfolding le_bool_def less_bool_def by simp_all
   1.185 +
   1.186 +
   1.187 +subsection {* Order on functions *}
   1.188 +
   1.189 +instantiation "fun" :: (type, ord) ord
   1.190 +begin
   1.191 +
   1.192 +definition
   1.193 +  le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
   1.194 +
   1.195 +definition
   1.196 +  less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
   1.197 +
   1.198 +instance ..
   1.199 +
   1.200 +end
   1.201 +
   1.202 +instance "fun" :: (type, preorder) preorder proof
   1.203 +qed (auto simp add: le_fun_def less_fun_def
   1.204 +  intro: order_trans order_antisym intro!: ext)
   1.205 +
   1.206 +instance "fun" :: (type, order) order proof
   1.207 +qed (auto simp add: le_fun_def intro: order_antisym ext)
   1.208 +
   1.209 +instantiation "fun" :: (type, top) top
   1.210 +begin
   1.211 +
   1.212 +definition
   1.213 +  top_fun_eq: "top = (\<lambda>x. top)"
   1.214 +
   1.215 +instance proof
   1.216 +qed (simp add: top_fun_eq le_fun_def)
   1.217 +
   1.218 +end
   1.219 +
   1.220 +instantiation "fun" :: (type, bot) bot
   1.221 +begin
   1.222 +
   1.223 +definition
   1.224 +  bot_fun_eq: "bot = (\<lambda>x. bot)"
   1.225 +
   1.226 +instance proof
   1.227 +qed (simp add: bot_fun_eq le_fun_def)
   1.228 +
   1.229 +end
   1.230 +
   1.231 +lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
   1.232 +  unfolding le_fun_def by simp
   1.233 +
   1.234 +lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
   1.235 +  unfolding le_fun_def by simp
   1.236 +
   1.237 +lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
   1.238 +  unfolding le_fun_def by simp
   1.239 +
   1.240 +text {*
   1.241 +  Handy introduction and elimination rules for @{text "\<le>"}
   1.242 +  on unary and binary predicates
   1.243 +*}
   1.244 +
   1.245 +lemma predicate1I:
   1.246 +  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
   1.247 +  shows "P \<le> Q"
   1.248 +  apply (rule le_funI)
   1.249 +  apply (rule le_boolI)
   1.250 +  apply (rule PQ)
   1.251 +  apply assumption
   1.252 +  done
   1.253 +
   1.254 +lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
   1.255 +  apply (erule le_funE)
   1.256 +  apply (erule le_boolE)
   1.257 +  apply assumption+
   1.258 +  done
   1.259 +
   1.260 +lemma predicate2I [Pure.intro!, intro!]:
   1.261 +  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
   1.262 +  shows "P \<le> Q"
   1.263 +  apply (rule le_funI)+
   1.264 +  apply (rule le_boolI)
   1.265 +  apply (rule PQ)
   1.266 +  apply assumption
   1.267 +  done
   1.268 +
   1.269 +lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   1.270 +  apply (erule le_funE)+
   1.271 +  apply (erule le_boolE)
   1.272 +  apply assumption+
   1.273 +  done
   1.274 +
   1.275 +lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
   1.276 +  by (rule predicate1D)
   1.277 +
   1.278 +lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
   1.279 +  by (rule predicate2D)
   1.280 +
   1.281 +end