src/Doc/Corec/Corec.thy
changeset 62739 628c97d39627
child 62742 bfb5a70e4319
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Doc/Corec/Corec.thy	Tue Mar 29 09:45:54 2016 +0200
     1.3 @@ -0,0 +1,111 @@
     1.4 +(*  Title:      Doc/Corec/Corec.thy
     1.5 +    Author:     Jasmin Blanchette, Inria, LORIA, MPII
     1.6 +    Author:     Aymeric Bouzy, Ecole polytechnique
     1.7 +    Author:     Andreas Lochbihler, ETH Zuerich
     1.8 +    Author:     Andrei Popescu, Middlesex University
     1.9 +    Author:     Dmitriy Traytel, ETH Zuerich
    1.10 +
    1.11 +Tutorial for nonprimitively corecursive definitions.
    1.12 +*)
    1.13 +
    1.14 +theory Corec
    1.15 +imports
    1.16 +  "../Datatypes/Setup"
    1.17 +  "~~/src/HOL/Library/BNF_Corec"
    1.18 +begin
    1.19 +
    1.20 +section \<open>Introduction
    1.21 +  \label{sec:introduction}\<close>
    1.22 +
    1.23 +text \<open>
    1.24 +...
    1.25 +\cite{isabelle-datatypes}
    1.26 +\<close>
    1.27 +
    1.28 +
    1.29 +section \<open>Introductory Examples
    1.30 +  \label{sec:introductory-examples}\<close>
    1.31 +
    1.32 +
    1.33 +subsection \<open>Simple Corecursion
    1.34 +  \label{ssec:simple-corecursion}\<close>
    1.35 +
    1.36 +
    1.37 +subsection \<open>Nested Corecursion
    1.38 +  \label{ssec:nested-corecursion}\<close>
    1.39 +
    1.40 +
    1.41 +subsection \<open>Polymorphism
    1.42 +  \label{ssec:polymorphism}\<close>
    1.43 +
    1.44 +
    1.45 +subsection \<open>Coinduction
    1.46 +  \label{ssec:coinduction}\<close>
    1.47 +
    1.48 +
    1.49 +subsection \<open>Uniqueness Reasoning
    1.50 +  \label{ssec:uniqueness-reasoning}\<close>
    1.51 +
    1.52 +
    1.53 +section \<open>Command Syntax
    1.54 +  \label{sec:command-syntax}\<close>
    1.55 +
    1.56 +
    1.57 +subsection \<open>corec and corecursive
    1.58 +  \label{ssec:corec-and-corecursive}\<close>
    1.59 +
    1.60 +
    1.61 +subsection \<open>friend_of_corec
    1.62 +  \label{ssec:friend-of-corec}\<close>
    1.63 +
    1.64 +
    1.65 +subsection \<open>coinduction_upto
    1.66 +  \label{ssec:coinduction-upto}\<close>
    1.67 +
    1.68 +
    1.69 +section \<open>Generated Theorems
    1.70 +  \label{sec:generated-theorems}\<close>
    1.71 +
    1.72 +
    1.73 +subsection \<open>corec and corecursive
    1.74 +  \label{ssec:corec-and-corecursive}\<close>
    1.75 +
    1.76 +
    1.77 +subsection \<open>friend_of_corec
    1.78 +  \label{ssec:friend-of-corec}\<close>
    1.79 +
    1.80 +
    1.81 +subsection \<open>coinduction_upto
    1.82 +  \label{ssec:coinduction-upto}\<close>
    1.83 +
    1.84 +
    1.85 +section \<open>Proof Method
    1.86 +  \label{sec:proof-method}\<close>
    1.87 +
    1.88 +
    1.89 +subsection \<open>corec_unique
    1.90 +  \label{ssec:corec-unique}\<close>
    1.91 +
    1.92 +
    1.93 +section \<open>Known Bugs and Limitations
    1.94 +  \label{sec:known-bugs-and-limitations}\<close>
    1.95 +
    1.96 +text \<open>
    1.97 +This section lists the known bugs and limitations of the corecursion package at
    1.98 +the time of this writing.
    1.99 +
   1.100 +\begin{enumerate}
   1.101 +\setlength{\itemsep}{0pt}
   1.102 +
   1.103 +\item
   1.104 +\emph{TODO.} TODO.
   1.105 +
   1.106 +  * no mutual types
   1.107 +  * limitation on type of friend
   1.108 +  * unfinished tactics
   1.109 +  * polymorphism of corecUU_transfer
   1.110 +
   1.111 +\end{enumerate}
   1.112 +\<close>
   1.113 +
   1.114 +end