src/HOL/Library/Zorn.thy
changeset 19736 d8d0f8f51d69
parent 18585 5d379fe2eb74
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Library/Zorn.thy	Sat May 27 17:42:00 2006 +0200
     1.2 +++ b/src/HOL/Library/Zorn.thy	Sat May 27 17:42:02 2006 +0200
     1.3 @@ -15,24 +15,23 @@
     1.4    \cite{Abrial-Laffitte}.
     1.5  *}
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    chain     ::  "'a set set => 'a set set set"
    1.10 -  "chain S  == {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
    1.11 +  "chain S  = {F. F \<subseteq> S & (\<forall>x \<in> F. \<forall>y \<in> F. x \<subseteq> y | y \<subseteq> x)}"
    1.12  
    1.13    super     ::  "['a set set,'a set set] => 'a set set set"
    1.14 -  "super S c == {d. d \<in> chain S & c \<subset> d}"
    1.15 +  "super S c = {d. d \<in> chain S & c \<subset> d}"
    1.16  
    1.17    maxchain  ::  "'a set set => 'a set set set"
    1.18 -  "maxchain S == {c. c \<in> chain S & super S c = {}}"
    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 -  "succ S c ==
    1.23 -    if c \<notin> chain S | c \<in> maxchain S
    1.24 -    then c else SOME c'. c' \<in> super S c"
    1.25 +  "succ S c =
    1.26 +    (if c \<notin> chain S | c \<in> maxchain S
    1.27 +    then c else SOME c'. c' \<in> super S c)"
    1.28  
    1.29  consts
    1.30    TFin :: "'a set set => 'a set set set"
    1.31 -
    1.32  inductive "TFin S"
    1.33    intros
    1.34      succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
    1.35 @@ -64,7 +63,7 @@
    1.36               !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
    1.37               !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
    1.38            ==> P(n)"
    1.39 -  apply (erule TFin.induct)
    1.40 +  apply (induct set: TFin)
    1.41     apply blast+
    1.42    done
    1.43