tuned specifications
authorhaftmann
Fri Mar 16 22:26:55 2012 +0100 (2012-03-16)
changeset 469806bc213e90401
parent 46974 7ca3608146d8
child 46981 d54cea5b64e4
tuned specifications
src/HOL/Library/Zorn.thy
     1.1 --- a/src/HOL/Library/Zorn.thy	Fri Mar 16 22:48:38 2012 +0100
     1.2 +++ b/src/HOL/Library/Zorn.thy	Fri Mar 16 22:26:55 2012 +0100
     1.3 @@ -12,38 +12,36 @@
     1.4  begin
     1.5  
     1.6  (* Define globally? In Set.thy? *)
     1.7 -definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^bsub>\<subseteq>\<^esub>") where
     1.8 -"chain\<^bsub>\<subseteq>\<^esub> C \<equiv> \<forall>A\<in>C.\<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
     1.9 +definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^bsub>\<subseteq>\<^esub>")
    1.10 +where
    1.11 +  "chain\<^bsub>\<subseteq>\<^esub> C \<equiv> \<forall>A\<in>C.\<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A"
    1.12  
    1.13  text{*
    1.14    The lemma and section numbers refer to an unpublished article
    1.15    \cite{Abrial-Laffitte}.
    1.16  *}
    1.17  
    1.18 -definition
    1.19 -  chain     ::  "'a set set => 'a set set set" where
    1.20 -  "chain S  = {F. F \<subseteq> S & chain\<^bsub>\<subseteq>\<^esub> F}"
    1.21 +definition chain :: "'a set set \<Rightarrow> 'a set set set"
    1.22 +where
    1.23 +  "chain S = {F. F \<subseteq> S \<and> chain\<^bsub>\<subseteq>\<^esub> F}"
    1.24  
    1.25 -definition
    1.26 -  super     ::  "['a set set,'a set set] => 'a set set set" where
    1.27 -  "super S c = {d. d \<in> chain S & c \<subset> d}"
    1.28 -
    1.29 -definition
    1.30 -  maxchain  ::  "'a set set => 'a set set set" where
    1.31 -  "maxchain S = {c. c \<in> chain S & super S c = {}}"
    1.32 +definition super :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set set set"
    1.33 +where
    1.34 +  "super S c = {d. d \<in> chain S \<and> c \<subset> d}"
    1.35  
    1.36 -definition
    1.37 -  succ      ::  "['a set set,'a set set] => 'a set set" where
    1.38 -  "succ S c =
    1.39 -    (if c \<notin> chain S | c \<in> maxchain S
    1.40 -    then c else SOME c'. c' \<in> super S c)"
    1.41 +definition maxchain  ::  "'a set set \<Rightarrow> 'a set set set"
    1.42 +where
    1.43 +  "maxchain S = {c. c \<in> chain S \<and> super S c = {}}"
    1.44  
    1.45 -inductive_set
    1.46 -  TFin :: "'a set set => 'a set set set"
    1.47 -  for S :: "'a set set"
    1.48 -  where
    1.49 -    succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
    1.50 -  | Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
    1.51 +definition succ :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
    1.52 +where
    1.53 +  "succ S c = (if c \<notin> chain S \<or> c \<in> maxchain S then c else SOME c'. c' \<in> super S c)"
    1.54 +
    1.55 +inductive_set TFin :: "'a set set \<Rightarrow> 'a set set set"
    1.56 +for S :: "'a set set"
    1.57 +where
    1.58 +  succI:      "x \<in> TFin S \<Longrightarrow> succ S x \<in> TFin S"
    1.59 +| Pow_UnionI: "Y \<in> Pow (TFin S) \<Longrightarrow> \<Union>Y \<in> TFin S"
    1.60  
    1.61  
    1.62  subsection{*Mathematical Preamble*}