author haftmann Fri Apr 20 11:21:36 2007 +0200 (2007-04-20) changeset 22738 4899f06effc6 parent 22737 d87ccbcc2702 child 22739 d12a9d75eee6
shifted min/max to class order
 src/HOL/Orderings.thy file | annotate | diff | revisions
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.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.22  notation
1.23 @@ -68,6 +81,22 @@
1.24  notation (input)
1.25    greater_eq  (infix "\<ge>" 50)
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.44  subsection {* Quasiorders (preorders) *}
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.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.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.70  subsection {* Name duplicates *}
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.87  in
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.106  structure Order_Tac = Order_Tac_Fun (
1.107 @@ -408,11 +417,6 @@
1.108  setup {*
1.109  let
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.116  fun prp t thm = (#prop (rep_thm thm) = t);
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.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.143 @@ -854,20 +858,6 @@
1.144    apply (auto intro!: order_antisym)
1.145    done
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.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.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.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]