author  ballarin 
Wed, 19 Jul 2006 19:25:58 +0200  
changeset 20168  ed7bced29e1b 
parent 20140  98acc6d0fab6 
child 23894  1a4167d761ac 
permissions  rwrr 
17456  1 
(* Title: CCL/Type.thy 
0  2 
ID: $Id$ 
3 
Author: Martin Coen 

4 
Copyright 1993 University of Cambridge 

5 
*) 

6 

17456  7 
header {* Types in CCL are defined as sets of terms *} 
8 

9 
theory Type 

10 
imports Term 

11 
begin 

0  12 

13 
consts 

14 

15 
Subtype :: "['a set, 'a => o] => 'a set" 

16 
Bool :: "i set" 

17 
Unit :: "i set" 

999
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

18 
"+" :: "[i set, i set] => i set" (infixr 55) 
0  19 
Pi :: "[i set, i => i set] => i set" 
20 
Sigma :: "[i set, i => i set] => i set" 

21 
Nat :: "i set" 

22 
List :: "i set => i set" 

23 
Lists :: "i set => i set" 

24 
ILists :: "i set => i set" 

999
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

25 
TAll :: "(i set => i set) => i set" (binder "TALL " 55) 
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

26 
TEx :: "(i set => i set) => i set" (binder "TEX " 55) 
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

27 
Lift :: "i set => i set" ("(3[_])") 
0  28 

29 
SPLIT :: "[i, [i, i] => i set] => i set" 

30 

14765  31 
syntax 
999
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

32 
"@Pi" :: "[idt, i set, i set] => i set" ("(3PROD _:_./ _)" 
1474  33 
[0,0,60] 60) 
999
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

34 

9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

35 
"@Sigma" :: "[idt, i set, i set] => i set" ("(3SUM _:_./ _)" 
1474  36 
[0,0,60] 60) 
17456  37 

999
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

38 
"@>" :: "[i set, i set] => i set" ("(_ >/ _)" [54, 53] 53) 
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

39 
"@*" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55) 
9bf3816298d0
Gave tighter priorities to SUM and PROD to reduce ambiguities.
lcp
parents:
22
diff
changeset

40 
"@Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})") 
0  41 

42 
translations 

43 
"PROD x:A. B" => "Pi(A, %x. B)" 

17782  44 
"A > B" => "Pi(A, %_. B)" 
0  45 
"SUM x:A. B" => "Sigma(A, %x. B)" 
17782  46 
"A * B" => "Sigma(A, %_. B)" 
0  47 
"{x: A. B}" == "Subtype(A, %x. B)" 
48 

17456  49 
print_translation {* 
50 
[("Pi", dependent_tr' ("@Pi", "@>")), 

51 
("Sigma", dependent_tr' ("@Sigma", "@*"))] *} 

0  52 

17456  53 
axioms 
54 
Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}" 

55 
Unit_def: "Unit == {x. x=one}" 

56 
Bool_def: "Bool == {x. x=true  x=false}" 

57 
Plus_def: "A+B == {x. (EX a:A. x=inl(a))  (EX b:B. x=inr(b))}" 

58 
Pi_def: "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}" 

59 
Sigma_def: "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}" 

60 
Nat_def: "Nat == lfp(% X. Unit + X)" 

61 
List_def: "List(A) == lfp(% X. Unit + A*X)" 

0  62 

17456  63 
Lists_def: "Lists(A) == gfp(% X. Unit + A*X)" 
64 
ILists_def: "ILists(A) == gfp(% X.{} + A*X)" 

0  65 

17456  66 
Tall_def: "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})" 
67 
Tex_def: "TEX X. B(X) == Union({X. EX Y. X=B(Y)})" 

68 
Lift_def: "[A] == A Un {bot}" 

0  69 

17456  70 
SPLIT_def: "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})" 
71 

20140  72 

73 
lemmas simp_type_defs = 

74 
Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def Tall_def Tex_def 

75 
and ind_type_defs = Nat_def List_def 

76 
and simp_data_defs = one_def inl_def inr_def 

77 
and ind_data_defs = zero_def succ_def nil_def cons_def 

78 

79 
lemma subsetXH: "A <= B <> (ALL x. x:A > x:B)" 

80 
by blast 

81 

82 

83 
subsection {* Exhaustion Rules *} 

84 

85 
lemma EmptyXH: "!!a. a : {} <> False" 

86 
and SubtypeXH: "!!a A P. a : {x:A. P(x)} <> (a:A & P(a))" 

87 
and UnitXH: "!!a. a : Unit <> a=one" 

88 
and BoolXH: "!!a. a : Bool <> a=true  a=false" 

89 
and PlusXH: "!!a A B. a : A+B <> (EX x:A. a=inl(x))  (EX x:B. a=inr(x))" 

90 
and PiXH: "!!a A B. a : PROD x:A. B(x) <> (EX b. a=lam x. b(x) & (ALL x:A. b(x):B(x)))" 

91 
and SgXH: "!!a A B. a : SUM x:A. B(x) <> (EX x:A. EX y:B(x).a=<x,y>)" 

92 
unfolding simp_type_defs by blast+ 

93 

94 
lemmas XHs = EmptyXH SubtypeXH UnitXH BoolXH PlusXH PiXH SgXH 

95 

96 
lemma LiftXH: "a : [A] <> (a=bot  a:A)" 

97 
and TallXH: "a : TALL X. B(X) <> (ALL X. a:B(X))" 

98 
and TexXH: "a : TEX X. B(X) <> (EX X. a:B(X))" 

99 
unfolding simp_type_defs by blast+ 

100 

101 
ML {* 

102 
bind_thms ("case_rls", XH_to_Es (thms "XHs")); 

103 
*} 

104 

105 

106 
subsection {* Canonical Type Rules *} 

107 

108 
lemma oneT: "one : Unit" 

109 
and trueT: "true : Bool" 

110 
and falseT: "false : Bool" 

111 
and lamT: "!!b B. [ !!x. x:A ==> b(x):B(x) ] ==> lam x. b(x) : Pi(A,B)" 

112 
and pairT: "!!b B. [ a:A; b:B(a) ] ==> <a,b>:Sigma(A,B)" 

113 
and inlT: "a:A ==> inl(a) : A+B" 

114 
and inrT: "b:B ==> inr(b) : A+B" 

115 
by (blast intro: XHs [THEN iffD2])+ 

116 

117 
lemmas canTs = oneT trueT falseT pairT lamT inlT inrT 

118 

119 

120 
subsection {* NonCanonical Type Rules *} 

121 

122 
lemma lem: "[ a:B(u); u=v ] ==> a : B(v)" 

123 
by blast 

124 

125 

126 
ML {* 

127 
local 

128 
val lemma = thm "lem" 

129 
val bspec = thm "bspec" 

130 
val bexE = thm "bexE" 

131 
in 

132 

133 
fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s 

134 
(fn major::prems => [(resolve_tac ([major] RL top_crls) 1), 

135 
(REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))), 

136 
(ALLGOALS (asm_simp_tac (simpset ()))), 

137 
(ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' 

138 
etac bspec )), 

139 
(safe_tac (claset () addSIs prems))]) 

140 

141 
val ncanT_tac = mk_ncanT_tac (the_context ()) [] case_rls case_rls 

142 
end 

143 
*} 

144 

145 
ML {* 

146 

147 
bind_thm ("ifT", ncanT_tac 

148 
"[ b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) ] ==> if b then t else u : A(b)"); 

149 

150 
bind_thm ("applyT", ncanT_tac "[ f : Pi(A,B); a:A ] ==> f ` a : B(a)"); 

151 

152 
bind_thm ("splitT", ncanT_tac 

153 
"[ p:Sigma(A,B); !!x y. [ x:A; y:B(x); p=<x,y> ] ==> c(x,y):C(<x,y>) ] ==> split(p,c):C(p)"); 

154 

155 
bind_thm ("whenT", ncanT_tac 

156 
"[ p:A+B; !!x.[ x:A; p=inl(x) ] ==> a(x):C(inl(x)); !!y.[ y:B; p=inr(y) ] ==> b(y):C(inr(y)) ] ==> when(p,a,b) : C(p)"); 

157 
*} 

158 

159 
lemmas ncanTs = ifT applyT splitT whenT 

160 

161 

162 
subsection {* Subtypes *} 

163 

164 
lemma SubtypeD1: "a : Subtype(A, P) ==> a : A" 

165 
and SubtypeD2: "a : Subtype(A, P) ==> P(a)" 

166 
by (simp_all add: SubtypeXH) 

167 

168 
lemma SubtypeI: "[ a:A; P(a) ] ==> a : {x:A. P(x)}" 

169 
by (simp add: SubtypeXH) 

170 

171 
lemma SubtypeE: "[ a : {x:A. P(x)}; [ a:A; P(a) ] ==> Q ] ==> Q" 

172 
by (simp add: SubtypeXH) 

173 

174 

175 
subsection {* Monotonicity *} 

176 

177 
lemma idM: "mono (%X. X)" 

178 
apply (rule monoI) 

179 
apply assumption 

180 
done 

181 

182 
lemma constM: "mono(%X. A)" 

183 
apply (rule monoI) 

184 
apply (rule subset_refl) 

185 
done 

186 

187 
lemma "mono(%X. A(X)) ==> mono(%X.[A(X)])" 

188 
apply (rule subsetI [THEN monoI]) 

189 
apply (drule LiftXH [THEN iffD1]) 

190 
apply (erule disjE) 

191 
apply (erule disjI1 [THEN LiftXH [THEN iffD2]]) 

192 
apply (rule disjI2 [THEN LiftXH [THEN iffD2]]) 

193 
apply (drule (1) monoD) 

194 
apply blast 

195 
done 

196 

197 
lemma SgM: 

198 
"[ mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) ] ==> 

199 
mono(%X. Sigma(A(X),B(X)))" 

200 
by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls 

201 
dest!: monoD [THEN subsetD]) 

202 

203 
lemma PiM: 

204 
"[ !!x. x:A ==> mono(%X. B(X,x)) ] ==> mono(%X. Pi(A,B(X)))" 

205 
by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls 

206 
dest!: monoD [THEN subsetD]) 

207 

208 
lemma PlusM: 

209 
"[ mono(%X. A(X)); mono(%X. B(X)) ] ==> mono(%X. A(X)+B(X))" 

210 
by (blast intro!: subsetI [THEN monoI] canTs elim!: case_rls 

211 
dest!: monoD [THEN subsetD]) 

212 

213 

214 
subsection {* Recursive types *} 

215 

216 
subsubsection {* Conversion Rules for Fixed Points via monotonicity and Tarski *} 

217 

218 
lemma NatM: "mono(%X. Unit+X)"; 

219 
apply (rule PlusM constM idM)+ 

220 
done 

221 

222 
lemma def_NatB: "Nat = Unit + Nat" 

223 
apply (rule def_lfp_Tarski [OF Nat_def]) 

224 
apply (rule NatM) 

225 
done 

226 

227 
lemma ListM: "mono(%X.(Unit+Sigma(A,%y. X)))" 

228 
apply (rule PlusM SgM constM idM)+ 

229 
done 

230 

231 
lemma def_ListB: "List(A) = Unit + A * List(A)" 

232 
apply (rule def_lfp_Tarski [OF List_def]) 

233 
apply (rule ListM) 

234 
done 

235 

236 
lemma def_ListsB: "Lists(A) = Unit + A * Lists(A)" 

237 
apply (rule def_gfp_Tarski [OF Lists_def]) 

238 
apply (rule ListM) 

239 
done 

240 

241 
lemma IListsM: "mono(%X.({} + Sigma(A,%y. X)))" 

242 
apply (rule PlusM SgM constM idM)+ 

243 
done 

244 

245 
lemma def_IListsB: "ILists(A) = {} + A * ILists(A)" 

246 
apply (rule def_gfp_Tarski [OF ILists_def]) 

247 
apply (rule IListsM) 

248 
done 

249 

250 
lemmas ind_type_eqs = def_NatB def_ListB def_ListsB def_IListsB 

251 

252 

253 
subsection {* Exhaustion Rules *} 

254 

255 
lemma NatXH: "a : Nat <> (a=zero  (EX x:Nat. a=succ(x)))" 

256 
and ListXH: "a : List(A) <> (a=[]  (EX x:A. EX xs:List(A).a=x$xs))" 

257 
and ListsXH: "a : Lists(A) <> (a=[]  (EX x:A. EX xs:Lists(A).a=x$xs))" 

258 
and IListsXH: "a : ILists(A) <> (EX x:A. EX xs:ILists(A).a=x$xs)" 

259 
unfolding ind_data_defs 

260 
by (rule ind_type_eqs [THEN XHlemma1], blast intro!: canTs elim!: case_rls)+ 

261 

262 
lemmas iXHs = NatXH ListXH 

263 

264 
ML {* bind_thms ("icase_rls", XH_to_Es (thms "iXHs")) *} 

265 

266 

267 
subsection {* Type Rules *} 

268 

269 
lemma zeroT: "zero : Nat" 

270 
and succT: "n:Nat ==> succ(n) : Nat" 

271 
and nilT: "[] : List(A)" 

272 
and consT: "[ h:A; t:List(A) ] ==> h$t : List(A)" 

273 
by (blast intro: iXHs [THEN iffD2])+ 

274 

275 
lemmas icanTs = zeroT succT nilT consT 

276 

277 
ML {* 

278 
val incanT_tac = mk_ncanT_tac (the_context ()) [] (thms "icase_rls") (thms "case_rls"); 

279 

280 
bind_thm ("ncaseT", incanT_tac 

281 
"[ n:Nat; n=zero ==> b:C(zero); !!x.[ x:Nat; n=succ(x) ] ==> c(x):C(succ(x)) ] ==> ncase(n,b,c) : C(n)"); 

282 

283 
bind_thm ("lcaseT", incanT_tac 

284 
"[ l:List(A); l=[] ==> b:C([]); !!h t.[ h:A; t:List(A); l=h$t ] ==> c(h,t):C(h$t) ] ==> lcase(l,b,c) : C(l)"); 

285 
*} 

286 

287 
lemmas incanTs = ncaseT lcaseT 

288 

289 

290 
subsection {* Induction Rules *} 

291 

292 
lemmas ind_Ms = NatM ListM 

293 

294 
lemma Nat_ind: "[ n:Nat; P(zero); !!x.[ x:Nat; P(x) ] ==> P(succ(x)) ] ==> P(n)" 

295 
apply (unfold ind_data_defs) 

296 
apply (erule def_induct [OF Nat_def _ NatM]) 

297 
apply (blast intro: canTs elim!: case_rls) 

298 
done 

299 

300 
lemma List_ind: 

301 
"[ l:List(A); P([]); !!x xs.[ x:A; xs:List(A); P(xs) ] ==> P(x$xs) ] ==> P(l)" 

302 
apply (unfold ind_data_defs) 

303 
apply (erule def_induct [OF List_def _ ListM]) 

304 
apply (blast intro: canTs elim!: case_rls) 

305 
done 

306 

307 
lemmas inds = Nat_ind List_ind 

308 

309 

310 
subsection {* Primitive Recursive Rules *} 

311 

312 
lemma nrecT: 

313 
"[ n:Nat; b:C(zero); 

314 
!!x g.[ x:Nat; g:C(x) ] ==> c(x,g):C(succ(x)) ] ==> 

315 
nrec(n,b,c) : C(n)" 

316 
by (erule Nat_ind) auto 

317 

318 
lemma lrecT: 

319 
"[ l:List(A); b:C([]); 

320 
!!x xs g.[ x:A; xs:List(A); g:C(xs) ] ==> c(x,xs,g):C(x$xs) ] ==> 

321 
lrec(l,b,c) : C(l)" 

322 
by (erule List_ind) auto 

323 

324 
lemmas precTs = nrecT lrecT 

325 

326 

327 
subsection {* Theorem proving *} 

328 

329 
lemma SgE2: 

330 
"[ <a,b> : Sigma(A,B); [ a:A; b:B(a) ] ==> P ] ==> P" 

331 
unfolding SgXH by blast 

332 

333 
(* General theorem proving ignores noncanonical termformers, *) 

334 
(*  intro rules are type rules for canonical terms *) 

335 
(*  elim rules are case rules (no noncanonical terms appear) *) 

336 

337 
ML {* bind_thms ("XHEs", XH_to_Es (thms "XHs")) *} 

338 

339 
lemmas [intro!] = SubtypeI canTs icanTs 

340 
and [elim!] = SubtypeE XHEs 

341 

342 

343 
subsection {* Infinite Data Types *} 

344 

345 
lemma lfp_subset_gfp: "mono(f) ==> lfp(f) <= gfp(f)" 

346 
apply (rule lfp_lowerbound [THEN subset_trans]) 

347 
apply (erule gfp_lemma3) 

348 
apply (rule subset_refl) 

349 
done 

350 

351 
lemma gfpI: 

352 
assumes "a:A" 

353 
and "!!x X.[ x:A; ALL y:A. t(y):X ] ==> t(x) : B(X)" 

354 
shows "t(a) : gfp(B)" 

355 
apply (rule coinduct) 

356 
apply (rule_tac P = "%x. EX y:A. x=t (y)" in CollectI) 

357 
apply (blast intro!: prems)+ 

358 
done 

359 

360 
lemma def_gfpI: 

361 
"[ C==gfp(B); a:A; !!x X.[ x:A; ALL y:A. t(y):X ] ==> t(x) : B(X) ] ==> 

362 
t(a) : C" 

363 
apply unfold 

364 
apply (erule gfpI) 

365 
apply blast 

366 
done 

367 

368 
(* EG *) 

369 
lemma "letrec g x be zero$g(x) in g(bot) : Lists(Nat)" 

370 
apply (rule refl [THEN UnitXH [THEN iffD2], THEN Lists_def [THEN def_gfpI]]) 

371 
apply (subst letrecB) 

372 
apply (unfold cons_def) 

373 
apply blast 

374 
done 

375 

376 

377 
subsection {* Lemmas and tactics for using the rule @{text 

378 
"coinduct3"} on @{text "[="} and @{text "="} *} 

379 

380 
lemma lfpI: "[ mono(f); a : f(lfp(f)) ] ==> a : lfp(f)" 

381 
apply (erule lfp_Tarski [THEN ssubst]) 

382 
apply assumption 

383 
done 

384 

385 
lemma ssubst_single: "[ a=a'; a' : A ] ==> a : A" 

386 
by simp 

387 

388 
lemma ssubst_pair: "[ a=a'; b=b'; <a',b'> : A ] ==> <a,b> : A" 

389 
by simp 

390 

391 

392 
(***) 

393 

394 
ML {* 

395 

396 
local 

397 
val lfpI = thm "lfpI" 

398 
val coinduct3_mono_lemma = thm "coinduct3_mono_lemma" 

399 
fun mk_thm s = prove_goal (the_context ()) s (fn mono::prems => 

400 
[fast_tac (claset () addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1]) 

401 
in 

402 
val ci3_RI = mk_thm "[ mono(Agen); a : R ] ==> a : lfp(%x. Agen(x) Un R Un A)" 

403 
val ci3_AgenI = mk_thm "[ mono(Agen); a : Agen(lfp(%x. Agen(x) Un R Un A)) ] ==> a : lfp(%x. Agen(x) Un R Un A)" 

404 
val ci3_AI = mk_thm "[ mono(Agen); a : A ] ==> a : lfp(%x. Agen(x) Un R Un A)" 

405 

406 
fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s 

407 
(fn prems => [rtac (genXH RS iffD2) 1, 

408 
simp_tac (simpset ()) 1, 

409 
TRY (fast_tac (claset () addIs 

410 
([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI] 

411 
@ prems)) 1)]) 

412 
end; 

413 

414 
bind_thm ("ci3_RI", ci3_RI); 

415 
bind_thm ("ci3_AgenI", ci3_AgenI); 

416 
bind_thm ("ci3_AI", ci3_AI); 

417 
*} 

418 

419 

420 
subsection {* POgen *} 

421 

422 
lemma PO_refl: "<a,a> : PO" 

423 
apply (rule po_refl [THEN PO_iff [THEN iffD1]]) 

424 
done 

425 

426 
ML {* 

427 

428 
val POgenIs = map (mk_genIs (the_context ()) (thms "data_defs") (thm "POgenXH") (thm "POgen_mono")) 

429 
["<true,true> : POgen(R)", 

430 
"<false,false> : POgen(R)", 

431 
"[ <a,a'> : R; <b,b'> : R ] ==> <<a,b>,<a',b'>> : POgen(R)", 

432 
"[!!x. <b(x),b'(x)> : R ] ==><lam x. b(x),lam x. b'(x)> : POgen(R)", 

433 
"<one,one> : POgen(R)", 

434 
"<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==> <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))", 

435 
"<b,b'> : lfp(%x. POgen(x) Un R Un PO) ==> <inr(b),inr(b')> : POgen(lfp(%x. POgen(x) Un R Un PO))", 

436 
"<zero,zero> : POgen(lfp(%x. POgen(x) Un R Un PO))", 

437 
"<n,n'> : lfp(%x. POgen(x) Un R Un PO) ==> <succ(n),succ(n')> : POgen(lfp(%x. POgen(x) Un R Un PO))", 

438 
"<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))", 

439 
"[ <h,h'> : lfp(%x. POgen(x) Un R Un PO); <t,t'> : lfp(%x. POgen(x) Un R Un PO) ] ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"]; 

440 

441 
fun POgen_tac (rla,rlb) i = 

442 
SELECT_GOAL (CLASET safe_tac) i THEN 

443 
rtac (rlb RS (rla RS (thm "ssubst_pair"))) i THEN 

444 
(REPEAT (resolve_tac (POgenIs @ [thm "PO_refl" RS (thm "POgen_mono" RS ci3_AI)] @ 

445 
(POgenIs RL [thm "POgen_mono" RS ci3_AgenI]) @ [thm "POgen_mono" RS ci3_RI]) i)); 

446 

447 
*} 

448 

449 

450 
subsection {* EQgen *} 

451 

452 
lemma EQ_refl: "<a,a> : EQ" 

453 
apply (rule refl [THEN EQ_iff [THEN iffD1]]) 

454 
done 

455 

456 
ML {* 

457 

458 
val EQgenIs = map (mk_genIs (the_context ()) (thms "data_defs") (thm "EQgenXH") (thm "EQgen_mono")) 

459 
["<true,true> : EQgen(R)", 

460 
"<false,false> : EQgen(R)", 

461 
"[ <a,a'> : R; <b,b'> : R ] ==> <<a,b>,<a',b'>> : EQgen(R)", 

462 
"[!!x. <b(x),b'(x)> : R ] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)", 

463 
"<one,one> : EQgen(R)", 

464 
"<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", 

465 
"<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==> <inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", 

466 
"<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", 

467 
"<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==> <succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", 

468 
"<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))", 

469 
"[ <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) ] ==> <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"]; 

470 

471 
fun EQgen_raw_tac i = 

472 
(REPEAT (resolve_tac (EQgenIs @ [thm "EQ_refl" RS (thm "EQgen_mono" RS ci3_AI)] @ 

473 
(EQgenIs RL [thm "EQgen_mono" RS ci3_AgenI]) @ [thm "EQgen_mono" RS ci3_RI]) i)) 

474 

475 
(* Goals of the form R <= EQgen(R)  rewrite elements <a,b> : EQgen(R) using rews and *) 

476 
(* then reduce this to a goal <a',b'> : R (hopefully?) *) 

477 
(* rews are rewrite rules that would cause looping in the simpifier *) 

478 

479 
fun EQgen_tac simp_set rews i = 

480 
SELECT_GOAL 

481 
(TRY (CLASET safe_tac) THEN 

482 
resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [thm "ssubst_pair"])) i THEN 

483 
ALLGOALS (simp_tac simp_set) THEN 

484 
ALLGOALS EQgen_raw_tac) i 

485 
*} 

0  486 

487 
end 