shifted min/max to class order
authorhaftmann
Fri Apr 20 11:21:36 2007 +0200 (2007-04-20)
changeset 227384899f06effc6
parent 22737 d87ccbcc2702
child 22739 d12a9d75eee6
shifted min/max to class order
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Orderings.thy	Fri Apr 20 11:21:35 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Apr 20 11:21:36 2007 +0200
     1.3 @@ -41,6 +41,19 @@
     1.4  notation (input)
     1.5    greater_eq  (infix "\<^loc>\<ge>" 50)
     1.6  
     1.7 +text {*
     1.8 +  syntactic min/max -- these definitions reach
     1.9 +  their usual semantics in class linorder ahead.
    1.10 +*}
    1.11 +
    1.12 +definition
    1.13 +  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.14 +  "min a b = (if a \<sqsubseteq> b then a else b)"
    1.15 +
    1.16 +definition
    1.17 +  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.18 +  "max a b = (if a \<sqsubseteq> b then b else a)"
    1.19 +
    1.20  end
    1.21  
    1.22  notation
    1.23 @@ -68,6 +81,22 @@
    1.24  notation (input)
    1.25    greater_eq  (infix "\<ge>" 50)
    1.26  
    1.27 +definition
    1.28 +  min :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.29 +  "min a b = (if a \<le> b then a else b)"
    1.30 +
    1.31 +definition
    1.32 +  max :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.33 +  "max a b = (if a \<le> b then b else a)"
    1.34 +
    1.35 +lemma min_linorder:
    1.36 +  "ord.min (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = min"
    1.37 +  by rule+ (simp add: min_def ord_class.min_def)
    1.38 +
    1.39 +lemma max_linorder:
    1.40 +  "ord.max (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = max"
    1.41 +  by rule+ (simp add: max_def ord_class.max_def)
    1.42 +
    1.43  
    1.44  subsection {* Quasiorders (preorders) *}
    1.45  
    1.46 @@ -228,20 +257,7 @@
    1.47  lemma not_leE: "\<not> y \<sqsubseteq> x \<Longrightarrow> x \<sqsubset> y"
    1.48    unfolding not_le .
    1.49  
    1.50 -text {* min/max *}
    1.51 -
    1.52 -definition
    1.53 -  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.54 -  "min a b = (if a \<sqsubseteq> b then a else b)"
    1.55 -
    1.56 -definition
    1.57 -  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.58 -  "max a b = (if a \<sqsubseteq> b then b else a)"
    1.59 -
    1.60 -end
    1.61 -
    1.62 -context linorder
    1.63 -begin
    1.64 +text {* min/max properties *}
    1.65  
    1.66  lemma min_le_iff_disj:
    1.67    "min x y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<or> y \<sqsubseteq> z"
    1.68 @@ -280,8 +296,6 @@
    1.69  
    1.70  subsection {* Name duplicates *}
    1.71  
    1.72 -(*lemmas order_refl [iff] = preorder_class.order_refl
    1.73 -lemmas order_trans = preorder_class.order_trans*)
    1.74  lemmas order_less_le = less_le
    1.75  lemmas order_eq_refl = preorder_class.eq_refl
    1.76  lemmas order_less_irrefl = preorder_class.less_irrefl
    1.77 @@ -310,7 +324,6 @@
    1.78  lemmas linorder_less_linear = linorder_class.less_linear
    1.79  lemmas linorder_le_less_linear = linorder_class.le_less_linear
    1.80  lemmas linorder_le_cases = linorder_class.le_cases
    1.81 -(*lemmas linorder_cases = linorder_class.linorder_cases*)
    1.82  lemmas linorder_not_less = linorder_class.not_less
    1.83  lemmas linorder_not_le = linorder_class.not_le
    1.84  lemmas linorder_neq_iff = linorder_class.neq_iff
    1.85 @@ -358,10 +371,6 @@
    1.86  
    1.87  in
    1.88  
    1.89 -(* The setting up of Quasi_Tac serves as a demo.  Since there is no
    1.90 -   class for quasi orders, the tactics Quasi_Tac.trans_tac and
    1.91 -   Quasi_Tac.quasi_tac are not of much use. *)
    1.92 -
    1.93  structure Quasi_Tac = Quasi_Tac_Fun (
    1.94  struct
    1.95    val le_trans = thm "order_trans";
    1.96 @@ -373,8 +382,8 @@
    1.97    val le_neq_trans = thm "order_le_neq_trans";
    1.98    val neq_le_trans = thm "order_neq_le_trans";
    1.99    val less_imp_neq = thm "less_imp_neq";
   1.100 -  val decomp_trans = decomp_gen ["Orderings.order"];
   1.101 -  val decomp_quasi = decomp_gen ["Orderings.order"];
   1.102 +  val decomp_trans = decomp_gen ["Orderings.preorder"];
   1.103 +  val decomp_quasi = decomp_gen ["Orderings.preorder"];
   1.104  end);
   1.105  
   1.106  structure Order_Tac = Order_Tac_Fun (
   1.107 @@ -408,11 +417,6 @@
   1.108  setup {*
   1.109  let
   1.110  
   1.111 -val order_antisym_conv = thm "order_antisym_conv"
   1.112 -val linorder_antisym_conv1 = thm "linorder_antisym_conv1"
   1.113 -val linorder_antisym_conv2 = thm "linorder_antisym_conv2"
   1.114 -val linorder_antisym_conv3 = thm "linorder_antisym_conv3"
   1.115 -
   1.116  fun prp t thm = (#prop (rep_thm thm) = t);
   1.117  
   1.118  fun prove_antisym_le sg ss ((le as Const(_,T)) $ r $ s) =
   1.119 @@ -424,9 +428,9 @@
   1.120           let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s))
   1.121           in case find_first (prp t) prems of
   1.122                NONE => NONE
   1.123 -            | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv1))
   1.124 +            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_antisym_conv1}))
   1.125           end
   1.126 -     | SOME thm => SOME(mk_meta_eq(thm RS order_antisym_conv))
   1.127 +     | SOME thm => SOME(mk_meta_eq(thm RS @{thm order_antisym_conv}))
   1.128    end
   1.129    handle THM _ => NONE;
   1.130  
   1.131 @@ -439,9 +443,9 @@
   1.132           let val t = HOLogic.mk_Trueprop(NotC $ (less $ s $ r))
   1.133           in case find_first (prp t) prems of
   1.134                NONE => NONE
   1.135 -            | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv3))
   1.136 +            | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_antisym_conv3}))
   1.137           end
   1.138 -     | SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv2))
   1.139 +     | SOME thm => SOME(mk_meta_eq(thm RS @{thm linorder_antisym_conv2}))
   1.140    end
   1.141    handle THM _ => NONE;
   1.142  
   1.143 @@ -854,20 +858,6 @@
   1.144    apply (auto intro!: order_antisym)
   1.145    done
   1.146  
   1.147 -constdefs
   1.148 -  min :: "['a::ord, 'a] => 'a"
   1.149 -  "min a b == (if a <= b then a else b)"
   1.150 -  max :: "['a::ord, 'a] => 'a"
   1.151 -  "max a b == (if a <= b then b else a)"
   1.152 -
   1.153 -lemma min_linorder:
   1.154 -  "linorder.min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = min"
   1.155 -  by rule+ (simp add: min_def linorder_class.min_def)
   1.156 -
   1.157 -lemma max_linorder:
   1.158 -  "linorder.max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = max"
   1.159 -  by rule+ (simp add: max_def linorder_class.max_def)
   1.160 -
   1.161  lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [unfolded min_linorder]
   1.162  lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [unfolded max_linorder]
   1.163  lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [unfolded min_linorder]