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