equal
deleted
inserted
replaced
430 |
430 |
431 lemma range_binary_eq: "range(binary a b) = {a,b}" |
431 lemma range_binary_eq: "range(binary a b) = {a,b}" |
432 by (auto simp add: binary_def) |
432 by (auto simp add: binary_def) |
433 |
433 |
434 lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)" |
434 lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)" |
435 by (simp add: SUP_def range_binary_eq) |
435 by (simp add: range_binary_eq cong del: strong_SUP_cong) |
436 |
436 |
437 lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)" |
437 lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)" |
438 by (simp add: INF_def range_binary_eq) |
438 by (simp add: range_binary_eq cong del: strong_INF_cong) |
439 |
439 |
440 lemma sigma_algebra_iff2: |
440 lemma sigma_algebra_iff2: |
441 "sigma_algebra \<Omega> M \<longleftrightarrow> |
441 "sigma_algebra \<Omega> M \<longleftrightarrow> |
442 M \<subseteq> Pow \<Omega> \<and> |
442 M \<subseteq> Pow \<Omega> \<and> |
443 {} \<in> M \<and> (\<forall>s \<in> M. \<Omega> - s \<in> M) \<and> |
443 {} \<in> M \<and> (\<forall>s \<in> M. \<Omega> - s \<in> M) \<and> |
533 also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)" |
533 also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)" |
534 by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+ |
534 by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+ |
535 finally show ?thesis . |
535 finally show ?thesis . |
536 qed |
536 qed |
537 |
537 |
538 lemma sigma_sets_UNION: "countable B \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets X A) \<Longrightarrow> (\<Union>B) \<in> sigma_sets X A" |
538 lemma sigma_sets_UNION: |
539 using from_nat_into[of B] range_from_nat_into[of B] sigma_sets.Union[of "from_nat_into B" X A] |
539 "countable B \<Longrightarrow> (\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets X A) \<Longrightarrow> (\<Union>B) \<in> sigma_sets X A" |
540 apply (cases "B = {}") |
540 apply (cases "B = {}") |
541 apply (simp add: sigma_sets.Empty) |
541 apply (simp add: sigma_sets.Empty) |
542 apply (simp del: Union_image_eq add: Union_image_eq[symmetric]) |
542 using from_nat_into [of B] range_from_nat_into [of B] sigma_sets.Union [of "from_nat_into B" X A] |
|
543 apply simp |
|
544 apply auto |
|
545 apply (metis Sup_bot_conv(1) Union_empty `\<lbrakk>B \<noteq> {}; countable B\<rbrakk> \<Longrightarrow> range (from_nat_into B) = B`) |
543 done |
546 done |
544 |
547 |
545 lemma (in sigma_algebra) sigma_sets_eq: |
548 lemma (in sigma_algebra) sigma_sets_eq: |
546 "sigma_sets \<Omega> M = M" |
549 "sigma_sets \<Omega> M = M" |
547 proof |
550 proof |
833 assumes "finite A" shows "A \<subseteq> generated_ring \<Longrightarrow> disjoint A \<Longrightarrow> \<Union>A \<in> generated_ring" |
836 assumes "finite A" shows "A \<subseteq> generated_ring \<Longrightarrow> disjoint A \<Longrightarrow> \<Union>A \<in> generated_ring" |
834 using assms by (induct A) (auto simp: disjoint_def intro!: generated_ring_disjoint_Un generated_ring_empty) |
837 using assms by (induct A) (auto simp: disjoint_def intro!: generated_ring_disjoint_Un generated_ring_empty) |
835 |
838 |
836 lemma (in semiring_of_sets) generated_ring_disjoint_UNION: |
839 lemma (in semiring_of_sets) generated_ring_disjoint_UNION: |
837 "finite I \<Longrightarrow> disjoint (A ` I) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> UNION I A \<in> generated_ring" |
840 "finite I \<Longrightarrow> disjoint (A ` I) \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> UNION I A \<in> generated_ring" |
838 unfolding SUP_def by (intro generated_ring_disjoint_Union) auto |
841 by (intro generated_ring_disjoint_Union) auto |
839 |
842 |
840 lemma (in semiring_of_sets) generated_ring_Int: |
843 lemma (in semiring_of_sets) generated_ring_Int: |
841 assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring" |
844 assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring" |
842 shows "a \<inter> b \<in> generated_ring" |
845 shows "a \<inter> b \<in> generated_ring" |
843 proof - |
846 proof - |
871 assumes "finite A" "A \<noteq> {}" shows "A \<subseteq> generated_ring \<Longrightarrow> \<Inter>A \<in> generated_ring" |
874 assumes "finite A" "A \<noteq> {}" shows "A \<subseteq> generated_ring \<Longrightarrow> \<Inter>A \<in> generated_ring" |
872 using assms by (induct A rule: finite_ne_induct) (auto intro: generated_ring_Int) |
875 using assms by (induct A rule: finite_ne_induct) (auto intro: generated_ring_Int) |
873 |
876 |
874 lemma (in semiring_of_sets) generated_ring_INTER: |
877 lemma (in semiring_of_sets) generated_ring_INTER: |
875 "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> INTER I A \<in> generated_ring" |
878 "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> A i \<in> generated_ring) \<Longrightarrow> INTER I A \<in> generated_ring" |
876 unfolding INF_def by (intro generated_ring_Inter) auto |
879 by (intro generated_ring_Inter) auto |
877 |
880 |
878 lemma (in semiring_of_sets) generating_ring: |
881 lemma (in semiring_of_sets) generating_ring: |
879 "ring_of_sets \<Omega> generated_ring" |
882 "ring_of_sets \<Omega> generated_ring" |
880 proof (rule ring_of_setsI) |
883 proof (rule ring_of_setsI) |
881 let ?R = generated_ring |
884 let ?R = generated_ring |
896 also have "\<dots> \<in> ?R" |
899 also have "\<dots> \<in> ?R" |
897 proof (intro generated_ring_INTER generated_ring_disjoint_UNION) |
900 proof (intro generated_ring_INTER generated_ring_disjoint_UNION) |
898 fix a b assume "a \<in> Ca" "b \<in> Cb" |
901 fix a b assume "a \<in> Ca" "b \<in> Cb" |
899 with Ca Cb Diff_cover[of a b] show "a - b \<in> ?R" |
902 with Ca Cb Diff_cover[of a b] show "a - b \<in> ?R" |
900 by (auto simp add: generated_ring_def) |
903 by (auto simp add: generated_ring_def) |
|
904 (metis DiffI Diff_eq_empty_iff empty_iff) |
901 next |
905 next |
902 show "disjoint ((\<lambda>a'. \<Inter>b'\<in>Cb. a' - b')`Ca)" |
906 show "disjoint ((\<lambda>a'. \<Inter>b'\<in>Cb. a' - b')`Ca)" |
903 using Ca by (auto simp add: disjoint_def \<open>Cb \<noteq> {}\<close>) |
907 using Ca by (auto simp add: disjoint_def \<open>Cb \<noteq> {}\<close>) |
904 next |
908 next |
905 show "finite Ca" "finite Cb" "Cb \<noteq> {}" by fact+ |
909 show "finite Ca" "finite Cb" "Cb \<noteq> {}" by fact+ |
933 apply (rule set_eqI) |
937 apply (rule set_eqI) |
934 apply (auto simp add: image_iff) |
938 apply (auto simp add: image_iff) |
935 done |
939 done |
936 |
940 |
937 lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B" |
941 lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B" |
938 by (simp add: SUP_def range_binaryset_eq) |
942 by (simp add: range_binaryset_eq cong del: strong_SUP_cong) |
939 |
943 |
940 subsubsection \<open>Closed CDI\<close> |
944 subsubsection \<open>Closed CDI\<close> |
941 |
945 |
942 definition closed_cdi where |
946 definition closed_cdi where |
943 "closed_cdi \<Omega> M \<longleftrightarrow> |
947 "closed_cdi \<Omega> M \<longleftrightarrow> |