1(* Title: HOL/Statespace/DistinctTreeProver.thy 2 Author: Norbert Schirmer, TU Muenchen 3*) 4 5section \<open>Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}\<close> 6 7theory DistinctTreeProver 8imports Main 9begin 10 11text \<open>A state space manages a set of (abstract) names and assumes 12that the names are distinct. The names are stored as parameters of a 13locale and distinctness as an assumption. The most common request is 14to proof distinctness of two given names. We maintain the names in a 15balanced binary tree and formulate a predicate that all nodes in the 16tree have distinct names. This setup leads to logarithmic certificates. 17\<close> 18 19subsection \<open>The Binary Tree\<close> 20 21datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip 22 23 24text \<open>The boolean flag in the node marks the content of the node as 25deleted, without having to build a new tree. We prefer the boolean 26flag to an option type, so that the ML-layer can still use the node 27content to facilitate binary search in the tree. The ML code keeps the 28nodes sorted using the term order. We do not have to push ordering to 29the HOL level.\<close> 30 31subsection \<open>Distinctness of Nodes\<close> 32 33 34primrec set_of :: "'a tree \<Rightarrow> 'a set" 35where 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" 38 39primrec all_distinct :: "'a tree \<Rightarrow> bool" 40where 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)" 46 47text \<open>Given a binary tree @{term "t"} for which 48@{const all_distinct} holds, given two different nodes contained in the tree, 49we want to write a ML function that generates a logarithmic 50certificate that the content of the nodes is distinct. We use the 51following lemmas to achieve this.\<close> 52 53lemma all_distinct_left: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct l" 54 by simp 55 56lemma all_distinct_right: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct r" 57 by simp 58 59lemma distinct_left: "all_distinct (Node l x False r) \<Longrightarrow> y \<in> set_of l \<Longrightarrow> x \<noteq> y" 60 by auto 61 62lemma distinct_right: "all_distinct (Node l x False r) \<Longrightarrow> y \<in> set_of r \<Longrightarrow> x \<noteq> y" 63 by auto 64 65lemma 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 68 69lemma in_set_root: "x \<in> set_of (Node l x False r)" 70 by simp 71 72lemma in_set_left: "y \<in> set_of l \<Longrightarrow> y \<in> set_of (Node l x False r)" 73 by simp 74 75lemma in_set_right: "y \<in> set_of r \<Longrightarrow> y \<in> set_of (Node l x False r)" 76 by simp 77 78lemma swap_neq: "x \<noteq> y \<Longrightarrow> y \<noteq> x" 79 by blast 80 81lemma neq_to_eq_False: "x\<noteq>y \<Longrightarrow> (x=y)\<equiv>False" 82 by simp 83 84subsection \<open>Containment of Trees\<close> 85 86text \<open>When deriving a state space from other ones, we create a new 87name tree which contains all the names of the parent state spaces and 88assume the predicate @{const all_distinct}. We then prove that the new 89locale interprets all parent locales. Hence we have to show that the 90new distinctness assumption on all names implies the distinctness 91assumptions of the parent locales. This proof is implemented in ML. We 92do this efficiently by defining a kind of containment check of trees 93by ``subtraction''. We subtract the parent tree from the new tree. If 94this succeeds we know that @{const all_distinct} of the new tree 95implies @{const all_distinct} of the parent tree. The resulting 96certificate is of the order @{term "n * log(m)"} where @{term "n"} is 97the size of the (smaller) parent tree and @{term "m"} the size of the 98(bigger) new tree.\<close> 99 100 101primrec delete :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option" 102where 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))" 114 115 116lemma delete_Some_set_of: "delete x t = Some t' \<Longrightarrow> set_of t' \<subseteq> set_of t" 117proof (induct t arbitrary: t') 118 case Tip thus ?case by simp 119next 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: if_split_asm) 138 next 139 case None 140 with l'_l Some x_l_Some del 141 show ?thesis 142 by (fastforce split: if_split_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: if_split_asm) 156 next 157 case None 158 with x_l_None del 159 show ?thesis 160 by (fastforce split: if_split_asm) 161 qed 162 qed 163qed 164 165lemma delete_Some_all_distinct: 166 "delete x t = Some t' \<Longrightarrow> all_distinct t \<Longrightarrow> all_distinct t'" 167proof (induct t arbitrary: t') 168 case Tip thus ?case by simp 169next 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". 196 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: if_split_asm) 225 qed 226 qed 227qed 228 229lemma delete_None_set_of_conv: "delete x t = None = (x \<notin> set_of t)" 230proof (induct t) 231 case Tip thus ?case by simp 232next 233 case (Node l y d r) 234 thus ?case 235 by (auto split: option.splits) 236qed 237 238lemma delete_Some_x_set_of: 239 "delete x t = Some t' \<Longrightarrow> x \<in> set_of t \<and> x \<notin> set_of t'" 240proof (induct t arbitrary: t') 241 case Tip thus ?case by simp 242next 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: if_split_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: if_split_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: if_split_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: if_split_asm) 290 qed 291 qed 292qed 293 294 295primrec subtract :: "'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree option" 296where 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)" 304 305lemma subtract_Some_set_of_res: 306 "subtract t\<^sub>1 t\<^sub>2 = Some t \<Longrightarrow> set_of t \<subseteq> set_of t\<^sub>2" 307proof (induct t\<^sub>1 arbitrary: t\<^sub>2 t) 308 case Tip thus ?case by simp 309next 310 case (Node l x b r) 311 have sub: "subtract (Node l x b r) t\<^sub>2 = Some t" by fact 312 show ?case 313 proof (cases "delete x t\<^sub>2") 314 case (Some t\<^sub>2') 315 note del_x_Some = this 316 from delete_Some_set_of [OF Some] 317 have t2'_t2: "set_of t\<^sub>2' \<subseteq> set_of t\<^sub>2" . 318 show ?thesis 319 proof (cases "subtract l t\<^sub>2'") 320 case (Some t\<^sub>2'') 321 note sub_l_Some = this 322 from Node.hyps (1) [OF Some] 323 have t2''_t2': "set_of t\<^sub>2'' \<subseteq> set_of t\<^sub>2'" . 324 show ?thesis 325 proof (cases "subtract r t\<^sub>2''") 326 case (Some t\<^sub>2''') 327 from Node.hyps (2) [OF Some ] 328 have "set_of t\<^sub>2''' \<subseteq> set_of t\<^sub>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 348qed 349 350lemma subtract_Some_set_of: 351 "subtract t\<^sub>1 t\<^sub>2 = Some t \<Longrightarrow> set_of t\<^sub>1 \<subseteq> set_of t\<^sub>2" 352proof (induct t\<^sub>1 arbitrary: t\<^sub>2 t) 353 case Tip thus ?case by simp 354next 355 case (Node l x d r) 356 have sub: "subtract (Node l x d r) t\<^sub>2 = Some t" by fact 357 show ?case 358 proof (cases "delete x t\<^sub>2") 359 case (Some t\<^sub>2') 360 note del_x_Some = this 361 from delete_Some_set_of [OF Some] 362 have t2'_t2: "set_of t\<^sub>2' \<subseteq> set_of t\<^sub>2" . 363 from delete_None_set_of_conv [of x t\<^sub>2] Some 364 have x_t2: "x \<in> set_of t\<^sub>2" 365 by simp 366 show ?thesis 367 proof (cases "subtract l t\<^sub>2'") 368 case (Some t\<^sub>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\<^sub>2'" . 372 from subtract_Some_set_of_res [OF Some] 373 have t2''_t2': "set_of t\<^sub>2'' \<subseteq> set_of t\<^sub>2'" . 374 show ?thesis 375 proof (cases "subtract r t\<^sub>2''") 376 case (Some t\<^sub>2''') 377 from Node.hyps (2) [OF Some ] 378 have r_t\<^sub>2'': "set_of r \<subseteq> set_of t\<^sub>2''" . 379 from Some sub_l_Some del_x_Some sub r_t\<^sub>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 398qed 399 400lemma subtract_Some_all_distinct_res: 401 "subtract t\<^sub>1 t\<^sub>2 = Some t \<Longrightarrow> all_distinct t\<^sub>2 \<Longrightarrow> all_distinct t" 402proof (induct t\<^sub>1 arbitrary: t\<^sub>2 t) 403 case Tip thus ?case by simp 404next 405 case (Node l x d r) 406 have sub: "subtract (Node l x d r) t\<^sub>2 = Some t" by fact 407 have dist_t2: "all_distinct t\<^sub>2" by fact 408 show ?case 409 proof (cases "delete x t\<^sub>2") 410 case (Some t\<^sub>2') 411 note del_x_Some = this 412 from delete_Some_all_distinct [OF Some dist_t2] 413 have dist_t2': "all_distinct t\<^sub>2'" . 414 show ?thesis 415 proof (cases "subtract l t\<^sub>2'") 416 case (Some t\<^sub>2'') 417 note sub_l_Some = this 418 from Node.hyps (1) [OF Some dist_t2'] 419 have dist_t2'': "all_distinct t\<^sub>2''" . 420 show ?thesis 421 proof (cases "subtract r t\<^sub>2''") 422 case (Some t\<^sub>2''') 423 from Node.hyps (2) [OF Some dist_t2''] 424 have dist_t2''': "all_distinct t\<^sub>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 445qed 446 447 448lemma subtract_Some_dist_res: 449 "subtract t\<^sub>1 t\<^sub>2 = Some t \<Longrightarrow> set_of t\<^sub>1 \<inter> set_of t = {}" 450proof (induct t\<^sub>1 arbitrary: t\<^sub>2 t) 451 case Tip thus ?case by simp 452next 453 case (Node l x d r) 454 have sub: "subtract (Node l x d r) t\<^sub>2 = Some t" by fact 455 show ?case 456 proof (cases "delete x t\<^sub>2") 457 case (Some t\<^sub>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\<^sub>2" and x_not_t2': "x \<notin> set_of t\<^sub>2'" 461 by simp 462 from delete_Some_set_of [OF Some] 463 have t2'_t2: "set_of t\<^sub>2' \<subseteq> set_of t\<^sub>2" . 464 show ?thesis 465 proof (cases "subtract l t\<^sub>2'") 466 case (Some t\<^sub>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\<^sub>2'' = {}". 470 from subtract_Some_set_of_res [OF Some] 471 have t2''_t2': "set_of t\<^sub>2'' \<subseteq> set_of t\<^sub>2'" . 472 show ?thesis 473 proof (cases "subtract r t\<^sub>2''") 474 case (Some t\<^sub>2''') 475 from Node.hyps (2) [OF Some] 476 have dist_r_t2''': "set_of r \<inter> set_of t\<^sub>2''' = {}" . 477 from subtract_Some_set_of_res [OF Some] 478 have t2'''_t2'': "set_of t\<^sub>2''' \<subseteq> set_of t\<^sub>2''". 479 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 500qed 501 502lemma subtract_Some_all_distinct: 503 "subtract t\<^sub>1 t\<^sub>2 = Some t \<Longrightarrow> all_distinct t\<^sub>2 \<Longrightarrow> all_distinct t\<^sub>1" 504proof (induct t\<^sub>1 arbitrary: t\<^sub>2 t) 505 case Tip thus ?case by simp 506next 507 case (Node l x d r) 508 have sub: "subtract (Node l x d r) t\<^sub>2 = Some t" by fact 509 have dist_t2: "all_distinct t\<^sub>2" by fact 510 show ?case 511 proof (cases "delete x t\<^sub>2") 512 case (Some t\<^sub>2') 513 note del_x_Some = this 514 from delete_Some_all_distinct [OF Some dist_t2 ] 515 have dist_t2': "all_distinct t\<^sub>2'" . 516 from delete_Some_set_of [OF Some] 517 have t2'_t2: "set_of t\<^sub>2' \<subseteq> set_of t\<^sub>2" . 518 from delete_Some_x_set_of [OF Some] 519 obtain x_t2: "x \<in> set_of t\<^sub>2" and x_not_t2': "x \<notin> set_of t\<^sub>2'" 520 by simp 521 522 show ?thesis 523 proof (cases "subtract l t\<^sub>2'") 524 case (Some t\<^sub>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\<^sub>2''" . 530 from subtract_Some_set_of [OF Some] 531 have l_t2': "set_of l \<subseteq> set_of t\<^sub>2'" . 532 from subtract_Some_set_of_res [OF Some] 533 have t2''_t2': "set_of t\<^sub>2'' \<subseteq> set_of t\<^sub>2'" . 534 from subtract_Some_dist_res [OF Some] 535 have dist_l_t2'': "set_of l \<inter> set_of t\<^sub>2'' = {}". 536 show ?thesis 537 proof (cases "subtract r t\<^sub>2''") 538 case (Some t\<^sub>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\<^sub>2''" . 543 from subtract_Some_dist_res [OF Some] 544 have dist_r_t2''': "set_of r \<inter> set_of t\<^sub>2''' = {}". 545 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 566qed 567 568 569lemma 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)" 573proof - 574 from delete_Some_x_set_of [OF del_l] 575 obtain x: "x \<in> set_of l" 576 by simp 577 with dist 578 have "delete x r = None" 579 by (cases "delete x r") (auto dest:delete_Some_x_set_of) 580 581 with x 582 show ?thesis 583 using del_l dist 584 by (auto split: option.splits) 585qed 586 587lemma 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')" 591proof - 592 from delete_Some_x_set_of [OF del_r] 593 obtain x: "x \<in> set_of r" 594 by simp 595 with dist 596 have "delete x l = None" 597 by (cases "delete x l") (auto dest:delete_Some_x_set_of) 598 599 with x 600 show ?thesis 601 using del_r dist 602 by (auto split: option.splits) 603qed 604 605lemma 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)" 608proof - 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) 617qed 618 619lemma 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'''" 624using del sub_l sub_r 625by simp 626 627lemma subtract_Tip: "subtract Tip t = Some t" 628 by simp 629 630text \<open>Now we have all the theorems in place that are needed for the 631certificate generating ML functions.\<close> 632 633ML_file "distinct_tree_prover.ML" 634 635end 636