## [7860bc]: thys / ClockSynchInst / LynchInstance.thy  Maximize  Restore  History

### 1043 lines (962 with data), 32.6 kB

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 (* Title: Instances of Schneider's generalized protocol of clock synchronization ID: $Id: LynchInstance.thy,v 1.12 2008-06-12 06:57:16 lsf37 Exp$ Author: Damiรกn Barsotti , 2006 Maintainer: Damiรกn Barsotti *) header {* Fault-tolerant Midpoint algorithm *} theory LynchInstance imports Complex_Main begin text {* This algorithm is presented in \cite{lynch_cs}. *} subsection {* Model of the system *} text {* The main ideas for the formalization of the system were obtained from \cite{shankar92mechanical}. *} subsubsection {* Types in the formalization *} text {* The election of the basics types was based on \cite{shankar92mechanical}. There, the process are natural numbers and the real time and the clock readings are reals. *} types process = nat time = real -- "real time" Clocktime = real -- "time of the clock readings (clock time)" subsubsection {* Some constants *} text{* Here we define some parameters of the algorithm that we use: the number of process and the number of lowest and highest readed values that the algorithm discards. The defined constants must satisfy this axiom. If not, the algorithm cannot obtain the maximum and minimum value, because it will have discarded all the values. *} axiomatization np :: nat -- "Number of processes" and khl :: nat -- "Number of lowest and highest values" where constants_ax: "2 * khl < np" text {* We define also the set of process that the algorithm manage. This definition exist only for readability matters. *} definition PR :: "process set" where [simp]: "PR = {.. Clocktime) \ process set \ process set" where "kmax f P = (SOME S. S \ P \ card S = khl \ (\ i\S. \ j\(P-S). f j <= f i))" definition kmin :: "(process \ Clocktime) \ process set \ process set" where "kmin f P = (SOME S. S \ P \ card S = khl \ (\ i\S. \ j\(P-S). f i <= f j))" text {* With the previus functions we define a new one @{term reduce}\footnote{The name of this function was taken from \cite{lynch_cs}.}. This take a function of clock readings and a set of processes and return de set of readings of the not dicarded processes. In order to define this function we use the image operator (@{term "op "}) of Isabelle.*} definition reduce :: "(process \ Clocktime) \ process set \ Clocktime set" where "reduce f P = f  (P - (kmax f P \ kmin f P))" text {* And finally the convergence function. This is defined with the builtin @{term Max} and @{term Min} functions of Isabelle. *} definition cfnl :: "process \ (process \ Clocktime) \ Clocktime" where "cfnl p f = (Max (reduce f PR) + Min (reduce f PR)) / 2" subsection {* Translation Invariance property.*} subsubsection {* Auxiliary lemmas *} text {* These lemmas proves the existence of the maximum and minimum of the image of a set, if the set is finite and not empty. *} (* The proofs are almost the same one that those of the lemmas @{thm *) (* [source] ex_Max} and @{thm [source] ex_Min} in the Isabelle's standard *) (* theories. *) lemma ex_Maxf: fixes S and f :: "'a \ ('b::linorder)" assumes fin: "finite S" shows "S \ {} ==> \m\S. \s \ S. f s \ f m" using fin proof (induct) case empty thus ?case by simp next case (insert x S) show ?case proof (cases) assume "S = {}" thus ?thesis by simp next assume nonempty: "S \ {}" then obtain m where m: "m\S" "\s\S. f s \ f m" using insert by blast show ?thesis proof (cases) assume "f x \ f m" thus ?thesis using m by blast next assume "~ f x \ f m" thus ?thesis using m by(simp add:linorder_not_le order_less_le) (blast intro: order_trans) qed qed qed lemma ex_Minf: fixes S and f :: "'a \ ('b::linorder)" assumes fin: "finite S" shows "S \ {} ==> \m\S. \s \ S. f m \ f s" using fin proof (induct) case empty thus ?case by simp next case (insert x S) show ?case proof (cases) assume "S = {}" thus ?thesis by simp next assume nonempty: "S \ {}" then obtain m where m: "m\S" "\s\S. f m \ f s" using insert by blast show ?thesis proof (cases) assume "f m \ f x" thus ?thesis using m by blast next assume "~ f m \ f x" thus ?thesis using m by(simp add:linorder_not_le order_less_le) (blast intro: order_trans) qed qed qed text {* This trivial lemma is needed by the next two. *} lemma khl_bound: "khl < np" using constants_ax by arith text {* The next two lemmas prove that de functions kmin and kmax return some values that satisfy their definition. This is not trivial because we need to prove the existence of these values, according to the rule of the Hilbert's operator. We will need this lemma many times because is the only thing that we know about these functions. *} lemma kmax_prop: fixes f :: "nat \ Clocktime" shows "(kmax f PR) \ PR \ card (kmax f PR) = khl \ (\i\(kmax f PR). \j\PR - (kmax f PR). f j \ f i)" proof- have "khl <= np \ (\ S. S \ PR \ card S = khl \ (\i\S. \j\PR - S. f j \ f i))" ( is "khl <= np \ ?P khl" ) proof(induct (khl)) have "?P 0" by force thus "0 <= np \ ?P 0" .. next fix n assume asm: "n <= np \ ?P n" show "Suc n <= np \ ?P (Suc n)" proof assume asm2: "Suc n <= np" with asm have "?P n" by simp then obtain S where SinPR : "S\PR" and cardS: "card S = n" and HI: "(\i\S. \j\PR - S. f j \ f i)" by blast let ?e = "SOME i. i\PR-S \ (\j\PR-S. f j \ f i)" let ?S = "insert ?e S" have "\i. i\PR-S \ (\j\PR-S. f j \ f i)" proof- from SinPR and finite_subset have "finite (PR-S)" by auto moreover from cardS and asm2 SinPR have "S\PR" by auto hence "PR-S \ {}" by auto ultimately show ?thesis using ex_Maxf by blast qed hence ePRS: "?e \ PR-S" and maxH: "(\j \ PR-S. f j \ f ?e)" by (auto dest!: someI_ex) from maxH and HI have "(\i\?S. \j\PR - ?S. f j \ f i)" by blast moreover from SinPR and finite_subset cardS and ePRS have "card ?S = Suc n" by (auto dest: card_insert_disjoint) moreover have "?S \ PR" using SinPR and ePRS by auto ultimately show "?P (Suc n)" by blast qed qed hence "?P khl" using khl_bound by auto then obtain S where "S\PR \ card S = khl \ (\i\S. \j\PR - S. f j \ f i)" .. thus ?thesis by (unfold kmax_def) (rule someI [where P="\S. S \ PR \ card S = khl \ (\i\S. \j\PR - S. f j \ f i)"]) qed lemma kmin_prop: fixes f :: "nat \ Clocktime" shows "(kmin f PR) \ PR \ card (kmin f PR) = khl \ (\i\(kmin f PR). \j\PR - (kmin f PR). f i \ f j)" proof- have "khl <= np \ (\ S. S \ PR \ card S = khl \ (\i\S. \j\PR - S. f i \ f j))" ( is "khl <= np \ ?P khl" ) proof(induct (khl)) have "?P 0" by force thus "0 <= np \ ?P 0" .. next fix n assume asm: "n <= np \ ?P n" show "Suc n <= np \ ?P (Suc n)" proof assume asm2: "Suc n <= np" with asm have "?P n" by simp then obtain S where SinPR : "S\PR" and cardS: "card S = n" and HI: "(\i\S. \j\PR - S. f i \ f j)" by blast let ?e = "SOME i. i\PR-S \ (\j\PR-S. f i \ f j)" let ?S = "insert ?e S" have "\i. i\PR-S \ (\j\PR-S. f i \ f j)" proof- from SinPR and finite_subset have "finite (PR-S)" by auto moreover from cardS and asm2 SinPR have "S\PR" by auto hence "PR-S \ {}" by auto ultimately show ?thesis using ex_Minf by blast qed hence ePRS: "?e \ PR-S" and minH: "(\j \ PR-S. f ?e \ f j)" by (auto dest!: someI_ex) from minH and HI have "(\i\?S. \j\PR - ?S. f i \ f j)" by blast moreover from SinPR and finite_subset and cardS and ePRS have "card ?S = Suc n" by (auto dest: card_insert_disjoint) moreover have "?S \ PR" using SinPR and ePRS by auto ultimately show "?P (Suc n)" by blast qed qed hence "?P khl" using khl_bound by auto then obtain S where "S\PR \ card S = khl \ (\i\S. \j\PR - S. f i \ f j)" .. thus ?thesis by (unfold kmin_def) (rule someI [where P="\S. S \ PR \ card S = khl \ (\i\S. \j\PR - S. f i \ f j)"]) qed text {* The next two lemmas are trivial from the previous ones *} lemma finite_kmax: "finite (kmax f PR)" proof- have "finite PR" by auto with kmax_prop and finite_subset show ?thesis by blast qed lemma finite_kmin: "finite (kmin f PR)" proof- have "finite PR" by auto with kmin_prop and finite_subset show ?thesis by blast qed text {* This lemma is necesary because the definition of the convergence function use the builtin Max and Min. *} lemma reduce_not_empty: "reduce f PR \ {}" proof- from constants_ax have "0 < (np - 2 * khl)" by arith also { from kmax_prop kmin_prop have "card (kmax f PR) = khl \ card (kmin f PR) = khl" by blast moreover from finite_kmax and finite_kmin card_Un_Int[THEN sym] have "card (kmax f PR \ kmin f PR) + card (kmax f PR \ kmin f PR) = card (kmax f PR) + card (kmin f PR)" by auto ultimately have "card (kmax f PR \ kmin f PR) <= 2 * khl" by auto } hence "... <= card PR - card (kmax f PR \ kmin f PR)" by simp also { from kmax_prop and kmin_prop have "(kmax f PR \ kmin f PR) \ PR" by blast } hence "... = card (PR-(kmax f PR \ kmin f PR))" apply (intro card_Diff_subset[THEN sym]) apply (rule finite_subset) by auto (* by (intro card_Diff_subset,auto) *) finally have "0 < card (PR-(kmax f PR \ kmin f PR))" . hence "(PR-(kmax f PR \ kmin f PR)) \ {}" by (intro notI, simp only: card_0_eq, simp) thus ?thesis by (auto simp add: reduce_def) qed text {* The next three are the main lemmas necessary for prove the Translation Invariance property.*} lemma reduce_shift: fixes f :: "nat \ Clocktime" shows "f  (PR - (kmax f PR \ kmin f PR)) = f  (PR - (kmax (\ p. f p + c) PR \ kmin (\ p. f p + c) PR))" apply (unfold kmin_def kmax_def) by simp lemma max_shift: fixes f :: "nat \ Clocktime" and S assumes notEmpFin: "S \ {}" "finite S" shows "Max (fS) + x = Max ( (\ p. f p + x)  S) " proof- from notEmpFin have "fS \ {}" and "(\ p. f p + x)  S \ {}" by auto with notEmpFin have "Max (fS) \ f  S " "Max ((\ p. f p + x)S) \ (\ p. f p + x)  S " "(\fs \ (fS). fs \ Max (fS))" "(\fs \ ((\ p. f p + x)S). fs \ Max ((\ p. f p + x)S))" by auto thus ?thesis by force qed lemma min_shift: fixes f :: "nat \ Clocktime" and S assumes notEmpFin: "S \ {}" "finite S" shows "Min (fS) + x = Min ( (\ p. f p + x)  S) " proof- from notEmpFin have "fS \ {}" and "(\ p. f p + x)  S \ {}" by auto with notEmpFin have "Min (fS) \ f  S " "Min ((\ p. f p + x)S) \ (\ p. f p + x)  S " "(\fs \ (fS). Min (fS) <= fs)" "(\fs \ ((\ p. f p + x)S). Min ((\ p. f p + x)S) <= fs)" by auto thus ?thesis by force qed subsubsection {* Main theorem *} theorem trans_inv: fixes f :: "nat \ Clocktime" shows "cfnl p f + x = cfnl p (\ p. f p + x)" proof- have "cfnl p (\ p. f p + x) = (Max (reduce (\ p. f p + x) PR) + Min (reduce (\ p. f p + x) PR)) / 2" by (unfold cfnl_def, simp) also have "... = (Max ((\ p. f p + x)  (PR - (kmax (\ p. f p + x) PR \ kmin (\ p. f p + x) PR))) + Min ((\ p. f p + x)  (PR - (kmax (\ p. f p + x) PR \ kmin (\ p. f p + x) PR)))) / 2" by (unfold reduce_def, simp) also have "... = (Max (f  (PR - (kmax (\ p. f p + x) PR \ kmin (\ p. f p + x) PR))) + x + Min (f  (PR - (kmax (\ p. f p + x) PR \ kmin (\ p. f p + x) PR))) + x ) / 2" proof- have "finite (PR - (kmax (\ p. f p + x) PR \ kmin (\ p. f p + x) PR))" by auto moreover from reduce_not_empty have "PR - (kmax (\ p. f p + x) PR \ kmin (\ p. f p + x) PR) \ {}" by (auto simp add: reduce_def) ultimately have "Max ((\ p. f p + x)  (PR - (kmax (\ p. f p + x) PR \ kmin (\ p. f p + x) PR))) = Max (f  (PR - (kmax (\ p. f p + x) PR \ kmin (\ p. f p + x) PR))) + x" and "Min ((\ p. f p + x)  (PR - (kmax (\ p. f p + x) PR \ kmin (\ p. f p + x) PR))) = Min (f  (PR - (kmax (\ p. f p + x) PR \ kmin (\ p. f p + x) PR))) + x" using max_shift and min_shift by auto thus ?thesis by auto qed also from reduce_shift have "... = (Max (f  (PR - (kmax f PR \ kmin f PR))) + x + Min (f  (PR - (kmax f PR \ kmin f PR))) + x ) / 2" by auto also have "... = ((Max (reduce f PR)+ x) + (Min (reduce f PR) + x)) / 2" by (auto simp add: reduce_def) also have "... = (Max (reduce f PR) + Min (reduce f PR)) / 2 + x" by auto finally show ?thesis by (auto simp add: cfnl_def) qed subsection {* Precision Enhancement property *} text {* An informal proof of this theorem can be found in \cite{miner93} *} subsubsection {* Auxiliary lemmas *} text {* This first lemma is most important for prove the property. This is a consecuence of the @{thm [source] card_Un_Int} lemma *} lemma pigeonhole: assumes finitA: "finite A" and Bss: "B \ A" and Css: "C \ A" and cardH: "card A + k <= card B + card C" shows "k <= card (B \ C)" proof- from Bss Css have "B \ C \ A" by blast with finitA have "card (B \ C) <= card A" by (simp add: card_mono) with cardH have h: "k <= card B + card C - card (B \ C)" by arith from finitA Bss Css and finite_subset have "finite B \ finite C" by auto thus ?thesis using card_Un_Int and h by force qed text {*This lemma is a trivial consecuence of the previous one. With only this lemma we can prove the Precision Enhancement property with the bound $\pi(x,y) = x + y$. But this bound not satisfy the property $\pi(2\Lambda + 2 \beta\rho, \delta_S + 2\rho(r_{max}+\beta) + 2\Lambda) \leq \delta_S$ that is used in \cite{shankar92mechanical} for prove the Schneider's schema. *} lemma subsets_int: assumes finitA: "finite A" and Bss: "B \ A" and Css: "C \ A" and cardH: "card A < card B + card C" shows "B \ C \ {}" proof- from finitA Bss Css cardH have "1 <= card (B \ C)" by (auto intro!: pigeonhole) thus ?thesis by auto qed text {* This lemma is true because @{term "reduce f PR"} is the image of @{term "PR-(kmax f PR \ kmin f PR)"} by the function @{term f}. *} lemma exist_reduce: "\ c \ reduce f PR. \ i\ PR-(kmax f PR \ kmin f PR). f i = c" proof fix c assume asm: "c \ reduce f PR" thus "\ i\ PR-(kmax f PR \ kmin f PR). f i = c" by (auto simp add: reduce_def kmax_def kmin_def) qed text {* The next three lemmas are consequence of the definition of @{term reduce}, @{term kmax} and @{term kmin} *} lemma finite_reduce: "finite (reduce f PR)" proof(unfold reduce_def) show "finite (f  (PR - (kmax f PR \ kmin f PR)))" by auto qed lemma kmax_ge: "\ i\ (kmax f PR). \ r \ (reduce f PR). r <= f i " proof fix i assume asm: "i \ kmax f PR" show "\r\reduce f PR. r \ f i" proof fix r assume asm2: "r \ reduce f PR" show "r \ f i" proof- from asm2 and exist_reduce have "\ j \ PR-(kmax f PR \ kmin f PR). f j = r" by blast then obtain j where fjr:"j \ PR-(kmax f PR \ kmin f PR) \ f j = r" by blast hence "j \ (PR - kmax f PR)" by blast from this fjr asm show ?thesis using kmax_prop by auto qed qed qed lemma kmin_le: "\ i\ (kmin f PR). \ r \ (reduce f PR). f i <= r " proof fix i assume asm: "i \ kmin f PR" show "\r\reduce f PR. f i \ r" proof fix r assume asm2: "r \ reduce f PR" show "f i <= r" proof- from asm2 and exist_reduce have "\ j\ PR-(kmax f PR \ kmin f PR). f j = r" by blast then obtain j where fjr:"j \ PR-(kmax f PR \ kmin f PR) \ f j = r" by blast hence "j \ (PR - kmin f PR)" by blast from this fjr asm show ?thesis using kmin_prop by auto qed qed qed text {* The next lemma is used for prove the Precision Enhancement property. This has been proved in ICS. The proof is in the appendix \ref{sec:abs_distrib_mult}. This cannot be prove by a simple @{text arith} or @{text auto} tactic. *} text{* This lemma is true also with @{text "0 <= c"} !! *} lemma abs_distrib_div: "0 < (c::real) \ \a / c - b / c\ = \a - b\ / c" proof- assume ch: "0a * d - b * d\ = \(a - b) * d\" by simp also with dh have "... = \a - b\ * d" by (simp add: abs_mult) finally have "\a * d - b * d\ = \a - b\ * d" . (* This sublemma is solved by ICS, file: abs_distrib_mult.ics *) (* It is not solved nor by (auto simp add: left_distrib real_diff_def)(arith) in Isabelle *) } with ch and divide_inverse show ?thesis by (auto simp add: divide_inverse) qed text {* The next three lemmas are about the existence of bounds of the values @{term "Max (reduce f PR)"} and @{term "Min (reduce f PR)"}. These are used in the proof of the main property. *} lemma uboundmax: assumes hC: "C \ PR" and hCk: "np <= card C + khl" shows "\ i\C. Max (reduce f PR) <= f i" proof- from reduce_not_empty and finite_reduce have maxrinr: "Max (reduce f PR) \ reduce f PR" by simp with exist_reduce have "\ i\ PR-(kmax f PR \ kmin f PR). f i = Max (reduce f PR)" by simp then obtain pmax where pmax_in_reduc: "pmax \ PR-(kmax f PR \ kmin f PR)" and fpmax_ismax: "f pmax = Max (reduce f PR)" .. hence "C \ insert pmax (kmax f PR) \ {}" proof- from kmax_prop and pmax_in_reduc and finite_kmax and hCk have "card PR < card C + card (insert pmax (kmax f PR))" by simp moreover from pmax_in_reduc and kmax_prop have "insert pmax (kmax f PR) \ PR" by blast moreover note hC ultimately show ?thesis using subsets_int[of PR C "insert pmax (kmax f PR)"] by simp qed hence res: "\ i\C. i=pmax \ i \ kmax f PR" by blast then obtain i where iinC: "i\C" and altern: "i=pmax \ i \ kmax f PR" .. thus ?thesis proof(cases "i=pmax") case True with iinC fpmax_ismax show ?thesis by force next case False with altern maxrinr fpmax_ismax kmax_ge have "f pmax <= f i" by simp with iinC fpmax_ismax show ?thesis by auto qed qed lemma lboundmin: assumes hC: "C \ PR" and hCk: "np <= card C + khl" shows "\ i\C. f i <= Min (reduce f PR)" proof- from reduce_not_empty and finite_reduce have minrinr: "Min (reduce f PR) \ reduce f PR" by simp with exist_reduce have "\ i\ PR-(kmax f PR \ kmin f PR). f i = Min (reduce f PR)" by simp then obtain pmin where pmin_in_reduc: "pmin \ PR-(kmax f PR \ kmin f PR)" and fpmin_ismin: "f pmin = Min (reduce f PR)" .. hence "C \ insert pmin (kmin f PR) \ {}" proof- from kmin_prop and pmin_in_reduc and finite_kmin and hCk have "card PR < card C + card (insert pmin (kmin f PR))" by simp moreover from pmin_in_reduc and kmin_prop have "insert pmin (kmin f PR) \ PR" by blast moreover note hC ultimately show ?thesis using subsets_int[of PR C "insert pmin (kmin f PR)"] by simp qed hence res: "\ i\C. i=pmin \ i \ kmin f PR" by blast then obtain i where iinC: "i\C" and altern: "i=pmin \ i \ kmin f PR" .. thus ?thesis proof(cases "i=pmin") case True with iinC fpmin_ismin show ?thesis by force next case False with altern minrinr fpmin_ismin kmin_le have "f i <= f pmin" by simp with iinC fpmin_ismin show ?thesis by auto qed qed lemma same_bound: assumes hC: "C \ PR" and hCk: "np <= card C + khl" and hnk: "3 * khl < np" shows "\ i\C. Min (reduce f PR) <= f i \ g i <= Max (reduce g PR) " proof- have b1: "khl + 1 <= card (C \ (PR - kmin f PR))" proof(rule pigeonhole) show "finite PR" by simp next show "C \ PR" by fact next show "PR - kmin f PR \ PR" by blast next show "card PR + (khl + 1) \ card C + card (PR - kmin f PR)" proof- from hnk and hCk have "np + khl < np + card C - khl" by arith also from kmin_prop have "... = np + card C - card (kmin f PR)" by auto also have "... = card C + (card PR - card (kmin f PR))" proof- from kmin_prop have "card (kmin f PR) <= card PR" by (intro card_mono, auto) thus ?thesis by (simp) qed also from kmin_prop have "... = card C + card (PR - kmin f PR)" proof- from kmin_prop and finite_kmin have "card PR - card (kmin f PR) = card (PR - kmin f PR)" by (intro card_Diff_subset[THEN sym])(auto) thus ?thesis by auto qed finally show ?thesis by (simp) qed qed have "C \ (PR - kmin f PR) \ (PR - kmax g PR) \ {}" proof(intro subsets_int) show "finite PR" by simp next show "C \ (PR - kmin f PR) \ PR" by blast next show "PR - kmax g PR \ PR" by blast next show "card PR < card (C \ (PR - kmin f PR)) + card (PR - kmax g PR)" proof- from kmax_prop and finite_kmax have "card (PR - kmax g PR)= card PR - card (kmax g PR) " by (intro card_Diff_subset, auto) with kmax_prop have "card (PR - kmax g PR) = card PR - khl" by simp with b1 show ?thesis by arith qed qed hence "\ i. i \ C \ i \ (PR - kmin f PR) \ i \ (PR - kmax g PR)" by blast then obtain i where in_C: "i \ C" and not_in_kmin: "i \ (PR - kmin f PR)" and not_in_kmax: "i \ (PR - kmax g PR)" by blast have "Min (reduce f PR) <= f i" proof(cases "i \ kmax f PR") case True from reduce_not_empty and finite_reduce have " Min (reduce f PR) \ reduce f PR" by auto with True show ?thesis using kmax_ge by blast next case False with not_in_kmin have "i \ PR - (kmax f PR \ kmin f PR)" by blast with reduce_def have "f i \ reduce f PR" by auto with reduce_not_empty and finite_reduce show ?thesis by auto qed moreover have "g i <= Max (reduce g PR)" proof(cases "i \ kmin g PR") case True from reduce_not_empty and finite_reduce have " Max (reduce g PR) \ reduce g PR" by auto with True show ?thesis using kmin_le by blast next case False with not_in_kmax have "i \ PR - (kmax g PR \ kmin g PR)" by blast with reduce_def have "g i \ reduce g PR" by auto with reduce_not_empty and finite_reduce show ?thesis by auto qed moreover note in_C ultimately show ?thesis by blast qed subsubsection {* Main theorem *} text {* The most part of this theorem can be proved with CVC-lite using the three previous lemmas (appendix \ref{sec:bound_prec_enh}).*} theorem prec_enh: assumes hC: "C \ PR" and hCF: "np - nF <= card C" and hFn: "3 * nF < np" and hFk: "nF = khl" and hbx: "\ l\C. \f l - g l\ <= x" and hby1: "\ l\C. \ m\C. \f l - f m\ <= y" and hby2: "\ l\C. \ m\C. \g l - g m\ <= y" and hpC: "p\C" and hqC: "q\C" shows "\ cfnl p f - cfnl q g \ <= y / 2 + x" proof- from hCF and hFk have hCk: "np <= card C + khl" by arith from hFn and hFk have hnk: "3 * khl < np" by arith let ?maxf = "Max (reduce f PR)" and ?minf = "Min (reduce f PR)" and ?maxg = "Max (reduce g PR)" and ?ming = "Min (reduce g PR)" from abs_distrib_div have "\cfnl p f - cfnl q g\ = \?maxf + ?minf + - ?maxg + - ?ming\ / 2" by (unfold cfnl_def, auto simp add: real_diff_def) moreover have "\?maxf + ?minf + - ?maxg + - ?ming\ <= y + 2 * x" -- {* The rest of the property can be proved by CVC-lite (see appendix \ref{sec:bound_prec_enh}) *} proof ( cases "0 <= ?maxf + ?minf + - ?maxg + - ?ming") case True hence "\?maxf + ?minf + - ?maxg + - ?ming\ = ?maxf + ?minf + - ?maxg + - ?ming" by arith moreover from uboundmax hC hCk obtain mxf where mxfinC: "mxf\C" and maxf: "?maxf <= f mxf" by blast moreover from lboundmin hC hCk obtain mng where mnginC: "mng\C" and ming: "g mng <= ?ming" by blast moreover from same_bound hC hCk hnk obtain mxn where mxninC: "mxn\C" and mxnf: "?minf \ f mxn" and mxng: "g mxn \ ?maxg" by blast ultimately have "\ ?maxf + ?minf + - ?maxg + - ?ming\ <= (f mxf + - g mng) + (f mxn + - g mxn)" by arith also from mxninC hbx abs_le_D1 have "... <= (f mxf + - g mng) + x" by (auto simp add: real_diff_def) also have "... = (f mxf + - f mng ) + ( f mng + - g mng) + x" by arith also have "... <= y + ( f mng + - g mng) + x" proof- from mxfinC mnginC hby1 abs_le_D1 have "f mxf + - f mng <= y" by (auto simp add: real_diff_def) thus ?thesis by (auto simp add: real_diff_def) qed also from mnginC hbx abs_le_D1 have "... <= y + 2 * x" by (auto simp add: real_diff_def) finally show ?thesis . next case False hence "\?maxf + ?minf + - ?maxg + - ?ming\ = ?maxg + ?ming + - ?maxf + - ?minf" by arith moreover from uboundmax hC hCk obtain mxg where mxginC: "mxg\C" and maxg: "?maxg <= g mxg" by blast moreover from lboundmin hC hCk obtain mnf where mnfinC: "mnf\C" and minf: "f mnf <= ?minf" by blast moreover from same_bound hC hCk hnk obtain mxn where mxninC: "mxn\C" and mxnf: "?ming \ g mxn" and mxng: "f mxn \ ?maxf" by blast ultimately have "\ ?maxf + ?minf + - ?maxg + - ?ming\ <= (g mxg + - f mnf) + (g mxn + - f mxn)" by arith also from mxninC hbx have "... <= (g mxg + - f mnf) + x" by (auto dest!: abs_le_D2) also have "... = (g mxg + - g mnf ) + ( g mnf + - f mnf) + x" by arith also have "... <= y + ( g mnf + - f mnf) + x" proof- from mxginC mnfinC hby2 abs_le_D1 have "g mxg + - g mnf <= y" by (auto simp add: real_diff_def) thus ?thesis by (auto simp add: real_diff_def) qed also from mnfinC hbx have "... <= y + 2 * x" by (auto dest!: abs_le_D2) finally show ?thesis . qed ultimately show ?thesis by simp qed subsection {* Accuracy Preservation property *} text {* No new lemmas are needed for prove this property. The bound has been found using the lemmas @{thm [source] uboundmax} and @{thm [source] lboundmin} *} text {* This theorem can be proved with ICS and CVC-lite assuming those lemmas (see appendix \ref{sec:accur_pres}). *} theorem accur_pres: assumes hC: "C \ PR" and hCF: "np - nF <= card C" and hFk: "nF = khl" and hby: "\ l\C. \ m\C. \f l - f m\ <= y" and hqC: "q\C" shows "\ cfnl p f - f q \ <= y" proof- from hCF and hFk have npleCk: "np <= card C + khl" by arith show ?thesis proof(cases "f q <= cfnl p f") case True from npleCk hC and uboundmax have "\ i\C. Max (reduce f PR) <= f i" by auto then obtain pi where hpiC: "pi \ C" and fpiGeMax: "Max (reduce f PR) <= f pi" by blast from reduce_not_empty have "Min (reduce f PR) <= Max (reduce f PR)" by (auto simp add: reduce_def) with fpiGeMax have cfnlLefpi: "cfnl p f <= f pi" by (auto simp add: cfnl_def) with True have "\ cfnl p f - f q \ <= \ f pi - f q \" by arith with hpiC and hqC and hby show ?thesis by force next case False from npleCk hC and lboundmin have "\ i\C. f i <= Min (reduce f PR)" by auto then obtain qi where hqiC: "qi \ C" and fqiLeMax: "f qi <= Min (reduce f PR)" by blast from reduce_not_empty have "Min (reduce f PR) <= Max (reduce f PR)" by (auto simp add: reduce_def) with fqiLeMax have "f qi <= cfnl p f" by (auto simp add: cfnl_def) with False have "\ cfnl p f - f q \ <= \ f qi - f q \" by arith with hqiC and hqC and hby show ?thesis by force qed qed end `