src/Doc/Corec/Corec.thy
author blanchet
Tue Mar 29 09:45:54 2016 +0200 (2016-03-29)
changeset 62739 628c97d39627
child 62742 bfb5a70e4319
permissions -rw-r--r--
added sketchy 'corec' documentation
     1 (*  Title:      Doc/Corec/Corec.thy
     2     Author:     Jasmin Blanchette, Inria, LORIA, MPII
     3     Author:     Aymeric Bouzy, Ecole polytechnique
     4     Author:     Andreas Lochbihler, ETH Zuerich
     5     Author:     Andrei Popescu, Middlesex University
     6     Author:     Dmitriy Traytel, ETH Zuerich
     7 
     8 Tutorial for nonprimitively corecursive definitions.
     9 *)
    10 
    11 theory Corec
    12 imports
    13   "../Datatypes/Setup"
    14   "~~/src/HOL/Library/BNF_Corec"
    15 begin
    16 
    17 section \<open>Introduction
    18   \label{sec:introduction}\<close>
    19 
    20 text \<open>
    21 ...
    22 \cite{isabelle-datatypes}
    23 \<close>
    24 
    25 
    26 section \<open>Introductory Examples
    27   \label{sec:introductory-examples}\<close>
    28 
    29 
    30 subsection \<open>Simple Corecursion
    31   \label{ssec:simple-corecursion}\<close>
    32 
    33 
    34 subsection \<open>Nested Corecursion
    35   \label{ssec:nested-corecursion}\<close>
    36 
    37 
    38 subsection \<open>Polymorphism
    39   \label{ssec:polymorphism}\<close>
    40 
    41 
    42 subsection \<open>Coinduction
    43   \label{ssec:coinduction}\<close>
    44 
    45 
    46 subsection \<open>Uniqueness Reasoning
    47   \label{ssec:uniqueness-reasoning}\<close>
    48 
    49 
    50 section \<open>Command Syntax
    51   \label{sec:command-syntax}\<close>
    52 
    53 
    54 subsection \<open>corec and corecursive
    55   \label{ssec:corec-and-corecursive}\<close>
    56 
    57 
    58 subsection \<open>friend_of_corec
    59   \label{ssec:friend-of-corec}\<close>
    60 
    61 
    62 subsection \<open>coinduction_upto
    63   \label{ssec:coinduction-upto}\<close>
    64 
    65 
    66 section \<open>Generated Theorems
    67   \label{sec:generated-theorems}\<close>
    68 
    69 
    70 subsection \<open>corec and corecursive
    71   \label{ssec:corec-and-corecursive}\<close>
    72 
    73 
    74 subsection \<open>friend_of_corec
    75   \label{ssec:friend-of-corec}\<close>
    76 
    77 
    78 subsection \<open>coinduction_upto
    79   \label{ssec:coinduction-upto}\<close>
    80 
    81 
    82 section \<open>Proof Method
    83   \label{sec:proof-method}\<close>
    84 
    85 
    86 subsection \<open>corec_unique
    87   \label{ssec:corec-unique}\<close>
    88 
    89 
    90 section \<open>Known Bugs and Limitations
    91   \label{sec:known-bugs-and-limitations}\<close>
    92 
    93 text \<open>
    94 This section lists the known bugs and limitations of the corecursion package at
    95 the time of this writing.
    96 
    97 \begin{enumerate}
    98 \setlength{\itemsep}{0pt}
    99 
   100 \item
   101 \emph{TODO.} TODO.
   102 
   103   * no mutual types
   104   * limitation on type of friend
   105   * unfinished tactics
   106   * polymorphism of corecUU_transfer
   107 
   108 \end{enumerate}
   109 \<close>
   110 
   111 end