10 theory Zorn |
10 theory Zorn |
11 imports Order_Relation Main |
11 imports Order_Relation Main |
12 begin |
12 begin |
13 |
13 |
14 (* Define globally? In Set.thy? *) |
14 (* Define globally? In Set.thy? *) |
15 definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^bsub>\<subseteq>\<^esub>") where |
15 definition chain_subset :: "'a set set \<Rightarrow> bool" ("chain\<^bsub>\<subseteq>\<^esub>") |
16 "chain\<^bsub>\<subseteq>\<^esub> C \<equiv> \<forall>A\<in>C.\<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A" |
16 where |
|
17 "chain\<^bsub>\<subseteq>\<^esub> C \<equiv> \<forall>A\<in>C.\<forall>B\<in>C. A \<subseteq> B \<or> B \<subseteq> A" |
17 |
18 |
18 text{* |
19 text{* |
19 The lemma and section numbers refer to an unpublished article |
20 The lemma and section numbers refer to an unpublished article |
20 \cite{Abrial-Laffitte}. |
21 \cite{Abrial-Laffitte}. |
21 *} |
22 *} |
22 |
23 |
23 definition |
24 definition chain :: "'a set set \<Rightarrow> 'a set set set" |
24 chain :: "'a set set => 'a set set set" where |
25 where |
25 "chain S = {F. F \<subseteq> S & chain\<^bsub>\<subseteq>\<^esub> F}" |
26 "chain S = {F. F \<subseteq> S \<and> chain\<^bsub>\<subseteq>\<^esub> F}" |
26 |
27 |
27 definition |
28 definition super :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set set set" |
28 super :: "['a set set,'a set set] => 'a set set set" where |
29 where |
29 "super S c = {d. d \<in> chain S & c \<subset> d}" |
30 "super S c = {d. d \<in> chain S \<and> c \<subset> d}" |
30 |
31 |
31 definition |
32 definition maxchain :: "'a set set \<Rightarrow> 'a set set set" |
32 maxchain :: "'a set set => 'a set set set" where |
33 where |
33 "maxchain S = {c. c \<in> chain S & super S c = {}}" |
34 "maxchain S = {c. c \<in> chain S \<and> super S c = {}}" |
34 |
35 |
35 definition |
36 definition succ :: "'a set set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" |
36 succ :: "['a set set,'a set set] => 'a set set" where |
37 where |
37 "succ S c = |
38 "succ S c = (if c \<notin> chain S \<or> c \<in> maxchain S then c else SOME c'. c' \<in> super S c)" |
38 (if c \<notin> chain S | c \<in> maxchain S |
39 |
39 then c else SOME c'. c' \<in> super S c)" |
40 inductive_set TFin :: "'a set set \<Rightarrow> 'a set set set" |
40 |
41 for S :: "'a set set" |
41 inductive_set |
42 where |
42 TFin :: "'a set set => 'a set set set" |
43 succI: "x \<in> TFin S \<Longrightarrow> succ S x \<in> TFin S" |
43 for S :: "'a set set" |
44 | Pow_UnionI: "Y \<in> Pow (TFin S) \<Longrightarrow> \<Union>Y \<in> TFin S" |
44 where |
|
45 succI: "x \<in> TFin S ==> succ S x \<in> TFin S" |
|
46 | Pow_UnionI: "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S" |
|
47 |
45 |
48 |
46 |
49 subsection{*Mathematical Preamble*} |
47 subsection{*Mathematical Preamble*} |
50 |
48 |
51 lemma Union_lemma0: |
49 lemma Union_lemma0: |