--- 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
--- 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 *}
--- 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
--- 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