author  wenzelm 
Sun, 11 Jan 2009 21:49:59 +0100  
changeset 29450  ac7f67be7f1f 
parent 28272  ed959a0f650b 
child 30607  c3d1590debd8 
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" 

24825  18 
Plus :: "[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 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset

133 
fun mk_ncanT_tac ctxt defs top_crls crls s = prove_goalw (ProofContext.theory_of ctxt) defs s 
20140  134 
(fn major::prems => [(resolve_tac ([major] RL top_crls) 1), 
135 
(REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))), 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset

136 
(ALLGOALS (asm_simp_tac (local_simpset_of ctxt))), 
20140  137 
(ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' 
138 
etac bspec )), 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset

139 
(safe_tac (local_claset_of ctxt addSIs prems))]) 
28272
ed959a0f650b
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
wenzelm
parents:
26342
diff
changeset

140 
end 
ed959a0f650b
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
wenzelm
parents:
26342
diff
changeset

141 
*} 
20140  142 

28272
ed959a0f650b
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
wenzelm
parents:
26342
diff
changeset

143 
ML {* 
ed959a0f650b
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
wenzelm
parents:
26342
diff
changeset

144 
val ncanT_tac = mk_ncanT_tac @{context} [] @{thms case_rls} @{thms case_rls} 
20140  145 
*} 
146 

147 
ML {* 

148 

149 
bind_thm ("ifT", ncanT_tac 

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

151 

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

153 

154 
bind_thm ("splitT", ncanT_tac 

155 
"[ 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)"); 

156 

157 
bind_thm ("whenT", ncanT_tac 

158 
"[ 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)"); 

159 
*} 

160 

161 
lemmas ncanTs = ifT applyT splitT whenT 

162 

163 

164 
subsection {* Subtypes *} 

165 

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

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

168 
by (simp_all add: SubtypeXH) 

169 

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

171 
by (simp add: SubtypeXH) 

172 

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

174 
by (simp add: SubtypeXH) 

175 

176 

177 
subsection {* Monotonicity *} 

178 

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

180 
apply (rule monoI) 

181 
apply assumption 

182 
done 

183 

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

185 
apply (rule monoI) 

186 
apply (rule subset_refl) 

187 
done 

188 

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

190 
apply (rule subsetI [THEN monoI]) 

191 
apply (drule LiftXH [THEN iffD1]) 

192 
apply (erule disjE) 

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

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

195 
apply (drule (1) monoD) 

196 
apply blast 

197 
done 

198 

199 
lemma SgM: 

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

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

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

203 
dest!: monoD [THEN subsetD]) 

204 

205 
lemma PiM: 

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

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

208 
dest!: monoD [THEN subsetD]) 

209 

210 
lemma PlusM: 

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

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

213 
dest!: monoD [THEN subsetD]) 

214 

215 

216 
subsection {* Recursive types *} 

217 

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

219 

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

221 
apply (rule PlusM constM idM)+ 

222 
done 

223 

224 
lemma def_NatB: "Nat = Unit + Nat" 

225 
apply (rule def_lfp_Tarski [OF Nat_def]) 

226 
apply (rule NatM) 

227 
done 

228 

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

230 
apply (rule PlusM SgM constM idM)+ 

231 
done 

232 

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

234 
apply (rule def_lfp_Tarski [OF List_def]) 

235 
apply (rule ListM) 

236 
done 

237 

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

239 
apply (rule def_gfp_Tarski [OF Lists_def]) 

240 
apply (rule ListM) 

241 
done 

242 

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

244 
apply (rule PlusM SgM constM idM)+ 

245 
done 

246 

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

248 
apply (rule def_gfp_Tarski [OF ILists_def]) 

249 
apply (rule IListsM) 

250 
done 

251 

252 
lemmas ind_type_eqs = def_NatB def_ListB def_ListsB def_IListsB 

253 

254 

255 
subsection {* Exhaustion Rules *} 

256 

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

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

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

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

261 
unfolding ind_data_defs 

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

263 

264 
lemmas iXHs = NatXH ListXH 

265 

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

267 

268 

269 
subsection {* Type Rules *} 

270 

271 
lemma zeroT: "zero : Nat" 

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

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

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

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

276 

277 
lemmas icanTs = zeroT succT nilT consT 

278 

279 
ML {* 

28272
ed959a0f650b
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
wenzelm
parents:
26342
diff
changeset

280 
val incanT_tac = mk_ncanT_tac @{context} [] @{thms icase_rls} @{thms case_rls}; 
ed959a0f650b
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
wenzelm
parents:
26342
diff
changeset

281 
*} 
20140  282 

28272
ed959a0f650b
proper thm antiquotations within ML solve obscure context problems (due to update of ML environment);
wenzelm
parents:
26342
diff
changeset

283 
ML {* 
20140  284 
bind_thm ("ncaseT", incanT_tac 
285 
"[ n:Nat; n=zero ==> b:C(zero); !!x.[ x:Nat; n=succ(x) ] ==> c(x):C(succ(x)) ] ==> ncase(n,b,c) : C(n)"); 

286 

287 
bind_thm ("lcaseT", incanT_tac 

288 
"[ 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)"); 

289 
*} 

290 

291 
lemmas incanTs = ncaseT lcaseT 

292 

293 

294 
subsection {* Induction Rules *} 

295 

296 
lemmas ind_Ms = NatM ListM 

297 

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

299 
apply (unfold ind_data_defs) 

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

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

302 
done 

303 

304 
lemma List_ind: 

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

306 
apply (unfold ind_data_defs) 

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

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

309 
done 

310 

311 
lemmas inds = Nat_ind List_ind 

312 

313 

314 
subsection {* Primitive Recursive Rules *} 

315 

316 
lemma nrecT: 

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

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

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

320 
by (erule Nat_ind) auto 

321 

322 
lemma lrecT: 

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

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

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

326 
by (erule List_ind) auto 

327 

328 
lemmas precTs = nrecT lrecT 

329 

330 

331 
subsection {* Theorem proving *} 

332 

333 
lemma SgE2: 

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

335 
unfolding SgXH by blast 

336 

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

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

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

340 

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

342 

343 
lemmas [intro!] = SubtypeI canTs icanTs 

344 
and [elim!] = SubtypeE XHEs 

345 

346 

347 
subsection {* Infinite Data Types *} 

348 

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

350 
apply (rule lfp_lowerbound [THEN subset_trans]) 

351 
apply (erule gfp_lemma3) 

352 
apply (rule subset_refl) 

353 
done 

354 

355 
lemma gfpI: 

356 
assumes "a:A" 

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

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

359 
apply (rule coinduct) 

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

361 
apply (blast intro!: prems)+ 

362 
done 

363 

364 
lemma def_gfpI: 

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

366 
t(a) : C" 

367 
apply unfold 

368 
apply (erule gfpI) 

369 
apply blast 

370 
done 

371 

372 
(* EG *) 

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

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

375 
apply (subst letrecB) 

376 
apply (unfold cons_def) 

377 
apply blast 

378 
done 

379 

380 

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

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

383 

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

385 
apply (erule lfp_Tarski [THEN ssubst]) 

386 
apply assumption 

387 
done 

388 

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

390 
by simp 

391 

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

393 
by simp 

394 

395 

396 
(***) 

397 

398 
ML {* 

399 

400 
local 

401 
val lfpI = thm "lfpI" 

402 
val coinduct3_mono_lemma = thm "coinduct3_mono_lemma" 

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

26342  404 
[fast_tac (@{claset} addIs ((mono RS coinduct3_mono_lemma RS lfpI)::prems)) 1]) 
20140  405 
in 
406 
val ci3_RI = mk_thm "[ mono(Agen); a : R ] ==> a : lfp(%x. Agen(x) Un R Un A)" 

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

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

409 

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

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

26342  412 
SIMPSET' simp_tac 1, 
413 
TRY (fast_tac (@{claset} addIs 

20140  414 
([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI] 
415 
@ prems)) 1)]) 

416 
end; 

417 

418 
bind_thm ("ci3_RI", ci3_RI); 

419 
bind_thm ("ci3_AgenI", ci3_AgenI); 

420 
bind_thm ("ci3_AI", ci3_AI); 

421 
*} 

422 

423 

424 
subsection {* POgen *} 

425 

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

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

428 
done 

429 

430 
ML {* 

431 

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

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

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

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

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

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

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

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

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

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

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

443 
"[ <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))"]; 

444 

445 
fun POgen_tac (rla,rlb) i = 

446 
SELECT_GOAL (CLASET safe_tac) i THEN 

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

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

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

450 

451 
*} 

452 

453 

454 
subsection {* EQgen *} 

455 

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

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

458 
done 

459 

460 
ML {* 

461 

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

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

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

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

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

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

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

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

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

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

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

473 
"[ <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))"]; 

474 

475 
fun EQgen_raw_tac i = 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset

476 
(REPEAT (resolve_tac (EQgenIs @ [@{thm EQ_refl} RS (@{thm EQgen_mono} RS ci3_AI)] @ 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset

477 
(EQgenIs RL [@{thm EQgen_mono} RS ci3_AgenI]) @ [@{thm EQgen_mono} RS ci3_RI]) i)) 
20140  478 

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

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

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

482 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset

483 
fun EQgen_tac ctxt rews i = 
20140  484 
SELECT_GOAL 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset

485 
(TRY (safe_tac (local_claset_of ctxt)) THEN 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset

486 
resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [@{thm ssubst_pair}])) i THEN 
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
20140
diff
changeset

487 
ALLGOALS (simp_tac (local_simpset_of ctxt)) THEN 
20140  488 
ALLGOALS EQgen_raw_tac) i 
489 
*} 

0  490 

491 
end 