src/HOL/Orderings.thy
changeset 23881 851c74f1bb69
parent 23417 42c1a89b45c1
child 23948 261bd4678076
     1.1 --- a/src/HOL/Orderings.thy	Fri Jul 20 14:28:05 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Jul 20 14:28:25 2007 +0200
     1.3 @@ -6,88 +6,12 @@
     1.4  header {* Syntactic and abstract orders *}
     1.5  
     1.6  theory Orderings
     1.7 -imports HOL
     1.8 +imports Set Fun
     1.9  uses
    1.10    (*"~~/src/Provers/quasi.ML"*)
    1.11    "~~/src/Provers/order.ML"
    1.12  begin
    1.13  
    1.14 -subsection {* Order syntax *}
    1.15 -
    1.16 -class ord = type +
    1.17 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
    1.18 -    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubset>" 50)
    1.19 -begin
    1.20 -
    1.21 -notation
    1.22 -  less_eq  ("op \<^loc><=") and
    1.23 -  less_eq  ("(_/ \<^loc><= _)" [51, 51] 50) and
    1.24 -  less  ("op \<^loc><") and
    1.25 -  less  ("(_/ \<^loc>< _)"  [51, 51] 50)
    1.26 -  
    1.27 -notation (xsymbols)
    1.28 -  less_eq  ("op \<^loc>\<le>") and
    1.29 -  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
    1.30 -
    1.31 -notation (HTML output)
    1.32 -  less_eq  ("op \<^loc>\<le>") and
    1.33 -  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
    1.34 -
    1.35 -abbreviation (input)
    1.36 -  greater  (infix "\<^loc>>" 50) where
    1.37 -  "x \<^loc>> y \<equiv> y \<^loc>< x"
    1.38 -
    1.39 -abbreviation (input)
    1.40 -  greater_eq  (infix "\<^loc>>=" 50) where
    1.41 -  "x \<^loc>>= y \<equiv> y \<^loc><= x"
    1.42 -
    1.43 -notation (input)
    1.44 -  greater_eq  (infix "\<^loc>\<ge>" 50)
    1.45 -
    1.46 -text {*
    1.47 -  syntactic min/max -- these definitions reach
    1.48 -  their usual semantics in class linorder ahead.
    1.49 -*}
    1.50 -
    1.51 -definition
    1.52 -  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.53 -  "min a b = (if a \<^loc>\<le> b then a else b)"
    1.54 -
    1.55 -definition
    1.56 -  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.57 -  "max a b = (if a \<^loc>\<le> b then b else a)"
    1.58 -
    1.59 -end
    1.60 -
    1.61 -notation
    1.62 -  less_eq  ("op <=") and
    1.63 -  less_eq  ("(_/ <= _)" [51, 51] 50) and
    1.64 -  less  ("op <") and
    1.65 -  less  ("(_/ < _)"  [51, 51] 50)
    1.66 -  
    1.67 -notation (xsymbols)
    1.68 -  less_eq  ("op \<le>") and
    1.69 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    1.70 -
    1.71 -notation (HTML output)
    1.72 -  less_eq  ("op \<le>") and
    1.73 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    1.74 -
    1.75 -abbreviation (input)
    1.76 -  greater  (infix ">" 50) where
    1.77 -  "x > y \<equiv> y < x"
    1.78 -
    1.79 -abbreviation (input)
    1.80 -  greater_eq  (infix ">=" 50) where
    1.81 -  "x >= y \<equiv> y <= x"
    1.82 -
    1.83 -notation (input)
    1.84 -  greater_eq  (infix "\<ge>" 50)
    1.85 -
    1.86 -lemmas min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
    1.87 -lemmas max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
    1.88 -
    1.89 -
    1.90  subsection {* Partial orders *}
    1.91  
    1.92  class order = ord +
    1.93 @@ -265,7 +189,20 @@
    1.94    (simp add: less_le, auto intro: antisym order_trans simp add: linear)
    1.95  
    1.96  
    1.97 -text {* min/max properties *}
    1.98 +text {* min/max *}
    1.99 +
   1.100 +text {* for historic reasons, definitions are done in context ord *}
   1.101 +
   1.102 +definition (in ord)
   1.103 +  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.104 +  "min a b = (if a \<^loc>\<le> b then a else b)"
   1.105 +
   1.106 +definition (in ord)
   1.107 +  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   1.108 +  "max a b = (if a \<^loc>\<le> b then b else a)"
   1.109 +
   1.110 +lemmas (in -) min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
   1.111 +lemmas (in -) max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
   1.112  
   1.113  lemma min_le_iff_disj:
   1.114    "min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
   1.115 @@ -370,11 +307,11 @@
   1.116            if of_sort t1
   1.117            then SOME (t1, "=", t2)
   1.118            else NONE
   1.119 -      | dec (Const (@{const_name Orderings.less_eq},  _) $ t1 $ t2) =
   1.120 +      | dec (Const (@{const_name HOL.less_eq},  _) $ t1 $ t2) =
   1.121            if of_sort t1
   1.122            then SOME (t1, "<=", t2)
   1.123            else NONE
   1.124 -      | dec (Const (@{const_name Orderings.less},  _) $ t1 $ t2) =
   1.125 +      | dec (Const (@{const_name HOL.less},  _) $ t1 $ t2) =
   1.126            if of_sort t1
   1.127            then SOME (t1, "<", t2)
   1.128            else NONE
   1.129 @@ -840,7 +777,81 @@
   1.130    unfolding le_bool_def less_bool_def by simp_all
   1.131  
   1.132  
   1.133 -subsection {* Monotonicity, syntactic least value operator and min/max *}
   1.134 +subsection {* Order on sets *}
   1.135 +
   1.136 +instance set :: (type) order
   1.137 +  by (intro_classes,
   1.138 +      (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
   1.139 +
   1.140 +lemmas basic_trans_rules [trans] =
   1.141 +  order_trans_rules set_rev_mp set_mp
   1.142 +
   1.143 +
   1.144 +subsection {* Order on functions *}
   1.145 +
   1.146 +instance "fun" :: (type, ord) ord
   1.147 +  le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
   1.148 +  less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
   1.149 +
   1.150 +lemmas [code func del] = le_fun_def less_fun_def
   1.151 +
   1.152 +instance "fun" :: (type, order) order
   1.153 +  by default
   1.154 +    (auto simp add: le_fun_def less_fun_def expand_fun_eq
   1.155 +       intro: order_trans order_antisym)
   1.156 +
   1.157 +lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
   1.158 +  unfolding le_fun_def by simp
   1.159 +
   1.160 +lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
   1.161 +  unfolding le_fun_def by simp
   1.162 +
   1.163 +lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
   1.164 +  unfolding le_fun_def by simp
   1.165 +
   1.166 +text {*
   1.167 +  Handy introduction and elimination rules for @{text "\<le>"}
   1.168 +  on unary and binary predicates
   1.169 +*}
   1.170 +
   1.171 +lemma predicate1I [Pure.intro!, intro!]:
   1.172 +  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
   1.173 +  shows "P \<le> Q"
   1.174 +  apply (rule le_funI)
   1.175 +  apply (rule le_boolI)
   1.176 +  apply (rule PQ)
   1.177 +  apply assumption
   1.178 +  done
   1.179 +
   1.180 +lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
   1.181 +  apply (erule le_funE)
   1.182 +  apply (erule le_boolE)
   1.183 +  apply assumption+
   1.184 +  done
   1.185 +
   1.186 +lemma predicate2I [Pure.intro!, intro!]:
   1.187 +  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
   1.188 +  shows "P \<le> Q"
   1.189 +  apply (rule le_funI)+
   1.190 +  apply (rule le_boolI)
   1.191 +  apply (rule PQ)
   1.192 +  apply assumption
   1.193 +  done
   1.194 +
   1.195 +lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
   1.196 +  apply (erule le_funE)+
   1.197 +  apply (erule le_boolE)
   1.198 +  apply assumption+
   1.199 +  done
   1.200 +
   1.201 +lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
   1.202 +  by (rule predicate1D)
   1.203 +
   1.204 +lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
   1.205 +  by (rule predicate2D)
   1.206 +
   1.207 +
   1.208 +subsection {* Monotonicity, least value operator and min/max *}
   1.209  
   1.210  locale mono =
   1.211    fixes f
   1.212 @@ -849,11 +860,6 @@
   1.213  lemmas monoI [intro?] = mono.intro
   1.214    and monoD [dest?] = mono.mono
   1.215  
   1.216 -constdefs
   1.217 -  Least :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
   1.218 -  "Least P == THE x. P x & (ALL y. P y --> x <= y)"
   1.219 -    -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *}
   1.220 -
   1.221  lemma LeastI2_order:
   1.222    "[| P (x::'a::order);
   1.223        !!y. P y ==> x <= y;
   1.224 @@ -864,6 +870,16 @@
   1.225    apply (blast intro: order_antisym)+
   1.226  done
   1.227  
   1.228 +lemma Least_mono:
   1.229 +  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
   1.230 +    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
   1.231 +    -- {* Courtesy of Stephan Merz *}
   1.232 +  apply clarify
   1.233 +  apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
   1.234 +  apply (rule LeastI2_order)
   1.235 +  apply (auto elim: monoD intro!: order_antisym)
   1.236 +  done
   1.237 +
   1.238  lemma Least_equality:
   1.239    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
   1.240  apply (simp add: Least_def)