src/HOL/Library/Zorn.thy
changeset 21404 eb85850d3eb7
parent 19736 d8d0f8f51d69
child 23755 1c4672d130b1
     1.1 --- a/src/HOL/Library/Zorn.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Library/Zorn.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -16,16 +16,19 @@
     1.4  *}
     1.5  
     1.6  definition
     1.7 -  chain     ::  "'a set set => 'a set set set"
     1.8 +  chain     ::  "'a set set => 'a set set set" where
     1.9    "chain S  = {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
    1.10  
    1.11 -  super     ::  "['a set set,'a set set] => 'a set set set"
    1.12 +definition
    1.13 +  super     ::  "['a set set,'a set set] => 'a set set set" where
    1.14    "super S c = {d. d \<in> chain S & c \<subset> d}"
    1.15  
    1.16 -  maxchain  ::  "'a set set => 'a set set set"
    1.17 +definition
    1.18 +  maxchain  ::  "'a set set => 'a set set set" where
    1.19    "maxchain S = {c. c \<in> chain S & super S c = {}}"
    1.20  
    1.21 -  succ      ::  "['a set set,'a set set] => 'a set set"
    1.22 +definition
    1.23 +  succ      ::  "['a set set,'a set set] => 'a set set" where
    1.24    "succ S c =
    1.25      (if c \<notin> chain S | c \<in> maxchain S
    1.26      then c else SOME c'. c' \<in> super S c)"