29 declare [[ sledgehammer_problem_prefix = "Abstraction__Collect_triv" ]] |
28 declare [[ sledgehammer_problem_prefix = "Abstraction__Collect_triv" ]] |
30 lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a" |
29 lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a" |
31 proof - |
30 proof - |
32 assume "a \<in> {x. P x}" |
31 assume "a \<in> {x. P x}" |
33 hence "a \<in> P" by (metis Collect_def) |
32 hence "a \<in> P" by (metis Collect_def) |
34 hence "P a" by (metis mem_def) |
33 thus "P a" by (metis mem_def) |
35 thus "P a" by metis |
|
36 qed |
34 qed |
37 |
35 |
38 lemma Collect_triv: "a \<in> {x. P x} ==> P a" |
36 lemma Collect_triv: "a \<in> {x. P x} ==> P a" |
39 by (metis mem_Collect_eq) |
37 by (metis mem_Collect_eq) |
40 |
38 |
41 |
|
42 declare [[ sledgehammer_problem_prefix = "Abstraction__Collect_mp" ]] |
39 declare [[ sledgehammer_problem_prefix = "Abstraction__Collect_mp" ]] |
43 lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}" |
40 lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}" |
44 by (metis Collect_imp_eq ComplD UnE) |
41 by (metis Collect_imp_eq ComplD UnE) |
45 |
42 |
46 declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_triv" ]] |
43 declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_triv" ]] |
47 lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a" |
44 lemma "(a, b) \<in> Sigma A B ==> a \<in> A & b \<in> B a" |
48 proof - |
45 proof - |
49 assume A1: "(a, b) \<in> Sigma A B" |
46 assume A1: "(a, b) \<in> Sigma A B" |
50 hence F1: "b \<in> B a" by (metis mem_Sigma_iff) |
47 hence F1: "b \<in> B a" by (metis mem_Sigma_iff) |
51 have F2: "a \<in> A" by (metis A1 mem_Sigma_iff) |
48 have F2: "a \<in> A" by (metis A1 mem_Sigma_iff) |
52 have "b \<in> B a" by (metis F1) |
49 have "b \<in> B a" by (metis F1) |
106 qed |
106 qed |
107 |
107 |
108 declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Int" ]] |
108 declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Int" ]] |
109 lemma |
109 lemma |
110 "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
110 "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
111 f \<in> pset cl \<inter> cl" |
111 f \<in> pset cl \<inter> cl" |
|
112 by (metis (no_types) Collect_conj_eq Int_def Sigma_triv inf_idem) |
|
113 |
|
114 lemma |
|
115 "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
|
116 f \<in> pset cl \<inter> cl" |
112 proof - |
117 proof - |
113 assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})" |
118 assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})" |
114 have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def) |
119 have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def) |
115 have "f \<in> {R. R \<in> pset cl \<inter> cl}" using A1 by simp |
120 have "f \<in> {R. R \<in> pset cl \<inter> cl}" using A1 by simp |
116 hence "f \<in> Id_on cl `` pset cl" by (metis F1 Int_commute Image_Id_on Collect_def) |
121 hence "f \<in> Id_on cl `` pset cl" by (metis F1 Int_commute Image_Id_on Collect_def) |
117 hence "f \<in> Id_on cl `` pset cl" by metis |
122 hence "f \<in> Id_on cl `` pset cl" by metis |
118 hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on) |
123 hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on) |
119 thus "f \<in> pset cl \<inter> cl" by (metis Int_commute) |
124 thus "f \<in> pset cl \<inter> cl" by (metis Int_commute) |
120 qed |
125 qed |
121 |
126 |
122 |
|
123 declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Pi_mono" ]] |
127 declare [[ sledgehammer_problem_prefix = "Abstraction__Sigma_Collect_Pi_mono" ]] |
124 lemma |
128 lemma |
125 "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==> |
129 "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==> |
126 (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" |
130 (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" |
127 by auto |
131 by auto |
130 lemma "(cl,f) \<in> CLF ==> |
134 lemma "(cl,f) \<in> CLF ==> |
131 CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
135 CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
132 f \<in> pset cl \<inter> cl" |
136 f \<in> pset cl \<inter> cl" |
133 by auto |
137 by auto |
134 |
138 |
135 |
|
136 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Int" ]] |
139 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Int" ]] |
137 lemma "(cl,f) \<in> CLF ==> |
140 lemma "(cl,f) \<in> CLF ==> |
138 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
141 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
139 f \<in> pset cl \<inter> cl" |
142 f \<in> pset cl \<inter> cl" |
140 by auto |
143 by auto |
141 |
144 |
142 |
|
143 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_subset_Collect_Pi" ]] |
145 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_subset_Collect_Pi" ]] |
144 lemma |
146 lemma |
145 "(cl,f) \<in> CLF ==> |
147 "(cl,f) \<in> CLF ==> |
146 CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> |
148 CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> |
147 f \<in> pset cl \<rightarrow> pset cl" |
149 f \<in> pset cl \<rightarrow> pset cl" |
148 by fast |
150 by fast |
149 |
151 |
150 |
|
151 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi" ]] |
152 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi" ]] |
152 lemma |
153 lemma |
153 "(cl,f) \<in> CLF ==> |
154 "(cl,f) \<in> CLF ==> |
154 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> |
155 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> |
155 f \<in> pset cl \<rightarrow> pset cl" |
156 f \<in> pset cl \<rightarrow> pset cl" |
156 by auto |
157 by auto |
157 |
158 |
158 |
|
159 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi_mono" ]] |
159 declare [[ sledgehammer_problem_prefix = "Abstraction__CLF_eq_Collect_Pi_mono" ]] |
160 lemma |
160 lemma |
161 "(cl,f) \<in> CLF ==> |
161 "(cl,f) \<in> CLF ==> |
162 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==> |
162 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==> |
163 (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" |
163 (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" |
164 by auto |
164 by auto |
165 |
165 |
166 declare [[ sledgehammer_problem_prefix = "Abstraction__map_eq_zipA" ]] |
166 declare [[ sledgehammer_problem_prefix = "Abstraction__map_eq_zipA" ]] |
167 lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)" |
167 lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)" |
168 apply (induct xs) |
168 apply (induct xs) |
169 apply (metis map_is_Nil_conv zip.simps(1)) |
169 apply (metis map.simps(1) zip_Nil) |
170 by auto |
170 by (metis (lam_lifting, no_types) map.simps(2) zip_Cons_Cons) |
171 |
171 |
172 declare [[ sledgehammer_problem_prefix = "Abstraction__map_eq_zipB" ]] |
172 declare [[ sledgehammer_problem_prefix = "Abstraction__map_eq_zipB" ]] |
173 lemma "map (%w. (w -> w, w \<times> w)) xs = |
173 lemma "map (%w. (w -> w, w \<times> w)) xs = |
174 zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)" |
174 zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)" |
175 apply (induct xs) |
175 apply (induct xs) |
176 apply (metis Nil_is_map_conv zip_Nil) |
176 apply (metis map.simps(1) zip_Nil) |
177 by auto |
177 by auto |
178 |
178 |
179 declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenA" ]] |
179 declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenA" ]] |
180 lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)" |
180 lemma "(%x. Suc (f x)) ` {x. even x} <= A ==> \<forall>x. even x --> Suc (f x) \<in> A" |
181 by (metis Collect_def image_subset_iff mem_def) |
181 by (metis Collect_def image_eqI mem_def subsetD) |
182 |
182 |
183 declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenB" ]] |
183 declare [[ sledgehammer_problem_prefix = "Abstraction__image_evenB" ]] |
184 lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A |
184 lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A |
185 ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)" |
185 ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)" |
186 by (metis Collect_def imageI image_image image_subset_iff mem_def) |
186 by (metis Collect_def imageI mem_def set_rev_mp) |
187 |
187 |
188 declare [[ sledgehammer_problem_prefix = "Abstraction__image_curry" ]] |
188 declare [[ sledgehammer_problem_prefix = "Abstraction__image_curry" ]] |
189 lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)" |
189 lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)" |
190 (*sledgehammer*) |
190 (* sledgehammer *) |
191 by auto |
191 by auto |
192 |
192 |
193 declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesA" ]] |
193 declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesA" ]] |
194 lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)" |
194 lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)" |
195 (*sledgehammer*) |
195 by (metis map_pair_def map_pair_surj_on) |
196 apply (rule equalityI) |
|
197 (***Even the two inclusions are far too difficult |
|
198 using [[ sledgehammer_problem_prefix = "Abstraction__image_TimesA_simpler"]] |
|
199 ***) |
|
200 apply (rule subsetI) |
|
201 apply (erule imageE) |
|
202 (*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*) |
|
203 apply (erule ssubst) |
|
204 apply (erule SigmaE) |
|
205 (*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*) |
|
206 apply (erule ssubst) |
|
207 apply (subst split_conv) |
|
208 apply (rule SigmaI) |
|
209 apply (erule imageI) + |
|
210 txt{*subgoal 2*} |
|
211 apply (clarify ) |
|
212 apply (simp add: ) |
|
213 apply (rule rev_image_eqI) |
|
214 apply (blast intro: elim:) |
|
215 apply (simp add: ) |
|
216 done |
|
217 |
|
218 (*Given the difficulty of the previous problem, these two are probably |
|
219 impossible*) |
|
220 |
196 |
221 declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesB" ]] |
197 declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesB" ]] |
222 lemma image_TimesB: |
198 lemma image_TimesB: |
223 "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)" |
199 "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)" |
224 (*sledgehammer*) |
200 (* sledgehammer *) |
225 by force |
201 by force |
226 |
202 |
227 declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesC" ]] |
203 declare [[ sledgehammer_problem_prefix = "Abstraction__image_TimesC" ]] |
228 lemma image_TimesC: |
204 lemma image_TimesC: |
229 "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = |
205 "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = |
230 ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" |
206 ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" |
231 (*sledgehammer*) |
207 by (metis image_TimesA) |
232 by auto |
|
233 |
208 |
234 end |
209 end |