author  paulson 
Thu, 04 Oct 2007 12:32:58 +0200  
changeset 24827  646bdc51eb7d 
parent 24783  5a3e336a2e37 
child 26819  56036226028b 
permissions  rwrr 
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 

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" 

23756  36 
by (metis mem_Collect_eq) 
23449  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}" 

23756  41 
by (metis CollectI Collect_imp_eq ComplD UnE mem_Collect_eq); 
23449  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 

24827  70 
(*singlestep*) 
71 
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b" 

72 
by (metis SigmaD1 SigmaD2 insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def vimage_singleton_eq) 

23449  73 

24827  74 

23449  75 
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b" 
76 
proof (neg_clausify) 

24827  77 
assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type) 
78 
\<in> Sigma (A\<Colon>'a\<Colon>type set) 

79 
(COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)))" 

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)" 

81 
have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)" 

82 
by (metis 0 SigmaD1) 

83 
have 3: "(b\<Colon>'b\<Colon>type) 

84 
\<in> COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)) (a\<Colon>'a\<Colon>type)" 

85 
by (metis 0 SigmaD2) 

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))" 

87 
by (metis 3) 

88 
have 5: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) \<noteq> (a\<Colon>'a\<Colon>type)" 

89 
by (metis 1 2) 

90 
have 6: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) = (a\<Colon>'a\<Colon>type)" 

91 
by (metis 4 vimage_singleton_eq insert_def singleton_conv2 union_empty2 vimage_Collect_eq vimage_def) 

23449  92 
show "False" 
24827  93 
by (metis 5 6) 
94 
qed 

95 

96 
(*Alternative structured proof, untyped*) 

97 
lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b" 

98 
proof (neg_clausify) 

99 
assume 0: "(a, b) \<in> Sigma A (COMBB Collect (COMBC (COMBB COMBB op =) f))" 

100 
have 1: "b \<in> Collect (COMBB (op = a) f)" 

101 
by (metis 0 SigmaD2) 

102 
have 2: "f b = a" 

103 
by (metis 1 vimage_Collect_eq singleton_conv2 insert_def union_empty2 vimage_singleton_eq vimage_def) 

104 
assume 3: "a \<notin> A \<or> a \<noteq> f b" 

105 
have 4: "a \<in> A" 

106 
by (metis 0 SigmaD1) 

107 
have 5: "f b \<noteq> a" 

108 
by (metis 4 3) 

109 
show "False" 

110 
by (metis 5 2) 

111 
qed 

23449  112 

113 

114 
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_in_pp"*} 

115 
lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl" 

24827  116 
by (metis Collect_mem_eq SigmaD2) 
23449  117 

24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
24632
diff
changeset

118 
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 sideeffect is that the ordering
paulson
parents:
24632
diff
changeset

119 
proof (neg_clausify) 
24827  120 
assume 0: "(cl, f) \<in> CLF" 
121 
assume 1: "CLF = Sigma CL (COMBB Collect (COMBB (COMBC op \<in>) pset))" 

122 
assume 2: "f \<notin> pset cl" 

123 
have 3: "\<And>X1 X2. X2 \<in> COMBB Collect (COMBB (COMBC op \<in>) pset) X1 \<or> (X1, X2) \<notin> CLF" 

124 
by (metis SigmaD2 1) 

125 
have 4: "\<And>X1 X2. X2 \<in> pset X1 \<or> (X1, X2) \<notin> CLF" 

126 
by (metis 3 Collect_mem_eq) 

127 
have 5: "(cl, f) \<notin> CLF" 

128 
by (metis 2 4) 

23449  129 
show "False" 
24827  130 
by (metis 5 0) 
131 
qed 

23449  132 

133 
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*} 

134 
lemma 

135 
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 

136 
f \<in> pset cl \<rightarrow> pset cl" 

24827  137 
proof (neg_clausify) 
138 
assume 0: "f \<notin> Pi (pset cl) (COMBK (pset cl))" 

139 
assume 1: "(cl, f) 

140 
\<in> Sigma CL 

141 
(COMBB Collect 

142 
(COMBB (COMBC op \<in>) (COMBS (COMBB Pi pset) (COMBB COMBK pset))))" 

143 
show "False" 

144 
(* by (metis 0 Collect_mem_eq SigmaD2 1) ??doesn't terminate*) 

145 
by (insert 0 1, simp add: COMBB_def COMBS_def COMBC_def) 

146 
qed 

23449  147 

148 

149 
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Int"*} 

150 
lemma 

151 
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> 

152 
f \<in> pset cl \<inter> cl" 

24827  153 
proof (neg_clausify) 
154 
assume 0: "(cl, f) 

155 
\<in> Sigma CL 

156 
(COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)))" 

157 
assume 1: "f \<notin> pset cl \<inter> cl" 

158 
have 2: "f \<in> COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)) cl" 

159 
by (insert 0, simp add: COMBB_def) 

160 
(* by (metis SigmaD2 0) ??doesn't terminate*) 

161 
have 3: "f \<in> COMBS (COMBB op \<inter> pset) COMBI cl" 

162 
by (metis 2 Collect_mem_eq) 

163 
have 4: "f \<notin> cl \<inter> pset cl" 

164 
by (metis 1 Int_commute) 

165 
have 5: "f \<in> cl \<inter> pset cl" 

166 
by (metis 3 Int_commute) 

167 
show "False" 

168 
by (metis 5 4) 

169 
qed 

170 

23449  171 

172 
ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi_mono"*} 

173 
lemma 

174 
"(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==> 

175 
(f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" 

176 
by auto 

177 

178 
ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Int"*} 

179 
lemma "(cl,f) \<in> CLF ==> 

180 
CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> 

181 
f \<in> pset cl \<inter> cl" 

24827  182 
by auto 
183 
(*??no longer terminates, with combinators 

23449  184 
by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1) 
185 
{*@{text Int_def} is redundant} 

24827  186 
*) 
23449  187 

188 
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Int"*} 

189 
lemma "(cl,f) \<in> CLF ==> 

190 
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==> 

191 
f \<in> pset cl \<inter> cl" 

24827  192 
by auto 
193 
(*??no longer terminates, with combinators 

23449  194 
by (metis Collect_mem_eq Int_commute SigmaD2) 
24827  195 
*) 
23449  196 

197 
ML{*ResAtp.problem_name := "Abstraction__CLF_subset_Collect_Pi"*} 

198 
lemma 

199 
"(cl,f) \<in> CLF ==> 

200 
CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> 

201 
f \<in> pset cl \<rightarrow> pset cl" 

24827  202 
by auto 
203 
(*??no longer terminates, with combinators 

23449  204 
by (metis Collect_mem_eq SigmaD2 subsetD) 
24827  205 
*) 
23449  206 

207 
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi"*} 

208 
lemma 

209 
"(cl,f) \<in> CLF ==> 

210 
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 

211 
f \<in> pset cl \<rightarrow> pset cl" 

24827  212 
by auto 
213 
(*??no longer terminates, with combinators 

23449  214 
by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE) 
24827  215 
*) 
23449  216 

217 
ML{*ResAtp.problem_name := "Abstraction__CLF_eq_Collect_Pi_mono"*} 

218 
lemma 

219 
"(cl,f) \<in> CLF ==> 

220 
CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) ==> 

221 
(f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))" 

222 
by auto 

223 

224 
ML{*ResAtp.problem_name := "Abstraction__map_eq_zipA"*} 

225 
lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)" 

226 
apply (induct xs) 

227 
(*sledgehammer*) 

228 
apply auto 

229 
done 

230 

231 
ML{*ResAtp.problem_name := "Abstraction__map_eq_zipB"*} 

232 
lemma "map (%w. (w > w, w \<times> w)) xs = 

233 
zip (map (%w. w > w) xs) (map (%w. w \<times> w) xs)" 

234 
apply (induct xs) 

235 
(*sledgehammer*) 

236 
apply auto 

237 
done 

238 

239 
ML{*ResAtp.problem_name := "Abstraction__image_evenA"*} 

240 
lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x > Suc(f x) \<in> A)"; 

241 
(*sledgehammer*) 

242 
by auto 

243 

244 
ML{*ResAtp.problem_name := "Abstraction__image_evenB"*} 

245 
lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A 

246 
==> (\<forall>x. even x > f (f (Suc(f x))) \<in> A)"; 

247 
(*sledgehammer*) 

248 
by auto 

249 

250 
ML{*ResAtp.problem_name := "Abstraction__image_curry"*} 

251 
lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)" 

252 
(*sledgehammer*) 

253 
by auto 

254 

255 
ML{*ResAtp.problem_name := "Abstraction__image_TimesA"*} 

256 
lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)" 

257 
(*sledgehammer*) 

258 
apply (rule equalityI) 

259 
(***Even the two inclusions are far too difficult 

260 
ML{*ResAtp.problem_name := "Abstraction__image_TimesA_simpler"*} 

261 
***) 

262 
apply (rule subsetI) 

263 
apply (erule imageE) 

264 
(*V manages from here with help: Abstraction__image_TimesA_simpler_1_b.p*) 

265 
apply (erule ssubst) 

266 
apply (erule SigmaE) 

267 
(*V manages from here: Abstraction__image_TimesA_simpler_1_a.p*) 

268 
apply (erule ssubst) 

269 
apply (subst split_conv) 

270 
apply (rule SigmaI) 

271 
apply (erule imageI) + 

272 
txt{*subgoal 2*} 

273 
apply (clarify ); 

274 
apply (simp add: ); 

275 
apply (rule rev_image_eqI) 

276 
apply (blast intro: elim:); 

277 
apply (simp add: ); 

278 
done 

279 

280 
(*Given the difficulty of the previous problem, these two are probably 

281 
impossible*) 

282 

283 
ML{*ResAtp.problem_name := "Abstraction__image_TimesB"*} 

284 
lemma image_TimesB: 

285 
"(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)" 

286 
(*sledgehammer*) 

287 
by force 

288 

289 
ML{*ResAtp.problem_name := "Abstraction__image_TimesC"*} 

290 
lemma image_TimesC: 

291 
"(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = 

292 
((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" 

293 
(*sledgehammer*) 

294 
by auto 

295 

296 
end 