Mercurialisabelle / file revision
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/ROOT
author nipkow
Sun Oct 25 17:30:06 2015 +0100 (2015-10-25)
changeset 61514 213556e498c2
parent 61469 cd82b1023932
child 61525 87244a9cfe40
permissions -rw-r--r--
added 234-Trees (slow) 
     1 chapter HOL

     2 

     3 session HOL (main) = Pure +

     4   description {*

     5     Classical Higher-order Logic.

     6   *}

     7   global_theories

     8     Main

     9     Complex_Main

    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" (slow) = Pure +

    18   description {*

    19     HOL-Main with explicit proof terms.

    20   *}

    21   options [document = false, quick_and_dirty = false]

    22   theories Proofs (*sequential change of global flag!*)

    23   theories "~~/src/HOL/Library/Old_Datatype"

    24   files

    25     "Tools/Quickcheck/Narrowing_Engine.hs"

    26     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"

    27 

    28 session "HOL-Library" (main) in Library = HOL +

    29   description {*

    30     Classical Higher-order Logic -- batteries included.

    31   *}

    32   theories

    33     Library

    34     Rewrite

    35     (*conflicting type class instantiations*)

    36     List_lexord

    37     Sublist_Order

    38     Product_Lexorder

    39     Product_Order

    40     Finite_Lattice

    41     (*data refinements and dependent applications*)

    42     AList_Mapping

    43     Code_Binary_Nat

    44     Code_Char

    45     Code_Prolog

    46     Code_Real_Approx_By_Float

    47     Code_Target_Numeral

    48     DAList

    49     DAList_Multiset

    50     RBT_Mapping

    51     RBT_Set

    52     (*legacy tools*)

    53     Refute

    54     Old_Datatype

    55     Old_Recdef

    56     Old_SMT

    57   document_files "root.bib" "root.tex"

    58 

    59 session "HOL-Hahn_Banach" in Hahn_Banach = HOL +

    60   description {*

    61     Author:     Gertrud Bauer, TU Munich

    62 

    63     The Hahn-Banach theorem for real vector spaces.

    64 

    65     This is the proof of the Hahn-Banach theorem for real vectorspaces,

    66     following H. Heuser, Funktionalanalysis, p. 228 -232. The Hahn-Banach

    67     theorem is one of the fundamental theorems of functional analysis. It is a

    68     conclusion of Zorn's lemma.

    69 

    70     Two different formaulations of the theorem are presented, one for general

    71     real vectorspaces and its application to normed vectorspaces.

    72 

    73     The theorem says, that every continous linearform, defined on arbitrary

    74     subspaces (not only one-dimensional subspaces), can be extended to a

    75     continous linearform on the whole vectorspace.

    76   *}

    77   theories Hahn_Banach

    78   document_files "root.bib" "root.tex"

    79 

    80 session "HOL-Induct" in Induct = HOL +

    81   description {*

    82     Examples of (Co)Inductive Definitions.

    83 

    84     Comb proves the Church-Rosser theorem for combinators (see

    85     http://www.cl.cam.ac.uk/ftp/papers/reports/TR396-lcp-generic-automatic-proof-tools.ps.gz).

    86 

    87     Mutil is the famous Mutilated Chess Board problem (see

    88     http://www.cl.cam.ac.uk/ftp/papers/reports/TR394-lcp-mutilated-chess-board.dvi.gz).

    89 

    90     PropLog proves the completeness of a formalization of propositional logic

    91     (see

    92     http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz).

    93 

    94     Exp demonstrates the use of iterated inductive definitions to reason about

    95     mutually recursive relations.

    96   *}

    97   theories [document = false]

    98     "~~/src/HOL/Library/Old_Datatype"

    99   theories [quick_and_dirty]

   100     Common_Patterns

   101   theories

   102     QuoDataType

   103     QuoNestedDataType

   104     Term

   105     SList

   106     ABexp

   107     Tree

   108     Ordinals

   109     Sigma_Algebra

   110     Comb

   111     PropLog

   112     Com

   113   document_files "root.tex"

   114 

   115 session "HOL-IMP" in IMP = HOL +

   116   options [document_variants = document]

   117   theories [document = false]

   118     "~~/src/Tools/Permanent_Interpretation"

   119     "~~/src/HOL/Library/While_Combinator"

   120     "~~/src/HOL/Library/Char_ord"

   121     "~~/src/HOL/Library/List_lexord"

   122     "~~/src/HOL/Library/Quotient_List"

   123     "~~/src/HOL/Library/Extended"

   124   theories

   125     BExp

   126     ASM

   127     Finite_Reachable

   128     Denotational

   129     Compiler2

   130     Poly_Types

   131     Sec_Typing

   132     Sec_TypingT

   133     Def_Init_Big

   134     Def_Init_Small

   135     Fold

   136     Live

   137     Live_True

   138     Hoare_Examples

   139     VCG

   140     Hoare_Total

   141     Collecting1

   142     Collecting_Examples

   143     Abs_Int_Tests

   144     Abs_Int1_parity

   145     Abs_Int1_const

   146     Abs_Int3

   147     "Abs_Int_ITP/Abs_Int1_parity_ITP"

   148     "Abs_Int_ITP/Abs_Int1_const_ITP"

   149     "Abs_Int_ITP/Abs_Int3_ITP"

   150     "Abs_Int_Den/Abs_Int_den2"

   151     Procs_Dyn_Vars_Dyn

   152     Procs_Stat_Vars_Dyn

   153     Procs_Stat_Vars_Stat

   154     C_like

   155     OO

   156   document_files "root.bib" "root.tex"

   157 

   158 session "HOL-IMPP" in IMPP = HOL +

   159   description {*

   160     Author:     David von Oheimb

   161     Copyright   1999 TUM

   162 

   163     IMPP -- An imperative language with procedures.

   164 

   165     This is an extension of IMP with local variables and mutually recursive

   166     procedures. For documentation see "Hoare Logic for Mutual Recursion and

   167     Local Variables" (http://isabelle.in.tum.de/Bali/papers/FSTTCS99.html).

   168   *}

   169   options [document = false]

   170   theories EvenOdd

   171 

   172 session "HOL-Data_Structures" in Data_Structures = HOL +

   173   options [document_variants = document]

   174   theories [document = false]

   175     "Less_False"

   176   theories

   177     Tree_Set

   178     Tree_Map

   179     AVL_Map

   180     RBT_Map

   181     Tree23_Map

   182     Tree234_Map

   183   document_files "root.tex" "root.bib"

   184 

   185 session "HOL-Import" in Import = HOL +

   186   theories HOL_Light_Maps

   187   theories [condition = HOL_LIGHT_BUNDLE] HOL_Light_Import

   188 

   189 session "HOL-Number_Theory" in Number_Theory = HOL +

   190   description {*

   191     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler

   192     Theorem, Wilson's Theorem, some lemmas for Quadratic Reciprocity.

   193   *}

   194   theories [document = false]

   195     "~~/src/HOL/Library/FuncSet"

   196     "~~/src/HOL/Library/Multiset"

   197     "~~/src/HOL/Algebra/Ring"

   198     "~~/src/HOL/Algebra/FiniteProduct"

   199   theories

   200     Pocklington

   201     Gauss

   202     Number_Theory

   203     Euclidean_Algorithm

   204     Factorial_Ring

   205   document_files

   206     "root.tex"

   207 

   208 session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +

   209   description {*

   210     Fundamental Theorem of Arithmetic, Chinese Remainder Theorem, Fermat/Euler

   211     Theorem, Wilson's Theorem, Quadratic Reciprocity.

   212   *}

   213   theories [document = false]

   214     "~~/src/HOL/Library/Infinite_Set"

   215     "~~/src/HOL/Library/Permutation"

   216   theories

   217     Fib

   218     Factorization

   219     Chinese

   220     WilsonRuss

   221     WilsonBij

   222     Quadratic_Reciprocity

   223     Primes

   224     Pocklington

   225   document_files

   226     "root.bib"

   227     "root.tex"

   228 

   229 session "HOL-Hoare" in Hoare = HOL +

   230   description {*

   231     Verification of imperative programs (verification conditions are generated

   232     automatically from pre/post conditions and loop invariants).

   233   *}

   234   theories Hoare

   235   document_files "root.bib" "root.tex"

   236 

   237 session "HOL-Hoare_Parallel" in Hoare_Parallel = HOL +

   238   description {*

   239     Verification of shared-variable imperative programs a la Owicki-Gries.

   240     (verification conditions are generated automatically).

   241   *}

   242   theories Hoare_Parallel

   243   document_files "root.bib" "root.tex"

   244 

   245 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +

   246   options [condition = ML_SYSTEM_POLYML, document = false, browser_info = false]

   247   theories

   248     Generate

   249     Generate_Binary_Nat

   250     Generate_Target_Nat

   251     Generate_Efficient_Datastructures

   252     Generate_Pretty_Char

   253   theories [condition = ISABELLE_GHC]

   254     Code_Test_GHC

   255   theories [condition = ISABELLE_MLTON]

   256     Code_Test_MLton

   257   theories [condition = ISABELLE_OCAMLC]

   258     Code_Test_OCaml

   259   theories [condition = ISABELLE_POLYML]

   260     Code_Test_PolyML

   261   theories [condition = ISABELLE_SCALA]

   262     Code_Test_Scala

   263   theories [condition = ISABELLE_SMLNJ]

   264     Code_Test_SMLNJ

   265 

   266 session "HOL-Metis_Examples" in Metis_Examples = HOL +

   267   description {*

   268     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

   269     Author:     Jasmin Blanchette, TU Muenchen

   270 

   271     Testing Metis and Sledgehammer.

   272   *}

   273   options [document = false]

   274   theories

   275     Abstraction

   276     Big_O

   277     Binary_Tree

   278     Clausification

   279     Message

   280     Proxies

   281     Tarski

   282     Trans_Closure

   283     Sets

   284 

   285 session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +

   286   description {*

   287     Author:     Jasmin Blanchette, TU Muenchen

   288     Copyright   2009

   289   *}

   290   options [document = false]

   291   theories [quick_and_dirty] Nitpick_Examples

   292 

   293 session "HOL-Algebra" (main) in Algebra = HOL +

   294   description {*

   295     Author: Clemens Ballarin, started 24 September 1999

   296 

   297     The Isabelle Algebraic Library.

   298   *}

   299   theories [document = false]

   300     (* Preliminaries from set and number theory *)

   301     "~~/src/HOL/Library/FuncSet"

   302     "~~/src/HOL/Number_Theory/Primes"

   303     "~~/src/HOL/Library/Permutation"

   304   theories

   305     (*** New development, based on explicit structures ***)

   306     (* Groups *)

   307     FiniteProduct        (* Product operator for commutative groups *)

   308     Sylow                (* Sylow's theorem *)

   309     Bij                  (* Automorphism Groups *)

   310 

   311     (* Rings *)

   312     Divisibility         (* Rings *)

   313     IntRing              (* Ideals and residue classes *)

   314     UnivPoly             (* Polynomials *)

   315   document_files "root.bib" "root.tex"

   316 

   317 session "HOL-Auth" in Auth = HOL +

   318   description {*

   319     A new approach to verifying authentication protocols.

   320   *}

   321   theories

   322     Auth_Shared

   323     Auth_Public

   324     "Smartcard/Auth_Smartcard"

   325     "Guard/Auth_Guard_Shared"

   326     "Guard/Auth_Guard_Public"

   327   document_files "root.tex"

   328 

   329 session "HOL-UNITY" in UNITY = "HOL-Auth" +

   330   description {*

   331     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

   332     Copyright   1998  University of Cambridge

   333 

   334     Verifying security protocols using Chandy and Misra's UNITY formalism.

   335   *}

   336   theories

   337     (*Basic meta-theory*)

   338     "UNITY_Main"

   339 

   340     (*Simple examples: no composition*)

   341     "Simple/Deadlock"

   342     "Simple/Common"

   343     "Simple/Network"

   344     "Simple/Token"

   345     "Simple/Channel"

   346     "Simple/Lift"

   347     "Simple/Mutex"

   348     "Simple/Reach"

   349     "Simple/Reachability"

   350 

   351     (*Verifying security protocols using UNITY*)

   352     "Simple/NSP_Bad"

   353 

   354     (*Example of composition*)

   355     "Comp/Handshake"

   356 

   357     (*Universal properties examples*)

   358     "Comp/Counter"

   359     "Comp/Counterc"

   360     "Comp/Priority"

   361 

   362     "Comp/TimerArray"

   363     "Comp/Progress"

   364 

   365     "Comp/Alloc"

   366     "Comp/AllocImpl"

   367     "Comp/Client"

   368 

   369     (*obsolete*)

   370     "ELT"

   371   document_files "root.tex"

   372 

   373 session "HOL-Unix" in Unix = HOL +

   374   options [print_mode = "no_brackets,no_type_brackets"]

   375   theories Unix

   376   document_files "root.bib" "root.tex"

   377 

   378 session "HOL-ZF" in ZF = HOL +

   379   theories MainZF Games

   380   document_files "root.tex"

   381 

   382 session "HOL-Imperative_HOL" in Imperative_HOL = HOL +

   383   options [print_mode = "iff,no_brackets"]

   384   theories [document = false]

   385     "~~/src/HOL/Library/Countable"

   386     "~~/src/HOL/Library/Monad_Syntax"

   387     "~~/src/HOL/Library/LaTeXsugar"

   388   theories Imperative_HOL_ex

   389   document_files "root.bib" "root.tex"

   390 

   391 session "HOL-Decision_Procs" in Decision_Procs = HOL +

   392   description {*

   393     Various decision procedures, typically involving reflection.

   394   *}

   395   options [condition = ML_SYSTEM_POLYML, document = false]

   396   theories Decision_Procs

   397 

   398 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +

   399   options [document = false, parallel_proofs = 0]

   400   theories

   401     Hilbert_Classical

   402     XML_Data

   403 

   404 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +

   405   description {*

   406     Examples for program extraction in Higher-Order Logic.

   407   *}

   408   options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0, quick_and_dirty = false]

   409   theories [document = false]

   410     "~~/src/HOL/Library/Code_Target_Numeral"

   411     "~~/src/HOL/Library/Monad_Syntax"

   412     "~~/src/HOL/Number_Theory/Primes"

   413     "~~/src/HOL/Number_Theory/UniqueFactorization"

   414     "~~/src/HOL/Library/State_Monad"

   415   theories

   416     Greatest_Common_Divisor

   417     Warshall

   418     Higman_Extraction

   419     Pigeonhole

   420     Euclid

   421   document_files "root.bib" "root.tex"

   422 

   423 session "HOL-Proofs-Lambda" in "Proofs/Lambda" = "HOL-Proofs" +

   424   description {*

   425     Lambda Calculus in de Bruijn's Notation.

   426 

   427     This session defines lambda-calculus terms with de Bruijn indixes and

   428     proves confluence of beta, eta and beta+eta.

   429 

   430     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole

   431     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).

   432   *}

   433   options [print_mode = "no_brackets", parallel_proofs = 0, quick_and_dirty = false]

   434   theories [document = false]

   435     "~~/src/HOL/Library/Code_Target_Int"

   436   theories

   437     Eta

   438     StrongNorm

   439     Standardization

   440     WeakNorm

   441   document_files "root.bib" "root.tex"

   442 

   443 session "HOL-Prolog" in Prolog = HOL +

   444   description {*

   445     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)

   446 

   447     A bare-bones implementation of Lambda-Prolog.

   448 

   449     This is a simple exploratory implementation of Lambda-Prolog in HOL,

   450     including some minimal examples (in Test.thy) and a more typical example of

   451     a little functional language and its type system.

   452   *}

   453   options [document = false]

   454   theories Test Type

   455 

   456 session "HOL-MicroJava" in MicroJava = HOL +

   457   description {*

   458     Formalization of a fragment of Java, together with a corresponding virtual

   459     machine and a specification of its bytecode verifier and a lightweight

   460     bytecode verifier, including proofs of type-safety.

   461   *}

   462   theories [document = false]

   463     "~~/src/HOL/Library/While_Combinator"

   464   theories

   465     MicroJava

   466   document_files

   467     "introduction.tex"

   468     "root.bib"

   469     "root.tex"

   470 

   471 session "HOL-NanoJava" in NanoJava = HOL +

   472   description {*

   473     Hoare Logic for a tiny fragment of Java.

   474   *}

   475   theories Example

   476   document_files "root.bib" "root.tex"

   477 

   478 session "HOL-Bali" in Bali = HOL +

   479   theories

   480     AxExample

   481     AxSound

   482     AxCompl

   483     Trans

   484     TypeSafe

   485   document_files "root.tex"

   486 

   487 session "HOL-IOA" in IOA = HOL +

   488   description {*

   489     Author:     Tobias Nipkow and Konrad Slind and Olaf Müller

   490     Copyright   1994--1996  TU Muenchen

   491 

   492     The meta-theory of I/O-Automata in HOL. This formalization has been

   493     significantly changed and extended, see HOLCF/IOA. There are also the

   494     proofs of two communication protocols which formerly have been here.

   495 

   496     @inproceedings{Nipkow-Slind-IOA,

   497     author={Tobias Nipkow and Konrad Slind},

   498     title={{I/O} Automata in {Isabelle/HOL}},

   499     booktitle={Proc.\ TYPES Workshop 1994},

   500     publisher=Springer,

   501     series=LNCS,

   502     note={To appear}}

   503     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz

   504 

   505     and

   506 

   507     @inproceedings{Mueller-Nipkow,

   508     author={Olaf M\"uller and Tobias Nipkow},

   509     title={Combining Model Checking and Deduction for {I/O}-Automata},

   510     booktitle={Proc.\ TACAS Workshop},

   511     organization={Aarhus University, BRICS report},

   512     year=1995}

   513     ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/tacas.dvi.gz

   514   *}

   515   options [document = false]

   516   theories Solve

   517 

   518 session "HOL-Lattice" in Lattice = HOL +

   519   description {*

   520     Author:     Markus Wenzel, TU Muenchen

   521 

   522     Basic theory of lattices and orders.

   523   *}

   524   theories CompleteLattice

   525   document_files "root.tex"

   526 

   527 session "HOL-ex" in ex = HOL +

   528   description {*

   529     Miscellaneous examples for Higher-Order Logic.

   530   *}

   531   options [condition = ML_SYSTEM_POLYML]

   532   theories [document = false]

   533     "~~/src/HOL/Library/State_Monad"

   534     Code_Binary_Nat_examples

   535     "~~/src/HOL/Library/FuncSet"

   536     Eval_Examples

   537     Normalization_by_Evaluation

   538     Hebrew

   539     Chinese

   540     Serbian

   541     "~~/src/HOL/Library/FinFun_Syntax"

   542     "~~/src/HOL/Library/Refute"

   543     "~~/src/HOL/Library/Transitive_Closure_Table"

   544     Cartouche_Examples

   545   theories

   546     Commands

   547     Adhoc_Overloading_Examples

   548     Iff_Oracle

   549     Coercion_Examples

   550     Higher_Order_Logic

   551     Abstract_NAT

   552     Guess

   553     Fundefs

   554     Induction_Schema

   555     LocaleTest2

   556     Records

   557     While_Combinator_Example

   558     MonoidGroup

   559     BinEx

   560     Hex_Bin_Examples

   561     Antiquote

   562     Multiquote

   563     PER

   564     NatSum

   565     ThreeDivides

   566     Cubic_Quartic

   567     Pythagoras

   568     Intuitionistic

   569     CTL

   570     Arith_Examples

   571     Tree23

   572     Bubblesort

   573     MergeSort

   574     Lagrange

   575     Groebner_Examples

   576     MT

   577     Unification

   578     Primrec

   579     Tarski

   580     Classical

   581     Set_Theory

   582     Termination

   583     Coherent

   584     PresburgerEx

   585     Reflection_Examples

   586     Sqrt

   587     Sqrt_Script

   588     Transfer_Debug

   589     Transfer_Ex

   590     Transfer_Int_Nat

   591     Transitive_Closure_Table_Ex

   592     HarmonicSeries

   593     Refute_Examples

   594     Execute_Choice

   595     Gauge_Integration

   596     Dedekind_Real

   597     Quicksort

   598     Birthday_Paradox

   599     List_to_Set_Comprehension_Examples

   600     Seq

   601     Simproc_Tests

   602     Executable_Relation

   603     FinFunPred

   604     Set_Comprehension_Pointfree_Examples

   605     Parallel_Example

   606     IArray_Examples

   607     Simps_Case_Conv_Examples

   608     ML

   609     Rewrite_Examples

   610     SAT_Examples

   611     SOS

   612     SOS_Cert

   613     Ballot

   614     Erdoes_Szekeres

   615     Sum_of_Powers

   616   theories [skip_proofs = false]

   617     Meson_Test

   618   theories [condition = ISABELLE_FULL_TEST]

   619     Sudoku

   620   document_files "root.bib" "root.tex"

   621 

   622 session "HOL-Isar_Examples" in Isar_Examples = HOL +

   623   description {*

   624     Miscellaneous Isabelle/Isar examples for Higher-Order Logic.

   625   *}

   626   theories [document = false]

   627     "~~/src/HOL/Library/Lattice_Syntax"

   628     "../Number_Theory/Primes"

   629   theories

   630     Basic_Logic

   631     Cantor

   632     Drinker

   633     Expr_Compiler

   634     Fibonacci

   635     Group

   636     Group_Context

   637     Group_Notepad

   638     Hoare_Ex

   639     Knaster_Tarski

   640     Mutilated_Checkerboard

   641     Nested_Datatype

   642     Peirce

   643     Puzzle

   644     Summation

   645   theories [quick_and_dirty]

   646     Structured_Statements

   647   document_files

   648     "root.bib"

   649     "root.tex"

   650     "style.tex"

   651 

   652 session "HOL-Eisbach" in Eisbach = HOL +

   653   description {*

   654     The Eisbach proof method language and "match" method.

   655   *}

   656   theories

   657     Eisbach

   658     Tests

   659     Examples

   660 

   661 session "HOL-SET_Protocol" in SET_Protocol = HOL +

   662   description {*

   663     Verification of the SET Protocol.

   664   *}

   665   theories [document = false] "~~/src/HOL/Library/Nat_Bijection"

   666   theories SET_Protocol

   667   document_files "root.tex"

   668 

   669 session "HOL-Matrix_LP" in Matrix_LP = HOL +

   670   description {*

   671     Two-dimensional matrices and linear programming.

   672   *}

   673   theories Cplex

   674   document_files "root.tex"

   675 

   676 session "HOL-TLA" in TLA = HOL +

   677   description {*

   678     Lamport's Temporal Logic of Actions.

   679   *}

   680   options [document = false]

   681   theories TLA

   682 

   683 session "HOL-TLA-Inc" in "TLA/Inc" = "HOL-TLA" +

   684   options [document = false]

   685   theories Inc

   686 

   687 session "HOL-TLA-Buffer" in "TLA/Buffer" = "HOL-TLA" +

   688   options [document = false]

   689   theories DBuffer

   690 

   691 session "HOL-TLA-Memory" in "TLA/Memory" = "HOL-TLA" +

   692   options [document = false]

   693   theories MemoryImplementation

   694 

   695 session "HOL-TPTP" in TPTP = HOL +

   696   description {*

   697     Author:     Jasmin Blanchette, TU Muenchen

   698     Author:     Nik Sultana, University of Cambridge

   699     Copyright   2011

   700 

   701     TPTP-related extensions.

   702   *}

   703   options [condition = ML_SYSTEM_POLYML, document = false]

   704   theories

   705     ATP_Theory_Export

   706     MaSh_Eval

   707     TPTP_Interpret

   708     THF_Arith

   709     TPTP_Proof_Reconstruction

   710   theories

   711     ATP_Problem_Import

   712 

   713 session "HOL-Multivariate_Analysis" (main) in Multivariate_Analysis = HOL +

   714   theories

   715     Multivariate_Analysis

   716     Determinants

   717     PolyRoots

   718     Complex_Analysis_Basics

   719     Complex_Transcendental

   720     Cauchy_Integral_Thm

   721   document_files

   722     "root.tex"

   723 

   724 session "HOL-Multivariate_Analysis-ex" in "Multivariate_Analysis/ex" = "HOL-Multivariate_Analysis" +

   725   theories

   726     Approximations

   727 

   728 session "HOL-Probability" in "Probability" = "HOL-Multivariate_Analysis" +

   729   theories [document = false]

   730     "~~/src/HOL/Library/Countable"

   731     "~~/src/HOL/Library/Permutation"

   732     "~~/src/HOL/Library/Order_Continuity"

   733     "~~/src/HOL/Library/Diagonal_Subsequence"

   734   theories

   735     Probability

   736     "ex/Dining_Cryptographers"

   737     "ex/Koepf_Duermuth_Countermeasure"

   738     "ex/Measure_Not_CCC"

   739   document_files "root.tex"

   740 

   741 session "HOL-Nominal" in Nominal = HOL +

   742   options [document = false]

   743   theories Nominal

   744 

   745 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +

   746   options [condition = ML_SYSTEM_POLYML, document = false]

   747   theories

   748     Class3

   749     CK_Machine

   750     Compile

   751     Contexts

   752     Crary

   753     CR_Takahashi

   754     CR

   755     Fsub

   756     Height

   757     Lambda_mu

   758     Lam_Funs

   759     LocalWeakening

   760     Pattern

   761     SN

   762     SOS

   763     Standardization

   764     Support

   765     Type_Preservation

   766     Weakening

   767     W

   768   theories [quick_and_dirty]

   769     VC_Condition

   770 

   771 session "HOL-Cardinals" in Cardinals = HOL +

   772   description {*

   773     Ordinals and Cardinals, Full Theories.

   774   *}

   775   options [document = false]

   776   theories

   777     Cardinals

   778     Bounded_Set

   779   document_files

   780     "intro.tex"

   781     "root.tex"

   782     "root.bib"

   783 

   784 session "HOL-Datatype_Examples" in Datatype_Examples = HOL +

   785   description {*

   786     (Co)datatype Examples, including large ones from John Harrison.

   787   *}

   788   options [document = false]

   789   theories

   790     "~~/src/HOL/Library/Old_Datatype"

   791     Compat

   792     Lambda_Term

   793     Process

   794     TreeFsetI

   795     "Derivation_Trees/Gram_Lang"

   796     "Derivation_Trees/Parallel"

   797     Koenig

   798     Lift_BNF

   799     Stream_Processor

   800     Misc_Codatatype

   801     Misc_Datatype

   802     Misc_Primcorec

   803     Misc_Primrec

   804   theories [condition = ISABELLE_FULL_TEST]

   805     Brackin

   806     IsaFoR

   807     Misc_N2M

   808 

   809 session "HOL-Word" (main) in Word = HOL +

   810   theories Word

   811   document_files "root.bib" "root.tex"

   812 

   813 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +

   814   options [document = false]

   815   theories WordExamples

   816 

   817 session "HOL-Statespace" in Statespace = HOL +

   818   theories [skip_proofs = false]

   819     StateSpaceEx

   820   document_files "root.tex"

   821 

   822 session "HOL-NSA" in NSA = HOL +

   823   description {*

   824     Nonstandard analysis.

   825   *}

   826   theories Hypercomplex

   827   document_files "root.tex"

   828 

   829 session "HOL-NSA-Examples" in "NSA/Examples" = "HOL-NSA" +

   830   options [document = false]

   831   theories NSPrimes

   832 

   833 session "HOL-Mirabelle" in Mirabelle = HOL +

   834   options [document = false]

   835   theories Mirabelle_Test

   836 

   837 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +

   838   options [condition = ML_SYSTEM_POLYML, document = false, timeout = 60]

   839   theories Ex

   840 

   841 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +

   842   options [document = false, quick_and_dirty]

   843   theories

   844     Boogie

   845     SMT_Examples

   846     SMT_Word_Examples

   847   theories [condition = ISABELLE_FULL_TEST]

   848     SMT_Tests

   849   files

   850     "Boogie_Dijkstra.certs"

   851     "Boogie_Max.certs"

   852     "SMT_Examples.certs"

   853     "SMT_Word_Examples.certs"

   854     "VCC_Max.certs"

   855 

   856 session "HOL-SPARK" (main) in "SPARK" = "HOL-Word" +

   857   options [document = false]

   858   theories SPARK

   859 

   860 session "HOL-SPARK-Examples" in "SPARK/Examples" = "HOL-SPARK" +

   861   options [document = false, spark_prv = false]

   862   theories

   863     "Gcd/Greatest_Common_Divisor"

   864 

   865     "Liseq/Longest_Increasing_Subsequence"

   866 

   867     "RIPEMD-160/F"

   868     "RIPEMD-160/Hash"

   869     "RIPEMD-160/K_L"

   870     "RIPEMD-160/K_R"

   871     "RIPEMD-160/R_L"

   872     "RIPEMD-160/Round"

   873     "RIPEMD-160/R_R"

   874     "RIPEMD-160/S_L"

   875     "RIPEMD-160/S_R"

   876 

   877     "Sqrt/Sqrt"

   878   files

   879     "Gcd/greatest_common_divisor/g_c_d.fdl"

   880     "Gcd/greatest_common_divisor/g_c_d.rls"

   881     "Gcd/greatest_common_divisor/g_c_d.siv"

   882     "Liseq/liseq/liseq_length.fdl"

   883     "Liseq/liseq/liseq_length.rls"

   884     "Liseq/liseq/liseq_length.siv"

   885     "RIPEMD-160/rmd/f.fdl"

   886     "RIPEMD-160/rmd/f.rls"

   887     "RIPEMD-160/rmd/f.siv"

   888     "RIPEMD-160/rmd/hash.fdl"

   889     "RIPEMD-160/rmd/hash.rls"

   890     "RIPEMD-160/rmd/hash.siv"

   891     "RIPEMD-160/rmd/k_l.fdl"

   892     "RIPEMD-160/rmd/k_l.rls"

   893     "RIPEMD-160/rmd/k_l.siv"

   894     "RIPEMD-160/rmd/k_r.fdl"

   895     "RIPEMD-160/rmd/k_r.rls"

   896     "RIPEMD-160/rmd/k_r.siv"

   897     "RIPEMD-160/rmd/r_l.fdl"

   898     "RIPEMD-160/rmd/r_l.rls"

   899     "RIPEMD-160/rmd/r_l.siv"

   900     "RIPEMD-160/rmd/round.fdl"

   901     "RIPEMD-160/rmd/round.rls"

   902     "RIPEMD-160/rmd/round.siv"

   903     "RIPEMD-160/rmd/r_r.fdl"

   904     "RIPEMD-160/rmd/r_r.rls"

   905     "RIPEMD-160/rmd/r_r.siv"

   906     "RIPEMD-160/rmd/s_l.fdl"

   907     "RIPEMD-160/rmd/s_l.rls"

   908     "RIPEMD-160/rmd/s_l.siv"

   909     "RIPEMD-160/rmd/s_r.fdl"

   910     "RIPEMD-160/rmd/s_r.rls"

   911     "RIPEMD-160/rmd/s_r.siv"

   912 

   913 session "HOL-SPARK-Manual" in "SPARK/Manual" = "HOL-SPARK" +

   914   options [show_question_marks = false, spark_prv = false]

   915   theories

   916     Example_Verification

   917     VC_Principles

   918     Reference

   919     Complex_Types

   920   files

   921     "complex_types_app/initialize.fdl"

   922     "complex_types_app/initialize.rls"

   923     "complex_types_app/initialize.siv"

   924     "loop_invariant/proc1.fdl"

   925     "loop_invariant/proc1.rls"

   926     "loop_invariant/proc1.siv"

   927     "loop_invariant/proc2.fdl"

   928     "loop_invariant/proc2.rls"

   929     "loop_invariant/proc2.siv"

   930     "simple_greatest_common_divisor/g_c_d.fdl"

   931     "simple_greatest_common_divisor/g_c_d.rls"

   932     "simple_greatest_common_divisor/g_c_d.siv"

   933   document_files

   934     "complex_types.ads"

   935     "complex_types_app.adb"

   936     "complex_types_app.ads"

   937     "Gcd.adb"

   938     "Gcd.ads"

   939     "intro.tex"

   940     "loop_invariant.adb"

   941     "loop_invariant.ads"

   942     "root.bib"

   943     "root.tex"

   944     "Simple_Gcd.adb"

   945     "Simple_Gcd.ads"

   946 

   947 session "HOL-Mutabelle" in Mutabelle = HOL +

   948   options [document = false]

   949   theories MutabelleExtra

   950 

   951 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +

   952   options [document = false]

   953   theories

   954     Quickcheck_Examples

   955     Quickcheck_Lattice_Examples

   956     Completeness

   957     Quickcheck_Interfaces

   958   theories [condition = ISABELLE_GHC]

   959     Hotel_Example

   960     Quickcheck_Narrowing_Examples

   961 

   962 session "HOL-Quickcheck_Benchmark" in Quickcheck_Benchmark = HOL +

   963   theories [condition = ISABELLE_FULL_TEST, quick_and_dirty]

   964     Find_Unused_Assms_Examples

   965     Needham_Schroeder_No_Attacker_Example

   966     Needham_Schroeder_Guided_Attacker_Example

   967     Needham_Schroeder_Unguided_Attacker_Example

   968 

   969 session "HOL-Quotient_Examples" in Quotient_Examples = HOL +

   970   description {*

   971     Author:     Cezary Kaliszyk and Christian Urban

   972   *}

   973   options [document = false]

   974   theories

   975     DList

   976     FSet

   977     Quotient_Int

   978     Quotient_Message

   979     Lift_FSet

   980     Lift_Set

   981     Lift_Fun

   982     Quotient_Rat

   983     Lift_DList

   984     Int_Pow

   985     Lifting_Code_Dt_Test

   986 

   987 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +

   988   options [document = false]

   989   theories

   990     Examples

   991     Predicate_Compile_Tests

   992     Predicate_Compile_Quickcheck_Examples

   993     Specialisation_Examples

   994     IMP_1

   995     IMP_2

   996     (* FIXME since 21-Jul-2011

   997     Hotel_Example_Small_Generator *)

   998     IMP_3

   999     IMP_4

  1000   theories [condition = "ISABELLE_SWIPL"]

  1001     Code_Prolog_Examples

  1002     Context_Free_Grammar_Example

  1003     Hotel_Example_Prolog

  1004     Lambda_Example

  1005     List_Examples

  1006   theories [condition = "ISABELLE_SWIPL", quick_and_dirty]

  1007     Reg_Exp_Example

  1008 

  1009 session HOLCF (main) 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   theories [document = false]

  1017     "~~/src/HOL/Library/Nat_Bijection"

  1018     "~~/src/HOL/Library/Countable"

  1019   theories

  1020     Plain_HOLCF

  1021     Fixrec

  1022     HOLCF

  1023   document_files "root.tex"

  1024 

  1025 session "HOLCF-Tutorial" in "HOLCF/Tutorial" = HOLCF +

  1026   theories

  1027     Domain_ex

  1028     Fixrec_ex

  1029     New_Domain

  1030   document_files "root.tex"

  1031 

  1032 session "HOLCF-Library" in "HOLCF/Library" = HOLCF +

  1033   options [document = false]

  1034   theories HOLCF_Library

  1035 

  1036 session "HOLCF-IMP" in "HOLCF/IMP" = HOLCF +

  1037   description {*

  1038     IMP -- A WHILE-language and its Semantics.

  1039 

  1040     This is the HOLCF-based denotational semantics of a simple WHILE-language.

  1041   *}

  1042   options [document = false]

  1043   theories HoareEx

  1044   document_files "root.tex"

  1045 

  1046 session "HOLCF-ex" in "HOLCF/ex" = HOLCF +

  1047   description {*

  1048     Miscellaneous examples for HOLCF.

  1049   *}

  1050   options [document = false]

  1051   theories

  1052     Dnat

  1053     Dagstuhl

  1054     Focus_ex

  1055     Fix2

  1056     Hoare

  1057     Concurrency_Monad

  1058     Loop

  1059     Powerdomain_ex

  1060     Domain_Proofs

  1061     Letrec

  1062     Pattern_Match

  1063 

  1064 session "HOLCF-FOCUS" in "HOLCF/FOCUS" = HOLCF +

  1065   description {*

  1066     FOCUS: a theory of stream-processing functions Isabelle/HOLCF.

  1067 

  1068     For introductions to FOCUS, see

  1069 

  1070     "The Design of Distributed Systems - An Introduction to FOCUS"

  1071     http://www4.in.tum.de/publ/html.php?e=2

  1072 

  1073     "Specification and Refinement of a Buffer of Length One"

  1074     http://www4.in.tum.de/publ/html.php?e=15

  1075 

  1076     "Specification and Development of Interactive Systems: Focus on Streams,

  1077     Interfaces, and Refinement" http://www4.in.tum.de/publ/html.php?e=321

  1078   *}

  1079   options [document = false]

  1080   theories

  1081     Fstreams

  1082     FOCUS

  1083     Buffer_adm

  1084 

  1085 session IOA in "HOLCF/IOA" = HOLCF +

  1086   description {*

  1087     Author:     Olaf Mueller

  1088     Copyright   1997 TU München

  1089 

  1090     A formalization of I/O automata in HOLCF.

  1091 

  1092     The distribution contains simulation relations, temporal logic, and an

  1093     abstraction theory. Everything is based upon a domain-theoretic model of

  1094     finite and infinite sequences.

  1095   *}

  1096   options [document = false]

  1097   theories "meta_theory/Abstraction"

  1098 

  1099 session "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   options [document = false]

  1106   theories

  1107     Correctness

  1108     Spec

  1109 

  1110 session "IOA-NTP" in "HOLCF/IOA/NTP" = IOA +

  1111   description {*

  1112     Author:     Tobias Nipkow & Konrad Slind

  1113 

  1114     A network transmission protocol, performed in the

  1115     I/O automata formalization by Olaf Mueller.

  1116   *}

  1117   options [document = false]

  1118   theories Correctness

  1119 

  1120 session "IOA-Storage" in "HOLCF/IOA/Storage" = IOA +

  1121   description {*

  1122     Author:     Olaf Mueller

  1123 

  1124     Memory storage case study.

  1125   *}

  1126   options [document = false]

  1127   theories Correctness

  1128 

  1129 session "IOA-ex" in "HOLCF/IOA/ex" = IOA +

  1130   description {*

  1131     Author:     Olaf Mueller

  1132   *}

  1133   options [document = false]

  1134   theories

  1135     TrivEx

  1136     TrivEx2

  1137 

  1138 session "HOL-Record_Benchmark" in Record_Benchmark = HOL +

  1139   description {*

  1140     Some benchmark on large record.

  1141   *}

  1142   options [document = false]

  1143   theories [condition = ISABELLE_FULL_TEST]

  1144     Record_Benchmark

  1145
isabelle