streamlined definitions
authorhaftmann
Fri Jun 20 21:00:21 2008 +0200 (2008-06-20)
changeset 272993447cd2e18e8
parent 27298 a5373b60e66c
child 27300 4cb3101d2bf7
streamlined definitions
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Orderings.thy	Fri Jun 20 21:00:16 2008 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Jun 20 21:00:21 2008 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4  
     1.5  text {* Least value operator *}
     1.6  
     1.7 -definition
     1.8 +definition (in ord)
     1.9    Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where
    1.10    "Least P = (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<le> y))"
    1.11  
    1.12 @@ -186,7 +186,6 @@
    1.13  lemma antisym_conv3: "\<not> y < x \<Longrightarrow> \<not> x < y \<longleftrightarrow> x = y"
    1.14  by (blast intro: antisym dest: not_less [THEN iffD1])
    1.15  
    1.16 -text{*Replacing the old Nat.leI*}
    1.17  lemma leI: "\<not> x < y \<Longrightarrow> y \<le> x"
    1.18  unfolding not_less .
    1.19  
    1.20 @@ -208,14 +207,10 @@
    1.21  
    1.22  text {* min/max *}
    1.23  
    1.24 -text {* for historic reasons, definitions are done in context ord *}
    1.25 -
    1.26 -definition (in ord)
    1.27 -  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.28 +definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.29    [code unfold, code inline del]: "min a b = (if a \<le> b then a else b)"
    1.30  
    1.31 -definition (in ord)
    1.32 -  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.33 +definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.34    [code unfold, code inline del]: "max a b = (if a \<le> b then b else a)"
    1.35  
    1.36  lemma min_le_iff_disj: