# HG changeset patch
# User haftmann
# Date 1224863317 -7200
# Node ID 275122631271d4c185bd094b0c595341dd0f2282
# Parent  48faac3240617b7097080a36a72d7a1f7118a605
new classes "top" and "bot"

diff -r 48faac324061 -r 275122631271 NEWS
--- a/NEWS	Fri Oct 24 17:48:36 2008 +0200
+++ b/NEWS	Fri Oct 24 17:48:37 2008 +0200
@@ -104,10 +104,19 @@
 
 *** HOL ***
 
+* New classes "top" and "bot" with corresponding operations "top" and "bot"
+in theory Orderings;  instantiation of class "complete_lattice" requires
+instantiation of classes "top" and "bot".  INCOMPATIBILITY.
+
+* Changed definition lemma "less_fun_def" in order to provide an instance
+for preorders on functions;  use lemma "less_le" instead.  INCOMPATIBILITY.
+
 * Unified theorem tables for both code code generators.  Thus
 [code func] has disappeared and only [code] remains.  INCOMPATIBILITY.
 
-* Constant "undefined" replaces "arbitrary" in most occurences.
+* Constants "undefined" and "default" replace "arbitrary".  Usually
+"undefined" is the right choice to replace "arbitrary", though logically
+there is no difference.  INCOMPATIBILITY.
 
 * Generic ATP manager for Sledgehammer, based on ML threads instead of
 Posix processes.  Avoids potentially expensive forking of the ML
diff -r 48faac324061 -r 275122631271 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Fri Oct 24 17:48:36 2008 +0200
+++ b/src/HOL/Lattices.thy	Fri Oct 24 17:48:37 2008 +0200
@@ -332,7 +332,7 @@
 
 subsection {* Complete lattices *}
 
-class complete_lattice = lattice +
+class complete_lattice = lattice + top + bot +
   fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
     and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
   assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
@@ -383,19 +383,13 @@
   "\<Squnion>{a, b} = a \<squnion> b"
   by (simp add: Sup_insert_simp)
 
-definition
-  top :: 'a where
+lemma top_def:
   "top = \<Sqinter>{}"
+  by (auto intro: antisym Inf_greatest)
 
-definition
-  bot :: 'a where
+lemma bot_def:
   "bot = \<Squnion>{}"
-
-lemma top_greatest [simp]: "x \<le> top"
-  by (unfold top_def, rule Inf_greatest, simp)
-
-lemma bot_least [simp]: "bot \<le> x"
-  by (unfold bot_def, rule Sup_least, simp)
+  by (auto intro: antisym Sup_least)
 
 definition
   SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
@@ -499,12 +493,6 @@
   "\<not> Sup {}"
   unfolding Sup_bool_def by auto
 
-lemma top_bool_eq: "top = True"
-  by (iprover intro!: order_antisym le_boolI top_greatest)
-
-lemma bot_bool_eq: "bot = False"
-  by (iprover intro!: order_antisym le_boolI bot_least)
-
 
 subsection {* Fun as lattice *}
 
@@ -556,12 +544,6 @@
   "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
   by rule (auto simp add: Sup_fun_def)
 
-lemma top_fun_eq: "top = (\<lambda>x. top)"
-  by (iprover intro!: order_antisym le_funI top_greatest)
-
-lemma bot_fun_eq: "bot = (\<lambda>x. bot)"
-  by (iprover intro!: order_antisym le_funI bot_least)
-
 
 subsection {* Set as lattice *}
 
diff -r 48faac324061 -r 275122631271 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Oct 24 17:48:36 2008 +0200
+++ b/src/HOL/Orderings.thy	Fri Oct 24 17:48:37 2008 +0200
@@ -1,4 +1,4 @@
- (*  Title:      HOL/Orderings.thy
+(*  Title:      HOL/Orderings.thy
     ID:         $Id$
     Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
 *)
@@ -962,112 +962,6 @@
   leave out the "(xtrans)" above.
 *)
 
-subsection {* Order on bool *}
-
-instantiation bool :: order
-begin
-
-definition
-  le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
-
-definition
-  less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> P \<le> Q \<and> P \<noteq> Q"
-
-instance
-  by intro_classes (auto simp add: le_bool_def less_bool_def)
-
-end
-
-lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
-by (simp add: le_bool_def)
-
-lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
-by (simp add: le_bool_def)
-
-lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
-by (simp add: le_bool_def)
-
-lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
-by (simp add: le_bool_def)
-
-lemma [code]:
-  "False \<le> b \<longleftrightarrow> True"
-  "True \<le> b \<longleftrightarrow> b"
-  "False < b \<longleftrightarrow> b"
-  "True < b \<longleftrightarrow> False"
-  unfolding le_bool_def less_bool_def by simp_all
-
-
-subsection {* Order on functions *}
-
-instantiation "fun" :: (type, ord) ord
-begin
-
-definition
-  le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
-
-definition
-  less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> f \<noteq> g"
-
-instance ..
-
-end
-
-instance "fun" :: (type, order) order
-  by default
-    (auto simp add: le_fun_def less_fun_def
-       intro: order_trans order_antisym intro!: ext)
-
-lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
-  unfolding le_fun_def by simp
-
-lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
-  unfolding le_fun_def by simp
-
-lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
-  unfolding le_fun_def by simp
-
-text {*
-  Handy introduction and elimination rules for @{text "\<le>"}
-  on unary and binary predicates
-*}
-
-lemma predicate1I:
-  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
-  shows "P \<le> Q"
-  apply (rule le_funI)
-  apply (rule le_boolI)
-  apply (rule PQ)
-  apply assumption
-  done
-
-lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
-  apply (erule le_funE)
-  apply (erule le_boolE)
-  apply assumption+
-  done
-
-lemma predicate2I [Pure.intro!, intro!]:
-  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
-  shows "P \<le> Q"
-  apply (rule le_funI)+
-  apply (rule le_boolI)
-  apply (rule PQ)
-  apply assumption
-  done
-
-lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
-  apply (erule le_funE)+
-  apply (erule le_boolE)
-  apply assumption+
-  done
-
-lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
-  by (rule predicate1D)
-
-lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
-  by (rule predicate2D)
-
 
 subsection {* Monotonicity, least value operator and min/max *}
 
@@ -1123,6 +1017,17 @@
 done
 
 
+subsection {* Top and bottom elements *}
+
+class top = preorder +
+  fixes top :: 'a
+  assumes top_greatest [simp]: "x \<le> top"
+
+class bot = preorder +
+  fixes bot :: 'a
+  assumes bot_least [simp]: "bot \<le> x"
+
+
 subsection {* Dense orders *}
 
 class dense_linear_order = linorder + 
@@ -1189,4 +1094,141 @@
 
 end  
 
+
+subsection {* Order on bool *}
+
+instantiation bool :: "{order, top, bot}"
+begin
+
+definition
+  le_bool_def [code del]: "P \<le> Q \<longleftrightarrow> P \<longrightarrow> Q"
+
+definition
+  less_bool_def [code del]: "(P\<Colon>bool) < Q \<longleftrightarrow> \<not> P \<and> Q"
+
+definition
+  top_bool_eq: "top = True"
+
+definition
+  bot_bool_eq: "bot = False"
+
+instance proof
+qed (auto simp add: le_bool_def less_bool_def top_bool_eq bot_bool_eq)
+
 end
+
+lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
+by (simp add: le_bool_def)
+
+lemma le_boolI': "P \<longrightarrow> Q \<Longrightarrow> P \<le> Q"
+by (simp add: le_bool_def)
+
+lemma le_boolE: "P \<le> Q \<Longrightarrow> P \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
+by (simp add: le_bool_def)
+
+lemma le_boolD: "P \<le> Q \<Longrightarrow> P \<longrightarrow> Q"
+by (simp add: le_bool_def)
+
+lemma [code]:
+  "False \<le> b \<longleftrightarrow> True"
+  "True \<le> b \<longleftrightarrow> b"
+  "False < b \<longleftrightarrow> b"
+  "True < b \<longleftrightarrow> False"
+  unfolding le_bool_def less_bool_def by simp_all
+
+
+subsection {* Order on functions *}
+
+instantiation "fun" :: (type, ord) ord
+begin
+
+definition
+  le_fun_def [code del]: "f \<le> g \<longleftrightarrow> (\<forall>x. f x \<le> g x)"
+
+definition
+  less_fun_def [code del]: "(f\<Colon>'a \<Rightarrow> 'b) < g \<longleftrightarrow> f \<le> g \<and> \<not> (g \<le> f)"
+
+instance ..
+
+end
+
+instance "fun" :: (type, preorder) preorder proof
+qed (auto simp add: le_fun_def less_fun_def
+  intro: order_trans order_antisym intro!: ext)
+
+instance "fun" :: (type, order) order proof
+qed (auto simp add: le_fun_def intro: order_antisym ext)
+
+instantiation "fun" :: (type, top) top
+begin
+
+definition
+  top_fun_eq: "top = (\<lambda>x. top)"
+
+instance proof
+qed (simp add: top_fun_eq le_fun_def)
+
+end
+
+instantiation "fun" :: (type, bot) bot
+begin
+
+definition
+  bot_fun_eq: "bot = (\<lambda>x. bot)"
+
+instance proof
+qed (simp add: bot_fun_eq le_fun_def)
+
+end
+
+lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
+  unfolding le_fun_def by simp
+
+lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
+  unfolding le_fun_def by simp
+
+lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
+  unfolding le_fun_def by simp
+
+text {*
+  Handy introduction and elimination rules for @{text "\<le>"}
+  on unary and binary predicates
+*}
+
+lemma predicate1I:
+  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
+  shows "P \<le> Q"
+  apply (rule le_funI)
+  apply (rule le_boolI)
+  apply (rule PQ)
+  apply assumption
+  done
+
+lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
+  apply (erule le_funE)
+  apply (erule le_boolE)
+  apply assumption+
+  done
+
+lemma predicate2I [Pure.intro!, intro!]:
+  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
+  shows "P \<le> Q"
+  apply (rule le_funI)+
+  apply (rule le_boolI)
+  apply (rule PQ)
+  apply assumption
+  done
+
+lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
+  apply (erule le_funE)+
+  apply (erule le_boolE)
+  apply assumption+
+  done
+
+lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
+  by (rule predicate1D)
+
+lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
+  by (rule predicate2D)
+
+end
diff -r 48faac324061 -r 275122631271 src/HOL/SizeChange/Graphs.thy
--- a/src/HOL/SizeChange/Graphs.thy	Fri Oct 24 17:48:36 2008 +0200
+++ b/src/HOL/SizeChange/Graphs.thy	Fri Oct 24 17:48:37 2008 +0200
@@ -89,6 +89,12 @@
   graph_less_def [code del]: "G < H \<longleftrightarrow> dest_graph G \<subset> dest_graph H"
 
 definition
+  [code del]: "bot = Graph {}"
+
+definition
+  [code del]: "top = Graph UNIV"
+
+definition
   [code del]: "inf G H = Graph (dest_graph G \<inter> dest_graph H)"
 
 definition
@@ -131,6 +137,10 @@
 
   { assume "y \<le> x" "z \<le> x" thus "sup y z \<le> x"
       unfolding sup_graph_def graph_leq_def graph_plus_def by auto }
+
+  show "bot \<le> x" unfolding graph_leq_def bot_graph_def by simp
+
+  show "x \<le> top" unfolding graph_leq_def top_graph_def by simp
   
   show "sup x (inf y z) = inf (sup x y) (sup x z)"
     unfolding inf_graph_def sup_graph_def graph_leq_def graph_plus_def by auto