- Now imports Code_Setup, rather than Set and Fun, since the theorems
about orderings are already needed in Set
- Moved "Dense orders" section to Set, since it requires set notation.
- The "Order on sets" section is no longer necessary, since it is subsumed by
the order on functions and booleans.
- Moved proofs of Least_mono and Least_equality to Set, since they require
set notation.
- In proof of "instance fun :: (type, order) order", use ext instead of
expand_fun_eq, since the latter is not yet available.
- predicate1I is no longer declared as introduction rule, since it interferes
with subsetI
--- a/src/HOL/Orderings.thy Wed May 07 10:56:37 2008 +0200
+++ b/src/HOL/Orderings.thy Wed May 07 10:56:38 2008 +0200
@@ -6,7 +6,7 @@
header {* Abstract orderings *}
theory Orderings
-imports Set Fun
+imports Code_Setup
uses
"~~/src/Provers/order.ML"
begin
@@ -537,21 +537,6 @@
*}
-subsection {* Dense orders *}
-
-class dense_linear_order = linorder +
- assumes gt_ex: "\<exists>y. x < y"
- and lt_ex: "\<exists>y. y < x"
- and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
- (*see further theory Dense_Linear_Order*)
-begin
-
-lemma interval_empty_iff:
- "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
- by (auto dest: dense)
-
-end
-
subsection {* Name duplicates *}
lemmas order_less_le = less_le
@@ -959,16 +944,6 @@
unfolding le_bool_def less_bool_def by simp_all
-subsection {* Order on sets *}
-
-instance set :: (type) order
- by (intro_classes,
- (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
-
-lemmas basic_trans_rules [trans] =
- order_trans_rules set_rev_mp set_mp
-
-
subsection {* Order on functions *}
instantiation "fun" :: (type, ord) ord
@@ -986,8 +961,8 @@
instance "fun" :: (type, order) order
by default
- (auto simp add: le_fun_def less_fun_def expand_fun_eq
- intro: order_trans order_antisym)
+ (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
@@ -1003,7 +978,7 @@
on unary and binary predicates
*}
-lemma predicate1I [Pure.intro!, intro!]:
+lemma predicate1I:
assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
shows "P \<le> Q"
apply (rule le_funI)
@@ -1087,23 +1062,6 @@
apply (blast intro: order_antisym)+
done
-lemma Least_mono:
- "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
- ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
- -- {* Courtesy of Stephan Merz *}
- apply clarify
- apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
- apply (rule LeastI2_order)
- apply (auto elim: monoD intro!: order_antisym)
- done
-
-lemma Least_equality:
- "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
-apply (simp add: Least_def)
-apply (rule the_equality)
-apply (auto intro!: order_antisym)
-done
-
lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
by (simp add: min_def)