author  nipkow 
Tue, 07 Sep 2010 10:05:19 +0200  
changeset 39198  f967a16dfcdd 
parent 36176  3fe7e97ccca8 
child 39302  d7728f65b353 
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" 

39198  112 
apply (simp add: Push_def ext_iff) 
20819  113 
apply (drule_tac x=0 in spec, simp) 
114 
done 

115 

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

39198  117 
apply (auto simp add: Push_def ext_iff) 
20819  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" 

39198  126 
by (auto simp add: Push_def ext_iff split: nat.split_asm) 
20819  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)" 

35216  147 
unfolding Atom_def Scons_def Push_Node_def One_nat_def 
148 
by (blast intro: Node_K0_I Rep_Node [THEN Node_Push_I] 

20819  149 
dest!: Abs_Node_inj 
150 
elim!: apfst_convE sym [THEN Push_neq_K0]) 

151 

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

20819  154 

155 
(*** Injectiveness ***) 

156 

157 
(** Atomic nodes **) 

158 

159 
lemma inj_Atom: "inj(Atom)" 

160 
apply (simp add: Atom_def) 

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

162 
done 

163 
lemmas Atom_inject = inj_Atom [THEN injD, standard] 

164 

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

166 
by (blast dest!: Atom_inject) 

167 

168 
lemma inj_Leaf: "inj(Leaf)" 

169 
apply (simp add: Leaf_def o_def) 

170 
apply (rule inj_onI) 

171 
apply (erule Atom_inject [THEN Inl_inject]) 

172 
done 

173 

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

176 
lemma inj_Numb: "inj(Numb)" 

177 
apply (simp add: Numb_def o_def) 

178 
apply (rule inj_onI) 

179 
apply (erule Atom_inject [THEN Inr_inject]) 

180 
done 

181 

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

184 

185 
(** Injectiveness of Push_Node **) 

186 

187 
lemma Push_Node_inject: 

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

189 
] ==> P" 

190 
apply (simp add: Push_Node_def) 

191 
apply (erule Abs_Node_inj [THEN apfst_convE]) 

192 
apply (rule Rep_Node [THEN Node_Push_I])+ 

193 
apply (erule sym [THEN apfst_convE]) 

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

195 
done 

196 

197 

198 
(** Injectiveness of Scons **) 

199 

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

35216  201 
unfolding Scons_def One_nat_def 
202 
by (blast dest!: Push_Node_inject) 

20819  203 

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

35216  205 
unfolding Scons_def One_nat_def 
206 
by (blast dest!: Push_Node_inject) 

20819  207 

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

209 
apply (erule equalityE) 

210 
apply (iprover intro: equalityI Scons_inject_lemma1) 

211 
done 

212 

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

214 
apply (erule equalityE) 

215 
apply (iprover intro: equalityI Scons_inject_lemma2) 

216 
done 

217 

218 
lemma Scons_inject: 

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

220 
by (iprover dest: Scons_inject1 Scons_inject2) 

221 

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

223 
by (blast elim!: Scons_inject) 

224 

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

226 

227 
(** Scons vs Leaf **) 

228 

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

35216  230 
unfolding Leaf_def o_def by (rule Scons_not_Atom) 
20819  231 

21407  232 
lemmas Leaf_not_Scons [iff] = Scons_not_Leaf [THEN not_sym, standard] 
20819  233 

234 
(** Scons vs Numb **) 

235 

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

35216  237 
unfolding Numb_def o_def by (rule Scons_not_Atom) 
20819  238 

21407  239 
lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard] 
20819  240 

241 

242 
(** Leaf vs Numb **) 

243 

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

245 
by (simp add: Leaf_def Numb_def) 

246 

21407  247 
lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym, standard] 
20819  248 

249 

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

251 

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

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

254 

255 
lemma ndepth_Push_Node_aux: 

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

257 
apply (induct_tac "k", auto) 

258 
apply (erule Least_le) 

259 
done 

260 

261 
lemma ndepth_Push_Node: 

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

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

264 
apply (auto simp add: ndepth_def Push_Node_def 

265 
Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse]) 

266 
apply (rule Least_equality) 

267 
apply (auto simp add: Push_def ndepth_Push_Node_aux) 

268 
apply (erule LeastI) 

269 
done 

270 

271 

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

273 

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

275 
by (simp add: ntrunc_def) 

276 

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

278 
by (auto simp add: Atom_def ntrunc_def ndepth_K0) 

279 

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

35216  281 
unfolding Leaf_def o_def by (rule ntrunc_Atom) 
20819  282 

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

35216  284 
unfolding Numb_def o_def by (rule ntrunc_Atom) 
20819  285 

286 
lemma ntrunc_Scons [simp]: 

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

35216  288 
unfolding Scons_def ntrunc_def One_nat_def 
289 
by (auto simp add: ndepth_Push_Node) 

20819  290 

291 

292 

293 
(** Injection nodes **) 

294 

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

296 
apply (simp add: In0_def) 

297 
apply (simp add: Scons_def) 

298 
done 

299 

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

301 
by (simp add: In0_def) 

302 

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

304 
apply (simp add: In1_def) 

305 
apply (simp add: Scons_def) 

306 
done 

307 

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

309 
by (simp add: In1_def) 

310 

311 

312 
subsection{*Set Constructions*} 

313 

314 

315 
(*** Cartesian Product ***) 

316 

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

318 
by (simp add: uprod_def) 

319 

320 
(*The general elimination rule*) 

321 
lemma uprodE [elim!]: 

322 
"[ c : uprod A B; 

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

324 
] ==> P" 

325 
by (auto simp add: uprod_def) 

326 

327 

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

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

330 
by (auto simp add: uprod_def) 

331 

332 

333 
(*** Disjoint Sum ***) 

334 

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

336 
by (simp add: usum_def) 

337 

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

339 
by (simp add: usum_def) 

340 

341 
lemma usumE [elim!]: 

342 
"[ u : usum A B; 

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

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

345 
] ==> P" 

346 
by (auto simp add: usum_def) 

347 

348 

349 
(** Injection **) 

350 

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

35216  352 
unfolding In0_def In1_def One_nat_def by auto 
20819  353 

21407  354 
lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard] 
20819  355 

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

357 
by (simp add: In0_def) 

358 

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

360 
by (simp add: In1_def) 

361 

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

363 
by (blast dest!: In0_inject) 

364 

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

366 
by (blast dest!: In1_inject) 

367 

368 
lemma inj_In0: "inj In0" 

369 
by (blast intro!: inj_onI) 

370 

371 
lemma inj_In1: "inj In1" 

372 
by (blast intro!: inj_onI) 

373 

374 

375 
(*** Function spaces ***) 

376 

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

378 
apply (simp add: Lim_def) 

379 
apply (rule ext) 

380 
apply (blast elim!: Push_Node_inject) 

381 
done 

382 

383 

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

385 

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

387 
by (auto simp add: ntrunc_def) 

388 

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

390 
by (auto simp add: ntrunc_def) 

391 

392 
(*A generalized form of the takelemma*) 

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

394 
apply (rule equalityI) 

395 
apply (rule_tac [!] ntrunc_subsetD) 

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

397 
done 

398 

399 
lemma ntrunc_o_equality: 

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

401 
apply (rule ntrunc_equality [THEN ext]) 

39198  402 
apply (simp add: ext_iff) 
20819  403 
done 
404 

405 

406 
(*** Monotonicity ***) 

407 

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

409 
by (simp add: uprod_def, blast) 

410 

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

412 
by (simp add: usum_def, blast) 

413 

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

415 
by (simp add: Scons_def, blast) 

416 

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

35216  418 
by (simp add: In0_def Scons_mono) 
20819  419 

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

35216  421 
by (simp add: In1_def Scons_mono) 
20819  422 

423 

424 
(*** Split and Case ***) 

425 

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

427 
by (simp add: Split_def) 

428 

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

430 
by (simp add: Case_def) 

431 

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

433 
by (simp add: Case_def) 

434 

435 

436 

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

438 

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

440 
by (simp add: ntrunc_def, blast) 

441 

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

443 
by (simp add: Scons_def, blast) 

444 

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

446 
by (simp add: Scons_def, blast) 

447 

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

449 
by (simp add: In0_def Scons_UN1_y) 

450 

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

452 
by (simp add: In1_def Scons_UN1_y) 

453 

454 

455 
(*** Equality for Cartesian Product ***) 

456 

457 
lemma dprodI [intro!]: 

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

459 
by (auto simp add: dprod_def) 

460 

461 
(*The general elimination rule*) 

462 
lemma dprodE [elim!]: 

463 
"[ c : dprod r s; 

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

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

466 
] ==> P" 

467 
by (auto simp add: dprod_def) 

468 

469 

470 
(*** Equality for Disjoint Sum ***) 

471 

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

473 
by (auto simp add: dsum_def) 

474 

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

476 
by (auto simp add: dsum_def) 

477 

478 
lemma dsumE [elim!]: 

479 
"[ w : dsum r s; 

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

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

482 
] ==> P" 

483 
by (auto simp add: dsum_def) 

484 

485 

486 
(*** Monotonicity ***) 

487 

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

489 
by blast 

490 

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

492 
by blast 

493 

494 

495 
(*** Bounding theorems ***) 

496 

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

498 
by blast 

499 

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

501 

502 
(*Dependent version*) 

503 
lemma dprod_subset_Sigma2: 

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

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

506 
by auto 

507 

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

509 
by blast 

510 

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

512 

513 

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

514 
text {* hides popular names *} 
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35216
diff
changeset

515 
hide_type (open) node item 
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35216
diff
changeset

516 
hide_const (open) Push Node Atom Leaf Numb Lim Split Case 
20819  517 

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

518 
use "Tools/Datatype/datatype.ML" 
12918  519 

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

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

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

522 

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

523 
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

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

525 

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

526 
end 