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