46 |
46 |
47 lemma Sigma_triv: "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a" |
47 lemma Sigma_triv: "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a" |
48 by (metis SigmaD1 SigmaD2) |
48 by (metis SigmaD1 SigmaD2) |
49 |
49 |
50 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b" |
50 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b" |
51 by (metis (full_types, lam_lifting) CollectD SigmaD1 SigmaD2) |
51 by (metis (full_types, lifting) CollectD SigmaD1 SigmaD2) |
52 |
52 |
53 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b" |
53 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b" |
54 proof - |
54 proof - |
55 assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})" |
55 assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})" |
56 hence F1: "a \<in> A" by (metis mem_Sigma_iff) |
56 hence F1: "a \<in> A" by (metis mem_Sigma_iff) |
108 |
108 |
109 lemma |
109 lemma |
110 "(cl, f) \<in> CLF \<Longrightarrow> |
110 "(cl, f) \<in> CLF \<Longrightarrow> |
111 CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow> |
111 CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow> |
112 f \<in> pset cl \<inter> cl" |
112 f \<in> pset cl \<inter> cl" |
113 by (metis (lam_lifting) CollectD Sigma_triv subsetD) |
113 by (metis (lifting) CollectD Sigma_triv subsetD) |
114 |
114 |
115 lemma |
115 lemma |
116 "(cl, f) \<in> CLF \<Longrightarrow> |
116 "(cl, f) \<in> CLF \<Longrightarrow> |
117 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow> |
117 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow> |
118 f \<in> pset cl \<inter> cl" |
118 f \<in> pset cl \<inter> cl" |
119 by (metis (lam_lifting) CollectD Sigma_triv) |
119 by (metis (lifting) CollectD Sigma_triv) |
120 |
120 |
121 lemma |
121 lemma |
122 "(cl, f) \<in> CLF \<Longrightarrow> |
122 "(cl, f) \<in> CLF \<Longrightarrow> |
123 CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) \<Longrightarrow> |
123 CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) \<Longrightarrow> |
124 f \<in> pset cl \<rightarrow> pset cl" |
124 f \<in> pset cl \<rightarrow> pset cl" |
125 by (metis (lam_lifting) CollectD Sigma_triv subsetD) |
125 by (metis (lifting) CollectD Sigma_triv subsetD) |
126 |
126 |
127 lemma |
127 lemma |
128 "(cl, f) \<in> CLF \<Longrightarrow> |
128 "(cl, f) \<in> CLF \<Longrightarrow> |
129 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow> |
129 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow> |
130 f \<in> pset cl \<rightarrow> pset cl" |
130 f \<in> pset cl \<rightarrow> pset cl" |
131 by (metis (lam_lifting) CollectD Sigma_triv) |
131 by (metis (lifting) CollectD Sigma_triv) |
132 |
132 |
133 lemma |
133 lemma |
134 "(cl, f) \<in> CLF \<Longrightarrow> |
134 "(cl, f) \<in> CLF \<Longrightarrow> |
135 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow> |
135 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow> |
136 (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" |
136 (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" |
155 "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow> |
155 "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow> |
156 (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)" |
156 (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)" |
157 by (metis mem_Collect_eq imageI set_rev_mp) |
157 by (metis mem_Collect_eq imageI set_rev_mp) |
158 |
158 |
159 lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)" |
159 lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)" |
160 by (metis (lam_lifting) imageE) |
160 by (metis (lifting) imageE) |
161 |
161 |
162 lemma image_TimesA: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)" |
162 lemma image_TimesA: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)" |
163 by (metis map_pair_def map_pair_surj_on) |
163 by (metis map_pair_def map_pair_surj_on) |
164 |
164 |
165 lemma image_TimesB: |
165 lemma image_TimesB: |