author  wenzelm 
Wed, 03 Nov 2010 21:53:56 +0100  
changeset 40335  3e4bb6e7c3ca 
parent 39159  0dec18004e75 
child 41526  54b4686704af 
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 
35113  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 

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

35113  37 
"_arrow" :: "[i set, i set] => i set" ("(_ >/ _)" [54, 53] 53) 
38 
"_star" :: "[i set, i set] => i set" ("(_ */ _)" [56, 55] 55) 

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

0  40 

41 
translations 

35054  42 
"PROD x:A. B" => "CONST Pi(A, %x. B)" 
43 
"A > B" => "CONST Pi(A, %_. B)" 

44 
"SUM x:A. B" => "CONST Sigma(A, %x. B)" 

45 
"A * B" => "CONST Sigma(A, %_. B)" 

46 
"{x: A. B}" == "CONST Subtype(A, %x. B)" 

0  47 

17456  48 
print_translation {* 
35113  49 
[(@{const_syntax Pi}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})), 
50 
(@{const_syntax Sigma}, dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))] 

51 
*} 

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 {* 

39159  102 
bind_thms ("case_rls", XH_to_Es @{thms XHs}); 
20140  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 {* 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

127 
fun mk_ncanT_tac top_crls crls = 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

128 
SUBPROOF (fn {context = ctxt, prems = major :: prems, ...} => 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

129 
resolve_tac ([major] RL top_crls) 1 THEN 
35409  130 
REPEAT_SOME (eresolve_tac (crls @ [@{thm exE}, @{thm bexE}, @{thm conjE}, @{thm disjE}])) THEN 
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

131 
ALLGOALS (asm_simp_tac (simpset_of ctxt)) THEN 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

132 
ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

133 
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

134 
*} 
20140  135 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

136 
method_setup ncanT = {* 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

137 
Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls}) 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

138 
*} "" 
20140  139 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

140 
lemma ifT: 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

141 
"[ b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) ] ==> 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

142 
if b then t else u : A(b)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

143 
by ncanT 
20140  144 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

145 
lemma applyT: "[ f : Pi(A,B); a:A ] ==> f ` a : B(a)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

146 
by ncanT 
20140  147 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

148 
lemma splitT: 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

149 
"[ p:Sigma(A,B); !!x y. [ x:A; y:B(x); p=<x,y> ] ==> c(x,y):C(<x,y>) ] 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

150 
==> split(p,c):C(p)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

151 
by ncanT 
20140  152 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

153 
lemma whenT: 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

154 
"[ p:A+B; !!x.[ x:A; p=inl(x) ] ==> a(x):C(inl(x)); !!y.[ y:B; p=inr(y) ] 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

155 
==> b(y):C(inr(y)) ] ==> when(p,a,b) : C(p)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

156 
by ncanT 
20140  157 

158 
lemmas ncanTs = ifT applyT splitT whenT 

159 

160 

161 
subsection {* Subtypes *} 

162 

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

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

165 
by (simp_all add: SubtypeXH) 

166 

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

168 
by (simp add: SubtypeXH) 

169 

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

171 
by (simp add: SubtypeXH) 

172 

173 

174 
subsection {* Monotonicity *} 

175 

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

177 
apply (rule monoI) 

178 
apply assumption 

179 
done 

180 

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

182 
apply (rule monoI) 

183 
apply (rule subset_refl) 

184 
done 

185 

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

187 
apply (rule subsetI [THEN monoI]) 

188 
apply (drule LiftXH [THEN iffD1]) 

189 
apply (erule disjE) 

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

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

192 
apply (drule (1) monoD) 

193 
apply blast 

194 
done 

195 

196 
lemma SgM: 

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

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

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

200 
dest!: monoD [THEN subsetD]) 

201 

202 
lemma PiM: 

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

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

205 
dest!: monoD [THEN subsetD]) 

206 

207 
lemma PlusM: 

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

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

210 
dest!: monoD [THEN subsetD]) 

211 

212 

213 
subsection {* Recursive types *} 

214 

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

216 

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

218 
apply (rule PlusM constM idM)+ 

219 
done 

220 

221 
lemma def_NatB: "Nat = Unit + Nat" 

222 
apply (rule def_lfp_Tarski [OF Nat_def]) 

223 
apply (rule NatM) 

224 
done 

225 

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

227 
apply (rule PlusM SgM constM idM)+ 

228 
done 

229 

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

231 
apply (rule def_lfp_Tarski [OF List_def]) 

232 
apply (rule ListM) 

233 
done 

234 

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

236 
apply (rule def_gfp_Tarski [OF Lists_def]) 

237 
apply (rule ListM) 

238 
done 

239 

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

241 
apply (rule PlusM SgM constM idM)+ 

242 
done 

243 

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

245 
apply (rule def_gfp_Tarski [OF ILists_def]) 

246 
apply (rule IListsM) 

247 
done 

248 

249 
lemmas ind_type_eqs = def_NatB def_ListB def_ListsB def_IListsB 

250 

251 

252 
subsection {* Exhaustion Rules *} 

253 

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

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

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

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

258 
unfolding ind_data_defs 

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

260 

261 
lemmas iXHs = NatXH ListXH 

262 

39159  263 
ML {* bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *} 
20140  264 

265 

266 
subsection {* Type Rules *} 

267 

268 
lemma zeroT: "zero : Nat" 

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

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

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

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

273 

274 
lemmas icanTs = zeroT succT nilT consT 

275 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

276 

a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

277 
method_setup incanT = {* 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

278 
Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms icase_rls} @{thms case_rls}) 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

279 
*} "" 
20140  280 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

281 
lemma ncaseT: 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

282 
"[ n:Nat; n=zero ==> b:C(zero); !!x.[ x:Nat; n=succ(x) ] ==> c(x):C(succ(x)) ] 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

283 
==> ncase(n,b,c) : C(n)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

284 
by incanT 
20140  285 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

286 
lemma lcaseT: 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

287 
"[ l:List(A); l=[] ==> b:C([]); !!h t.[ h:A; t:List(A); l=h$t ] ==> 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

288 
c(h,t):C(h$t) ] ==> lcase(l,b,c) : C(l)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

289 
by incanT 
20140  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 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

341 
ML {* bind_thms ("XHEs", XH_to_Es @{thms XHs}) *} 
20140  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 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

396 
ML {* 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

397 
val coinduct3_tac = SUBPROOF (fn {context = ctxt, prems = mono :: prems, ...} => 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

398 
(fast_tac (claset_of ctxt addIs 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

399 
(mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1)); 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

400 
*} 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

401 

a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

402 
method_setup coinduct3 = {* 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

403 
Scan.succeed (SIMPLE_METHOD' o coinduct3_tac) 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

404 
*} "" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

405 

a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

406 
lemma ci3_RI: "[ mono(Agen); a : R ] ==> a : lfp(%x. Agen(x) Un R Un A)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

407 
by coinduct3 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

408 

a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

409 
lemma ci3_AgenI: "[ mono(Agen); a : Agen(lfp(%x. Agen(x) Un R Un A)) ] ==> 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

410 
a : lfp(%x. Agen(x) Un R Un A)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

411 
by coinduct3 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

412 

a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

413 
lemma ci3_AI: "[ mono(Agen); a : A ] ==> a : lfp(%x. Agen(x) Un R Un A)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

414 
by coinduct3 
20140  415 

416 
ML {* 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

417 
fun genIs_tac ctxt genXH gen_mono = 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

418 
rtac (genXH RS iffD2) THEN' 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

419 
simp_tac (simpset_of ctxt) THEN' 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

420 
TRY o fast_tac (claset_of ctxt addIs 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

421 
[genXH RS iffD2, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}]) 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

422 
*} 
20140  423 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

424 
method_setup genIs = {* 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

425 
Attrib.thm  Attrib.thm >> (fn (genXH, gen_mono) => fn ctxt => 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

426 
SIMPLE_METHOD' (genIs_tac ctxt genXH gen_mono)) 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

427 
*} "" 
20140  428 

429 

430 
subsection {* POgen *} 

431 

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

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

433 
by (rule po_refl [THEN PO_iff [THEN iffD1]]) 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

434 

a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

435 
lemma POgenIs: 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

436 
"<true,true> : POgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

437 
"<false,false> : POgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

438 
"[ <a,a'> : R; <b,b'> : R ] ==> <<a,b>,<a',b'>> : POgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

439 
"!!b b'. [!!x. <b(x),b'(x)> : R ] ==><lam x. b(x),lam x. b'(x)> : POgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

440 
"<one,one> : POgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

441 
"<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==> 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

442 
<inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

443 
"<b,b'> : lfp(%x. POgen(x) Un R Un PO) ==> 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

444 
<inr(b),inr(b')> : POgen(lfp(%x. POgen(x) Un R Un PO))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

445 
"<zero,zero> : POgen(lfp(%x. POgen(x) Un R Un PO))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

446 
"<n,n'> : lfp(%x. POgen(x) Un R Un PO) ==> 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

447 
<succ(n),succ(n')> : POgen(lfp(%x. POgen(x) Un R Un PO))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

448 
"<[],[]> : POgen(lfp(%x. POgen(x) Un R Un PO))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

449 
"[ <h,h'> : lfp(%x. POgen(x) Un R Un PO); <t,t'> : lfp(%x. POgen(x) Un R Un PO) ] 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

450 
==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

451 
unfolding data_defs by (genIs POgenXH POgen_mono)+ 
20140  452 

453 
ML {* 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

454 
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

455 
SELECT_GOAL (safe_tac (claset_of ctxt)) i THEN 
32010  456 
rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN 
32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

457 
(REPEAT (resolve_tac 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

458 
(@{thms POgenIs} @ [@{thm PO_refl} RS (@{thm POgen_mono} RS @{thm ci3_AI})] @ 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

459 
(@{thms POgenIs} RL [@{thm POgen_mono} RS @{thm ci3_AgenI}]) @ 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

460 
[@{thm POgen_mono} RS @{thm ci3_RI}]) i)) 
20140  461 
*} 
462 

463 

464 
subsection {* EQgen *} 

465 

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

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

467 
by (rule refl [THEN EQ_iff [THEN iffD1]]) 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

468 

a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

469 
lemma EQgenIs: 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

470 
"<true,true> : EQgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

471 
"<false,false> : EQgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

472 
"[ <a,a'> : R; <b,b'> : R ] ==> <<a,b>,<a',b'>> : EQgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

473 
"!!b b'. [!!x. <b(x),b'(x)> : R ] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

474 
"<one,one> : EQgen(R)" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

475 
"<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

476 
<inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

477 
"<b,b'> : lfp(%x. EQgen(x) Un R Un EQ) ==> 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

478 
<inr(b),inr(b')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

479 
"<zero,zero> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

480 
"<n,n'> : lfp(%x. EQgen(x) Un R Un EQ) ==> 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

481 
<succ(n),succ(n')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

482 
"<[],[]> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

483 
"[ <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) ] 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

484 
==> <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))" 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

485 
unfolding data_defs by (genIs EQgenXH EQgen_mono)+ 
20140  486 

487 
ML {* 

488 
fun EQgen_raw_tac i = 

32153
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

489 
(REPEAT (resolve_tac (@{thms EQgenIs} @ 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

490 
[@{thm EQ_refl} RS (@{thm EQgen_mono} RS @{thm ci3_AI})] @ 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

491 
(@{thms EQgenIs} RL [@{thm EQgen_mono} RS @{thm ci3_AgenI}]) @ 
a0e57fb1b930
misc modernization: proper method setup instead of adhoc ML proofs;
wenzelm
parents:
32149
diff
changeset

492 
[@{thm EQgen_mono} RS @{thm ci3_RI}]) i)) 
20140  493 

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

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

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

497 

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

498 
fun EQgen_tac ctxt rews i = 
20140  499 
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

500 
(TRY (safe_tac (claset_of ctxt)) THEN 
35409  501 
resolve_tac ((rews @ [@{thm refl}]) RL ((rews @ [@{thm 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

502 
ALLGOALS (simp_tac (simpset_of ctxt)) THEN 
20140  503 
ALLGOALS EQgen_raw_tac) i 
504 
*} 

0  505 

506 
end 