summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Statespace/DistinctTreeProver.thy

author | hoelzl |

Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) | |

changeset 51474 | 1e9e68247ad1 |

parent 48891 | c0eafbd55de3 |

child 53015 | a1119cf551e8 |

permissions | -rw-r--r-- |

generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun

1 (* Title: HOL/Statespace/DistinctTreeProver.thy

2 Author: Norbert Schirmer, TU Muenchen

3 *)

5 header {* Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}*}

7 theory DistinctTreeProver

8 imports Main

9 begin

11 text {* A state space manages a set of (abstract) names and assumes

12 that the names are distinct. The names are stored as parameters of a

13 locale and distinctness as an assumption. The most common request is

14 to proof distinctness of two given names. We maintain the names in a

15 balanced binary tree and formulate a predicate that all nodes in the

16 tree have distinct names. This setup leads to logarithmic certificates.

17 *}

19 subsection {* The Binary Tree *}

21 datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip

24 text {* The boolean flag in the node marks the content of the node as

25 deleted, without having to build a new tree. We prefer the boolean

26 flag to an option type, so that the ML-layer can still use the node

27 content to facilitate binary search in the tree. The ML code keeps the

28 nodes sorted using the term order. We do not have to push ordering to

29 the HOL level. *}

31 subsection {* Distinctness of Nodes *}

34 primrec set_of :: "'a tree \<Rightarrow> 'a set"

35 where

36 "set_of Tip = {}"

37 | "set_of (Node l x d r) = (if d then {} else {x}) \<union> set_of l \<union> set_of r"

39 primrec all_distinct :: "'a tree \<Rightarrow> bool"

40 where

41 "all_distinct Tip = True"

42 | "all_distinct (Node l x d r) =

43 ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and>

44 set_of l \<inter> set_of r = {} \<and>

45 all_distinct l \<and> all_distinct r)"

47 text {* Given a binary tree @{term "t"} for which

48 @{const all_distinct} holds, given two different nodes contained in the tree,

49 we want to write a ML function that generates a logarithmic

50 certificate that the content of the nodes is distinct. We use the

51 following lemmas to achieve this. *}

53 lemma all_distinct_left: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct l"

54 by simp

56 lemma all_distinct_right: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct r"

57 by simp

59 lemma distinct_left: "all_distinct (Node l x False r) \<Longrightarrow> y \<in> set_of l \<Longrightarrow> x \<noteq> y"

60 by auto

62 lemma distinct_right: "all_distinct (Node l x False r) \<Longrightarrow> y \<in> set_of r \<Longrightarrow> x \<noteq> y"

63 by auto

65 lemma distinct_left_right:

66 "all_distinct (Node l z b r) \<Longrightarrow> x \<in> set_of l \<Longrightarrow> y \<in> set_of r \<Longrightarrow> x \<noteq> y"

67 by auto

69 lemma in_set_root: "x \<in> set_of (Node l x False r)"

70 by simp

72 lemma in_set_left: "y \<in> set_of l \<Longrightarrow> y \<in> set_of (Node l x False r)"

73 by simp

75 lemma in_set_right: "y \<in> set_of r \<Longrightarrow> y \<in> set_of (Node l x False r)"

76 by simp

78 lemma swap_neq: "x \<noteq> y \<Longrightarrow> y \<noteq> x"

79 by blast

81 lemma neq_to_eq_False: "x\<noteq>y \<Longrightarrow> (x=y)\<equiv>False"

82 by simp

84 subsection {* Containment of Trees *}

86 text {* When deriving a state space from other ones, we create a new

87 name tree which contains all the names of the parent state spaces and

88 assume the predicate @{const all_distinct}. We then prove that the new

89 locale interprets all parent locales. Hence we have to show that the

90 new distinctness assumption on all names implies the distinctness

91 assumptions of the parent locales. This proof is implemented in ML. We

92 do this efficiently by defining a kind of containment check of trees

93 by ``subtraction''. We subtract the parent tree from the new tree. If

94 this succeeds we know that @{const all_distinct} of the new tree

95 implies @{const all_distinct} of the parent tree. The resulting

96 certificate is of the order @{term "n * log(m)"} where @{term "n"} is

97 the size of the (smaller) parent tree and @{term "m"} the size of the

98 (bigger) new tree. *}

101 primrec delete :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"

102 where

103 "delete x Tip = None"

104 | "delete x (Node l y d r) = (case delete x l of

105 Some l' \<Rightarrow>

106 (case delete x r of

107 Some r' \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r')

108 | None \<Rightarrow> Some (Node l' y (d \<or> (x=y)) r))

109 | None \<Rightarrow>

110 (case delete x r of

111 Some r' \<Rightarrow> Some (Node l y (d \<or> (x=y)) r')

112 | None \<Rightarrow> if x=y \<and> \<not>d then Some (Node l y True r)

113 else None))"

116 lemma delete_Some_set_of: "delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t"

117 proof (induct t arbitrary: t')

118 case Tip thus ?case by simp

119 next

120 case (Node l y d r)

121 have del: "delete x (Node l y d r) = Some t'" by fact

122 show ?case

123 proof (cases "delete x l")

124 case (Some l')

125 note x_l_Some = this

126 with Node.hyps

127 have l'_l: "set_of l' \<subseteq> set_of l"

128 by simp

129 show ?thesis

130 proof (cases "delete x r")

131 case (Some r')

132 with Node.hyps

133 have "set_of r' \<subseteq> set_of r"

134 by simp

135 with l'_l Some x_l_Some del

136 show ?thesis

137 by (auto split: split_if_asm)

138 next

139 case None

140 with l'_l Some x_l_Some del

141 show ?thesis

142 by (fastforce split: split_if_asm)

143 qed

144 next

145 case None

146 note x_l_None = this

147 show ?thesis

148 proof (cases "delete x r")

149 case (Some r')

150 with Node.hyps

151 have "set_of r' \<subseteq> set_of r"

152 by simp

153 with Some x_l_None del

154 show ?thesis

155 by (fastforce split: split_if_asm)

156 next

157 case None

158 with x_l_None del

159 show ?thesis

160 by (fastforce split: split_if_asm)

161 qed

162 qed

163 qed

165 lemma delete_Some_all_distinct:

166 "delete x t = Some t' \<Longrightarrow> all_distinct t \<Longrightarrow> all_distinct t'"

167 proof (induct t arbitrary: t')

168 case Tip thus ?case by simp

169 next

170 case (Node l y d r)

171 have del: "delete x (Node l y d r) = Some t'" by fact

172 have "all_distinct (Node l y d r)" by fact

173 then obtain

174 dist_l: "all_distinct l" and

175 dist_r: "all_distinct r" and

176 d: "d \<or> (y \<notin> set_of l \<and> y \<notin> set_of r)" and

177 dist_l_r: "set_of l \<inter> set_of r = {}"

178 by auto

179 show ?case

180 proof (cases "delete x l")

181 case (Some l')

182 note x_l_Some = this

183 from Node.hyps (1) [OF Some dist_l]

184 have dist_l': "all_distinct l'"

185 by simp

186 from delete_Some_set_of [OF x_l_Some]

187 have l'_l: "set_of l' \<subseteq> set_of l".

188 show ?thesis

189 proof (cases "delete x r")

190 case (Some r')

191 from Node.hyps (2) [OF Some dist_r]

192 have dist_r': "all_distinct r'"

193 by simp

194 from delete_Some_set_of [OF Some]

195 have "set_of r' \<subseteq> set_of r".

197 with dist_l' dist_r' l'_l Some x_l_Some del d dist_l_r

198 show ?thesis

199 by fastforce

200 next

201 case None

202 with l'_l dist_l' x_l_Some del d dist_l_r dist_r

203 show ?thesis

204 by fastforce

205 qed

206 next

207 case None

208 note x_l_None = this

209 show ?thesis

210 proof (cases "delete x r")

211 case (Some r')

212 with Node.hyps (2) [OF Some dist_r]

213 have dist_r': "all_distinct r'"

214 by simp

215 from delete_Some_set_of [OF Some]

216 have "set_of r' \<subseteq> set_of r".

217 with Some dist_r' x_l_None del dist_l d dist_l_r

218 show ?thesis

219 by fastforce

220 next

221 case None

222 with x_l_None del dist_l dist_r d dist_l_r

223 show ?thesis

224 by (fastforce split: split_if_asm)

225 qed

226 qed

227 qed

229 lemma delete_None_set_of_conv: "delete x t = None = (x \<notin> set_of t)"

230 proof (induct t)

231 case Tip thus ?case by simp

232 next

233 case (Node l y d r)

234 thus ?case

235 by (auto split: option.splits)

236 qed

238 lemma delete_Some_x_set_of:

239 "delete x t = Some t' \<Longrightarrow> x \<in> set_of t \<and> x \<notin> set_of t'"

240 proof (induct t arbitrary: t')

241 case Tip thus ?case by simp

242 next

243 case (Node l y d r)

244 have del: "delete x (Node l y d r) = Some t'" by fact

245 show ?case

246 proof (cases "delete x l")

247 case (Some l')

248 note x_l_Some = this

249 from Node.hyps (1) [OF Some]

250 obtain x_l: "x \<in> set_of l" "x \<notin> set_of l'"

251 by simp

252 show ?thesis

253 proof (cases "delete x r")

254 case (Some r')

255 from Node.hyps (2) [OF Some]

256 obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"

257 by simp

258 from x_r x_l Some x_l_Some del

259 show ?thesis

260 by (clarsimp split: split_if_asm)

261 next

262 case None

263 then have "x \<notin> set_of r"

264 by (simp add: delete_None_set_of_conv)

265 with x_l None x_l_Some del

266 show ?thesis

267 by (clarsimp split: split_if_asm)

268 qed

269 next

270 case None

271 note x_l_None = this

272 then have x_notin_l: "x \<notin> set_of l"

273 by (simp add: delete_None_set_of_conv)

274 show ?thesis

275 proof (cases "delete x r")

276 case (Some r')

277 from Node.hyps (2) [OF Some]

278 obtain x_r: "x \<in> set_of r" "x \<notin> set_of r'"

279 by simp

280 from x_r x_notin_l Some x_l_None del

281 show ?thesis

282 by (clarsimp split: split_if_asm)

283 next

284 case None

285 then have "x \<notin> set_of r"

286 by (simp add: delete_None_set_of_conv)

287 with None x_l_None x_notin_l del

288 show ?thesis

289 by (clarsimp split: split_if_asm)

290 qed

291 qed

292 qed

295 primrec subtract :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"

296 where

297 "subtract Tip t = Some t"

298 | "subtract (Node l x b r) t =

299 (case delete x t of

300 Some t' \<Rightarrow> (case subtract l t' of

301 Some t'' \<Rightarrow> subtract r t''

302 | None \<Rightarrow> None)

303 | None \<Rightarrow> None)"

305 lemma subtract_Some_set_of_res:

306 "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t \<subseteq> set_of t\<^isub>2"

307 proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)

308 case Tip thus ?case by simp

309 next

310 case (Node l x b r)

311 have sub: "subtract (Node l x b r) t\<^isub>2 = Some t" by fact

312 show ?case

313 proof (cases "delete x t\<^isub>2")

314 case (Some t\<^isub>2')

315 note del_x_Some = this

316 from delete_Some_set_of [OF Some]

317 have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .

318 show ?thesis

319 proof (cases "subtract l t\<^isub>2'")

320 case (Some t\<^isub>2'')

321 note sub_l_Some = this

322 from Node.hyps (1) [OF Some]

323 have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .

324 show ?thesis

325 proof (cases "subtract r t\<^isub>2''")

326 case (Some t\<^isub>2''')

327 from Node.hyps (2) [OF Some ]

328 have "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''" .

329 with Some sub_l_Some del_x_Some sub t2''_t2' t2'_t2

330 show ?thesis

331 by simp

332 next

333 case None

334 with del_x_Some sub_l_Some sub

335 show ?thesis

336 by simp

337 qed

338 next

339 case None

340 with del_x_Some sub

341 show ?thesis

342 by simp

343 qed

344 next

345 case None

346 with sub show ?thesis by simp

347 qed

348 qed

350 lemma subtract_Some_set_of:

351 "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<subseteq> set_of t\<^isub>2"

352 proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)

353 case Tip thus ?case by simp

354 next

355 case (Node l x d r)

356 have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact

357 show ?case

358 proof (cases "delete x t\<^isub>2")

359 case (Some t\<^isub>2')

360 note del_x_Some = this

361 from delete_Some_set_of [OF Some]

362 have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .

363 from delete_None_set_of_conv [of x t\<^isub>2] Some

364 have x_t2: "x \<in> set_of t\<^isub>2"

365 by simp

366 show ?thesis

367 proof (cases "subtract l t\<^isub>2'")

368 case (Some t\<^isub>2'')

369 note sub_l_Some = this

370 from Node.hyps (1) [OF Some]

371 have l_t2': "set_of l \<subseteq> set_of t\<^isub>2'" .

372 from subtract_Some_set_of_res [OF Some]

373 have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .

374 show ?thesis

375 proof (cases "subtract r t\<^isub>2''")

376 case (Some t\<^isub>2''')

377 from Node.hyps (2) [OF Some ]

378 have r_t\<^isub>2'': "set_of r \<subseteq> set_of t\<^isub>2''" .

379 from Some sub_l_Some del_x_Some sub r_t\<^isub>2'' l_t2' t2'_t2 t2''_t2' x_t2

380 show ?thesis

381 by auto

382 next

383 case None

384 with del_x_Some sub_l_Some sub

385 show ?thesis

386 by simp

387 qed

388 next

389 case None

390 with del_x_Some sub

391 show ?thesis

392 by simp

393 qed

394 next

395 case None

396 with sub show ?thesis by simp

397 qed

398 qed

400 lemma subtract_Some_all_distinct_res:

401 "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> all_distinct t\<^isub>2 \<Longrightarrow> all_distinct t"

402 proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)

403 case Tip thus ?case by simp

404 next

405 case (Node l x d r)

406 have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact

407 have dist_t2: "all_distinct t\<^isub>2" by fact

408 show ?case

409 proof (cases "delete x t\<^isub>2")

410 case (Some t\<^isub>2')

411 note del_x_Some = this

412 from delete_Some_all_distinct [OF Some dist_t2]

413 have dist_t2': "all_distinct t\<^isub>2'" .

414 show ?thesis

415 proof (cases "subtract l t\<^isub>2'")

416 case (Some t\<^isub>2'')

417 note sub_l_Some = this

418 from Node.hyps (1) [OF Some dist_t2']

419 have dist_t2'': "all_distinct t\<^isub>2''" .

420 show ?thesis

421 proof (cases "subtract r t\<^isub>2''")

422 case (Some t\<^isub>2''')

423 from Node.hyps (2) [OF Some dist_t2'']

424 have dist_t2''': "all_distinct t\<^isub>2'''" .

425 from Some sub_l_Some del_x_Some sub

426 dist_t2'''

427 show ?thesis

428 by simp

429 next

430 case None

431 with del_x_Some sub_l_Some sub

432 show ?thesis

433 by simp

434 qed

435 next

436 case None

437 with del_x_Some sub

438 show ?thesis

439 by simp

440 qed

441 next

442 case None

443 with sub show ?thesis by simp

444 qed

445 qed

448 lemma subtract_Some_dist_res:

449 "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> set_of t\<^isub>1 \<inter> set_of t = {}"

450 proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)

451 case Tip thus ?case by simp

452 next

453 case (Node l x d r)

454 have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact

455 show ?case

456 proof (cases "delete x t\<^isub>2")

457 case (Some t\<^isub>2')

458 note del_x_Some = this

459 from delete_Some_x_set_of [OF Some]

460 obtain x_t2: "x \<in> set_of t\<^isub>2" and x_not_t2': "x \<notin> set_of t\<^isub>2'"

461 by simp

462 from delete_Some_set_of [OF Some]

463 have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .

464 show ?thesis

465 proof (cases "subtract l t\<^isub>2'")

466 case (Some t\<^isub>2'')

467 note sub_l_Some = this

468 from Node.hyps (1) [OF Some ]

469 have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}".

470 from subtract_Some_set_of_res [OF Some]

471 have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .

472 show ?thesis

473 proof (cases "subtract r t\<^isub>2''")

474 case (Some t\<^isub>2''')

475 from Node.hyps (2) [OF Some]

476 have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}" .

477 from subtract_Some_set_of_res [OF Some]

478 have t2'''_t2'': "set_of t\<^isub>2''' \<subseteq> set_of t\<^isub>2''".

480 from Some sub_l_Some del_x_Some sub t2'''_t2'' dist_l_t2'' dist_r_t2'''

481 t2''_t2' t2'_t2 x_not_t2'

482 show ?thesis

483 by auto

484 next

485 case None

486 with del_x_Some sub_l_Some sub

487 show ?thesis

488 by simp

489 qed

490 next

491 case None

492 with del_x_Some sub

493 show ?thesis

494 by simp

495 qed

496 next

497 case None

498 with sub show ?thesis by simp

499 qed

500 qed

502 lemma subtract_Some_all_distinct:

503 "subtract t\<^isub>1 t\<^isub>2 = Some t \<Longrightarrow> all_distinct t\<^isub>2 \<Longrightarrow> all_distinct t\<^isub>1"

504 proof (induct t\<^isub>1 arbitrary: t\<^isub>2 t)

505 case Tip thus ?case by simp

506 next

507 case (Node l x d r)

508 have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact

509 have dist_t2: "all_distinct t\<^isub>2" by fact

510 show ?case

511 proof (cases "delete x t\<^isub>2")

512 case (Some t\<^isub>2')

513 note del_x_Some = this

514 from delete_Some_all_distinct [OF Some dist_t2 ]

515 have dist_t2': "all_distinct t\<^isub>2'" .

516 from delete_Some_set_of [OF Some]

517 have t2'_t2: "set_of t\<^isub>2' \<subseteq> set_of t\<^isub>2" .

518 from delete_Some_x_set_of [OF Some]

519 obtain x_t2: "x \<in> set_of t\<^isub>2" and x_not_t2': "x \<notin> set_of t\<^isub>2'"

520 by simp

522 show ?thesis

523 proof (cases "subtract l t\<^isub>2'")

524 case (Some t\<^isub>2'')

525 note sub_l_Some = this

526 from Node.hyps (1) [OF Some dist_t2' ]

527 have dist_l: "all_distinct l" .

528 from subtract_Some_all_distinct_res [OF Some dist_t2']

529 have dist_t2'': "all_distinct t\<^isub>2''" .

530 from subtract_Some_set_of [OF Some]

531 have l_t2': "set_of l \<subseteq> set_of t\<^isub>2'" .

532 from subtract_Some_set_of_res [OF Some]

533 have t2''_t2': "set_of t\<^isub>2'' \<subseteq> set_of t\<^isub>2'" .

534 from subtract_Some_dist_res [OF Some]

535 have dist_l_t2'': "set_of l \<inter> set_of t\<^isub>2'' = {}".

536 show ?thesis

537 proof (cases "subtract r t\<^isub>2''")

538 case (Some t\<^isub>2''')

539 from Node.hyps (2) [OF Some dist_t2'']

540 have dist_r: "all_distinct r" .

541 from subtract_Some_set_of [OF Some]

542 have r_t2'': "set_of r \<subseteq> set_of t\<^isub>2''" .

543 from subtract_Some_dist_res [OF Some]

544 have dist_r_t2''': "set_of r \<inter> set_of t\<^isub>2''' = {}".

546 from dist_l dist_r Some sub_l_Some del_x_Some r_t2'' l_t2' x_t2 x_not_t2'

547 t2''_t2' dist_l_t2'' dist_r_t2'''

548 show ?thesis

549 by auto

550 next

551 case None

552 with del_x_Some sub_l_Some sub

553 show ?thesis

554 by simp

555 qed

556 next

557 case None

558 with del_x_Some sub

559 show ?thesis

560 by simp

561 qed

562 next

563 case None

564 with sub show ?thesis by simp

565 qed

566 qed

569 lemma delete_left:

570 assumes dist: "all_distinct (Node l y d r)"

571 assumes del_l: "delete x l = Some l'"

572 shows "delete x (Node l y d r) = Some (Node l' y d r)"

573 proof -

574 from delete_Some_x_set_of [OF del_l]

575 obtain "x \<in> set_of l"

576 by simp

577 moreover with dist

578 have "delete x r = None"

579 by (cases "delete x r") (auto dest:delete_Some_x_set_of)

581 ultimately

582 show ?thesis

583 using del_l dist

584 by (auto split: option.splits)

585 qed

587 lemma delete_right:

588 assumes dist: "all_distinct (Node l y d r)"

589 assumes del_r: "delete x r = Some r'"

590 shows "delete x (Node l y d r) = Some (Node l y d r')"

591 proof -

592 from delete_Some_x_set_of [OF del_r]

593 obtain "x \<in> set_of r"

594 by simp

595 moreover with dist

596 have "delete x l = None"

597 by (cases "delete x l") (auto dest:delete_Some_x_set_of)

599 ultimately

600 show ?thesis

601 using del_r dist

602 by (auto split: option.splits)

603 qed

605 lemma delete_root:

606 assumes dist: "all_distinct (Node l x False r)"

607 shows "delete x (Node l x False r) = Some (Node l x True r)"

608 proof -

609 from dist have "delete x r = None"

610 by (cases "delete x r") (auto dest:delete_Some_x_set_of)

611 moreover

612 from dist have "delete x l = None"

613 by (cases "delete x l") (auto dest:delete_Some_x_set_of)

614 ultimately show ?thesis

615 using dist

616 by (auto split: option.splits)

617 qed

619 lemma subtract_Node:

620 assumes del: "delete x t = Some t'"

621 assumes sub_l: "subtract l t' = Some t''"

622 assumes sub_r: "subtract r t'' = Some t'''"

623 shows "subtract (Node l x False r) t = Some t'''"

624 using del sub_l sub_r

625 by simp

627 lemma subtract_Tip: "subtract Tip t = Some t"

628 by simp

630 text {* Now we have all the theorems in place that are needed for the

631 certificate generating ML functions. *}

633 ML_file "distinct_tree_prover.ML"

635 (* Uncomment for profiling or debugging *)

636 (*

637 ML {*

638 (*

639 val nums = (0 upto 10000);

640 val nums' = (200 upto 3000);

641 *)

642 val nums = (0 upto 10000);

643 val nums' = (0 upto 3000);

644 val const_decls = map (fn i => ("const" ^ string_of_int i, Type ("nat", []), NoSyn)) nums

646 val consts = sort Term_Ord.fast_term_ord

647 (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums)

648 val consts' = sort Term_Ord.fast_term_ord

649 (map (fn i => Const ("DistinctTreeProver.const"^string_of_int i,Type ("nat",[]))) nums')

651 val t = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts

654 val t' = DistinctTreeProver.mk_tree I (Type ("nat",[])) consts'

657 val dist =

658 HOLogic.Trueprop$

659 (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t)

661 val dist' =

662 HOLogic.Trueprop$

663 (Const ("DistinctTreeProver.all_distinct",DistinctTreeProver.treeT (Type ("nat",[])) --> HOLogic.boolT)$t')

665 val da = Unsynchronized.ref refl;

667 *}

669 setup {*

670 Theory.add_consts_i const_decls

671 #> (fn thy => let val ([thm],thy') = Global_Theory.add_axioms [(("dist_axiom",dist),[])] thy

672 in (da := thm; thy') end)

673 *}

676 ML {*

677 val ct' = cterm_of @{theory} t';

678 *}

680 ML {*

681 timeit (fn () => (DistinctTreeProver.subtractProver (term_of ct') ct' (!da);()))

682 *}

684 (* 590 s *)

686 ML {*

689 val p1 =

690 the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const1",Type ("nat",[]))) t)

691 val p2 =

692 the (DistinctTreeProver.find_tree (Const ("DistinctTreeProver.const10000",Type ("nat",[]))) t)

693 *}

696 ML {* timeit (fn () => DistinctTreeProver.distinctTreeProver (!da )

697 p1

698 p2)*}

701 ML {* timeit (fn () => (DistinctTreeProver.deleteProver (!da) p1;())) *}

706 ML {*

707 val cdist' = cterm_of @{theory} dist';

708 DistinctTreeProver.distinct_implProver (!da) cdist';

709 *}

711 *)

713 end