- Now imports Code_Setup, rather than Set and Fun, since the theorems
authorberghofe
Wed May 07 10:56:38 2008 +0200 (2008-05-07)
changeset 26796c554b77061e5
parent 26795 a27607030a1c
child 26797 a6cb51c314f2
- 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
src/HOL/Orderings.thy
     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"
    1.87 -apply (simp add: Least_def)
    1.88 -apply (rule the_equality)
    1.89 -apply (auto intro!: order_antisym)
    1.90 -done
    1.91 -
    1.92  lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
    1.93  by (simp add: min_def)
    1.94