src/HOL/Library/Extended_Nat.thy
changeset 56777 9c3f0ae99532
parent 54419 0c50894fc0d9
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Mon Apr 28 17:48:59 2014 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Mon Apr 28 17:50:03 2014 +0200
     1.3 @@ -615,19 +615,18 @@
     1.4  begin
     1.5  
     1.6  definition inf_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
     1.7 -  "inf_enat \<equiv> min"
     1.8 +  "inf_enat = min"
     1.9  
    1.10  definition sup_enat :: "enat \<Rightarrow> enat \<Rightarrow> enat" where
    1.11 -  "sup_enat \<equiv> max"
    1.12 +  "sup_enat = max"
    1.13  
    1.14  definition Inf_enat :: "enat set \<Rightarrow> enat" where
    1.15 -  "Inf_enat A \<equiv> if A = {} then \<infinity> else (LEAST x. x \<in> A)"
    1.16 +  "Inf_enat A = (if A = {} then \<infinity> else (LEAST x. x \<in> A))"
    1.17  
    1.18  definition Sup_enat :: "enat set \<Rightarrow> enat" where
    1.19 -  "Sup_enat A \<equiv> if A = {} then 0
    1.20 -    else if finite A then Max A
    1.21 -                     else \<infinity>"
    1.22 -instance proof
    1.23 +  "Sup_enat A = (if A = {} then 0 else if finite A then Max A else \<infinity>)"
    1.24 +instance
    1.25 +proof
    1.26    fix x :: "enat" and A :: "enat set"
    1.27    { assume "x \<in> A" then show "Inf A \<le> x"
    1.28        unfolding Inf_enat_def by (auto intro: Least_le) }