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