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