author  wenzelm 
Thu, 23 Jul 2009 18:44:09 +0200  
changeset 32149  ef59550a55d3 
parent 32010  cb1a1c94b4cd 
child 32153  a0e57fb1b930 
permissions  rwrr 
17456  1 
(* Title: CCL/Type.thy 
0  2 
Author: Martin Coen 
3 
Copyright 1993 University of Cambridge 

4 
*) 

5 

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

8 
theory Type 

9 
imports Term 

10 
begin 

0  11 

12 
consts 

13 

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

15 
Bool :: "i set" 

16 
Unit :: "i set" 

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

20 
Nat :: "i set" 

21 
List :: "i set => i set" 

22 
Lists :: "i set => i set" 

23 
ILists :: "i set => i set" 

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

24 
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

25 
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

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

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

29 

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

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

33 

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

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

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

37 
"@>" :: "[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

38 
"@*" :: "[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

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

41 
translations 

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

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

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

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

0  51 

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

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

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

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

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

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

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

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

0  61 

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

0  64 

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

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

0  68 

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

20140  71 

72 
lemmas simp_type_defs = 

73 
Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def Tall_def Tex_def 

74 
and ind_type_defs = Nat_def List_def 

75 
and simp_data_defs = one_def inl_def inr_def 

76 
and ind_data_defs = zero_def succ_def nil_def cons_def 

77 

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

79 
by blast 

80 

81 

82 
subsection {* Exhaustion Rules *} 

83 

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

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

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

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

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

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

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

91 
unfolding simp_type_defs by blast+ 

92 

93 
lemmas XHs = EmptyXH SubtypeXH UnitXH BoolXH PlusXH PiXH SgXH 

94 

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

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

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

98 
unfolding simp_type_defs by blast+ 

99 

100 
ML {* 

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

102 
*} 

103 

104 

105 
subsection {* Canonical Type Rules *} 

106 

107 
lemma oneT: "one : Unit" 

108 
and trueT: "true : Bool" 

109 
and falseT: "false : Bool" 

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

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

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

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

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

115 

116 
lemmas canTs = oneT trueT falseT pairT lamT inlT inrT 

117 

118 

119 
subsection {* NonCanonical Type Rules *} 

120 

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

122 
by blast 

123 

124 

125 
ML {* 

126 
local 

127 
val lemma = thm "lem" 

128 
val bspec = thm "bspec" 

129 
val bexE = thm "bexE" 

130 
in 

131 

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

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

32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32010
diff
changeset

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

32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32010
diff
changeset

138 
(safe_tac (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

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

140 
*} 
20140  141 

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

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

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

146 
ML {* 

147 

148 
bind_thm ("ifT", ncanT_tac 

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

150 

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

152 

153 
bind_thm ("splitT", ncanT_tac 

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

155 

156 
bind_thm ("whenT", ncanT_tac 

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

158 
*} 

159 

160 
lemmas ncanTs = ifT applyT splitT whenT 

161 

162 

163 
subsection {* Subtypes *} 

164 

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

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

167 
by (simp_all add: SubtypeXH) 

168 

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

170 
by (simp add: SubtypeXH) 

171 

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

173 
by (simp add: SubtypeXH) 

174 

175 

176 
subsection {* Monotonicity *} 

177 

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

179 
apply (rule monoI) 

180 
apply assumption 

181 
done 

182 

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

184 
apply (rule monoI) 

185 
apply (rule subset_refl) 

186 
done 

187 

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

189 
apply (rule subsetI [THEN monoI]) 

190 
apply (drule LiftXH [THEN iffD1]) 

191 
apply (erule disjE) 

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

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

194 
apply (drule (1) monoD) 

195 
apply blast 

196 
done 

197 

198 
lemma SgM: 

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

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

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

202 
dest!: monoD [THEN subsetD]) 

203 

204 
lemma PiM: 

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

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

207 
dest!: monoD [THEN subsetD]) 

208 

209 
lemma PlusM: 

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

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

212 
dest!: monoD [THEN subsetD]) 

213 

214 

215 
subsection {* Recursive types *} 

216 

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

218 

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

220 
apply (rule PlusM constM idM)+ 

221 
done 

222 

223 
lemma def_NatB: "Nat = Unit + Nat" 

224 
apply (rule def_lfp_Tarski [OF Nat_def]) 

225 
apply (rule NatM) 

226 
done 

227 

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

229 
apply (rule PlusM SgM constM idM)+ 

230 
done 

231 

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

233 
apply (rule def_lfp_Tarski [OF List_def]) 

234 
apply (rule ListM) 

235 
done 

236 

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

238 
apply (rule def_gfp_Tarski [OF Lists_def]) 

239 
apply (rule ListM) 

240 
done 

241 

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

243 
apply (rule PlusM SgM constM idM)+ 

244 
done 

245 

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

247 
apply (rule def_gfp_Tarski [OF ILists_def]) 

248 
apply (rule IListsM) 

249 
done 

250 

251 
lemmas ind_type_eqs = def_NatB def_ListB def_ListsB def_IListsB 

252 

253 

254 
subsection {* Exhaustion Rules *} 

255 

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

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

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

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

260 
unfolding ind_data_defs 

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

262 

263 
lemmas iXHs = NatXH ListXH 

264 

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

266 

267 

268 
subsection {* Type Rules *} 

269 

270 
lemma zeroT: "zero : Nat" 

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

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

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

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

275 

276 
lemmas icanTs = zeroT succT nilT consT 

277 

278 
ML {* 

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

279 
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

280 
*} 
20140  281 

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

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

285 

286 
bind_thm ("lcaseT", incanT_tac 

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

288 
*} 

289 

290 
lemmas incanTs = ncaseT lcaseT 

291 

292 

293 
subsection {* Induction Rules *} 

294 

295 
lemmas ind_Ms = NatM ListM 

296 

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

298 
apply (unfold ind_data_defs) 

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

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

301 
done 

302 

303 
lemma List_ind: 

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

305 
apply (unfold ind_data_defs) 

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

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

308 
done 

309 

310 
lemmas inds = Nat_ind List_ind 

311 

312 

313 
subsection {* Primitive Recursive Rules *} 

314 

315 
lemma nrecT: 

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

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

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

319 
by (erule Nat_ind) auto 

320 

321 
lemma lrecT: 

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

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

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

325 
by (erule List_ind) auto 

326 

327 
lemmas precTs = nrecT lrecT 

328 

329 

330 
subsection {* Theorem proving *} 

331 

332 
lemma SgE2: 

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

334 
unfolding SgXH by blast 

335 

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

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

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

339 

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

341 

342 
lemmas [intro!] = SubtypeI canTs icanTs 

343 
and [elim!] = SubtypeE XHEs 

344 

345 

346 
subsection {* Infinite Data Types *} 

347 

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

349 
apply (rule lfp_lowerbound [THEN subset_trans]) 

350 
apply (erule gfp_lemma3) 

351 
apply (rule subset_refl) 

352 
done 

353 

354 
lemma gfpI: 

355 
assumes "a:A" 

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

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

358 
apply (rule coinduct) 

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

360 
apply (blast intro!: prems)+ 

361 
done 

362 

363 
lemma def_gfpI: 

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

365 
t(a) : C" 

366 
apply unfold 

367 
apply (erule gfpI) 

368 
apply blast 

369 
done 

370 

371 
(* EG *) 

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

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

374 
apply (subst letrecB) 

375 
apply (unfold cons_def) 

376 
apply blast 

377 
done 

378 

379 

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

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

382 

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

384 
apply (erule lfp_Tarski [THEN ssubst]) 

385 
apply assumption 

386 
done 

387 

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

389 
by simp 

390 

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

392 
by simp 

393 

394 

395 
(***) 

396 

397 
ML {* 

398 

399 
local 

400 
val lfpI = thm "lfpI" 

401 
val coinduct3_mono_lemma = thm "coinduct3_mono_lemma" 

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

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

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

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

408 

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

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

32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32010
diff
changeset

411 
simp_tac (global_simpset_of thy) 1, 
26342  412 
TRY (fast_tac (@{claset} addIs 
20140  413 
([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI] 
414 
@ prems)) 1)]) 

415 
end; 

416 

417 
bind_thm ("ci3_RI", ci3_RI); 

418 
bind_thm ("ci3_AgenI", ci3_AgenI); 

419 
bind_thm ("ci3_AI", ci3_AI); 

420 
*} 

421 

422 

423 
subsection {* POgen *} 

424 

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

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

427 
done 

428 

429 
ML {* 

430 

32010  431 
val POgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm POgenXH} @{thm POgen_mono}) 
20140  432 
["<true,true> : POgen(R)", 
433 
"<false,false> : POgen(R)", 

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

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

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

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

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

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

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

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

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

443 

30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
28272
diff
changeset

444 
fun POgen_tac ctxt (rla,rlb) i = 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32010
diff
changeset

445 
SELECT_GOAL (safe_tac (claset_of ctxt)) i THEN 
32010  446 
rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN 
447 
(REPEAT (resolve_tac (POgenIs @ [@{thm PO_refl} RS (@{thm POgen_mono} RS ci3_AI)] @ 

448 
(POgenIs RL [@{thm POgen_mono} RS ci3_AgenI]) @ [@{thm POgen_mono} RS ci3_RI]) i)); 

20140  449 

450 
*} 

451 

452 

453 
subsection {* EQgen *} 

454 

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

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

457 
done 

458 

459 
ML {* 

460 

32010  461 
val EQgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm EQgenXH} @{thm EQgen_mono}) 
20140  462 
["<true,true> : EQgen(R)", 
463 
"<false,false> : EQgen(R)", 

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

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

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

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

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

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

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

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

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

473 

474 
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

475 
(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

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

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

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

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

481 

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

482 
fun EQgen_tac ctxt rews i = 
20140  483 
SELECT_GOAL 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32010
diff
changeset

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

485 
resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [@{thm ssubst_pair}])) i THEN 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
32010
diff
changeset

486 
ALLGOALS (simp_tac (simpset_of ctxt)) THEN 
20140  487 
ALLGOALS EQgen_raw_tac) i 
488 
*} 

0  489 

490 
end 