author  wenzelm 
Thu, 15 Mar 2012 22:08:53 +0100  
changeset 46950  d0181abdbdac 
parent 45694  4a8743618257 
child 47488  be6dd389639d 
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 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
45694
diff
changeset

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

11 
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

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

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

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

40969  17 
subsection {* Prelude: lifting over function space *} 
18 

41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41372
diff
changeset

19 
enriched_type map_fun: map_fun 
40969  20 
by (simp_all add: fun_eq_iff) 
21 

22 

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

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

24 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45607
diff
changeset

25 
definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45607
diff
changeset

26 

4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45607
diff
changeset

27 
typedef (open) ('a, 'b) node = "Node :: ((nat => 'b + nat) * ('a + nat)) set" 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45607
diff
changeset

28 
morphisms Rep_Node Abs_Node 
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45607
diff
changeset

29 
unfolding Node_def by auto 
20819  30 

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

32 

42163
392fd6c4669c
renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents:
41505
diff
changeset

33 
type_synonym 'a item = "('a, unit) node set" 
392fd6c4669c
renewing specifications in HOL: replacing types by type_synonym
bulwahn
parents:
41505
diff
changeset

34 
type_synonym ('a, 'b) dtree = "('a, 'b) node set" 
20819  35 

36 
consts 

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

38 

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

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

41 

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

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

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

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

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

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

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

49 

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

51 

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

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

54 

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

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

57 

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

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

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

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

62 

63 

64 
defs 

65 

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

67 

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

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

70 

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

72 

73 
(*Sexpression constructors*) 

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

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

76 

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

78 
Leaf_def: "Leaf == Atom o Inl" 

79 
Numb_def: "Numb == Atom o Inr" 

80 

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

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

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

84 

85 
(*Function spaces*) 

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

87 

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

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

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

91 

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

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

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

95 

96 
(*the corresponding eliminators*) 

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

98 

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

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

101 

102 

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

104 

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

106 

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

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

109 

110 

111 

112 
lemma apfst_convE: 

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

114 
] ==> R" 

115 
by (force simp add: apfst_def) 

116 

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

118 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

120 
apply (simp add: Push_def fun_eq_iff) 
20819  121 
apply (drule_tac x=0 in spec, simp) 
122 
done 

123 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

125 
apply (auto simp add: Push_def fun_eq_iff) 
20819  126 
apply (drule_tac x="Suc x" in spec, simp) 
127 
done 

128 

129 
lemma Push_inject: 

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

131 
by (blast dest: Push_inject1 Push_inject2) 

132 

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

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

134 
by (auto simp add: Push_def fun_eq_iff split: nat.split_asm) 
20819  135 

45607  136 
lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1] 
20819  137 

138 

139 
(*** Introduction rules for Node ***) 

140 

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

142 
by (simp add: Node_def) 

143 

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

145 
apply (simp add: Node_def Push_def) 

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

147 
done 

148 

149 

150 
subsection{*Freeness: Distinctness of Constructors*} 

151 

152 
(** Scons vs Atom **) 

153 

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

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

20819  157 
dest!: Abs_Node_inj 
158 
elim!: apfst_convE sym [THEN Push_neq_K0]) 

159 

45607  160 
lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym] 
21407  161 

20819  162 

163 
(*** Injectiveness ***) 

164 

165 
(** Atomic nodes **) 

166 

167 
lemma inj_Atom: "inj(Atom)" 

168 
apply (simp add: Atom_def) 

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

170 
done 

45607  171 
lemmas Atom_inject = inj_Atom [THEN injD] 
20819  172 

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

174 
by (blast dest!: Atom_inject) 

175 

176 
lemma inj_Leaf: "inj(Leaf)" 

177 
apply (simp add: Leaf_def o_def) 

178 
apply (rule inj_onI) 

179 
apply (erule Atom_inject [THEN Inl_inject]) 

180 
done 

181 

45607  182 
lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD] 
20819  183 

184 
lemma inj_Numb: "inj(Numb)" 

185 
apply (simp add: Numb_def o_def) 

186 
apply (rule inj_onI) 

187 
apply (erule Atom_inject [THEN Inr_inject]) 

188 
done 

189 

45607  190 
lemmas Numb_inject [dest!] = inj_Numb [THEN injD] 
20819  191 

192 

193 
(** Injectiveness of Push_Node **) 

194 

195 
lemma Push_Node_inject: 

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

197 
] ==> P" 

198 
apply (simp add: Push_Node_def) 

199 
apply (erule Abs_Node_inj [THEN apfst_convE]) 

200 
apply (rule Rep_Node [THEN Node_Push_I])+ 

201 
apply (erule sym [THEN apfst_convE]) 

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

203 
done 

204 

205 

206 
(** Injectiveness of Scons **) 

207 

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

35216  209 
unfolding Scons_def One_nat_def 
210 
by (blast dest!: Push_Node_inject) 

20819  211 

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

35216  213 
unfolding Scons_def One_nat_def 
214 
by (blast dest!: Push_Node_inject) 

20819  215 

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

217 
apply (erule equalityE) 

218 
apply (iprover intro: equalityI Scons_inject_lemma1) 

219 
done 

220 

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

222 
apply (erule equalityE) 

223 
apply (iprover intro: equalityI Scons_inject_lemma2) 

224 
done 

225 

226 
lemma Scons_inject: 

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

228 
by (iprover dest: Scons_inject1 Scons_inject2) 

229 

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

231 
by (blast elim!: Scons_inject) 

232 

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

234 

235 
(** Scons vs Leaf **) 

236 

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

35216  238 
unfolding Leaf_def o_def by (rule Scons_not_Atom) 
20819  239 

45607  240 
lemmas Leaf_not_Scons [iff] = Scons_not_Leaf [THEN not_sym] 
20819  241 

242 
(** Scons vs Numb **) 

243 

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

35216  245 
unfolding Numb_def o_def by (rule Scons_not_Atom) 
20819  246 

45607  247 
lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym] 
20819  248 

249 

250 
(** Leaf vs Numb **) 

251 

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

253 
by (simp add: Leaf_def Numb_def) 

254 

45607  255 
lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym] 
20819  256 

257 

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

259 

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

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

262 

263 
lemma ndepth_Push_Node_aux: 

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

265 
apply (induct_tac "k", auto) 

266 
apply (erule Least_le) 

267 
done 

268 

269 
lemma ndepth_Push_Node: 

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

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

272 
apply (auto simp add: ndepth_def Push_Node_def 

273 
Rep_Node [THEN Node_Push_I, THEN Abs_Node_inverse]) 

274 
apply (rule Least_equality) 

275 
apply (auto simp add: Push_def ndepth_Push_Node_aux) 

276 
apply (erule LeastI) 

277 
done 

278 

279 

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

281 

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

283 
by (simp add: ntrunc_def) 

284 

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

286 
by (auto simp add: Atom_def ntrunc_def ndepth_K0) 

287 

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

35216  289 
unfolding Leaf_def o_def by (rule ntrunc_Atom) 
20819  290 

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

35216  292 
unfolding Numb_def o_def by (rule ntrunc_Atom) 
20819  293 

294 
lemma ntrunc_Scons [simp]: 

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

35216  296 
unfolding Scons_def ntrunc_def One_nat_def 
297 
by (auto simp add: ndepth_Push_Node) 

20819  298 

299 

300 

301 
(** Injection nodes **) 

302 

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

304 
apply (simp add: In0_def) 

305 
apply (simp add: Scons_def) 

306 
done 

307 

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

309 
by (simp add: In0_def) 

310 

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

312 
apply (simp add: In1_def) 

313 
apply (simp add: Scons_def) 

314 
done 

315 

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

317 
by (simp add: In1_def) 

318 

319 

320 
subsection{*Set Constructions*} 

321 

322 

323 
(*** Cartesian Product ***) 

324 

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

326 
by (simp add: uprod_def) 

327 

328 
(*The general elimination rule*) 

329 
lemma uprodE [elim!]: 

330 
"[ c : uprod A B; 

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

332 
] ==> P" 

333 
by (auto simp add: uprod_def) 

334 

335 

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

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

338 
by (auto simp add: uprod_def) 

339 

340 

341 
(*** Disjoint Sum ***) 

342 

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

344 
by (simp add: usum_def) 

345 

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

347 
by (simp add: usum_def) 

348 

349 
lemma usumE [elim!]: 

350 
"[ u : usum A B; 

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

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

353 
] ==> P" 

354 
by (auto simp add: usum_def) 

355 

356 

357 
(** Injection **) 

358 

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

35216  360 
unfolding In0_def In1_def One_nat_def by auto 
20819  361 

45607  362 
lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym] 
20819  363 

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

365 
by (simp add: In0_def) 

366 

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

368 
by (simp add: In1_def) 

369 

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

371 
by (blast dest!: In0_inject) 

372 

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

374 
by (blast dest!: In1_inject) 

375 

376 
lemma inj_In0: "inj In0" 

377 
by (blast intro!: inj_onI) 

378 

379 
lemma inj_In1: "inj In1" 

380 
by (blast intro!: inj_onI) 

381 

382 

383 
(*** Function spaces ***) 

384 

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

386 
apply (simp add: Lim_def) 

387 
apply (rule ext) 

388 
apply (blast elim!: Push_Node_inject) 

389 
done 

390 

391 

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

393 

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

395 
by (auto simp add: ntrunc_def) 

396 

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

398 
by (auto simp add: ntrunc_def) 

399 

400 
(*A generalized form of the takelemma*) 

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

402 
apply (rule equalityI) 

403 
apply (rule_tac [!] ntrunc_subsetD) 

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

405 
done 

406 

407 
lemma ntrunc_o_equality: 

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

409 
apply (rule ntrunc_equality [THEN ext]) 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

410 
apply (simp add: fun_eq_iff) 
20819  411 
done 
412 

413 

414 
(*** Monotonicity ***) 

415 

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

417 
by (simp add: uprod_def, blast) 

418 

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

420 
by (simp add: usum_def, blast) 

421 

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

423 
by (simp add: Scons_def, blast) 

424 

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

35216  426 
by (simp add: In0_def Scons_mono) 
20819  427 

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

35216  429 
by (simp add: In1_def Scons_mono) 
20819  430 

431 

432 
(*** Split and Case ***) 

433 

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

435 
by (simp add: Split_def) 

436 

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

438 
by (simp add: Case_def) 

439 

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

441 
by (simp add: Case_def) 

442 

443 

444 

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

446 

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

448 
by (simp add: ntrunc_def, blast) 

449 

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

451 
by (simp add: Scons_def, blast) 

452 

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

454 
by (simp add: Scons_def, blast) 

455 

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

457 
by (simp add: In0_def Scons_UN1_y) 

458 

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

460 
by (simp add: In1_def Scons_UN1_y) 

461 

462 

463 
(*** Equality for Cartesian Product ***) 

464 

465 
lemma dprodI [intro!]: 

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

467 
by (auto simp add: dprod_def) 

468 

469 
(*The general elimination rule*) 

470 
lemma dprodE [elim!]: 

471 
"[ c : dprod r s; 

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

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

474 
] ==> P" 

475 
by (auto simp add: dprod_def) 

476 

477 

478 
(*** Equality for Disjoint Sum ***) 

479 

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

481 
by (auto simp add: dsum_def) 

482 

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

484 
by (auto simp add: dsum_def) 

485 

486 
lemma dsumE [elim!]: 

487 
"[ w : dsum r s; 

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

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

490 
] ==> P" 

491 
by (auto simp add: dsum_def) 

492 

493 

494 
(*** Monotonicity ***) 

495 

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

497 
by blast 

498 

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

500 
by blast 

501 

502 

503 
(*** Bounding theorems ***) 

504 

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

506 
by blast 

507 

45607  508 
lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma] 
20819  509 

510 
(*Dependent version*) 

511 
lemma dprod_subset_Sigma2: 

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

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

514 
by auto 

515 

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

517 
by blast 

518 

45607  519 
lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma] 
20819  520 

521 

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

522 
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

523 
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

524 
hide_const (open) Push Node Atom Leaf Numb Lim Split Case 
20819  525 

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

526 
use "Tools/Datatype/datatype.ML" 
12918  527 

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

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

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

530 

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

531 
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

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

533 

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

534 
end 