author | blanchet |
Thu, 29 Apr 2010 19:02:04 +0200 | |
changeset 36566 | f91342f218a9 |
parent 33027 | 9cf389429f6d |
child 36571 | 16ec4fe058cb |
permissions | -rw-r--r-- |
33027 | 1 |
(* Title: HOL/Metis_Examples/Abstraction.thy |
23449 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
||
33027 | 4 |
Testing the metis method. |
23449 | 5 |
*) |
6 |
||
27368 | 7 |
theory Abstraction |
8 |
imports Main FuncSet |
|
23449 | 9 |
begin |
10 |
||
11 |
(*For Christoph Benzmueller*) |
|
12 |
lemma "x<1 & ((op=) = (op=)) ==> ((op=) = (op=)) & (x<(2::nat))"; |
|
13 |
by (metis One_nat_def less_Suc0 not_less0 not_less_eq numeral_2_eq_2) |
|
14 |
||
15 |
(*this is a theorem, but we can't prove it unless ext is applied explicitly |
|
16 |
lemma "(op=) = (%x y. y=x)" |
|
17 |
*) |
|
18 |
||
19 |
consts |
|
20 |
monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool" |
|
21 |
pset :: "'a set => 'a set" |
|
22 |
order :: "'a set => ('a * 'a) set" |
|
23 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
24 |
declare [[ atp_problem_prefix = "Abstraction__Collect_triv" ]] |
23449 | 25 |
lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a" |
36566 | 26 |
proof - |
27 |
assume "a \<in> {x. P x}" |
|
28 |
hence "a \<in> P" by (metis Collect_def) |
|
29 |
hence "P a" by (metis mem_def) |
|
30 |
thus "P a" by metis |
|
23449 | 31 |
qed |
32 |
||
33 |
lemma Collect_triv: "a \<in> {x. P x} ==> P a" |
|
23756 | 34 |
by (metis mem_Collect_eq) |
23449 | 35 |
|
36 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
37 |
declare [[ atp_problem_prefix = "Abstraction__Collect_mp" ]] |
23449 | 38 |
lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}" |
36566 | 39 |
by (metis Collect_imp_eq ComplD UnE) |
23449 | 40 |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
41 |
declare [[ atp_problem_prefix = "Abstraction__Sigma_triv" ]] |
23449 | 42 |
lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a" |
36566 | 43 |
proof - |
44 |
assume A1: "(a, b) \<in> Sigma A B" |
|
45 |
hence F1: "b \<in> B a" by (metis mem_Sigma_iff) |
|
46 |
have F2: "a \<in> A" by (metis A1 mem_Sigma_iff) |
|
47 |
have "b \<in> B a" by (metis F1) |
|
48 |
thus "a \<in> A \<and> b \<in> B a" by (metis F2) |
|
23449 | 49 |
qed |
50 |
||
51 |
lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a" |
|
52 |
by (metis SigmaD1 SigmaD2) |
|
53 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
54 |
declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect" ]] |
36566 | 55 |
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b" |
56 |
(* Metis says this is satisfiable! |
|
29676 | 57 |
by (metis CollectD SigmaD1 SigmaD2) |
58 |
*) |
|
23449 | 59 |
by (meson CollectD SigmaD1 SigmaD2) |
60 |
||
61 |
||
36566 | 62 |
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b" |
63 |
by (metis mem_Sigma_iff singleton_conv2 vimage_Collect_eq vimage_singleton_eq) |
|
24827 | 64 |
|
36566 | 65 |
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b" |
66 |
proof - |
|
67 |
assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})" |
|
68 |
have F1: "\<forall>u. {u} = op = u" by (metis singleton_conv2 Collect_def) |
|
69 |
have F2: "\<forall>x w. (\<lambda>R. w (x R)) = x -` w" by (metis vimage_Collect_eq Collect_def) |
|
70 |
have F3: "\<forall>v w y. v \<in> w -` op = y \<longrightarrow> w v = y" by (metis F1 vimage_singleton_eq) |
|
71 |
have F4: "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff) |
|
72 |
have F5: "a \<in> A" by (metis A1 mem_Sigma_iff) |
|
73 |
have "b \<in> f -` op = a" by (metis F2 F4 Collect_def) |
|
74 |
hence "f b = a" by (metis F3) |
|
75 |
thus "a \<in> A \<and> a = f b" by (metis F5) |
|
24827 | 76 |
qed |
77 |
||
36566 | 78 |
(* Alternative structured proof *) |
79 |
lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b" |
|
80 |
proof - |
|
81 |
assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})" |
|
82 |
hence F1: "a \<in> A" by (metis mem_Sigma_iff) |
|
83 |
have "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff) |
|
84 |
hence F2: "b \<in> (\<lambda>R. a = f R)" by (metis Collect_def) |
|
85 |
hence "a = f b" by (unfold mem_def) |
|
86 |
thus "a \<in> A \<and> a = f b" by (metis F1) |
|
24827 | 87 |
qed |
23449 | 88 |
|
89 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
90 |
declare [[ atp_problem_prefix = "Abstraction__CLF_eq_in_pp" ]] |
23449 | 91 |
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl" |
24827 | 92 |
by (metis Collect_mem_eq SigmaD2) |
23449 | 93 |
|
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
24632
diff
changeset
|
94 |
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl" |
36566 | 95 |
proof - |
96 |
assume A1: "(cl, f) \<in> CLF" |
|
97 |
assume A2: "CLF = (SIGMA cl:CL. {f. f \<in> pset cl})" |
|
98 |
have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def) |
|
99 |
have "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> {R. R \<in> pset u}" by (metis A2 mem_Sigma_iff) |
|
100 |
hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis F1 Collect_def) |
|
101 |
hence "f \<in> pset cl" by (metis A1) |
|
102 |
thus "f \<in> pset cl" by metis |
|
24827 | 103 |
qed |
23449 | 104 |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
105 |
declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Pi" ]] |
23449 | 106 |
lemma |
107 |
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> |
|
108 |
f \<in> pset cl \<rightarrow> pset cl" |
|
36566 | 109 |
proof - |
110 |
assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})" |
|
111 |
have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def) |
|
112 |
have "f \<in> {R. R \<in> pset cl \<rightarrow> pset cl}" using A1 by simp |
|
113 |
hence "f \<in> pset cl \<rightarrow> pset cl" by (metis F1 Collect_def) |
|
114 |
thus "f \<in> pset cl \<rightarrow> pset cl" by metis |
|
24827 | 115 |
qed |
23449 | 116 |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
117 |
declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Int" ]] |
23449 | 118 |
lemma |
119 |
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
|
120 |
f \<in> pset cl \<inter> cl" |
|
36566 | 121 |
proof - |
122 |
assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})" |
|
123 |
have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def) |
|
124 |
have "f \<in> {R. R \<in> pset cl \<inter> cl}" using A1 by simp |
|
125 |
hence "f \<in> Id_on cl `` pset cl" by (metis F1 Int_commute Image_Id_on Collect_def) |
|
126 |
hence "f \<in> Id_on cl `` pset cl" by metis |
|
127 |
hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on) |
|
128 |
thus "f \<in> pset cl \<inter> cl" by (metis Int_commute) |
|
24827 | 129 |
qed |
130 |
||
23449 | 131 |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
132 |
declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Pi_mono" ]] |
23449 | 133 |
lemma |
134 |
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==> |
|
135 |
(f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" |
|
136 |
by auto |
|
137 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
138 |
declare [[ atp_problem_prefix = "Abstraction__CLF_subset_Collect_Int" ]] |
23449 | 139 |
lemma "(cl,f) \<in> CLF ==> |
140 |
CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
|
141 |
f \<in> pset cl \<inter> cl" |
|
24827 | 142 |
by auto |
27368 | 143 |
|
23449 | 144 |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
145 |
declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Int" ]] |
23449 | 146 |
lemma "(cl,f) \<in> CLF ==> |
147 |
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
|
148 |
f \<in> pset cl \<inter> cl" |
|
24827 | 149 |
by auto |
36566 | 150 |
|
23449 | 151 |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
152 |
declare [[ atp_problem_prefix = "Abstraction__CLF_subset_Collect_Pi" ]] |
23449 | 153 |
lemma |
154 |
"(cl,f) \<in> CLF ==> |
|
155 |
CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> |
|
156 |
f \<in> pset cl \<rightarrow> pset cl" |
|
31754 | 157 |
by fast |
36566 | 158 |
|
23449 | 159 |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
160 |
declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Pi" ]] |
23449 | 161 |
lemma |
162 |
"(cl,f) \<in> CLF ==> |
|
163 |
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> |
|
164 |
f \<in> pset cl \<rightarrow> pset cl" |
|
24827 | 165 |
by auto |
36566 | 166 |
|
23449 | 167 |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
168 |
declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Pi_mono" ]] |
23449 | 169 |
lemma |
170 |
"(cl,f) \<in> CLF ==> |
|
171 |
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==> |
|
172 |
(f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" |
|
173 |
by auto |
|
174 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
175 |
declare [[ atp_problem_prefix = "Abstraction__map_eq_zipA" ]] |
23449 | 176 |
lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)" |
177 |
apply (induct xs) |
|
36566 | 178 |
apply (metis map_is_Nil_conv zip.simps(1)) |
179 |
by auto |
|
23449 | 180 |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
181 |
declare [[ atp_problem_prefix = "Abstraction__map_eq_zipB" ]] |
23449 | 182 |
lemma "map (%w. (w -> w, w \<times> w)) xs = |
183 |
zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)" |
|
184 |
apply (induct xs) |
|
36566 | 185 |
apply (metis Nil_is_map_conv zip_Nil) |
186 |
by auto |
|
23449 | 187 |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
188 |
declare [[ atp_problem_prefix = "Abstraction__image_evenA" ]] |
36566 | 189 |
lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)" |
190 |
by (metis Collect_def image_subset_iff mem_def) |
|
23449 | 191 |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
192 |
declare [[ atp_problem_prefix = "Abstraction__image_evenB" ]] |
23449 | 193 |
lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A |
194 |
==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"; |
|
36566 | 195 |
by (metis Collect_def imageI image_image image_subset_iff mem_def) |
23449 | 196 |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
197 |
declare [[ atp_problem_prefix = "Abstraction__image_curry" ]] |
23449 | 198 |
lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)" |
36566 | 199 |
(*sledgehammer*) |
23449 | 200 |
by auto |
201 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
202 |
declare [[ atp_problem_prefix = "Abstraction__image_TimesA" ]] |
23449 | 203 |
lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)" |
36566 | 204 |
(*sledgehammer*) |
23449 | 205 |
apply (rule equalityI) |
206 |
(***Even the two inclusions are far too difficult |
|
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
207 |
using [[ atp_problem_prefix = "Abstraction__image_TimesA_simpler"]] |
23449 | 208 |
***) |
209 |
apply (rule subsetI) |
|
210 |
apply (erule imageE) |
|
211 |
(*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*) |
|
212 |
apply (erule ssubst) |
|
213 |
apply (erule SigmaE) |
|
214 |
(*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*) |
|
215 |
apply (erule ssubst) |
|
216 |
apply (subst split_conv) |
|
217 |
apply (rule SigmaI) |
|
218 |
apply (erule imageI) + |
|
219 |
txt{*subgoal 2*} |
|
220 |
apply (clarify ); |
|
221 |
apply (simp add: ); |
|
222 |
apply (rule rev_image_eqI) |
|
223 |
apply (blast intro: elim:); |
|
224 |
apply (simp add: ); |
|
225 |
done |
|
226 |
||
227 |
(*Given the difficulty of the previous problem, these two are probably |
|
228 |
impossible*) |
|
229 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
230 |
declare [[ atp_problem_prefix = "Abstraction__image_TimesB" ]] |
23449 | 231 |
lemma image_TimesB: |
36566 | 232 |
"(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)" |
233 |
(*sledgehammer*) |
|
23449 | 234 |
by force |
235 |
||
32864
a226f29d4bdc
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
31754
diff
changeset
|
236 |
declare [[ atp_problem_prefix = "Abstraction__image_TimesC" ]] |
23449 | 237 |
lemma image_TimesC: |
238 |
"(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = |
|
239 |
((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" |
|
36566 | 240 |
(*sledgehammer*) |
23449 | 241 |
by auto |
242 |
||
243 |
end |