reduced dependencies + updated docs
authorblanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 550739b96fb4c8cfd
parent 55072 8488fdc4ddc0
child 55074 2b0b6f69b148
reduced dependencies + updated docs
src/Doc/Datatypes/Datatypes.thy
src/Doc/Datatypes/Setup.thy
src/Doc/ROOT
src/HOL/BNF/README.html
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -8,7 +8,11 @@
     1.4  *)
     1.5  
     1.6  theory Datatypes
     1.7 -imports Setup "~~/src/HOL/Library/Simps_Case_Conv"
     1.8 +imports
     1.9 +  Setup
    1.10 +  "~~/src/HOL/BNF/BNF_Decl"
    1.11 +  "~~/src/HOL/BNF/More_BNFs"
    1.12 +  "~~/src/HOL/Library/Simps_Case_Conv"
    1.13  begin
    1.14  
    1.15  section {* Introduction
    1.16 @@ -74,20 +78,10 @@
    1.17  finitely many direct subtrees, whereas those of the second and fourth may have
    1.18  infinite branching.
    1.19  
    1.20 -To use the package, it is necessary to import the @{theory BNF} theory, which
    1.21 -can be precompiled into the \texttt{HOL-BNF} image. The following commands show
    1.22 -how to launch jEdit/PIDE with the image loaded and how to build the image
    1.23 -without launching jEdit:
    1.24 -*}
    1.25 -
    1.26 -text {*
    1.27 -\noindent
    1.28 -\ \ \ \ \texttt{isabelle jedit -l HOL-BNF} \\
    1.29 -\noindent
    1.30 -\hbox{}\ \ \ \ \texttt{isabelle build -b HOL-BNF}
    1.31 -*}
    1.32 -
    1.33 -text {*
    1.34 +The package is part of @{theory Main}. Additional functionality is provided by
    1.35 +the theories @{theory BNF_Decl} and @{theory More_BNFs}, located in the
    1.36 +@{text "~~/src/HOL/BNF"} directory.
    1.37 +
    1.38  The package, like its predecessor, fully adheres to the LCF philosophy
    1.39  \cite{mgordon79}: The characteristic theorems associated with the specified
    1.40  (co)datatypes are derived rather than introduced axiomatically.%
    1.41 @@ -2512,7 +2506,7 @@
    1.42  Tobias Nipkow and Makarius Wenzel encouraged us to implement the new
    1.43  (co)datatype package. Andreas Lochbihler provided lots of comments on earlier
    1.44  versions of the package, especially for the coinductive part. Brian Huffman
    1.45 -suggested major simplifications to the internal constructions, much of which has
    1.46 +suggested major simplifications to the internal constructions, many of which has
    1.47  yet to be implemented. Florian Haftmann and Christian Urban provided general
    1.48  advice on Isabelle and package writing. Stefan Milius and Lutz Schr\"oder
    1.49  found an elegant proof to eliminate one of the BNF assumptions. Andreas
     2.1 --- a/src/Doc/Datatypes/Setup.thy	Mon Jan 20 18:24:56 2014 +0100
     2.2 +++ b/src/Doc/Datatypes/Setup.thy	Mon Jan 20 18:24:56 2014 +0100
     2.3 @@ -1,5 +1,5 @@
     2.4  theory Setup
     2.5 -imports BNF
     2.6 +imports Main
     2.7  begin
     2.8  
     2.9  ML_file "../antiquote_setup.ML"
     3.1 --- a/src/Doc/ROOT	Mon Jan 20 18:24:56 2014 +0100
     3.2 +++ b/src/Doc/ROOT	Mon Jan 20 18:24:56 2014 +0100
     3.3 @@ -37,7 +37,7 @@
     3.4      "document/root.tex"
     3.5      "document/style.sty"
     3.6  
     3.7 -session Datatypes (doc) in "Datatypes" = "HOL-BNF" +
     3.8 +session Datatypes (doc) in "Datatypes" = HOL +
     3.9    options [document_variants = "datatypes"]
    3.10    theories [document = false] Setup
    3.11    theories Datatypes
     4.1 --- a/src/HOL/BNF/README.html	Mon Jan 20 18:24:56 2014 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,49 +0,0 @@
     4.4 -<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     4.5 -
     4.6 -<html>
     4.7 -
     4.8 -<head>
     4.9 -  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
    4.10 -  <title>BNF Package</title>
    4.11 -</head>
    4.12 -
    4.13 -<body>
    4.14 -
    4.15 -<h3><i>BNF</i>: A (co)datatype package based on bounded natural functors
    4.16 -(BNFs)</h3>
    4.17 -
    4.18 -<p>
    4.19 -The <i>BNF</i> package provides a fully modular framework for constructing
    4.20 -inductive and coinductive datatypes in HOL, with support for mixed mutual and
    4.21 -nested (co)recursion. Mixed (co)recursion enables type definitions involving
    4.22 -both datatypes and codatatypes, such as the type of finitely branching trees of
    4.23 -possibly infinite depth. The framework draws heavily from category theory.
    4.24 -
    4.25 -<p>
    4.26 -The package is described in <tt>isabelle doc datatypes</tt> and in the following
    4.27 -paper:
    4.28 -
    4.29 -<ul>
    4.30 -  <li><a href="http://www21.in.tum.de/~traytel/papers/lics12-codatatypes/index.html">Foundational, Compositional (Co)datatypes for Higher-Order Logic&mdash;Category Theory Applied to Theorem Proving</a>, <br>
    4.31 -  Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette.<br>
    4.32 -  <i>Logic in Computer Science (LICS 2012)</i>, 2012.
    4.33 -</ul>
    4.34 -
    4.35 -<p>
    4.36 -Most of the package is loaded as part of <tt>Main.thy</tt>. Additional
    4.37 -functionality is provided by <tt>BNF.thy</tt>. The <tt>Examples</tt> directory
    4.38 -contains various examples of (co)datatypes, including the examples from the
    4.39 -paper.
    4.40 -
    4.41 -<p>
    4.42 -The key notion underlying the package is that of a <i>bounded natural functor</i>
    4.43 -(<i>BNF</i>)&mdash;an enriched type constructor satisfying specific properties
    4.44 -preserved by interesting categorical operations (composition, least fixed point,
    4.45 -and greatest fixed point). The <tt>Basic_BNFs.thy</tt>, <tt>More_BNFs.thy</tt>,
    4.46 -and <tt>Countable_Set_Type.thy</tt> files register various basic types, notably
    4.47 -for sums, products, function spaces, finite sets, multisets, and countable sets.
    4.48 -Custom BNFs can be registered as well.
    4.49 -
    4.50 -</body>
    4.51 -
    4.52 -</html>