src/HOL/Orderings.thy
changeset 23087 ad7244663431
parent 23032 b6cb6a131511
child 23182 01fa88b79ddc
     1.1 --- a/src/HOL/Orderings.thy	Thu May 24 08:37:37 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Thu May 24 08:37:39 2007 +0200
     1.3 @@ -81,26 +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 -
    1.13 -definition
    1.14 -  max :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.15 -  "max a b = (if a \<le> b then b else a)"
    1.16 -
    1.17 -declare min_def[code unfold, code inline del]
    1.18 -        max_def[code unfold, code inline del]
    1.19 -
    1.20 -lemma linorder_class_min:
    1.21 -  "ord.min (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = min"
    1.22 -  by rule+ (simp add: min_def ord_class.min_def)
    1.23 -
    1.24 -lemma linorder_class_max:
    1.25 -  "ord.max (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = max"
    1.26 -  by rule+ (simp add: max_def ord_class.max_def)
    1.27 +lemmas min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
    1.28 +lemmas max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
    1.29  
    1.30  
    1.31  subsection {* Partial orders *}
    1.32 @@ -351,14 +333,14 @@
    1.33  lemmas leD = linorder_class.leD
    1.34  lemmas not_leE = linorder_class.not_leE
    1.35  
    1.36 -lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [unfolded linorder_class_min]
    1.37 -lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [unfolded linorder_class_max]
    1.38 -lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [unfolded linorder_class_min]
    1.39 -lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [unfolded linorder_class_max]
    1.40 -lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [unfolded linorder_class_min]
    1.41 -lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [unfolded linorder_class_max]
    1.42 -lemmas split_min = linorder_class.split_min [unfolded linorder_class_min]
    1.43 -lemmas split_max = linorder_class.split_max [unfolded linorder_class_max]
    1.44 +lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [folded ord_class.min]
    1.45 +lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [folded ord_class.max]
    1.46 +lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [folded ord_class.min]
    1.47 +lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [folded ord_class.max]
    1.48 +lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [folded ord_class.min]
    1.49 +lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [folded ord_class.max]
    1.50 +lemmas split_min = linorder_class.split_min [folded ord_class.min]
    1.51 +lemmas split_max = linorder_class.split_max [folded ord_class.max]
    1.52  
    1.53  
    1.54  subsection {* Reasoning tools setup *}