paulson@23449
|
1 |
(* Title: HOL/MetisExamples/Abstraction.thy
|
paulson@23449
|
2 |
ID: $Id$
|
paulson@23449
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
paulson@23449
|
4 |
|
paulson@23449
|
5 |
Testing the metis method
|
paulson@23449
|
6 |
*)
|
paulson@23449
|
7 |
|
paulson@23449
|
8 |
theory Abstraction imports FuncSet
|
paulson@23449
|
9 |
begin
|
paulson@23449
|
10 |
|
paulson@23449
|
11 |
(*For Christoph Benzmueller*)
|
paulson@23449
|
12 |
lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))";
|
paulson@23449
|
13 |
by (metis One_nat_def less_Suc0 not_less0 not_less_eq numeral_2_eq_2)
|
paulson@23449
|
14 |
|
paulson@23449
|
15 |
(*this is a theorem, but we can't prove it unless ext is applied explicitly
|
paulson@23449
|
16 |
lemma "(op=) = (%x y. y=x)"
|
paulson@23449
|
17 |
*)
|
paulson@23449
|
18 |
|
paulson@23449
|
19 |
consts
|
paulson@23449
|
20 |
monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
|
paulson@23449
|
21 |
pset :: "'a set => 'a set"
|
paulson@23449
|
22 |
order :: "'a set => ('a * 'a) set"
|
paulson@23449
|
23 |
|
paulson@23449
|
24 |
ML{*ResAtp.problem_name := "Abstraction__Collect_triv"*}
|
paulson@23449
|
25 |
lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
|
paulson@23449
|
26 |
proof (neg_clausify)
|
paulson@23449
|
27 |
assume 0: "(a\<Colon>'a\<Colon>type) \<in> Collect (P\<Colon>'a\<Colon>type \<Rightarrow> bool)"
|
paulson@23449
|
28 |
assume 1: "\<not> (P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
|
paulson@23449
|
29 |
have 2: "(P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
|
paulson@23449
|
30 |
by (metis CollectD 0)
|
paulson@23449
|
31 |
show "False"
|
paulson@23449
|
32 |
by (metis 2 1)
|
paulson@23449
|
33 |
qed
|
paulson@23449
|
34 |
|
paulson@23449
|
35 |
lemma Collect_triv: "a \<in> {x. P x} ==> P a"
|
berghofe@23756
|
36 |
by (metis mem_Collect_eq)
|
paulson@23449
|
37 |
|
paulson@23449
|
38 |
|
paulson@23449
|
39 |
ML{*ResAtp.problem_name := "Abstraction__Collect_mp"*}
|
paulson@23449
|
40 |
lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
|
berghofe@23756
|
41 |
by (metis CollectI Collect_imp_eq ComplD UnE mem_Collect_eq);
|
paulson@23449
|
42 |
--{*34 secs*}
|
paulson@23449
|
43 |
|
paulson@23449
|
44 |
ML{*ResAtp.problem_name := "Abstraction__Sigma_triv"*}
|
paulson@23449
|
45 |
lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
|
paulson@23449
|
46 |
proof (neg_clausify)
|
paulson@23449
|
47 |
assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type) \<in> Sigma (A\<Colon>'a\<Colon>type set) (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set)"
|
paulson@23449
|
48 |
assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> (b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) a"
|
paulson@23449
|
49 |
have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
|
paulson@23449
|
50 |
by (metis SigmaD1 0)
|
paulson@23449
|
51 |
have 3: "(b\<Colon>'b\<Colon>type) \<in> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"
|
paulson@23449
|
52 |
by (metis SigmaD2 0)
|
paulson@23449
|
53 |
have 4: "(b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"
|
paulson@23449
|
54 |
by (metis 1 2)
|
paulson@23449
|
55 |
show "False"
|
paulson@23449
|
56 |
by (metis 3 4)
|
paulson@23449
|
57 |
qed
|
paulson@23449
|
58 |
|
paulson@23449
|
59 |
lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
|
paulson@23449
|
60 |
by (metis SigmaD1 SigmaD2)
|
paulson@23449
|
61 |
|
paulson@23449
|
62 |
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect"*}
|
paulson@23449
|
63 |
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
|
paulson@23449
|
64 |
(*???metis cannot prove this
|
paulson@23449
|
65 |
by (metis CollectD SigmaD1 SigmaD2 UN_eq)
|
paulson@23449
|
66 |
Also, UN_eq is unnecessary*)
|
paulson@23449
|
67 |
by (meson CollectD SigmaD1 SigmaD2)
|
paulson@23449
|
68 |
|
paulson@23449
|
69 |
|
paulson@23449
|
70 |
(*single-step*)
|
paulson@23449
|
71 |
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
|
paulson@24827
|
72 |
by (metis SigmaD1 SigmaD2 insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def vimage_singleton_eq)
|
paulson@24827
|
73 |
|
paulson@24827
|
74 |
|
paulson@24827
|
75 |
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
|
paulson@23449
|
76 |
proof (neg_clausify)
|
paulson@24827
|
77 |
assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type)
|
paulson@24827
|
78 |
\<in> Sigma (A\<Colon>'a\<Colon>type set)
|
paulson@24827
|
79 |
(COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)))"
|
paulson@24827
|
80 |
assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> a \<noteq> (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type)"
|
paulson@24827
|
81 |
have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
|
paulson@24827
|
82 |
by (metis 0 SigmaD1)
|
paulson@24827
|
83 |
have 3: "(b\<Colon>'b\<Colon>type)
|
paulson@24827
|
84 |
\<in> COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)) (a\<Colon>'a\<Colon>type)"
|
paulson@24827
|
85 |
by (metis 0 SigmaD2)
|
paulson@24827
|
86 |
have 4: "(b\<Colon>'b\<Colon>type) \<in> Collect (COMBB (op = (a\<Colon>'a\<Colon>type)) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type))"
|
paulson@24827
|
87 |
by (metis 3)
|
paulson@24827
|
88 |
have 5: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) \<noteq> (a\<Colon>'a\<Colon>type)"
|
paulson@24827
|
89 |
by (metis 1 2)
|
paulson@24827
|
90 |
have 6: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) = (a\<Colon>'a\<Colon>type)"
|
paulson@24827
|
91 |
by (metis 4 vimage_singleton_eq insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def)
|
paulson@23449
|
92 |
show "False"
|
paulson@24827
|
93 |
by (metis 5 6)
|
paulson@24827
|
94 |
qed
|
paulson@24827
|
95 |
|
paulson@24827
|
96 |
(*Alternative structured proof, untyped*)
|
paulson@24827
|
97 |
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
|
paulson@24827
|
98 |
proof (neg_clausify)
|
paulson@24827
|
99 |
assume 0: "(a, b) \<in> Sigma A (COMBB Collect (COMBC (COMBB COMBB op =) f))"
|
paulson@24827
|
100 |
have 1: "b \<in> Collect (COMBB (op = a) f)"
|
paulson@24827
|
101 |
by (metis 0 SigmaD2)
|
paulson@24827
|
102 |
have 2: "f b = a"
|
paulson@24827
|
103 |
by (metis 1 vimage_Collect_eq singleton_conv2 insert_def union_empty2 vimage_singleton_eq vimage_def)
|
paulson@24827
|
104 |
assume 3: "a \<notin> A \<or> a \<noteq> f b"
|
paulson@24827
|
105 |
have 4: "a \<in> A"
|
paulson@24827
|
106 |
by (metis 0 SigmaD1)
|
paulson@24827
|
107 |
have 5: "f b \<noteq> a"
|
paulson@24827
|
108 |
by (metis 4 3)
|
paulson@24827
|
109 |
show "False"
|
paulson@24827
|
110 |
by (metis 5 2)
|
paulson@24827
|
111 |
qed
|
paulson@23449
|
112 |
|
paulson@23449
|
113 |
|
paulson@23449
|
114 |
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_in_pp"*}
|
paulson@23449
|
115 |
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
|
paulson@24827
|
116 |
by (metis Collect_mem_eq SigmaD2)
|
paulson@23449
|
117 |
|
paulson@24742
|
118 |
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
|
paulson@24742
|
119 |
proof (neg_clausify)
|
paulson@24827
|
120 |
assume 0: "(cl, f) \<in> CLF"
|
paulson@24827
|
121 |
assume 1: "CLF = Sigma CL (COMBB Collect (COMBB (COMBC op \<in>) pset))"
|
paulson@24827
|
122 |
assume 2: "f \<notin> pset cl"
|
paulson@24827
|
123 |
have 3: "\<And>X1 X2. X2 \<in> COMBB Collect (COMBB (COMBC op \<in>) pset) X1 \<or> (X1, X2) \<notin> CLF"
|
paulson@24827
|
124 |
by (metis SigmaD2 1)
|
paulson@24827
|
125 |
have 4: "\<And>X1 X2. X2 \<in> pset X1 \<or> (X1, X2) \<notin> CLF"
|
paulson@24827
|
126 |
by (metis 3 Collect_mem_eq)
|
paulson@24827
|
127 |
have 5: "(cl, f) \<notin> CLF"
|
paulson@24827
|
128 |
by (metis 2 4)
|
paulson@23449
|
129 |
show "False"
|
paulson@24827
|
130 |
by (metis 5 0)
|
paulson@24827
|
131 |
qed
|
paulson@23449
|
132 |
|
paulson@23449
|
133 |
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*}
|
paulson@23449
|
134 |
lemma
|
paulson@23449
|
135 |
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
|
paulson@23449
|
136 |
f \<in> pset cl \<rightarrow> pset cl"
|
paulson@24827
|
137 |
proof (neg_clausify)
|
paulson@24827
|
138 |
assume 0: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
|
paulson@24827
|
139 |
assume 1: "(cl, f)
|
paulson@24827
|
140 |
\<in> Sigma CL
|
paulson@24827
|
141 |
(COMBB Collect
|
paulson@24827
|
142 |
(COMBB (COMBC op \<in>) (COMBS (COMBB Pi pset) (COMBB COMBK pset))))"
|
paulson@24827
|
143 |
show "False"
|
paulson@24827
|
144 |
(* by (metis 0 Collect_mem_eq SigmaD2 1) ??doesn't terminate*)
|
paulson@24827
|
145 |
by (insert 0 1, simp add: COMBB_def COMBS_def COMBC_def)
|
paulson@24827
|
146 |
qed
|
paulson@23449
|
147 |
|
paulson@23449
|
148 |
|
paulson@23449
|
149 |
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Int"*}
|
paulson@23449
|
150 |
lemma
|
paulson@23449
|
151 |
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
|
paulson@23449
|
152 |
f \<in> pset cl \<inter> cl"
|
paulson@24827
|
153 |
proof (neg_clausify)
|
paulson@24827
|
154 |
assume 0: "(cl, f)
|
paulson@24827
|
155 |
\<in> Sigma CL
|
paulson@24827
|
156 |
(COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)))"
|
paulson@24827
|
157 |
assume 1: "f \<notin> pset cl \<inter> cl"
|
paulson@24827
|
158 |
have 2: "f \<in> COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)) cl"
|
paulson@24827
|
159 |
by (insert 0, simp add: COMBB_def)
|
paulson@24827
|
160 |
(* by (metis SigmaD2 0) ??doesn't terminate*)
|
paulson@24827
|
161 |
have 3: "f \<in> COMBS (COMBB op \<inter> pset) COMBI cl"
|
paulson@24827
|
162 |
by (metis 2 Collect_mem_eq)
|
paulson@24827
|
163 |
have 4: "f \<notin> cl \<inter> pset cl"
|
paulson@24827
|
164 |
by (metis 1 Int_commute)
|
paulson@24827
|
165 |
have 5: "f \<in> cl \<inter> pset cl"
|
paulson@24827
|
166 |
by (metis 3 Int_commute)
|
paulson@24827
|
167 |
show "False"
|
paulson@24827
|
168 |
by (metis 5 4)
|
paulson@24827
|
169 |
qed
|
paulson@24827
|
170 |
|
paulson@23449
|
171 |
|
paulson@23449
|
172 |
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*}
|
paulson@23449
|
173 |
lemma
|
paulson@23449
|
174 |
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
|
paulson@23449
|
175 |
(f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"
|
paulson@23449
|
176 |
by auto
|
paulson@23449
|
177 |
|
paulson@23449
|
178 |
ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Int"*}
|
paulson@23449
|
179 |
lemma "(cl,f) \<in> CLF ==>
|
paulson@23449
|
180 |
CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
|
paulson@23449
|
181 |
f \<in> pset cl \<inter> cl"
|
paulson@24827
|
182 |
by auto
|
paulson@24827
|
183 |
(*??no longer terminates, with combinators
|
paulson@23449
|
184 |
by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1)
|
paulson@23449
|
185 |
--{*@{text Int_def} is redundant}
|
paulson@24827
|
186 |
*)
|
paulson@23449
|
187 |
|
paulson@23449
|
188 |
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*}
|
paulson@23449
|
189 |
lemma "(cl,f) \<in> CLF ==>
|
paulson@23449
|
190 |
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
|
paulson@23449
|
191 |
f \<in> pset cl \<inter> cl"
|
paulson@24827
|
192 |
by auto
|
paulson@24827
|
193 |
(*??no longer terminates, with combinators
|
paulson@23449
|
194 |
by (metis Collect_mem_eq Int_commute SigmaD2)
|
paulson@24827
|
195 |
*)
|
paulson@23449
|
196 |
|
paulson@23449
|
197 |
ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Pi"*}
|
paulson@23449
|
198 |
lemma
|
paulson@23449
|
199 |
"(cl,f) \<in> CLF ==>
|
paulson@23449
|
200 |
CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==>
|
paulson@23449
|
201 |
f \<in> pset cl \<rightarrow> pset cl"
|
paulson@24827
|
202 |
by auto
|
paulson@24827
|
203 |
(*??no longer terminates, with combinators
|
paulson@23449
|
204 |
by (metis Collect_mem_eq SigmaD2 subsetD)
|
paulson@24827
|
205 |
*)
|
paulson@23449
|
206 |
|
paulson@23449
|
207 |
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi"*}
|
paulson@23449
|
208 |
lemma
|
paulson@23449
|
209 |
"(cl,f) \<in> CLF ==>
|
paulson@23449
|
210 |
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==>
|
paulson@23449
|
211 |
f \<in> pset cl \<rightarrow> pset cl"
|
paulson@24827
|
212 |
by auto
|
paulson@24827
|
213 |
(*??no longer terminates, with combinators
|
paulson@23449
|
214 |
by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE)
|
paulson@24827
|
215 |
*)
|
paulson@23449
|
216 |
|
paulson@23449
|
217 |
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*}
|
paulson@23449
|
218 |
lemma
|
paulson@23449
|
219 |
"(cl,f) \<in> CLF ==>
|
paulson@23449
|
220 |
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==>
|
paulson@23449
|
221 |
(f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"
|
paulson@23449
|
222 |
by auto
|
paulson@23449
|
223 |
|
paulson@23449
|
224 |
ML{*ResAtp.problem_name := "Abstraction__map_eq_zipA"*}
|
paulson@23449
|
225 |
lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
|
paulson@23449
|
226 |
apply (induct xs)
|
paulson@23449
|
227 |
(*sledgehammer*)
|
paulson@23449
|
228 |
apply auto
|
paulson@23449
|
229 |
done
|
paulson@23449
|
230 |
|
paulson@23449
|
231 |
ML{*ResAtp.problem_name := "Abstraction__map_eq_zipB"*}
|
paulson@23449
|
232 |
lemma "map (%w. (w -> w, w \<times> w)) xs =
|
paulson@23449
|
233 |
zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
|
paulson@23449
|
234 |
apply (induct xs)
|
paulson@23449
|
235 |
(*sledgehammer*)
|
paulson@23449
|
236 |
apply auto
|
paulson@23449
|
237 |
done
|
paulson@23449
|
238 |
|
paulson@23449
|
239 |
ML{*ResAtp.problem_name := "Abstraction__image_evenA"*}
|
paulson@23449
|
240 |
lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)";
|
paulson@23449
|
241 |
(*sledgehammer*)
|
paulson@23449
|
242 |
by auto
|
paulson@23449
|
243 |
|
paulson@23449
|
244 |
ML{*ResAtp.problem_name := "Abstraction__image_evenB"*}
|
paulson@23449
|
245 |
lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A
|
paulson@23449
|
246 |
==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
|
paulson@23449
|
247 |
(*sledgehammer*)
|
paulson@23449
|
248 |
by auto
|
paulson@23449
|
249 |
|
paulson@23449
|
250 |
ML{*ResAtp.problem_name := "Abstraction__image_curry"*}
|
paulson@23449
|
251 |
lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)"
|
paulson@23449
|
252 |
(*sledgehammer*)
|
paulson@23449
|
253 |
by auto
|
paulson@23449
|
254 |
|
paulson@23449
|
255 |
ML{*ResAtp.problem_name := "Abstraction__image_TimesA"*}
|
paulson@23449
|
256 |
lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
|
paulson@23449
|
257 |
(*sledgehammer*)
|
paulson@23449
|
258 |
apply (rule equalityI)
|
paulson@23449
|
259 |
(***Even the two inclusions are far too difficult
|
paulson@23449
|
260 |
ML{*ResAtp.problem_name := "Abstraction__image_TimesA_simpler"*}
|
paulson@23449
|
261 |
***)
|
paulson@23449
|
262 |
apply (rule subsetI)
|
paulson@23449
|
263 |
apply (erule imageE)
|
paulson@23449
|
264 |
(*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*)
|
paulson@23449
|
265 |
apply (erule ssubst)
|
paulson@23449
|
266 |
apply (erule SigmaE)
|
paulson@23449
|
267 |
(*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*)
|
paulson@23449
|
268 |
apply (erule ssubst)
|
paulson@23449
|
269 |
apply (subst split_conv)
|
paulson@23449
|
270 |
apply (rule SigmaI)
|
paulson@23449
|
271 |
apply (erule imageI) +
|
paulson@23449
|
272 |
txt{*subgoal 2*}
|
paulson@23449
|
273 |
apply (clarify );
|
paulson@23449
|
274 |
apply (simp add: );
|
paulson@23449
|
275 |
apply (rule rev_image_eqI)
|
paulson@23449
|
276 |
apply (blast intro: elim:);
|
paulson@23449
|
277 |
apply (simp add: );
|
paulson@23449
|
278 |
done
|
paulson@23449
|
279 |
|
paulson@23449
|
280 |
(*Given the difficulty of the previous problem, these two are probably
|
paulson@23449
|
281 |
impossible*)
|
paulson@23449
|
282 |
|
paulson@23449
|
283 |
ML{*ResAtp.problem_name := "Abstraction__image_TimesB"*}
|
paulson@23449
|
284 |
lemma image_TimesB:
|
paulson@23449
|
285 |
"(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)"
|
paulson@23449
|
286 |
(*sledgehammer*)
|
paulson@23449
|
287 |
by force
|
paulson@23449
|
288 |
|
paulson@23449
|
289 |
ML{*ResAtp.problem_name := "Abstraction__image_TimesC"*}
|
paulson@23449
|
290 |
lemma image_TimesC:
|
paulson@23449
|
291 |
"(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) =
|
paulson@23449
|
292 |
((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)"
|
paulson@23449
|
293 |
(*sledgehammer*)
|
paulson@23449
|
294 |
by auto
|
paulson@23449
|
295 |
|
paulson@23449
|
296 |
end
|