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 +definition super :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set set set"
1.29 +where
1.30 + "super S c = {d. d \<in> chain S \<and> c \<subset> d}"
1.31
1.32 -definition
1.33 - maxchain :: "'a set set => 'a set set set" where
1.34 - "maxchain S = {c. c \<in> chain S & super S c = {}}"
1.35 +definition maxchain :: "'a set set \<Rightarrow> 'a set set set"
1.36 +where
1.37 + "maxchain S = {c. c \<in> chain S \<and> super S c = {}}"
1.38
1.39 -definition
1.40 - succ :: "['a set set,'a set set] => 'a set set" where
1.41 - "succ S c =
1.42 - (if c \<notin> chain S | c \<in> maxchain S
1.43 - then c else SOME c'. c' \<in> super S c)"
1.44 +definition succ :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set set"
1.45 +where
1.46 + "succ S c = (if c \<notin> chain S \<or> c \<in> maxchain S then c else SOME c'. c' \<in> super S c)"
1.47
1.48 -inductive_set
1.49 - TFin :: "'a set set => 'a set set set"
1.50 - for S :: "'a set set"
1.51 - where
1.52 - succI: "x \<in> TFin S ==> succ S x \<in> TFin S"
1.53 - | Pow_UnionI: "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
1.54 +inductive_set TFin :: "'a set set \<Rightarrow> 'a set set set"
1.55 +for S :: "'a set set"
1.56 +where
1.57 + succI: "x \<in> TFin S \<Longrightarrow> succ S x \<in> TFin S"
1.58 +| Pow_UnionI: "Y \<in> Pow (TFin S) \<Longrightarrow> \<Union>Y \<in> TFin S"
1.59
1.60
1.61 subsection{*Mathematical Preamble*}