src/HOL/Orderings.thy
changeset 22916 8caf6da610e2
parent 22886 cdff6ef76009
child 22997 d4f3b015b50b
     1.1 --- a/src/HOL/Orderings.thy	Thu May 10 04:06:56 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Thu May 10 10:21:44 2007 +0200
     1.3 @@ -81,6 +81,8 @@
     1.4  notation (input)
     1.5    greater_eq  (infix "\<ge>" 50)
     1.6  
     1.7 +hide const min max
     1.8 +
     1.9  definition
    1.10    min :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.11    "min a b = (if a \<le> b then a else b)"
    1.12 @@ -89,11 +91,11 @@
    1.13    max :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.14    "max a b = (if a \<le> b then b else a)"
    1.15  
    1.16 -lemma min_linorder:
    1.17 +lemma linorder_class_min:
    1.18    "ord.min (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = min"
    1.19    by rule+ (simp add: min_def ord_class.min_def)
    1.20  
    1.21 -lemma max_linorder:
    1.22 +lemma linorder_class_max:
    1.23    "ord.max (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = max"
    1.24    by rule+ (simp add: max_def ord_class.max_def)
    1.25  
    1.26 @@ -193,6 +195,14 @@
    1.27  lemma less_asym': "a \<^loc>< b \<Longrightarrow> b \<^loc>< a \<Longrightarrow> P"
    1.28    by (rule less_asym)
    1.29  
    1.30 +
    1.31 +text {* Reverse order *}
    1.32 +
    1.33 +lemma order_reverse:
    1.34 +  "order_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
    1.35 +  by unfold_locales
    1.36 +    (simp add: less_le, auto intro: antisym order_trans)
    1.37 +
    1.38  end
    1.39  
    1.40  
    1.41 @@ -252,6 +262,15 @@
    1.42  lemma not_leE: "\<not> y \<^loc>\<le> x \<Longrightarrow> x \<^loc>< y"
    1.43    unfolding not_le .
    1.44  
    1.45 +
    1.46 +text {* Reverse order *}
    1.47 +
    1.48 +lemma linorder_reverse:
    1.49 +  "linorder_pred (\<lambda>x y. y \<^loc>\<le> x) (\<lambda>x y. y \<^loc>< x)"
    1.50 +  by unfold_locales
    1.51 +    (simp add: less_le, auto intro: antisym order_trans simp add: linear)
    1.52 +
    1.53 +
    1.54  text {* min/max properties *}
    1.55  
    1.56  lemma min_le_iff_disj:
    1.57 @@ -288,8 +307,7 @@
    1.58  
    1.59  end
    1.60  
    1.61 -
    1.62 -subsection {* Name duplicates *}
    1.63 +subsection {* Name duplicates -- including min/max interpretation *}
    1.64  
    1.65  lemmas order_less_le = less_le
    1.66  lemmas order_eq_refl = order_class.eq_refl
    1.67 @@ -330,6 +348,15 @@
    1.68  lemmas leD = linorder_class.leD
    1.69  lemmas not_leE = linorder_class.not_leE
    1.70  
    1.71 +lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [unfolded linorder_class_min]
    1.72 +lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [unfolded linorder_class_max]
    1.73 +lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [unfolded linorder_class_min]
    1.74 +lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [unfolded linorder_class_max]
    1.75 +lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [unfolded linorder_class_min]
    1.76 +lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [unfolded linorder_class_max]
    1.77 +lemmas split_min = linorder_class.split_min [unfolded linorder_class_min]
    1.78 +lemmas split_max = linorder_class.split_max [unfolded linorder_class_max]
    1.79 +
    1.80  
    1.81  subsection {* Reasoning tools setup *}
    1.82  
    1.83 @@ -346,18 +373,18 @@
    1.84          T <> HOLogic.natT andalso T <> HOLogic.intT
    1.85            andalso T <> HOLogic.realT andalso Sign.of_sort thy (T, sort)
    1.86        end;
    1.87 -    fun dec (Const ("Not", _) $ t) = (case dec t
    1.88 +    fun dec (Const (@{const_name Not}, _) $ t) = (case dec t
    1.89            of NONE => NONE
    1.90             | SOME (t1, rel, t2) => SOME (t1, "~" ^ rel, t2))
    1.91 -      | dec (Const ("op =",  _) $ t1 $ t2) =
    1.92 +      | dec (Const (@{const_name "op ="},  _) $ t1 $ t2) =
    1.93            if of_sort t1
    1.94            then SOME (t1, "=", t2)
    1.95            else NONE
    1.96 -      | dec (Const ("Orderings.less_eq",  _) $ t1 $ t2) =
    1.97 +      | dec (Const (@{const_name less_eq},  _) $ t1 $ t2) =
    1.98            if of_sort t1
    1.99            then SOME (t1, "<=", t2)
   1.100            else NONE
   1.101 -      | dec (Const ("Orderings.less",  _) $ t1 $ t2) =
   1.102 +      | dec (Const (@{const_name less},  _) $ t1 $ t2) =
   1.103            if of_sort t1
   1.104            then SOME (t1, "<", t2)
   1.105            else NONE
   1.106 @@ -417,7 +444,7 @@
   1.107  
   1.108  fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
   1.109    let val prems = prems_of_ss ss;
   1.110 -      val less = Const("Orderings.less",T);
   1.111 +      val less = Const (@{const_name less}, T);
   1.112        val t = HOLogic.mk_Trueprop(le $ s $ r);
   1.113    in case find_first (prp t) prems of
   1.114         NONE =>
   1.115 @@ -432,7 +459,7 @@
   1.116  
   1.117  fun prove_antisym_less sg ss (NotC $ ((less as Const(_,T)) $ r $ s)) =
   1.118    let val prems = prems_of_ss ss;
   1.119 -      val le = Const("Orderings.less_eq",T);
   1.120 +      val le = Const (@{const_name less_eq}, T);
   1.121        val t = HOLogic.mk_Trueprop(le $ r $ s);
   1.122    in case find_first (prp t) prems of
   1.123         NONE =>
   1.124 @@ -521,12 +548,12 @@
   1.125  
   1.126  print_translation {*
   1.127  let
   1.128 -  val All_binder = Syntax.binder_name @{const_syntax "All"};
   1.129 -  val Ex_binder = Syntax.binder_name @{const_syntax "Ex"};
   1.130 +  val All_binder = Syntax.binder_name @{const_syntax All};
   1.131 +  val Ex_binder = Syntax.binder_name @{const_syntax Ex};
   1.132    val impl = @{const_syntax "op -->"};
   1.133    val conj = @{const_syntax "op &"};
   1.134 -  val less = @{const_syntax "less"};
   1.135 -  val less_eq = @{const_syntax "less_eq"};
   1.136 +  val less = @{const_syntax less};
   1.137 +  val less_eq = @{const_syntax less_eq};
   1.138  
   1.139    val trans =
   1.140     [((All_binder, impl, less), ("_All_less", "_All_greater")),
   1.141 @@ -801,7 +828,7 @@
   1.142  instance bool :: order 
   1.143    le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
   1.144    less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
   1.145 -  by default (auto simp add: le_bool_def less_bool_def)
   1.146 +  by intro_classes (auto simp add: le_bool_def less_bool_def)
   1.147  
   1.148  lemma le_boolI: "(P \<Longrightarrow> Q) \<Longrightarrow> P \<le> Q"
   1.149    by (simp add: le_bool_def)
   1.150 @@ -854,15 +881,6 @@
   1.151    apply (auto intro!: order_antisym)
   1.152    done
   1.153  
   1.154 -lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [unfolded min_linorder]
   1.155 -lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [unfolded max_linorder]
   1.156 -lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [unfolded min_linorder]
   1.157 -lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [unfolded max_linorder]
   1.158 -lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [unfolded min_linorder]
   1.159 -lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [unfolded max_linorder]
   1.160 -lemmas split_min = linorder_class.split_min [unfolded min_linorder]
   1.161 -lemmas split_max = linorder_class.split_max [unfolded max_linorder]
   1.162 -
   1.163  lemma min_leastL: "(!!x. least <= x) ==> min least x = least"
   1.164    by (simp add: min_def)
   1.165