author berghofe Wed May 07 10:56:38 2008 +0200 (2008-05-07) changeset 26796 c554b77061e5 parent 26795 a27607030a1c child 26797 a6cb51c314f2
- Now imports Code_Setup, rather than Set and Fun, since the theorems
- 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
 src/HOL/Orderings.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Orderings.thy	Wed May 07 10:56:37 2008 +0200
1.2 +++ b/src/HOL/Orderings.thy	Wed May 07 10:56:38 2008 +0200
1.3 @@ -6,7 +6,7 @@
1.4  header {* Abstract orderings *}
1.5
1.6  theory Orderings
1.7 -imports Set Fun
1.8 +imports Code_Setup
1.9  uses
1.10    "~~/src/Provers/order.ML"
1.11  begin
1.12 @@ -537,21 +537,6 @@
1.13  *}
1.14
1.15
1.16 -subsection {* Dense orders *}
1.17 -
1.18 -class dense_linear_order = linorder +
1.19 -  assumes gt_ex: "\<exists>y. x < y"
1.20 -  and lt_ex: "\<exists>y. y < x"
1.21 -  and dense: "x < y \<Longrightarrow> (\<exists>z. x < z \<and> z < y)"
1.22 -  (*see further theory Dense_Linear_Order*)
1.23 -begin
1.24 -
1.25 -lemma interval_empty_iff:
1.26 -  "{y. x < y \<and> y < z} = {} \<longleftrightarrow> \<not> x < z"
1.27 -  by (auto dest: dense)
1.28 -
1.29 -end
1.30 -
1.31  subsection {* Name duplicates *}
1.32
1.33  lemmas order_less_le = less_le
1.34 @@ -959,16 +944,6 @@
1.35    unfolding le_bool_def less_bool_def by simp_all
1.36
1.37
1.38 -subsection {* Order on sets *}
1.39 -
1.40 -instance set :: (type) order
1.41 -  by (intro_classes,
1.42 -      (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
1.43 -
1.44 -lemmas basic_trans_rules [trans] =
1.45 -  order_trans_rules set_rev_mp set_mp
1.46 -
1.47 -
1.48  subsection {* Order on functions *}
1.49
1.50  instantiation "fun" :: (type, ord) ord
1.51 @@ -986,8 +961,8 @@
1.52
1.53  instance "fun" :: (type, order) order
1.54    by default
1.55 -    (auto simp add: le_fun_def less_fun_def expand_fun_eq
1.56 -       intro: order_trans order_antisym)
1.57 +    (auto simp add: le_fun_def less_fun_def
1.58 +       intro: order_trans order_antisym intro!: ext)
1.59
1.60  lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
1.61    unfolding le_fun_def by simp
1.62 @@ -1003,7 +978,7 @@
1.63    on unary and binary predicates
1.64  *}
1.65
1.66 -lemma predicate1I [Pure.intro!, intro!]:
1.67 +lemma predicate1I:
1.68    assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
1.69    shows "P \<le> Q"
1.70    apply (rule le_funI)
1.71 @@ -1087,23 +1062,6 @@
1.72    apply (blast intro: order_antisym)+
1.73  done
1.74
1.75 -lemma Least_mono:
1.76 -  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
1.77 -    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
1.78 -    -- {* Courtesy of Stephan Merz *}
1.79 -  apply clarify
1.80 -  apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
1.81 -  apply (rule LeastI2_order)
1.82 -  apply (auto elim: monoD intro!: order_antisym)
1.83 -  done
1.84 -
1.85 -lemma Least_equality:
1.86 -  "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"