author  haftmann 
Mon, 30 Nov 2009 11:42:49 +0100  
changeset 33968  f94fb13ecbb3 
parent 33963  977b94b64905 
child 35216  7641e8d831d2 
permissions  rwrr 
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

1 
(* Title: HOL/Datatype.thy 
20819  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
11954  3 
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen 
5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

4 
*) 
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

5 

33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

6 
header {* Datatype package: constructing datatypes from Cartesian Products and Disjoint Sums *} 
11954  7 

15131  8 
theory Datatype 
33959
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

9 
imports Product_Type Sum_Type Nat 
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

10 
uses 
33963
977b94b64905
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33959
diff
changeset

11 
("Tools/Datatype/datatype.ML") 
33959
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

12 
("Tools/inductive_realizer.ML") 
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

13 
("Tools/Datatype/datatype_realizer.ML") 
15131  14 
begin 
11954  15 

33959
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

16 
subsection {* The datatype universe *} 
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

17 

20819  18 
typedef (Node) 
19 
('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" 

20 
{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*} 

21 
by auto 

22 

23 
text{*Datatypes will be represented by sets of type @{text node}*} 

24 

25 
types 'a item = "('a, unit) node set" 

26 
('a, 'b) dtree = "('a, 'b) node set" 

27 

28 
consts 

29 
Push :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))" 

30 

31 
Push_Node :: "[('b + nat), ('a, 'b) node] => ('a, 'b) node" 

32 
ndepth :: "('a, 'b) node => nat" 

33 

34 
Atom :: "('a + nat) => ('a, 'b) dtree" 

35 
Leaf :: "'a => ('a, 'b) dtree" 

36 
Numb :: "nat => ('a, 'b) dtree" 

37 
Scons :: "[('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree" 

38 
In0 :: "('a, 'b) dtree => ('a, 'b) dtree" 

39 
In1 :: "('a, 'b) dtree => ('a, 'b) dtree" 

40 
Lim :: "('b => ('a, 'b) dtree) => ('a, 'b) dtree" 

41 

42 
ntrunc :: "[nat, ('a, 'b) dtree] => ('a, 'b) dtree" 

43 

44 
uprod :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set" 

45 
usum :: "[('a, 'b) dtree set, ('a, 'b) dtree set]=> ('a, 'b) dtree set" 

46 

47 
Split :: "[[('a, 'b) dtree, ('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c" 

48 
Case :: "[[('a, 'b) dtree]=>'c, [('a, 'b) dtree]=>'c, ('a, 'b) dtree] => 'c" 

49 

50 
dprod :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 

51 
=> (('a, 'b) dtree * ('a, 'b) dtree)set" 

52 
dsum :: "[(('a, 'b) dtree * ('a, 'b) dtree)set, (('a, 'b) dtree * ('a, 'b) dtree)set] 

53 
=> (('a, 'b) dtree * ('a, 'b) dtree)set" 

54 

55 

56 
defs 

57 

58 
Push_Node_def: "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))" 

59 

60 
(*crude "lists" of nats  needed for the constructions*) 

61 
Push_def: "Push == (%b h. nat_case b h)" 

62 

63 
(** operations on Sexpressions  sets of nodes **) 

64 

65 
(*Sexpression constructors*) 

66 
Atom_def: "Atom == (%x. {Abs_Node((%k. Inr 0, x))})" 

67 
Scons_def: "Scons M N == (Push_Node (Inr 1) ` M) Un (Push_Node (Inr (Suc 1)) ` N)" 

68 

69 
(*Leaf nodes, with arbitrary or nat labels*) 

70 
Leaf_def: "Leaf == Atom o Inl" 

71 
Numb_def: "Numb == Atom o Inr" 

72 

73 
(*Injections of the "disjoint sum"*) 

74 
In0_def: "In0(M) == Scons (Numb 0) M" 

75 
In1_def: "In1(M) == Scons (Numb 1) M" 

76 

77 
(*Function spaces*) 

78 
Lim_def: "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}" 

79 

80 
(*the set of nodes with depth less than k*) 

81 
ndepth_def: "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)" 

82 
ntrunc_def: "ntrunc k N == {n. n:N & ndepth(n)<k}" 

83 

84 
(*products and sums for the "universe"*) 

85 
uprod_def: "uprod A B == UN x:A. UN y:B. { Scons x y }" 

86 
usum_def: "usum A B == In0`A Un In1`B" 

87 

88 
(*the corresponding eliminators*) 

89 
Split_def: "Split c M == THE u. EX x y. M = Scons x y & u = c x y" 

90 

91 
Case_def: "Case c d M == THE u. (EX x . M = In0(x) & u = c(x)) 

92 
 (EX y . M = In1(y) & u = d(y))" 

93 

94 

95 
(** equality for the "universe" **) 

96 

97 
dprod_def: "dprod r s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}" 

98 

99 
dsum_def: "dsum r s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un 

100 
(UN (y,y'):s. {(In1(y),In1(y'))})" 

101 

102 

103 

104 
lemma apfst_convE: 

105 
"[ q = apfst f p; !!x y. [ p = (x,y); q = (f(x),y) ] ==> R 

106 
] ==> R" 

107 
by (force simp add: apfst_def) 

108 

109 
(** Push  an injection, analogous to Cons on lists **) 

110 

111 
lemma Push_inject1: "Push i f = Push j g ==> i=j" 

112 
apply (simp add: Push_def expand_fun_eq) 

113 
apply (drule_tac x=0 in spec, simp) 

114 
done 

115 

116 
lemma Push_inject2: "Push i f = Push j g ==> f=g" 

117 
apply (auto simp add: Push_def expand_fun_eq) 

118 
apply (drule_tac x="Suc x" in spec, simp) 

119 
done 

120 

121 
lemma Push_inject: 

122 
"[ Push i f =Push j g; [ i=j; f=g ] ==> P ] ==> P" 

123 
by (blast dest: Push_inject1 Push_inject2) 

124 

125 
lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P" 

126 
by (auto simp add: Push_def expand_fun_eq split: nat.split_asm) 

127 

128 
lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard] 

129 

130 

131 
(*** Introduction rules for Node ***) 

132 

133 
lemma Node_K0_I: "(%k. Inr 0, a) : Node" 

134 
by (simp add: Node_def) 

135 

136 
lemma Node_Push_I: "p: Node ==> apfst (Push i) p : Node" 

137 
apply (simp add: Node_def Push_def) 

138 
apply (fast intro!: apfst_conv nat_case_Suc [THEN trans]) 

139 
done 

140 

141 

142 
subsection{*Freeness: Distinctness of Constructors*} 

143 

144 
(** Scons vs Atom **) 

145 

146 
lemma Scons_not_Atom [iff]: "Scons M N \<noteq> Atom(a)" 

147 
apply (simp add: Atom_def Scons_def Push_Node_def One_nat_def) 

148 
apply (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 

149 
dest!: Abs_Node_inj 

150 
elim!: apfst_convE sym [THEN Push_neq_K0]) 

151 
done 

152 

21407  153 
lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard] 
154 

20819  155 

156 
(*** Injectiveness ***) 

157 

158 
(** Atomic nodes **) 

159 

160 
lemma inj_Atom: "inj(Atom)" 

161 
apply (simp add: Atom_def) 

162 
apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj) 

163 
done 

164 
lemmas Atom_inject = inj_Atom [THEN injD, standard] 

165 

166 
lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)" 

167 
by (blast dest!: Atom_inject) 

168 

169 
lemma inj_Leaf: "inj(Leaf)" 

170 
apply (simp add: Leaf_def o_def) 

171 
apply (rule inj_onI) 

172 
apply (erule Atom_inject [THEN Inl_inject]) 

173 
done 

174 

21407  175 
lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD, standard] 
20819  176 

177 
lemma inj_Numb: "inj(Numb)" 

178 
apply (simp add: Numb_def o_def) 

179 
apply (rule inj_onI) 

180 
apply (erule Atom_inject [THEN Inr_inject]) 

181 
done 

182 

21407  183 
lemmas Numb_inject [dest!] = inj_Numb [THEN injD, standard] 
20819  184 

185 

186 
(** Injectiveness of Push_Node **) 

187 

188 
lemma Push_Node_inject: 

189 
"[ Push_Node i m =Push_Node j n; [ i=j; m=n ] ==> P 

190 
] ==> P" 

191 
apply (simp add: Push_Node_def) 

192 
apply (erule Abs_Node_inj [THEN apfst_convE]) 

193 
apply (rule Rep_Node [THEN Node_Push_I])+ 

194 
apply (erule sym [THEN apfst_convE]) 

195 
apply (blast intro: Rep_Node_inject [THEN iffD1] trans sym elim!: Push_inject) 

196 
done 

197 

198 

199 
(** Injectiveness of Scons **) 

200 

201 
lemma Scons_inject_lemma1: "Scons M N <= Scons M' N' ==> M<=M'" 

202 
apply (simp add: Scons_def One_nat_def) 

203 
apply (blast dest!: Push_Node_inject) 

204 
done 

205 

206 
lemma Scons_inject_lemma2: "Scons M N <= Scons M' N' ==> N<=N'" 

207 
apply (simp add: Scons_def One_nat_def) 

208 
apply (blast dest!: Push_Node_inject) 

209 
done 

210 

211 
lemma Scons_inject1: "Scons M N = Scons M' N' ==> M=M'" 

212 
apply (erule equalityE) 

213 
apply (iprover intro: equalityI Scons_inject_lemma1) 

214 
done 

215 

216 
lemma Scons_inject2: "Scons M N = Scons M' N' ==> N=N'" 

217 
apply (erule equalityE) 

218 
apply (iprover intro: equalityI Scons_inject_lemma2) 

219 
done 

220 

221 
lemma Scons_inject: 

222 
"[ Scons M N = Scons M' N'; [ M=M'; N=N' ] ==> P ] ==> P" 

223 
by (iprover dest: Scons_inject1 Scons_inject2) 

224 

225 
lemma Scons_Scons_eq [iff]: "(Scons M N = Scons M' N') = (M=M' & N=N')" 

226 
by (blast elim!: Scons_inject) 

227 

228 
(*** Distinctness involving Leaf and Numb ***) 

229 

230 
(** Scons vs Leaf **) 

231 

232 
lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)" 

233 
by (simp add: Leaf_def o_def Scons_not_Atom) 

234 

21407  235 
lemmas Leaf_not_Scons [iff] = Scons_not_Leaf [THEN not_sym, standard] 
20819  236 

237 
(** Scons vs Numb **) 

238 

239 
lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)" 

240 
by (simp add: Numb_def o_def Scons_not_Atom) 

241 

21407  242 
lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard] 
20819  243 

244 

245 
(** Leaf vs Numb **) 

246 

247 
lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)" 

248 
by (simp add: Leaf_def Numb_def) 

249 

21407  250 
lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym, standard] 
20819  251 

252 

253 
(*** ndepth  the depth of a node ***) 

254 

255 
lemma ndepth_K0: "ndepth (Abs_Node(%k. Inr 0, x)) = 0" 

256 
by (simp add: ndepth_def Node_K0_I [THEN Abs_Node_inverse] Least_equality) 

257 

258 
lemma ndepth_Push_Node_aux: 

259 
"nat_case (Inr (Suc i)) f k = Inr 0 > Suc(LEAST x. f x = Inr 0) <= k" 

260 
apply (induct_tac "k", auto) 

261 
apply (erule Least_le) 

262 
done 

263 

264 
lemma ndepth_Push_Node: 

265 
"ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))" 

266 
apply (insert Rep_Node [of n, unfolded Node_def]) 

267 
apply (auto simp add: ndepth_def Push_Node_def 

268 
Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse]) 

269 
apply (rule Least_equality) 

270 
apply (auto simp add: Push_def ndepth_Push_Node_aux) 

271 
apply (erule LeastI) 

272 
done 

273 

274 

275 
(*** ntrunc applied to the various node sets ***) 

276 

277 
lemma ntrunc_0 [simp]: "ntrunc 0 M = {}" 

278 
by (simp add: ntrunc_def) 

279 

280 
lemma ntrunc_Atom [simp]: "ntrunc (Suc k) (Atom a) = Atom(a)" 

281 
by (auto simp add: Atom_def ntrunc_def ndepth_K0) 

282 

283 
lemma ntrunc_Leaf [simp]: "ntrunc (Suc k) (Leaf a) = Leaf(a)" 

284 
by (simp add: Leaf_def o_def ntrunc_Atom) 

285 

286 
lemma ntrunc_Numb [simp]: "ntrunc (Suc k) (Numb i) = Numb(i)" 

287 
by (simp add: Numb_def o_def ntrunc_Atom) 

288 

289 
lemma ntrunc_Scons [simp]: 

290 
"ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)" 

291 
by (auto simp add: Scons_def ntrunc_def One_nat_def ndepth_Push_Node) 

292 

293 

294 

295 
(** Injection nodes **) 

296 

297 
lemma ntrunc_one_In0 [simp]: "ntrunc (Suc 0) (In0 M) = {}" 

298 
apply (simp add: In0_def) 

299 
apply (simp add: Scons_def) 

300 
done 

301 

302 
lemma ntrunc_In0 [simp]: "ntrunc (Suc(Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)" 

303 
by (simp add: In0_def) 

304 

305 
lemma ntrunc_one_In1 [simp]: "ntrunc (Suc 0) (In1 M) = {}" 

306 
apply (simp add: In1_def) 

307 
apply (simp add: Scons_def) 

308 
done 

309 

310 
lemma ntrunc_In1 [simp]: "ntrunc (Suc(Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)" 

311 
by (simp add: In1_def) 

312 

313 

314 
subsection{*Set Constructions*} 

315 

316 

317 
(*** Cartesian Product ***) 

318 

319 
lemma uprodI [intro!]: "[ M:A; N:B ] ==> Scons M N : uprod A B" 

320 
by (simp add: uprod_def) 

321 

322 
(*The general elimination rule*) 

323 
lemma uprodE [elim!]: 

324 
"[ c : uprod A B; 

325 
!!x y. [ x:A; y:B; c = Scons x y ] ==> P 

326 
] ==> P" 

327 
by (auto simp add: uprod_def) 

328 

329 

330 
(*Elimination of a pair  introduces no eigenvariables*) 

331 
lemma uprodE2: "[ Scons M N : uprod A B; [ M:A; N:B ] ==> P ] ==> P" 

332 
by (auto simp add: uprod_def) 

333 

334 

335 
(*** Disjoint Sum ***) 

336 

337 
lemma usum_In0I [intro]: "M:A ==> In0(M) : usum A B" 

338 
by (simp add: usum_def) 

339 

340 
lemma usum_In1I [intro]: "N:B ==> In1(N) : usum A B" 

341 
by (simp add: usum_def) 

342 

343 
lemma usumE [elim!]: 

344 
"[ u : usum A B; 

345 
!!x. [ x:A; u=In0(x) ] ==> P; 

346 
!!y. [ y:B; u=In1(y) ] ==> P 

347 
] ==> P" 

348 
by (auto simp add: usum_def) 

349 

350 

351 
(** Injection **) 

352 

353 
lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)" 

354 
by (auto simp add: In0_def In1_def One_nat_def) 

355 

21407  356 
lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard] 
20819  357 

358 
lemma In0_inject: "In0(M) = In0(N) ==> M=N" 

359 
by (simp add: In0_def) 

360 

361 
lemma In1_inject: "In1(M) = In1(N) ==> M=N" 

362 
by (simp add: In1_def) 

363 

364 
lemma In0_eq [iff]: "(In0 M = In0 N) = (M=N)" 

365 
by (blast dest!: In0_inject) 

366 

367 
lemma In1_eq [iff]: "(In1 M = In1 N) = (M=N)" 

368 
by (blast dest!: In1_inject) 

369 

370 
lemma inj_In0: "inj In0" 

371 
by (blast intro!: inj_onI) 

372 

373 
lemma inj_In1: "inj In1" 

374 
by (blast intro!: inj_onI) 

375 

376 

377 
(*** Function spaces ***) 

378 

379 
lemma Lim_inject: "Lim f = Lim g ==> f = g" 

380 
apply (simp add: Lim_def) 

381 
apply (rule ext) 

382 
apply (blast elim!: Push_Node_inject) 

383 
done 

384 

385 

386 
(*** proving equality of sets and functions using ntrunc ***) 

387 

388 
lemma ntrunc_subsetI: "ntrunc k M <= M" 

389 
by (auto simp add: ntrunc_def) 

390 

391 
lemma ntrunc_subsetD: "(!!k. ntrunc k M <= N) ==> M<=N" 

392 
by (auto simp add: ntrunc_def) 

393 

394 
(*A generalized form of the takelemma*) 

395 
lemma ntrunc_equality: "(!!k. ntrunc k M = ntrunc k N) ==> M=N" 

396 
apply (rule equalityI) 

397 
apply (rule_tac [!] ntrunc_subsetD) 

398 
apply (rule_tac [!] ntrunc_subsetI [THEN [2] subset_trans], auto) 

399 
done 

400 

401 
lemma ntrunc_o_equality: 

402 
"[ !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) ] ==> h1=h2" 

403 
apply (rule ntrunc_equality [THEN ext]) 

404 
apply (simp add: expand_fun_eq) 

405 
done 

406 

407 

408 
(*** Monotonicity ***) 

409 

410 
lemma uprod_mono: "[ A<=A'; B<=B' ] ==> uprod A B <= uprod A' B'" 

411 
by (simp add: uprod_def, blast) 

412 

413 
lemma usum_mono: "[ A<=A'; B<=B' ] ==> usum A B <= usum A' B'" 

414 
by (simp add: usum_def, blast) 

415 

416 
lemma Scons_mono: "[ M<=M'; N<=N' ] ==> Scons M N <= Scons M' N'" 

417 
by (simp add: Scons_def, blast) 

418 

419 
lemma In0_mono: "M<=N ==> In0(M) <= In0(N)" 

420 
by (simp add: In0_def subset_refl Scons_mono) 

421 

422 
lemma In1_mono: "M<=N ==> In1(M) <= In1(N)" 

423 
by (simp add: In1_def subset_refl Scons_mono) 

424 

425 

426 
(*** Split and Case ***) 

427 

428 
lemma Split [simp]: "Split c (Scons M N) = c M N" 

429 
by (simp add: Split_def) 

430 

431 
lemma Case_In0 [simp]: "Case c d (In0 M) = c(M)" 

432 
by (simp add: Case_def) 

433 

434 
lemma Case_In1 [simp]: "Case c d (In1 N) = d(N)" 

435 
by (simp add: Case_def) 

436 

437 

438 

439 
(**** UN x. B(x) rules ****) 

440 

441 
lemma ntrunc_UN1: "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))" 

442 
by (simp add: ntrunc_def, blast) 

443 

444 
lemma Scons_UN1_x: "Scons (UN x. f x) M = (UN x. Scons (f x) M)" 

445 
by (simp add: Scons_def, blast) 

446 

447 
lemma Scons_UN1_y: "Scons M (UN x. f x) = (UN x. Scons M (f x))" 

448 
by (simp add: Scons_def, blast) 

449 

450 
lemma In0_UN1: "In0(UN x. f(x)) = (UN x. In0(f(x)))" 

451 
by (simp add: In0_def Scons_UN1_y) 

452 

453 
lemma In1_UN1: "In1(UN x. f(x)) = (UN x. In1(f(x)))" 

454 
by (simp add: In1_def Scons_UN1_y) 

455 

456 

457 
(*** Equality for Cartesian Product ***) 

458 

459 
lemma dprodI [intro!]: 

460 
"[ (M,M'):r; (N,N'):s ] ==> (Scons M N, Scons M' N') : dprod r s" 

461 
by (auto simp add: dprod_def) 

462 

463 
(*The general elimination rule*) 

464 
lemma dprodE [elim!]: 

465 
"[ c : dprod r s; 

466 
!!x y x' y'. [ (x,x') : r; (y,y') : s; 

467 
c = (Scons x y, Scons x' y') ] ==> P 

468 
] ==> P" 

469 
by (auto simp add: dprod_def) 

470 

471 

472 
(*** Equality for Disjoint Sum ***) 

473 

474 
lemma dsum_In0I [intro]: "(M,M'):r ==> (In0(M), In0(M')) : dsum r s" 

475 
by (auto simp add: dsum_def) 

476 

477 
lemma dsum_In1I [intro]: "(N,N'):s ==> (In1(N), In1(N')) : dsum r s" 

478 
by (auto simp add: dsum_def) 

479 

480 
lemma dsumE [elim!]: 

481 
"[ w : dsum r s; 

482 
!!x x'. [ (x,x') : r; w = (In0(x), In0(x')) ] ==> P; 

483 
!!y y'. [ (y,y') : s; w = (In1(y), In1(y')) ] ==> P 

484 
] ==> P" 

485 
by (auto simp add: dsum_def) 

486 

487 

488 
(*** Monotonicity ***) 

489 

490 
lemma dprod_mono: "[ r<=r'; s<=s' ] ==> dprod r s <= dprod r' s'" 

491 
by blast 

492 

493 
lemma dsum_mono: "[ r<=r'; s<=s' ] ==> dsum r s <= dsum r' s'" 

494 
by blast 

495 

496 

497 
(*** Bounding theorems ***) 

498 

499 
lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)" 

500 
by blast 

501 

502 
lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma, standard] 

503 

504 
(*Dependent version*) 

505 
lemma dprod_subset_Sigma2: 

506 
"(dprod (Sigma A B) (Sigma C D)) <= 

507 
Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))" 

508 
by auto 

509 

510 
lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)" 

511 
by blast 

512 

513 
lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard] 

514 

515 

24162
8dfd5dd65d82
split off theory Option for benefit of code generator
haftmann
parents:
22886
diff
changeset

516 
text {* hides popular names *} 
8dfd5dd65d82
split off theory Option for benefit of code generator
haftmann
parents:
22886
diff
changeset

517 
hide (open) type node item 
20819  518 
hide (open) const Push Node Atom Leaf Numb Lim Split Case 
519 

33963
977b94b64905
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33959
diff
changeset

520 
use "Tools/Datatype/datatype.ML" 
12918  521 

33959
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

522 
use "Tools/inductive_realizer.ML" 
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

523 
setup InductiveRealizer.setup 
13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

524 

33959
2afc55e8ed27
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
haftmann
parents:
33633
diff
changeset

525 
use "Tools/Datatype/datatype_realizer.ML" 
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33963
diff
changeset

526 
setup Datatype_Realizer.setup 
13635
c41e88151b54
Added functions Suml and Sumr which are useful for constructing
berghofe
parents:
12918
diff
changeset

527 

5181
4ba3787d9709
New theory Datatype. Needed as an ancestor when defining datatypes.
berghofe
parents:
diff
changeset

528 
end 