author  blanchet 
Mon, 15 Sep 2014 10:49:07 +0200  
changeset 58335  a5a3b576fcfb 
parent 56199  8e8d28ed7529 
child 58889  5b7a9633cfa8 
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 {* 
42284  49 
[(@{const_syntax Pi}, 
52143  50 
fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})), 
42284  51 
(@{const_syntax Sigma}, 
52143  52 
fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))] 
35113  53 
*} 
0  54 

42156  55 
defs 
17456  56 
Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}" 
57 
Unit_def: "Unit == {x. x=one}" 

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

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

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

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

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

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

0  64 

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

0  67 

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

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

0  71 

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

20140  74 

75 
lemmas simp_type_defs = 

76 
Subtype_def Unit_def Bool_def Plus_def Sigma_def Pi_def Lift_def Tall_def Tex_def 

77 
and ind_type_defs = Nat_def List_def 

78 
and simp_data_defs = one_def inl_def inr_def 

79 
and ind_data_defs = zero_def succ_def nil_def cons_def 

80 

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

82 
by blast 

83 

84 

85 
subsection {* Exhaustion Rules *} 

86 

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

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

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

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

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

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

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

94 
unfolding simp_type_defs by blast+ 

95 

96 
lemmas XHs = EmptyXH SubtypeXH UnitXH BoolXH PlusXH PiXH SgXH 

97 

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

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

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

101 
unfolding simp_type_defs by blast+ 

102 

103 
ML {* 

56199  104 
ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs}); 
20140  105 
*} 
106 

107 

108 
subsection {* Canonical Type Rules *} 

109 

110 
lemma oneT: "one : Unit" 

111 
and trueT: "true : Bool" 

112 
and falseT: "false : Bool" 

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

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

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

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

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

118 

119 
lemmas canTs = oneT trueT falseT pairT lamT inlT inrT 

120 

121 

122 
subsection {* NonCanonical Type Rules *} 

123 

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

125 
by blast 

126 

127 

128 
ML {* 

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

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

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

131 
resolve_tac ([major] RL top_crls) 1 THEN 
35409  132 
REPEAT_SOME (eresolve_tac (crls @ [@{thm exE}, @{thm bexE}, @{thm conjE}, @{thm disjE}])) THEN 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42814
diff
changeset

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

134 
ALLGOALS (ares_tac (prems RL [@{thm lem}]) ORELSE' etac @{thm bspec}) THEN 
42793  135 
safe_tac (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

136 
*} 
20140  137 

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

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

139 
Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls}) 
42814  140 
*} 
20140  141 

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

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

143 
"[ 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

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

145 
by ncanT 
20140  146 

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

147 
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

148 
by ncanT 
20140  149 

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

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

151 
"[ 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

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

153 
by ncanT 
20140  154 

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

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

156 
"[ 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

157 
==> 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

158 
by ncanT 
20140  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 

41526  219 
lemma NatM: "mono(%X. Unit+X)" 
20140  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 

56199  265 
ML {* ML_Thms.bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *} 
20140  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 

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

278 

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

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

280 
Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms icase_rls} @{thms case_rls}) 
42814  281 
*} 
20140  282 

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

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

284 
"[ 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

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

286 
by incanT 
20140  287 

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

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

289 
"[ 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

290 
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

291 
by incanT 
20140  292 

293 
lemmas incanTs = ncaseT lcaseT 

294 

295 

296 
subsection {* Induction Rules *} 

297 

298 
lemmas ind_Ms = NatM ListM 

299 

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

301 
apply (unfold ind_data_defs) 

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

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

304 
done 

305 

306 
lemma List_ind: 

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

308 
apply (unfold ind_data_defs) 

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

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

311 
done 

312 

313 
lemmas inds = Nat_ind List_ind 

314 

315 

316 
subsection {* Primitive Recursive Rules *} 

317 

318 
lemma nrecT: 

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

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

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

322 
by (erule Nat_ind) auto 

323 

324 
lemma lrecT: 

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

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

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

328 
by (erule List_ind) auto 

329 

330 
lemmas precTs = nrecT lrecT 

331 

332 

333 
subsection {* Theorem proving *} 

334 

335 
lemma SgE2: 

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

337 
unfolding SgXH by blast 

338 

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

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

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

342 

56199  343 
ML {* ML_Thms.bind_thms ("XHEs", XH_to_Es @{thms XHs}) *} 
20140  344 

345 
lemmas [intro!] = SubtypeI canTs icanTs 

346 
and [elim!] = SubtypeE XHEs 

347 

348 

349 
subsection {* Infinite Data Types *} 

350 

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

352 
apply (rule lfp_lowerbound [THEN subset_trans]) 

353 
apply (erule gfp_lemma3) 

354 
apply (rule subset_refl) 

355 
done 

356 

357 
lemma gfpI: 

358 
assumes "a:A" 

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

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

361 
apply (rule coinduct) 

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

41526  363 
apply (blast intro!: assms)+ 
20140  364 
done 
365 

366 
lemma def_gfpI: 

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

368 
t(a) : C" 

369 
apply unfold 

370 
apply (erule gfpI) 

371 
apply blast 

372 
done 

373 

374 
(* EG *) 

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

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

377 
apply (subst letrecB) 

378 
apply (unfold cons_def) 

379 
apply blast 

380 
done 

381 

382 

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

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

385 

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

387 
apply (erule lfp_Tarski [THEN ssubst]) 

388 
apply assumption 

389 
done 

390 

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

392 
by simp 

393 

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

395 
by simp 

396 

397 

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

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

399 
val coinduct3_tac = SUBPROOF (fn {context = ctxt, prems = mono :: prems, ...} => 
42793  400 
fast_tac (ctxt addIs (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1); 
32153
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 

42814  403 
method_setup coinduct3 = {* Scan.succeed (SIMPLE_METHOD' o coinduct3_tac) *} 
32153
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 
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

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

407 

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

408 
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

409 
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

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

411 

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

412 
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

413 
by coinduct3 
20140  414 

415 
ML {* 

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

416 
fun genIs_tac ctxt genXH gen_mono = 
42480  417 
rtac (genXH RS @{thm iffD2}) THEN' 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42814
diff
changeset

418 
simp_tac ctxt THEN' 
42793  419 
TRY o fast_tac 
420 
(ctxt addIs [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}]) 

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

421 
*} 
20140  422 

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

423 
method_setup genIs = {* 
42814  424 
Attrib.thm  Attrib.thm >> 
425 
(fn (genXH, gen_mono) => fn ctxt => SIMPLE_METHOD' (genIs_tac ctxt genXH gen_mono)) 

426 
*} 

20140  427 

428 

429 
subsection {* POgen *} 

430 

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

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

432 
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

433 

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

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

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

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

437 
"[ <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

438 
"!!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

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

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

441 
<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

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

443 
<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

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

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

446 
<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

447 
"<[],[]> : 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 
"[ <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

449 
==> <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

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

452 
ML {* 

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

453 
fun POgen_tac ctxt (rla, rlb) i = 
42793  454 
SELECT_GOAL (safe_tac ctxt) i THEN 
32010  455 
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

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

457 
(@{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

458 
(@{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

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

462 

463 
subsection {* EQgen *} 

464 

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

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

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

467 

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

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

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

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

471 
"[ <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

472 
"!!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

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

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

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

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

477 
<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

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

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

480 
<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

481 
"<[],[]> : 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 
"[ <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

483 
==> <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

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

486 
ML {* 

487 
fun EQgen_raw_tac i = 

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

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

489 
[@{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

490 
(@{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

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

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

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

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

496 

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

497 
fun EQgen_tac ctxt rews i = 
20140  498 
SELECT_GOAL 
42793  499 
(TRY (safe_tac ctxt) THEN 
35409  500 
resolve_tac ((rews @ [@{thm refl}]) RL ((rews @ [@{thm refl}]) RL [@{thm ssubst_pair}])) i THEN 
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42814
diff
changeset

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

0  504 

505 
end 