|
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 |
|
8 theory Abstraction imports FuncSet |
|
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 |
|
24 ML{*ResAtp.problem_name := "Abstraction__Collect_triv"*} |
|
25 lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a" |
|
26 proof (neg_clausify) |
|
27 assume 0: "(a\<Colon>'a\<Colon>type) \<in> Collect (P\<Colon>'a\<Colon>type \<Rightarrow> bool)" |
|
28 assume 1: "\<not> (P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)" |
|
29 have 2: "(P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)" |
|
30 by (metis CollectD 0) |
|
31 show "False" |
|
32 by (metis 2 1) |
|
33 qed |
|
34 |
|
35 lemma Collect_triv: "a \<in> {x. P x} ==> P a" |
|
36 by (metis member_Collect_eq member_def) |
|
37 |
|
38 |
|
39 ML{*ResAtp.problem_name := "Abstraction__Collect_mp"*} |
|
40 lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}" |
|
41 by (metis CollectI Collect_imp_eq ComplD UnE memberI member_Collect_eq); |
|
42 --{*34 secs*} |
|
43 |
|
44 ML{*ResAtp.problem_name := "Abstraction__Sigma_triv"*} |
|
45 lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a" |
|
46 proof (neg_clausify) |
|
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)" |
|
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" |
|
49 have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)" |
|
50 by (metis SigmaD1 0) |
|
51 have 3: "(b\<Colon>'b\<Colon>type) \<in> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)" |
|
52 by (metis SigmaD2 0) |
|
53 have 4: "(b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)" |
|
54 by (metis 1 2) |
|
55 show "False" |
|
56 by (metis 3 4) |
|
57 qed |
|
58 |
|
59 lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a" |
|
60 by (metis SigmaD1 SigmaD2) |
|
61 |
|
62 ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect"*} |
|
63 lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b" |
|
64 (*???metis cannot prove this |
|
65 by (metis CollectD SigmaD1 SigmaD2 UN_eq) |
|
66 Also, UN_eq is unnecessary*) |
|
67 by (meson CollectD SigmaD1 SigmaD2) |
|
68 |
|
69 |
|
70 |
|
71 (*single-step*) |
|
72 lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b" |
|
73 proof (neg_clausify) |
|
74 assume 0: "(a, b) \<in> Sigma A (llabs_subgoal_1 f)" |
|
75 assume 1: "\<And>f x. llabs_subgoal_1 f x = Collect (COMBB (op = x) f)" |
|
76 assume 2: "a \<notin> A \<or> a \<noteq> f b" |
|
77 have 3: "a \<in> A" |
|
78 by (metis SigmaD1 0) |
|
79 have 4: "b \<in> llabs_subgoal_1 f a" |
|
80 by (metis SigmaD2 0) |
|
81 have 5: "\<And>X1 X2. X2 -` {X1} = llabs_subgoal_1 X2 X1" |
|
82 by (metis 1 vimage_Collect_eq singleton_conv2) |
|
83 have 6: "\<And>X1 X2 X3. X1 X2 = X3 \<or> X2 \<notin> llabs_subgoal_1 X1 X3" |
|
84 by (metis vimage_singleton_eq 5) |
|
85 have 7: "f b \<noteq> a" |
|
86 by (metis 2 3) |
|
87 have 8: "f b = a" |
|
88 by (metis 6 4) |
|
89 show "False" |
|
90 by (metis 8 7) |
|
91 qed finish_clausify |
|
92 |
|
93 |
|
94 ML{*ResAtp.problem_name := "Abstraction__CLF_eq_in_pp"*} |
|
95 lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl" |
|
96 apply (metis Collect_mem_eq SigmaD2); |
|
97 done |
|
98 |
|
99 lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"proof (neg_clausify) |
|
100 assume 0: "(cl, f) \<in> CLF" |
|
101 assume 1: "CLF = Sigma CL llabs_subgoal_1" |
|
102 assume 2: "\<And>cl. llabs_subgoal_1 cl = |
|
103 Collect (llabs_Predicate_XRangeP_def_2_ op \<in> (pset cl))" |
|
104 assume 3: "f \<notin> pset cl" |
|
105 show "False" |
|
106 by (metis 0 1 SigmaD2 3 2 Collect_mem_eq) |
|
107 qed finish_clausify (*ugly hack: combinators??*) |
|
108 |
|
109 ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*} |
|
110 lemma |
|
111 "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> |
|
112 f \<in> pset cl \<rightarrow> pset cl" |
|
113 apply (metis Collect_mem_eq SigmaD2); |
|
114 done |
|
115 |
|
116 lemma |
|
117 "(cl,f) \<in> (SIGMA cl::'a set : CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> |
|
118 f \<in> pset cl \<rightarrow> pset cl" |
|
119 proof (neg_clausify) |
|
120 assume 0: "(cl, f) \<in> Sigma CL llabs_subgoal_1" |
|
121 assume 1: "\<And>cl. llabs_subgoal_1 cl = |
|
122 Collect |
|
123 (llabs_Predicate_XRangeP_def_2_ op \<in> (Pi (pset cl) (COMBK (pset cl))))" |
|
124 assume 2: "f \<notin> Pi (pset cl) (COMBK (pset cl))" |
|
125 show "False" |
|
126 by (metis Collect_mem_eq 1 2 SigmaD2 0 member2_def) |
|
127 qed finish_clausify |
|
128 (*Hack to prevent the "Additional hypotheses" error*) |
|
129 |
|
130 ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Int"*} |
|
131 lemma |
|
132 "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
|
133 f \<in> pset cl \<inter> cl" |
|
134 by (metis Collect_mem_eq SigmaD2) |
|
135 |
|
136 ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*} |
|
137 lemma |
|
138 "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==> |
|
139 (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" |
|
140 by auto |
|
141 |
|
142 ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Int"*} |
|
143 lemma "(cl,f) \<in> CLF ==> |
|
144 CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
|
145 f \<in> pset cl \<inter> cl" |
|
146 by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1) |
|
147 --{*@{text Int_def} is redundant} |
|
148 |
|
149 ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*} |
|
150 lemma "(cl,f) \<in> CLF ==> |
|
151 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> |
|
152 f \<in> pset cl \<inter> cl" |
|
153 by (metis Collect_mem_eq Int_commute SigmaD2) |
|
154 |
|
155 ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Pi"*} |
|
156 lemma |
|
157 "(cl,f) \<in> CLF ==> |
|
158 CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> |
|
159 f \<in> pset cl \<rightarrow> pset cl" |
|
160 by (metis Collect_mem_eq SigmaD2 subsetD) |
|
161 |
|
162 ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi"*} |
|
163 lemma |
|
164 "(cl,f) \<in> CLF ==> |
|
165 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> |
|
166 f \<in> pset cl \<rightarrow> pset cl" |
|
167 by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE) |
|
168 |
|
169 ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*} |
|
170 lemma |
|
171 "(cl,f) \<in> CLF ==> |
|
172 CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==> |
|
173 (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" |
|
174 by auto |
|
175 |
|
176 ML{*ResAtp.problem_name := "Abstraction__map_eq_zipA"*} |
|
177 lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)" |
|
178 apply (induct xs) |
|
179 (*sledgehammer*) |
|
180 apply auto |
|
181 done |
|
182 |
|
183 ML{*ResAtp.problem_name := "Abstraction__map_eq_zipB"*} |
|
184 lemma "map (%w. (w -> w, w \<times> w)) xs = |
|
185 zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)" |
|
186 apply (induct xs) |
|
187 (*sledgehammer*) |
|
188 apply auto |
|
189 done |
|
190 |
|
191 ML{*ResAtp.problem_name := "Abstraction__image_evenA"*} |
|
192 lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)"; |
|
193 (*sledgehammer*) |
|
194 by auto |
|
195 |
|
196 ML{*ResAtp.problem_name := "Abstraction__image_evenB"*} |
|
197 lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A |
|
198 ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"; |
|
199 (*sledgehammer*) |
|
200 by auto |
|
201 |
|
202 ML{*ResAtp.problem_name := "Abstraction__image_curry"*} |
|
203 lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)" |
|
204 (*sledgehammer*) |
|
205 by auto |
|
206 |
|
207 ML{*ResAtp.problem_name := "Abstraction__image_TimesA"*} |
|
208 lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)" |
|
209 (*sledgehammer*) |
|
210 apply (rule equalityI) |
|
211 (***Even the two inclusions are far too difficult |
|
212 ML{*ResAtp.problem_name := "Abstraction__image_TimesA_simpler"*} |
|
213 ***) |
|
214 apply (rule subsetI) |
|
215 apply (erule imageE) |
|
216 (*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*) |
|
217 apply (erule ssubst) |
|
218 apply (erule SigmaE) |
|
219 (*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*) |
|
220 apply (erule ssubst) |
|
221 apply (subst split_conv) |
|
222 apply (rule SigmaI) |
|
223 apply (erule imageI) + |
|
224 txt{*subgoal 2*} |
|
225 apply (clarify ); |
|
226 apply (simp add: ); |
|
227 apply (rule rev_image_eqI) |
|
228 apply (blast intro: elim:); |
|
229 apply (simp add: ); |
|
230 done |
|
231 |
|
232 (*Given the difficulty of the previous problem, these two are probably |
|
233 impossible*) |
|
234 |
|
235 ML{*ResAtp.problem_name := "Abstraction__image_TimesB"*} |
|
236 lemma image_TimesB: |
|
237 "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)" |
|
238 (*sledgehammer*) |
|
239 by force |
|
240 |
|
241 ML{*ResAtp.problem_name := "Abstraction__image_TimesC"*} |
|
242 lemma image_TimesC: |
|
243 "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = |
|
244 ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" |
|
245 (*sledgehammer*) |
|
246 by auto |
|
247 |
|
248 end |