1chapter HOL 2 3session HOL (main) = Pure + 4 description " 5 Classical Higher-order Logic. 6 " 7 options [strict_facts] 8 sessions Tools 9 theories 10 Main (global) 11 Complex_Main (global) 12 document_files 13 "root.bib" 14 "root.tex" 15 16session "HOL-Proofs" (timing) in Proofs = Pure + 17 description " 18 HOL-Main with explicit proof terms. 19 " 20 options [quick_and_dirty = false, record_proofs = 2, parallel_limit = 500] 21 sessions 22 "HOL-Library" 23 theories 24 "HOL-Library.Realizers" 25 26session "HOL-Library" (main timing) in Library = HOL + 27 description " 28 Classical Higher-order Logic -- batteries included. 29 " 30 theories 31 Library 32 (*conflicting type class instantiations and dependent applications*) 33 Finite_Lattice 34 List_Lexorder 35 Prefix_Order 36 Product_Lexorder 37 Product_Order 38 Subseq_Order 39 (*conflicting syntax*) 40 Datatype_Records 41 (*data refinements and dependent applications*) 42 AList_Mapping 43 Code_Binary_Nat 44 Code_Prolog 45 Code_Real_Approx_By_Float 46 Code_Target_Numeral 47 DAList 48 DAList_Multiset 49 RBT_Mapping 50 RBT_Set 51 (*printing modifications*) 52 OptionalSugar 53 (*prototypic tools*) 54 Predicate_Compile_Quickcheck 55 Quantified_Premise_Simproc 56 (*legacy tools*) 57 Old_Datatype 58 Old_Recdef 59 Realizers 60 Refute 61 document_files "root.bib" "root.tex" 62 63session "HOL-Analysis" (main timing) in Analysis = HOL + 64 options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", 65 document_variants = "document:manual=-proof,-ML,-unimportant"] 66 sessions 67 "HOL-Library" 68 "HOL-Computational_Algebra" 69 theories 70 Analysis 71 document_files 72 "root.tex" 73 "root.bib" 74 75session "HOL-Complex_Analysis" (main timing) in Complex_Analysis = "HOL-Analysis" + 76 options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", 77 document_variants = "document:manual=-proof,-ML,-unimportant"] 78 theories 79 Complex_Analysis 80 document_files 81 "root.tex" 82 "root.bib" 83 84session "HOL-Analysis-ex" in "Analysis/ex" = "HOL-Analysis" + 85 theories 86 Approximations 87 Metric_Arith_Examples 88 89session "HOL-Homology" (timing) in Homology = "HOL-Analysis" + 90 options [document_tags = "theorem%important,corollary%important,proposition%important,class%important,instantiation%important,subsubsection%unimportant,%unimportant", 91 document_variants = "document:manual=-proof,-ML,-unimportant"] 92 sessions 93 "HOL-Algebra" 94 theories 95 Homology 96 document_files 97 "root.tex" 98 99session "HOL-Computational_Algebra" (main timing) in "Computational_Algebra" = "HOL-Library" + 100 theories 101 Computational_Algebra 102 (*conflicting type class instantiations and dependent applications*) 103 Field_as_Ring 104 105session "HOL-Real_Asymp" in Real_Asymp = HOL + 106 sessions 107 "HOL-Decision_Procs" 108 theories 109 Real_Asymp 110 Real_Asymp_Approx 111 Real_Asymp_Examples 112 113session "HOL-Real_Asymp-Manual" in "Real_Asymp/Manual" = "HOL-Real_Asymp" + 114 theories 115 Real_Asymp_Doc 116 document_files (in "~~/src/Doc") 117 "iman.sty" 118 "extra.sty" 119 "isar.sty" 120 document_files 121 "root.tex" 122 "style.sty" 123 124session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" + 125 description " 126 Author: Gertrud Bauer, TU Munich 127 128 The Hahn-Banach theorem for real vector spaces. 129 130 This is the proof of the Hahn-Banach theorem for real vectorspaces, 131 following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach 132 theorem is one of the fundamental theorems of functional analysis. It is a 133 conclusion of Zorn's lemma. 134 135 Two different formaulations of the theorem are presented, one for general 136 real vectorspaces and its application to normed vectorspaces. 137 138 The theorem says, that every continous linearform, defined on arbitrary 139 subspaces (not only one-dimensional subspaces), can be extended to a 140 continous linearform on the whole vectorspace. 141 " 142 sessions 143 "HOL-Analysis" 144 theories 145 Hahn_Banach 146 document_files "root.bib" "root.tex" 147 148session "HOL-Induct" in Induct = "HOL-Library" + 149 description " 150 Examples of (Co)Inductive Definitions. 151 152 Comb proves the Church-Rosser theorem for combinators (see 153 http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz). 154 155 Mutil is the famous Mutilated Chess Board problem (see 156 http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz). 157 158 PropLog proves the completeness of a formalization of propositional logic 159 (see 160 http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz). 161 162 Exp demonstrates the use of iterated inductive definitions to reason about 163 mutually recursive relations. 164 " 165 theories [quick_and_dirty] 166 Common_Patterns 167 theories 168 Nested_Datatype 169 QuoDataType 170 QuoNestedDataType 171 Term 172 SList 173 ABexp 174 Infinitely_Branching_Tree 175 Ordinals 176 Sigma_Algebra 177 Comb 178 PropLog 179 Com 180 document_files "root.tex" 181 182session "HOL-IMP" (timing) in IMP = "HOL-Library" + 183 options [document_variants = document] 184 theories 185 BExp 186 ASM 187 Finite_Reachable 188 Denotational 189 Compiler2 190 Poly_Types 191 Sec_Typing 192 Sec_TypingT 193 Def_Init_Big 194 Def_Init_Small 195 Fold 196 Live 197 Live_True 198 Hoare_Examples 199 Hoare_Sound_Complete 200 VCG 201 Hoare_Total 202 VCG_Total_EX 203 VCG_Total_EX2 204 Collecting1 205 Collecting_Examples 206 Abs_Int_Tests 207 Abs_Int1_parity 208 Abs_Int1_const 209 Abs_Int3 210 Procs_Dyn_Vars_Dyn 211 Procs_Stat_Vars_Dyn 212 Procs_Stat_Vars_Stat 213 C_like 214 OO 215 document_files "root.bib" "root.tex" 216 217session "HOL-IMPP" in IMPP = HOL + 218 description \<open> 219 Author: David von Oheimb 220 Copyright 1999 TUM 221 222 IMPP -- An imperative language with procedures. 223 224 This is an extension of IMP with local variables and mutually recursive 225 procedures. For documentation see "Hoare Logic for Mutual Recursion and 226 Local Variables" (https://isabelle.in.tum.de/Bali/papers/FSTTCS99.html). 227 \<close> 228 theories EvenOdd 229 230session "HOL-Data_Structures" (timing) in Data_Structures = HOL + 231 options [document_variants = document] 232 sessions 233 "HOL-Number_Theory" 234 theories [document = false] 235 Less_False 236 theories 237 Sorting 238 Balance 239 Tree_Map 240 Interval_Tree 241 AVL_Map 242 RBT_Set2 243 RBT_Map 244 Tree23_Map 245 Tree234_Map 246 Brother12_Map 247 AA_Map 248 Set2_Join_RBT 249 Array_Braun 250 Trie_Fun 251 Trie_Map 252 Tries_Binary 253 Leftist_Heap 254 Binomial_Heap 255 document_files "root.tex" "root.bib" 256 257session "HOL-Import" in Import = HOL + 258 theories HOL_Light_Maps 259 theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import 260 261session "HOL-Number_Theory" (main timing) in Number_Theory = "HOL-Computational_Algebra" + 262 description " 263 Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler 264 Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity. 265 " 266 sessions 267 "HOL-Algebra" 268 theories 269 Number_Theory 270 document_files 271 "root.tex" 272 273session "HOL-Hoare" in Hoare = HOL + 274 description " 275 Verification of imperative programs (verification conditions are generated 276 automatically from pre/post conditions and loop invariants). 277 " 278 theories Hoare 279 document_files "root.bib" "root.tex" 280 281session "HOL-Hoare_Parallel" (timing) in Hoare_Parallel = HOL + 282 description " 283 Verification of shared-variable imperative programs a la Owicki-Gries. 284 (verification conditions are generated automatically). 285 " 286 theories Hoare_Parallel 287 document_files "root.bib" "root.tex" 288 289session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Number_Theory" + 290 sessions 291 "HOL-Data_Structures" 292 "HOL-ex" 293 theories 294 Generate 295 Generate_Binary_Nat 296 Generate_Target_Nat 297 Generate_Efficient_Datastructures 298 Code_Lazy_Test 299 Code_Test_PolyML 300 Code_Test_Scala 301 theories [condition = ISABELLE_GHC] 302 Code_Test_GHC 303 theories [condition = ISABELLE_MLTON] 304 Code_Test_MLton 305 theories [condition = ISABELLE_OCAMLFIND] 306 Code_Test_OCaml 307 theories [condition = ISABELLE_SMLNJ] 308 Code_Test_SMLNJ 309 310session "HOL-Metis_Examples" (timing) in Metis_Examples = "HOL-Library" + 311 description " 312 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 313 Author: Jasmin Blanchette, TU Muenchen 314 315 Testing Metis and Sledgehammer. 316 " 317 sessions 318 "HOL-Decision_Procs" 319 theories 320 Abstraction 321 Big_O 322 Binary_Tree 323 Clausification 324 Message 325 Proxies 326 Tarski 327 Trans_Closure 328 Sets 329 330session "HOL-Nitpick_Examples" in Nitpick_Examples = "HOL-Library" + 331 description " 332 Author: Jasmin Blanchette, TU Muenchen 333 Copyright 2009 334 " 335 theories [quick_and_dirty] Nitpick_Examples 336 337session "HOL-Algebra" (main timing) in Algebra = "HOL-Computational_Algebra" + 338 description " 339 Author: Clemens Ballarin, started 24 September 1999, and many others 340 341 The Isabelle Algebraic Library. 342 " 343 sessions 344 "HOL-Cardinals" 345 theories 346 (* Orders and Lattices *) 347 Galois_Connection (* Knaster-Tarski theorem and Galois connections *) 348 (* Groups *) 349 FiniteProduct (* Product operator for commutative groups *) 350 Sylow (* Sylow's theorem *) 351 Bij (* Automorphism Groups *) 352 Multiplicative_Group 353 Zassenhaus (* The Zassenhaus lemma *) 354 (* Rings *) 355 Divisibility (* Rings *) 356 IntRing (* Ideals and residue classes *) 357 UnivPoly (* Polynomials *) 358 (* Main theory *) 359 Algebra 360 document_files "root.bib" "root.tex" 361 362session "HOL-Auth" (timing) in Auth = "HOL-Library" + 363 description " 364 A new approach to verifying authentication protocols. 365 " 366 directories "Smartcard" "Guard" 367 theories 368 Auth_Shared 369 Auth_Public 370 "Smartcard/Auth_Smartcard" 371 "Guard/Auth_Guard_Shared" 372 "Guard/Auth_Guard_Public" 373 document_files "root.tex" 374 375session "HOL-UNITY" (timing) in UNITY = "HOL-Auth" + 376 description " 377 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 378 Copyright 1998 University of Cambridge 379 380 Verifying security protocols using Chandy and Misra's UNITY formalism. 381 " 382 directories "Simple" "Comp" 383 theories 384 (*Basic meta-theory*) 385 UNITY_Main 386 387 (*Simple examples: no composition*) 388 "Simple/Deadlock" 389 "Simple/Common" 390 "Simple/Network" 391 "Simple/Token" 392 "Simple/Channel" 393 "Simple/Lift" 394 "Simple/Mutex" 395 "Simple/Reach" 396 "Simple/Reachability" 397 398 (*Verifying security protocols using UNITY*) 399 "Simple/NSP_Bad" 400 401 (*Example of composition*) 402 "Comp/Handshake" 403 404 (*Universal properties examples*) 405 "Comp/Counter" 406 "Comp/Counterc" 407 "Comp/Priority" 408 409 "Comp/TimerArray" 410 "Comp/Progress" 411 412 "Comp/Alloc" 413 "Comp/AllocImpl" 414 "Comp/Client" 415 416 (*obsolete*) 417 ELT 418 document_files "root.tex" 419 420session "HOL-Unix" in Unix = "HOL-Library" + 421 options [print_mode = "no_brackets,no_type_brackets"] 422 theories Unix 423 document_files "root.bib" "root.tex" 424 425session "HOL-ZF" in ZF = "HOL-Library" + 426 theories 427 MainZF 428 Games 429 document_files "root.tex" 430 431session "HOL-Imperative_HOL" (timing) in Imperative_HOL = "HOL-Library" + 432 options [print_mode = "iff,no_brackets"] 433 directories "ex" 434 theories Imperative_HOL_ex 435 document_files "root.bib" "root.tex" 436 437session "HOL-Decision_Procs" (timing) in Decision_Procs = "HOL-Algebra" + 438 description " 439 Various decision procedures, typically involving reflection. 440 " 441 directories "ex" 442 theories 443 Decision_Procs 444 445session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" + 446 sessions 447 "HOL-Isar_Examples" 448 theories 449 Hilbert_Classical 450 Proof_Terms 451 XML_Data 452 453session "HOL-Proofs-Extraction" (timing) in "Proofs/Extraction" = "HOL-Proofs" + 454 description " 455 Examples for program extraction in Higher-Order Logic. 456 " 457 options [quick_and_dirty = false] 458 sessions 459 "HOL-Computational_Algebra" 460 theories 461 Greatest_Common_Divisor 462 Warshall 463 Higman_Extraction 464 Pigeonhole 465 Euclid 466 document_files "root.bib" "root.tex" 467 468session "HOL-Proofs-Lambda" (timing) in "Proofs/Lambda" = "HOL-Proofs" + 469 description \<open> 470 Lambda Calculus in de Bruijn's Notation. 471 472 This session defines lambda-calculus terms with de Bruijn indixes and 473 proves confluence of beta, eta and beta+eta. 474 475 The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole 476 theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html). 477 \<close> 478 options [print_mode = "no_brackets", quick_and_dirty = false] 479 sessions 480 "HOL-Library" 481 theories 482 Eta 483 StrongNorm 484 Standardization 485 WeakNorm 486 document_files "root.bib" "root.tex" 487 488session "HOL-Prolog" in Prolog = HOL + 489 description " 490 Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) 491 492 A bare-bones implementation of Lambda-Prolog. 493 494 This is a simple exploratory implementation of Lambda-Prolog in HOL, 495 including some minimal examples (in Test.thy) and a more typical example of 496 a little functional language and its type system. 497 " 498 theories Test Type 499 500session "HOL-MicroJava" (timing) in MicroJava = "HOL-Library" + 501 description " 502 Formalization of a fragment of Java, together with a corresponding virtual 503 machine and a specification of its bytecode verifier and a lightweight 504 bytecode verifier, including proofs of type-safety. 505 " 506 sessions 507 "HOL-Eisbach" 508 directories "BV" "Comp" "DFA" "J" "JVM" 509 theories 510 MicroJava 511 document_files 512 "introduction.tex" 513 "root.bib" 514 "root.tex" 515 516session "HOL-NanoJava" in NanoJava = HOL + 517 description " 518 Hoare Logic for a tiny fragment of Java. 519 " 520 theories Example 521 document_files "root.bib" "root.tex" 522 523session "HOL-Bali" (timing) in Bali = "HOL-Library" + 524 theories 525 AxExample 526 AxSound 527 AxCompl 528 Trans 529 TypeSafe 530 document_files "root.tex" 531 532session "HOL-IOA" in IOA = HOL + 533 description \<open> 534 Author: Tobias Nipkow and Konrad Slind and Olaf M��ller 535 Copyright 1994--1996 TU Muenchen 536 537 The meta-theory of I/O-Automata in HOL. This formalization has been 538 significantly changed and extended, see HOLCF/IOA. There are also the 539 proofs of two communication protocols which formerly have been here. 540 541 @inproceedings{Nipkow-Slind-IOA, 542 author={Tobias Nipkow and Konrad Slind}, 543 title={{I/O} Automata in {Isabelle/HOL}}, 544 booktitle={Proc.\ TYPES Workshop 1994}, 545 publisher=Springer, 546 series=LNCS, 547 note={To appear}} 548 ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz 549 550 and 551 552 @inproceedings{Mueller-Nipkow, 553 author={Olaf M\"uller and Tobias Nipkow}, 554 title={Combining Model Checking and Deduction for {I/O}-Automata}, 555 booktitle={Proc.\ TACAS Workshop}, 556 organization={Aarhus University, BRICS report}, 557 year=1995} 558 ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz 559 \<close> 560 theories Solve 561 562session "HOL-Lattice" in Lattice = HOL + 563 description " 564 Author: Markus Wenzel, TU Muenchen 565 566 Basic theory of lattices and orders. 567 " 568 theories CompleteLattice 569 document_files "root.tex" 570 571session "HOL-ex" (timing) in ex = "HOL-Number_Theory" + 572 description " 573 Miscellaneous examples for Higher-Order Logic. 574 " 575 theories 576 Adhoc_Overloading_Examples 577 Antiquote 578 Argo_Examples 579 Arith_Examples 580 Ballot 581 BinEx 582 Birthday_Paradox 583 Bit_Lists 584 Bubblesort 585 CTL 586 Cartouche_Examples 587 Case_Product 588 Chinese 589 Classical 590 Code_Binary_Nat_examples 591 Code_Lazy_Demo 592 Code_Timing 593 Coercion_Examples 594 Coherent 595 Commands 596 Computations 597 Conditional_Parametricity_Examples 598 Cubic_Quartic 599 Datatype_Record_Examples 600 Dedekind_Real 601 Erdoes_Szekeres 602 Eval_Examples 603 Executable_Relation 604 Execute_Choice 605 Functions 606 Function_Growth 607 Gauge_Integration 608 Groebner_Examples 609 Guess 610 HarmonicSeries 611 Hebrew 612 Hex_Bin_Examples 613 IArray_Examples 614 Iff_Oracle 615 Induction_Schema 616 Intuitionistic 617 Join_Theory 618 Lagrange 619 List_to_Set_Comprehension_Examples 620 LocaleTest2 621 "ML" 622 MergeSort 623 MonoidGroup 624 Multiquote 625 NatSum 626 Normalization_by_Evaluation 627 PER 628 Parallel_Example 629 Peano_Axioms 630 Perm_Fragments 631 PresburgerEx 632 Primrec 633 Pythagoras 634 Quicksort 635 Radix_Sort 636 Records 637 Reflection_Examples 638 Refute_Examples 639 Residue_Ring 640 Rewrite_Examples 641 SOS 642 SOS_Cert 643 Seq 644 Serbian 645 Set_Comprehension_Pointfree_Examples 646 Set_Theory 647 Simproc_Tests 648 Simps_Case_Conv_Examples 649 Sketch_and_Explore 650 Sorting_Algorithms_Examples 651 Sqrt 652 Sqrt_Script 653 Sudoku 654 Sum_of_Powers 655 Tarski 656 Termination 657 ThreeDivides 658 Transfer_Debug 659 Transfer_Int_Nat 660 Transitive_Closure_Table_Ex 661 Tree23 662 Triangular_Numbers 663 Unification 664 While_Combinator_Example 665 Word 666 veriT_Preprocessing 667 theories [skip_proofs = false] 668 SAT_Examples 669 Meson_Test 670 671session "HOL-Isar_Examples" in Isar_Examples = "HOL-Computational_Algebra" + 672 description " 673 Miscellaneous Isabelle/Isar examples. 674 " 675 options [quick_and_dirty] 676 theories 677 Knaster_Tarski 678 Peirce 679 Drinker 680 Cantor 681 Structured_Statements 682 Basic_Logic 683 Expr_Compiler 684 Fibonacci 685 Group 686 Group_Context 687 Group_Notepad 688 Hoare_Ex 689 Mutilated_Checkerboard 690 Puzzle 691 Summation 692 First_Order_Logic 693 Higher_Order_Logic 694 document_files 695 "root.bib" 696 "root.tex" 697 698session "HOL-Eisbach" in Eisbach = HOL + 699 description \<open> 700 The Eisbach proof method language and "match" method. 701 \<close> 702 sessions 703 FOL 704 "HOL-Analysis" 705 theories 706 Eisbach 707 Tests 708 Examples 709 Examples_FOL 710 Example_Metric 711 712session "HOL-SET_Protocol" (timing) in SET_Protocol = "HOL-Library" + 713 description " 714 Verification of the SET Protocol. 715 " 716 theories 717 SET_Protocol 718 document_files "root.tex" 719 720session "HOL-Matrix_LP" in Matrix_LP = "HOL-Library" + 721 description " 722 Two-dimensional matrices and linear programming. 723 " 724 directories "Compute_Oracle" 725 theories Cplex 726 document_files "root.tex" 727 728session "HOL-TLA" in TLA = HOL + 729 description " 730 Lamport's Temporal Logic of Actions. 731 " 732 theories TLA 733 734session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" + 735 theories Inc 736 737session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" + 738 theories DBuffer 739 740session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" + 741 theories MemoryImplementation 742 743session "HOL-TPTP" in TPTP = "HOL-Library" + 744 description " 745 Author: Jasmin Blanchette, TU Muenchen 746 Author: Nik Sultana, University of Cambridge 747 Copyright 2011 748 749 TPTP-related extensions. 750 " 751 theories 752 ATP_Theory_Export 753 MaSh_Eval 754 TPTP_Interpret 755 THF_Arith 756 TPTP_Proof_Reconstruction 757 theories 758 ATP_Problem_Import 759 760session "HOL-Probability" (main timing) in "Probability" = "HOL-Analysis" + 761 theories 762 Probability 763 document_files "root.tex" 764 765session "HOL-Probability-ex" (timing) in "Probability/ex" = "HOL-Probability" + 766 theories 767 Dining_Cryptographers 768 Koepf_Duermuth_Countermeasure 769 Measure_Not_CCC 770 771session "HOL-Nominal" in Nominal = "HOL-Library" + 772 theories 773 Nominal 774 775session "HOL-Nominal-Examples" (timing) in "Nominal/Examples" = "HOL-Nominal" + 776 theories 777 Class3 778 CK_Machine 779 Compile 780 Contexts 781 Crary 782 CR_Takahashi 783 CR 784 Fsub 785 Height 786 Lambda_mu 787 Lam_Funs 788 LocalWeakening 789 Pattern 790 SN 791 SOS 792 Standardization 793 Support 794 Type_Preservation 795 Weakening 796 W 797 theories [quick_and_dirty] 798 VC_Condition 799 800session "HOL-Cardinals" (timing) in Cardinals = HOL + 801 description " 802 Ordinals and Cardinals, Full Theories. 803 " 804 theories 805 Cardinals 806 Bounded_Set 807 document_files 808 "intro.tex" 809 "root.tex" 810 "root.bib" 811 812session "HOL-Datatype_Examples" (timing) in Datatype_Examples = "HOL-Library" + 813 description " 814 (Co)datatype Examples. 815 " 816 directories "Derivation_Trees" 817 theories 818 Compat 819 Lambda_Term 820 Process 821 TreeFsetI 822 "Derivation_Trees/Gram_Lang" 823 "Derivation_Trees/Parallel_Composition" 824 Koenig 825 Lift_BNF 826 Milner_Tofte 827 Stream_Processor 828 Cyclic_List 829 Free_Idempotent_Monoid 830 LDL 831 TLList 832 Misc_Codatatype 833 Misc_Datatype 834 Misc_Primcorec 835 Misc_Primrec 836 837session "HOL-Corec_Examples" (timing) in Corec_Examples = "HOL-Library" + 838 description " 839 Corecursion Examples. 840 " 841 directories "Tests" 842 theories 843 LFilter 844 Paper_Examples 845 Stream_Processor 846 "Tests/Simple_Nesting" 847 "Tests/Iterate_GPV" 848 theories [quick_and_dirty] 849 "Tests/GPV_Bare_Bones" 850 "Tests/Merge_D" 851 "Tests/Merge_Poly" 852 "Tests/Misc_Mono" 853 "Tests/Misc_Poly" 854 "Tests/Small_Concrete" 855 "Tests/Stream_Friends" 856 "Tests/TLList_Friends" 857 "Tests/Type_Class" 858 859session "HOL-Word" (main timing) in Word = HOL + 860 sessions 861 "HOL-Library" 862 theories 863 Word 864 More_Word 865 Word_Examples 866 document_files "root.bib" "root.tex" 867 868session "HOL-Statespace" in Statespace = HOL + 869 theories [skip_proofs = false] 870 StateSpaceEx 871 document_files "root.tex" 872 873session "HOL-Nonstandard_Analysis" (timing) in Nonstandard_Analysis = "HOL-Computational_Algebra" + 874 description " 875 Nonstandard analysis. 876 " 877 theories 878 Nonstandard_Analysis 879 document_files "root.tex" 880 881session "HOL-Nonstandard_Analysis-Examples" (timing) in "Nonstandard_Analysis/Examples" = "HOL-Nonstandard_Analysis" + 882 theories 883 NSPrimes 884 885session "HOL-Mirabelle" in Mirabelle = HOL + 886 theories Mirabelle_Test 887 888session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" + 889 options [timeout = 60] 890 theories Ex 891 892session "HOL-Word-SMT_Examples" (timing) in SMT_Examples = "HOL-Word" + 893 options [quick_and_dirty] 894 theories 895 Boogie 896 SMT_Examples 897 SMT_Word_Examples 898 SMT_Tests 899 900session "HOL-SPARK" in "SPARK" = "HOL-Word" + 901 theories 902 SPARK 903 904session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" + 905 directories "Gcd" "Liseq" "RIPEMD-160" "Sqrt" 906 theories 907 "Gcd/Greatest_Common_Divisor" 908 "Liseq/Longest_Increasing_Subsequence" 909 "RIPEMD-160/F" 910 "RIPEMD-160/Hash" 911 "RIPEMD-160/K_L" 912 "RIPEMD-160/K_R" 913 "RIPEMD-160/R_L" 914 "RIPEMD-160/Round" 915 "RIPEMD-160/R_R" 916 "RIPEMD-160/S_L" 917 "RIPEMD-160/S_R" 918 "Sqrt/Sqrt" 919 export_files (in ".") "*:**.prv" 920 921session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" + 922 options [show_question_marks = false] 923 sessions 924 "HOL-SPARK-Examples" 925 theories 926 Example_Verification 927 VC_Principles 928 Reference 929 Complex_Types 930 document_files 931 "complex_types.ads" 932 "complex_types_app.adb" 933 "complex_types_app.ads" 934 "Gcd.adb" 935 "Gcd.ads" 936 "intro.tex" 937 "loop_invariant.adb" 938 "loop_invariant.ads" 939 "root.bib" 940 "root.tex" 941 "Simple_Gcd.adb" 942 "Simple_Gcd.ads" 943 944session "HOL-Mutabelle" in Mutabelle = "HOL-Library" + 945 theories MutabelleExtra 946 947session "HOL-Quickcheck_Examples" (timing) in Quickcheck_Examples = "HOL-Library" + 948 theories 949 Quickcheck_Examples 950 Quickcheck_Lattice_Examples 951 Completeness 952 Quickcheck_Interfaces 953 Quickcheck_Nesting_Example 954 theories [condition = ISABELLE_GHC] 955 Hotel_Example 956 Quickcheck_Narrowing_Examples 957 958session "HOL-Quotient_Examples" (timing) in Quotient_Examples = "HOL-Algebra" + 959 description " 960 Author: Cezary Kaliszyk and Christian Urban 961 " 962 theories 963 DList 964 Quotient_FSet 965 Quotient_Int 966 Quotient_Message 967 Lift_FSet 968 Lift_Set 969 Lift_Fun 970 Quotient_Rat 971 Lift_DList 972 Int_Pow 973 Lifting_Code_Dt_Test 974 975session "HOL-Predicate_Compile_Examples" (timing) in Predicate_Compile_Examples = "HOL-Library" + 976 theories 977 Examples 978 Predicate_Compile_Tests 979 Predicate_Compile_Quickcheck_Examples 980 Specialisation_Examples 981 IMP_1 982 IMP_2 983 (* FIXME since 21-Jul-2011 984 Hotel_Example_Small_Generator *) 985 IMP_3 986 IMP_4 987 theories [condition = ISABELLE_SWIPL] 988 Code_Prolog_Examples 989 Context_Free_Grammar_Example 990 Hotel_Example_Prolog 991 Lambda_Example 992 List_Examples 993 theories [condition = ISABELLE_SWIPL, quick_and_dirty] 994 Reg_Exp_Example 995 996session "HOL-Types_To_Sets" in Types_To_Sets = HOL + 997 description " 998 Experimental extension of Higher-Order Logic to allow translation of types to sets. 999 " 1000 directories "Examples" 1001 theories 1002 Types_To_Sets 1003 "Examples/Prerequisites" 1004 "Examples/Finite" 1005 "Examples/T2_Spaces" 1006 "Examples/Unoverload_Def" 1007 "Examples/Linear_Algebra_On" 1008 1009session HOLCF (main timing) in HOLCF = HOL + 1010 description " 1011 Author: Franz Regensburger 1012 Author: Brian Huffman 1013 1014 HOLCF -- a semantic extension of HOL by the LCF logic. 1015 " 1016 sessions 1017 "HOL-Library" 1018 theories 1019 HOLCF (global) 1020 document_files "root.tex" 1021 1022session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF + 1023 theories 1024 Domain_ex 1025 Fixrec_ex 1026 New_Domain 1027 document_files "root.tex" 1028 1029session "HOLCF-Library" in "HOLCF/Library" = HOLCF + 1030 theories 1031 HOLCF_Library 1032 HOL_Cpo 1033 1034session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF + 1035 description " 1036 IMP -- A WHILE-language and its Semantics. 1037 1038 This is the HOLCF-based denotational semantics of a simple WHILE-language. 1039 " 1040 sessions 1041 "HOL-IMP" 1042 theories 1043 HoareEx 1044 document_files 1045 "isaverbatimwrite.sty" 1046 "root.tex" 1047 "root.bib" 1048 1049session "HOLCF-ex" in "HOLCF/ex" = "HOLCF-Library" + 1050 description " 1051 Miscellaneous examples for HOLCF. 1052 " 1053 theories 1054 Dnat 1055 Dagstuhl 1056 Focus_ex 1057 Fix2 1058 Hoare 1059 Concurrency_Monad 1060 Loop 1061 Powerdomain_ex 1062 Domain_Proofs 1063 Letrec 1064 Pattern_Match 1065 1066session "HOLCF-FOCUS" in "HOLCF/FOCUS" = "HOLCF-Library" + 1067 description \<open> 1068 FOCUS: a theory of stream-processing functions Isabelle/HOLCF. 1069 1070 For introductions to FOCUS, see 1071 1072 "The Design of Distributed Systems - An Introduction to FOCUS" 1073 http://www4.in.tum.de/publ/html.php?e=2 1074 1075 "Specification and Refinement of a Buffer of Length One" 1076 http://www4.in.tum.de/publ/html.php?e=15 1077 1078 "Specification and Development of Interactive Systems: Focus on Streams, 1079 Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321 1080 \<close> 1081 theories 1082 Fstreams 1083 FOCUS 1084 Buffer_adm 1085 1086session IOA (timing) in "HOLCF/IOA" = HOLCF + 1087 description " 1088 Author: Olaf Mueller 1089 Copyright 1997 TU M��nchen 1090 1091 A formalization of I/O automata in HOLCF. 1092 1093 The distribution contains simulation relations, temporal logic, and an 1094 abstraction theory. Everything is based upon a domain-theoretic model of 1095 finite and infinite sequences. 1096 " 1097 theories Abstraction 1098 1099session "IOA-ABP" in "HOLCF/IOA/ABP" = IOA + 1100 description " 1101 Author: Olaf Mueller 1102 1103 The Alternating Bit Protocol performed in I/O-Automata. 1104 " 1105 theories 1106 Correctness 1107 Spec 1108 1109session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA + 1110 description " 1111 Author: Tobias Nipkow & Konrad Slind 1112 1113 A network transmission protocol, performed in the 1114 I/O automata formalization by Olaf Mueller. 1115 " 1116 theories Correctness 1117 1118session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA + 1119 description " 1120 Author: Olaf Mueller 1121 1122 Memory storage case study. 1123 " 1124 theories Correctness 1125 1126session "IOA-ex" in "HOLCF/IOA/ex" = IOA + 1127 description " 1128 Author: Olaf Mueller 1129 " 1130 theories 1131 TrivEx 1132 TrivEx2 1133