new classes "top" and "bot"
authorhaftmann
Fri Oct 24 17:48:37 2008 +0200 (2008-10-24)
changeset 28685275122631271
parent 28684 48faac324061
child 28686 5d63184c10c7
new classes "top" and "bot"
NEWS
src/HOL/Lattices.thy
src/HOL/Orderings.thy
src/HOL/SizeChange/Graphs.thy
     1.1 --- a/NEWS	Fri Oct 24 17:48:36 2008 +0200
     1.2 +++ b/NEWS	Fri Oct 24 17:48:37 2008 +0200
     1.3 @@ -104,10 +104,19 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New classes "top" and "bot" with corresponding operations "top" and "bot"
     1.8 +in theory Orderings;  instantiation of class "complete_lattice" requires
     1.9 +instantiation of classes "top" and "bot".  INCOMPATIBILITY.
    1.10 +
    1.11 +* Changed definition lemma "less_fun_def" in order to provide an instance
    1.12 +for preorders on functions;  use lemma "less_le" instead.  INCOMPATIBILITY.
    1.13 +
    1.14  * Unified theorem tables for both code code generators.  Thus
    1.15  [code func] has disappeared and only [code] remains.  INCOMPATIBILITY.
    1.16  
    1.17 -* Constant "undefined" replaces "arbitrary" in most occurences.
    1.18 +* Constants "undefined" and "default" replace "arbitrary".  Usually
    1.19 +"undefined" is the right choice to replace "arbitrary", though logically
    1.20 +there is no difference.  INCOMPATIBILITY.
    1.21  
    1.22  * Generic ATP manager for Sledgehammer, based on ML threads instead of
    1.23  Posix processes.  Avoids potentially expensive forking of the ML
     2.1 --- a/src/HOL/Lattices.thy	Fri Oct 24 17:48:36 2008 +0200
     2.2 +++ b/src/HOL/Lattices.thy	Fri Oct 24 17:48:37 2008 +0200
     2.3 @@ -332,7 +332,7 @@
     2.4  
     2.5  subsection {* Complete lattices *}
     2.6  
     2.7 -class complete_lattice = lattice +
     2.8 +class complete_lattice = lattice + top + bot +
     2.9    fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
    2.10      and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
    2.11    assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
    2.12 @@ -383,19 +383,13 @@
    2.13    "\<Squnion>{a, b} = a \<squnion> b"
    2.14    by (simp add: Sup_insert_simp)
    2.15  
    2.16 -definition
    2.17 -  top :: 'a where
    2.18 +lemma top_def:
    2.19    "top = \<Sqinter>{}"
    2.20 +  by (auto intro: antisym Inf_greatest)
    2.21  
    2.22 -definition
    2.23 -  bot :: 'a where
    2.24 +lemma bot_def:
    2.25    "bot = \<Squnion>{}"
    2.26 -
    2.27 -lemma top_greatest [simp]: "x \<le> top"
    2.28 -  by (unfold top_def, rule Inf_greatest, simp)
    2.29 -
    2.30 -lemma bot_least [simp]: "bot \<le> x"
    2.31 -  by (unfold bot_def, rule Sup_least, simp)
    2.32 +  by (auto intro: antisym Sup_least)
    2.33  
    2.34  definition
    2.35    SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    2.36 @@ -499,12 +493,6 @@
    2.37    "\<not> Sup {}"
    2.38    unfolding Sup_bool_def by auto
    2.39  
    2.40 -lemma top_bool_eq: "top = True"
    2.41 -  by (iprover intro!: order_antisym le_boolI top_greatest)
    2.42 -
    2.43 -lemma bot_bool_eq: "bot = False"
    2.44 -  by (iprover intro!: order_antisym le_boolI bot_least)
    2.45 -
    2.46  
    2.47  subsection {* Fun as lattice *}
    2.48  
    2.49 @@ -556,12 +544,6 @@
    2.50    "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
    2.51    by rule (auto simp add: Sup_fun_def)
    2.52  
    2.53 -lemma top_fun_eq: "top = (\<lambda>x. top)"
    2.54 -  by (iprover intro!: order_antisym le_funI top_greatest)
    2.55 -
    2.56 -lemma bot_fun_eq: "bot = (\<lambda>x. bot)"
    2.57 -  by (iprover intro!: order_antisym le_funI bot_least)
    2.58 -
    2.59  
    2.60  subsection {* Set as lattice *}
    2.61  
     3.1 --- a/src/HOL/Orderings.thy	Fri Oct 24 17:48:36 2008 +0200
     3.2 +++ b/src/HOL/Orderings.thy	Fri Oct 24 17:48:37 2008 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 - (*  Title:      HOL/Orderings.thy
     3.5 +(*  Title:      HOL/Orderings.thy
     3.6      ID:         $Id$
     3.7      Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
     3.8  *)
     3.9 @@ -962,112 +962,6 @@
    3.10    leave out the "(xtrans)" above.
    3.11  *)
    3.12  
    3.13 -subsection {* Order on bool *}
    3.14 -
    3.15 -instantiation bool :: order
    3.16 -begin
    3.17 -
    3.18 -definition
    3.19 -  le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
    3.20 -
    3.21 -definition
    3.22 -  less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
    3.23 -
    3.24 -instance
    3.25 -  by intro_classes (auto simp add: le_bool_def less_bool_def)
    3.26 -
    3.27 -end
    3.28 -
    3.29 -lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
    3.30 -by (simp add: le_bool_def)
    3.31 -
    3.32 -lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
    3.33 -by (simp add: le_bool_def)
    3.34 -
    3.35 -lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
    3.36 -by (simp add: le_bool_def)
    3.37 -
    3.38 -lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
    3.39 -by (simp add: le_bool_def)
    3.40 -
    3.41 -lemma [code]:
    3.42 -  "False \<le> b \<longleftrightarrow> True"
    3.43 -  "True \<le> b \<longleftrightarrow> b"
    3.44 -  "False < b \<longleftrightarrow> b"
    3.45 -  "True < b \<longleftrightarrow> False"
    3.46 -  unfolding le_bool_def less_bool_def by simp_all
    3.47 -
    3.48 -
    3.49 -subsection {* Order on functions *}
    3.50 -
    3.51 -instantiation "fun" :: (type, ord) ord
    3.52 -begin
    3.53 -
    3.54 -definition
    3.55 -  le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
    3.56 -
    3.57 -definition
    3.58 -  less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
    3.59 -
    3.60 -instance ..
    3.61 -
    3.62 -end
    3.63 -
    3.64 -instance "fun" :: (type, order) order
    3.65 -  by default
    3.66 -    (auto simp add: le_fun_def less_fun_def
    3.67 -       intro: order_trans order_antisym intro!: ext)
    3.68 -
    3.69 -lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
    3.70 -  unfolding le_fun_def by simp
    3.71 -
    3.72 -lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
    3.73 -  unfolding le_fun_def by simp
    3.74 -
    3.75 -lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
    3.76 -  unfolding le_fun_def by simp
    3.77 -
    3.78 -text {*
    3.79 -  Handy introduction and elimination rules for @{text "\<le>"}
    3.80 -  on unary and binary predicates
    3.81 -*}
    3.82 -
    3.83 -lemma predicate1I:
    3.84 -  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
    3.85 -  shows "P \<le> Q"
    3.86 -  apply (rule le_funI)
    3.87 -  apply (rule le_boolI)
    3.88 -  apply (rule PQ)
    3.89 -  apply assumption
    3.90 -  done
    3.91 -
    3.92 -lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
    3.93 -  apply (erule le_funE)
    3.94 -  apply (erule le_boolE)
    3.95 -  apply assumption+
    3.96 -  done
    3.97 -
    3.98 -lemma predicate2I [Pure.intro!, intro!]:
    3.99 -  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
   3.100 -  shows "P \<le> Q"
   3.101 -  apply (rule le_funI)+
   3.102 -  apply (rule le_boolI)
   3.103 -  apply (rule PQ)
   3.104 -  apply assumption
   3.105 -  done
   3.106 -
   3.107 -lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   3.108 -  apply (erule le_funE)+
   3.109 -  apply (erule le_boolE)
   3.110 -  apply assumption+
   3.111 -  done
   3.112 -
   3.113 -lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
   3.114 -  by (rule predicate1D)
   3.115 -
   3.116 -lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
   3.117 -  by (rule predicate2D)
   3.118 -
   3.119  
   3.120  subsection {* Monotonicity, least value operator and min/max *}
   3.121  
   3.122 @@ -1123,6 +1017,17 @@
   3.123  done
   3.124  
   3.125  
   3.126 +subsection {* Top and bottom elements *}
   3.127 +
   3.128 +class top = preorder +
   3.129 +  fixes top :: 'a
   3.130 +  assumes top_greatest [simp]: "x \<le> top"
   3.131 +
   3.132 +class bot = preorder +
   3.133 +  fixes bot :: 'a
   3.134 +  assumes bot_least [simp]: "bot \<le> x"
   3.135 +
   3.136 +
   3.137  subsection {* Dense orders *}
   3.138  
   3.139  class dense_linear_order = linorder + 
   3.140 @@ -1189,4 +1094,141 @@
   3.141  
   3.142  end  
   3.143  
   3.144 +
   3.145 +subsection {* Order on bool *}
   3.146 +
   3.147 +instantiation bool :: "{order, top, bot}"
   3.148 +begin
   3.149 +
   3.150 +definition
   3.151 +  le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
   3.152 +
   3.153 +definition
   3.154 +  less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
   3.155 +
   3.156 +definition
   3.157 +  top_bool_eq: "top = True"
   3.158 +
   3.159 +definition
   3.160 +  bot_bool_eq: "bot = False"
   3.161 +
   3.162 +instance proof
   3.163 +qed (auto simp add: le_bool_def less_bool_def top_bool_eq bot_bool_eq)
   3.164 +
   3.165  end
   3.166 +
   3.167 +lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
   3.168 +by (simp add: le_bool_def)
   3.169 +
   3.170 +lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
   3.171 +by (simp add: le_bool_def)
   3.172 +
   3.173 +lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   3.174 +by (simp add: le_bool_def)
   3.175 +
   3.176 +lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
   3.177 +by (simp add: le_bool_def)
   3.178 +
   3.179 +lemma [code]:
   3.180 +  "False \<le> b \<longleftrightarrow> True"
   3.181 +  "True \<le> b \<longleftrightarrow> b"
   3.182 +  "False < b \<longleftrightarrow> b"
   3.183 +  "True < b \<longleftrightarrow> False"
   3.184 +  unfolding le_bool_def less_bool_def by simp_all
   3.185 +
   3.186 +
   3.187 +subsection {* Order on functions *}
   3.188 +
   3.189 +instantiation "fun" :: (type, ord) ord
   3.190 +begin
   3.191 +
   3.192 +definition
   3.193 +  le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
   3.194 +
   3.195 +definition
   3.196 +  less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
   3.197 +
   3.198 +instance ..
   3.199 +
   3.200 +end
   3.201 +
   3.202 +instance "fun" :: (type, preorder) preorder proof
   3.203 +qed (auto simp add: le_fun_def less_fun_def
   3.204 +  intro: order_trans order_antisym intro!: ext)
   3.205 +
   3.206 +instance "fun" :: (type, order) order proof
   3.207 +qed (auto simp add: le_fun_def intro: order_antisym ext)
   3.208 +
   3.209 +instantiation "fun" :: (type, top) top
   3.210 +begin
   3.211 +
   3.212 +definition
   3.213 +  top_fun_eq: "top = (\<lambda>x. top)"
   3.214 +
   3.215 +instance proof
   3.216 +qed (simp add: top_fun_eq le_fun_def)
   3.217 +
   3.218 +end
   3.219 +
   3.220 +instantiation "fun" :: (type, bot) bot
   3.221 +begin
   3.222 +
   3.223 +definition
   3.224 +  bot_fun_eq: "bot = (\<lambda>x. bot)"
   3.225 +
   3.226 +instance proof
   3.227 +qed (simp add: bot_fun_eq le_fun_def)
   3.228 +
   3.229 +end
   3.230 +
   3.231 +lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
   3.232 +  unfolding le_fun_def by simp
   3.233 +
   3.234 +lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
   3.235 +  unfolding le_fun_def by simp
   3.236 +
   3.237 +lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
   3.238 +  unfolding le_fun_def by simp
   3.239 +
   3.240 +text {*
   3.241 +  Handy introduction and elimination rules for @{text "\<le>"}
   3.242 +  on unary and binary predicates
   3.243 +*}
   3.244 +
   3.245 +lemma predicate1I:
   3.246 +  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
   3.247 +  shows "P \<le> Q"
   3.248 +  apply (rule le_funI)
   3.249 +  apply (rule le_boolI)
   3.250 +  apply (rule PQ)
   3.251 +  apply assumption
   3.252 +  done
   3.253 +
   3.254 +lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
   3.255 +  apply (erule le_funE)
   3.256 +  apply (erule le_boolE)
   3.257 +  apply assumption+
   3.258 +  done
   3.259 +
   3.260 +lemma predicate2I [Pure.intro!, intro!]:
   3.261 +  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
   3.262 +  shows "P \<le> Q"
   3.263 +  apply (rule le_funI)+
   3.264 +  apply (rule le_boolI)
   3.265 +  apply (rule PQ)
   3.266 +  apply assumption
   3.267 +  done
   3.268 +
   3.269 +lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   3.270 +  apply (erule le_funE)+
   3.271 +  apply (erule le_boolE)
   3.272 +  apply assumption+
   3.273 +  done
   3.274 +
   3.275 +lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
   3.276 +  by (rule predicate1D)
   3.277 +
   3.278 +lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
   3.279 +  by (rule predicate2D)
   3.280 +
   3.281 +end
     4.1 --- a/src/HOL/SizeChange/Graphs.thy	Fri Oct 24 17:48:36 2008 +0200
     4.2 +++ b/src/HOL/SizeChange/Graphs.thy	Fri Oct 24 17:48:37 2008 +0200
     4.3 @@ -89,6 +89,12 @@
     4.4    graph_less_def [code del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
     4.5  
     4.6  definition
     4.7 +  [code del]: "bot = Graph {}"
     4.8 +
     4.9 +definition
    4.10 +  [code del]: "top = Graph UNIV"
    4.11 +
    4.12 +definition
    4.13    [code del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
    4.14  
    4.15  definition
    4.16 @@ -131,6 +137,10 @@
    4.17  
    4.18    { assume "y \<le> x" "z \<le> x" thus "sup y z \<le> x"
    4.19        unfolding sup_graph_def graph_leq_def graph_plus_def by auto }
    4.20 +
    4.21 +  show "bot \<le> x" unfolding graph_leq_def bot_graph_def by simp
    4.22 +
    4.23 +  show "x \<le> top" unfolding graph_leq_def top_graph_def by simp
    4.24    
    4.25    show "sup x (inf y z) = inf (sup x y) (sup x z)"
    4.26      unfolding inf_graph_def sup_graph_def graph_leq_def graph_plus_def by auto