22 |
22 |
23 lemma comp_single_set_bd: |
23 lemma comp_single_set_bd: |
24 assumes fbd_Card_order: "Card_order fbd" and |
24 assumes fbd_Card_order: "Card_order fbd" and |
25 fset_bd: "\<And>x. |fset x| \<le>o fbd" and |
25 fset_bd: "\<And>x. |fset x| \<le>o fbd" and |
26 gset_bd: "\<And>x. |gset x| \<le>o gbd" |
26 gset_bd: "\<And>x. |gset x| \<le>o gbd" |
27 shows "|\<Union>fset ` gset x| \<le>o gbd *c fbd" |
27 shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd" |
28 apply (subst sym[OF SUP_def]) |
28 apply (subst sym[OF SUP_def]) |
29 apply (rule ordLeq_transitive) |
29 apply (rule ordLeq_transitive) |
30 apply (rule card_of_UNION_Sigma) |
30 apply (rule card_of_UNION_Sigma) |
31 apply (subst SIGMA_CSUM) |
31 apply (subst SIGMA_CSUM) |
32 apply (rule ordLeq_transitive) |
32 apply (rule ordLeq_transitive) |
40 apply (rule ordIso_imp_ordLeq) |
40 apply (rule ordIso_imp_ordLeq) |
41 apply (rule ordIso_refl) |
41 apply (rule ordIso_refl) |
42 apply (rule Card_order_cprod) |
42 apply (rule Card_order_cprod) |
43 done |
43 done |
44 |
44 |
45 lemma Union_image_insert: "\<Union>f ` insert a B = f a \<union> \<Union>f ` B" |
45 lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)" |
46 by simp |
46 by simp |
47 |
47 |
48 lemma Union_image_empty: "A \<union> \<Union>f ` {} = A" |
48 lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A" |
49 by simp |
49 by simp |
50 |
50 |
51 lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F" |
51 lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F" |
52 by (rule ext) (auto simp add: collect_def) |
52 by (rule ext) (auto simp add: collect_def) |
53 |
53 |
54 lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})" |
54 lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})" |
55 by blast |
55 by blast |
56 |
56 |
57 lemma UN_image_subset: "\<Union>f ` g x \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})" |
57 lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})" |
58 by blast |
58 by blast |
59 |
59 |
60 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>(\<lambda>f. f x) ` X| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd" |
60 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd" |
61 by (unfold o_apply collect_def SUP_def) |
61 by (unfold o_apply collect_def SUP_def) |
62 |
62 |
63 lemma wpull_cong: |
63 lemma wpull_cong: |
64 "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2" |
64 "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2" |
65 by simp |
65 by simp |