8 |
8 |
9 definition prod_sets where |
9 definition prod_sets where |
10 "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}" |
10 "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}" |
11 |
11 |
12 lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B" |
12 lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B" |
13 by (auto simp add: prod_sets_def) |
13 by (auto simp add: prod_sets_def) |
|
14 |
|
15 lemma sigma_prod_sets_finite: |
|
16 assumes "finite A" and "finite B" |
|
17 shows "sets (sigma (A \<times> B) (prod_sets (Pow A) (Pow B))) = Pow (A \<times> B)" |
|
18 proof (simp add: sigma_def, safe) |
|
19 have fin: "finite (A \<times> B)" using assms by (rule finite_cartesian_product) |
|
20 |
|
21 fix x assume subset: "x \<subseteq> A \<times> B" |
|
22 hence "finite x" using fin by (rule finite_subset) |
|
23 from this subset show "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))" |
|
24 (is "x \<in> sigma_sets ?prod ?sets") |
|
25 proof (induct x) |
|
26 case empty show ?case by (rule sigma_sets.Empty) |
|
27 next |
|
28 case (insert a x) |
|
29 hence "{a} \<in> sigma_sets ?prod ?sets" by (auto simp: prod_sets_def intro!: sigma_sets.Basic) |
|
30 moreover have "x \<in> sigma_sets ?prod ?sets" using insert by auto |
|
31 ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un) |
|
32 qed |
|
33 next |
|
34 fix x a b |
|
35 assume "x \<in> sigma_sets (A\<times>B) (prod_sets (Pow A) (Pow B))" and "(a, b) \<in> x" |
|
36 from sigma_sets_into_sp[OF _ this(1)] this(2) |
|
37 show "a \<in> A" and "b \<in> B" |
|
38 by (auto simp: prod_sets_def) |
|
39 qed |
|
40 |
14 |
41 |
15 definition |
42 definition |
16 closed_cdi where |
43 closed_cdi where |
17 "closed_cdi M \<longleftrightarrow> |
44 "closed_cdi M \<longleftrightarrow> |
18 sets M \<subseteq> Pow (space M) & |
45 sets M \<subseteq> Pow (space M) & |
24 |
51 |
25 inductive_set |
52 inductive_set |
26 smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set" |
53 smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set" |
27 for M |
54 for M |
28 where |
55 where |
29 Basic [intro]: |
56 Basic [intro]: |
30 "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M" |
57 "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M" |
31 | Compl [intro]: |
58 | Compl [intro]: |
32 "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M" |
59 "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M" |
33 | Inc: |
60 | Inc: |
34 "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n)) |
61 "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n)) |