added sketchy 'corec' documentation
authorblanchet
Tue Mar 29 09:45:54 2016 +0200 (2016-03-29)
changeset 62739628c97d39627
parent 62738 fe827c6fa8c5
child 62740 69e4a4fffea9
added sketchy 'corec' documentation
doc/Contents
src/Doc/Corec/Corec.thy
src/Doc/Corec/document/build
src/Doc/Corec/document/root.tex
src/Doc/Corec/document/style.sty
src/Doc/ROOT
     1.1 --- a/doc/Contents	Mon Mar 28 12:11:54 2016 +0200
     1.2 +++ b/doc/Contents	Tue Mar 29 09:45:54 2016 +0200
     1.3 @@ -4,6 +4,7 @@
     1.4    classes         Tutorial on Type Classes
     1.5    datatypes       Tutorial on (Co)datatype Definitions
     1.6    functions       Tutorial on Function Definitions
     1.7 +  corec           Tutorial on Nonprimitively Corecursive Definitions
     1.8    codegen         Tutorial on Code Generation
     1.9    nitpick         User's Guide to Nitpick
    1.10    sledgehammer    User's Guide to Sledgehammer
    1.11 @@ -22,4 +23,3 @@
    1.12    intro           Old Introduction to Isabelle
    1.13    logics          Isabelle's Logics: HOL and misc logics
    1.14    logics-ZF       Isabelle's Logics: FOL and ZF
    1.15 -
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Doc/Corec/Corec.thy	Tue Mar 29 09:45:54 2016 +0200
     2.3 @@ -0,0 +1,111 @@
     2.4 +(*  Title:      Doc/Corec/Corec.thy
     2.5 +    Author:     Jasmin Blanchette, Inria, LORIA, MPII
     2.6 +    Author:     Aymeric Bouzy, Ecole polytechnique
     2.7 +    Author:     Andreas Lochbihler, ETH Zuerich
     2.8 +    Author:     Andrei Popescu, Middlesex University
     2.9 +    Author:     Dmitriy Traytel, ETH Zuerich
    2.10 +
    2.11 +Tutorial for nonprimitively corecursive definitions.
    2.12 +*)
    2.13 +
    2.14 +theory Corec
    2.15 +imports
    2.16 +  "../Datatypes/Setup"
    2.17 +  "~~/src/HOL/Library/BNF_Corec"
    2.18 +begin
    2.19 +
    2.20 +section \<open>Introduction
    2.21 +  \label{sec:introduction}\<close>
    2.22 +
    2.23 +text \<open>
    2.24 +...
    2.25 +\cite{isabelle-datatypes}
    2.26 +\<close>
    2.27 +
    2.28 +
    2.29 +section \<open>Introductory Examples
    2.30 +  \label{sec:introductory-examples}\<close>
    2.31 +
    2.32 +
    2.33 +subsection \<open>Simple Corecursion
    2.34 +  \label{ssec:simple-corecursion}\<close>
    2.35 +
    2.36 +
    2.37 +subsection \<open>Nested Corecursion
    2.38 +  \label{ssec:nested-corecursion}\<close>
    2.39 +
    2.40 +
    2.41 +subsection \<open>Polymorphism
    2.42 +  \label{ssec:polymorphism}\<close>
    2.43 +
    2.44 +
    2.45 +subsection \<open>Coinduction
    2.46 +  \label{ssec:coinduction}\<close>
    2.47 +
    2.48 +
    2.49 +subsection \<open>Uniqueness Reasoning
    2.50 +  \label{ssec:uniqueness-reasoning}\<close>
    2.51 +
    2.52 +
    2.53 +section \<open>Command Syntax
    2.54 +  \label{sec:command-syntax}\<close>
    2.55 +
    2.56 +
    2.57 +subsection \<open>corec and corecursive
    2.58 +  \label{ssec:corec-and-corecursive}\<close>
    2.59 +
    2.60 +
    2.61 +subsection \<open>friend_of_corec
    2.62 +  \label{ssec:friend-of-corec}\<close>
    2.63 +
    2.64 +
    2.65 +subsection \<open>coinduction_upto
    2.66 +  \label{ssec:coinduction-upto}\<close>
    2.67 +
    2.68 +
    2.69 +section \<open>Generated Theorems
    2.70 +  \label{sec:generated-theorems}\<close>
    2.71 +
    2.72 +
    2.73 +subsection \<open>corec and corecursive
    2.74 +  \label{ssec:corec-and-corecursive}\<close>
    2.75 +
    2.76 +
    2.77 +subsection \<open>friend_of_corec
    2.78 +  \label{ssec:friend-of-corec}\<close>
    2.79 +
    2.80 +
    2.81 +subsection \<open>coinduction_upto
    2.82 +  \label{ssec:coinduction-upto}\<close>
    2.83 +
    2.84 +
    2.85 +section \<open>Proof Method
    2.86 +  \label{sec:proof-method}\<close>
    2.87 +
    2.88 +
    2.89 +subsection \<open>corec_unique
    2.90 +  \label{ssec:corec-unique}\<close>
    2.91 +
    2.92 +
    2.93 +section \<open>Known Bugs and Limitations
    2.94 +  \label{sec:known-bugs-and-limitations}\<close>
    2.95 +
    2.96 +text \<open>
    2.97 +This section lists the known bugs and limitations of the corecursion package at
    2.98 +the time of this writing.
    2.99 +
   2.100 +\begin{enumerate}
   2.101 +\setlength{\itemsep}{0pt}
   2.102 +
   2.103 +\item
   2.104 +\emph{TODO.} TODO.
   2.105 +
   2.106 +  * no mutual types
   2.107 +  * limitation on type of friend
   2.108 +  * unfinished tactics
   2.109 +  * polymorphism of corecUU_transfer
   2.110 +
   2.111 +\end{enumerate}
   2.112 +\<close>
   2.113 +
   2.114 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Doc/Corec/document/build	Tue Mar 29 09:45:54 2016 +0200
     3.3 @@ -0,0 +1,9 @@
     3.4 +#!/usr/bin/env bash
     3.5 +
     3.6 +set -e
     3.7 +
     3.8 +FORMAT="$1"
     3.9 +VARIANT="$2"
    3.10 +
    3.11 +"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
    3.12 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Doc/Corec/document/root.tex	Tue Mar 29 09:45:54 2016 +0200
     4.3 @@ -0,0 +1,92 @@
     4.4 +\documentclass[12pt,a4paper]{article} % fleqn
     4.5 +\usepackage{lmodern}
     4.6 +\usepackage[T1]{fontenc}
     4.7 +\usepackage{amsmath}
     4.8 +\usepackage{cite}
     4.9 +\usepackage{enumitem}
    4.10 +\usepackage{footmisc}
    4.11 +\usepackage{latexsym}
    4.12 +\usepackage{graphicx}
    4.13 +\usepackage{iman}
    4.14 +\usepackage{extra}
    4.15 +\usepackage{isar}
    4.16 +\usepackage{isabelle}
    4.17 +\usepackage{isabellesym}
    4.18 +\usepackage{style}
    4.19 +\usepackage{pdfsetup}
    4.20 +\usepackage{railsetup}
    4.21 +\usepackage{framed}
    4.22 +\usepackage{regexpatch}
    4.23 +
    4.24 +\makeatletter
    4.25 +\xpatchcmd{\chaptermark}{\MakeUppercase}{}{}{}%
    4.26 +\xpatchcmd{\sectionmark}{\MakeUppercase}{}{}{}%
    4.27 +\xpatchcmd*{\tableofcontents}{\MakeUppercase}{}{}{}%
    4.28 +\makeatother
    4.29 +
    4.30 +\setcounter{secnumdepth}{3}
    4.31 +\setcounter{tocdepth}{3}
    4.32 +
    4.33 +\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
    4.34 +
    4.35 +\newbox\boxA
    4.36 +\setbox\boxA=\hbox{\ }
    4.37 +\parindent=4\wd\boxA
    4.38 +
    4.39 +\newcommand\blankline{\vskip-.25\baselineskip}
    4.40 +
    4.41 +\newenvironment{indentblock}{\list{}{\setlength{\leftmargin}{\parindent}}\item[]}{\endlist}
    4.42 +
    4.43 +\newcommand{\keyw}[1]{\textbf{#1}}
    4.44 +\newcommand{\synt}[1]{\textit{#1}}
    4.45 +\newcommand{\hthm}[1]{\textbf{\textit{#1}}}
    4.46 +
    4.47 +%\renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$}
    4.48 +\renewcommand\isactrlsub[1]{\/$\sb{#1}$}
    4.49 +\renewcommand\isadigit[1]{\/\ensuremath{\mathrm{#1}}}
    4.50 +\renewcommand\isacharprime{\isamath{{'}\mskip-2mu}}
    4.51 +\renewcommand\isacharunderscore{\mbox{\_}}
    4.52 +\renewcommand\isacharunderscorekeyword{\mbox{\_}}
    4.53 +\renewcommand\isachardoublequote{\mbox{\upshape{``}}}
    4.54 +\renewcommand\isachardoublequoteopen{\mbox{\upshape{``}\kern.1ex}}
    4.55 +\renewcommand\isachardoublequoteclose{\/\kern.15ex\mbox{\upshape{''}}}
    4.56 +\renewcommand\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
    4.57 +\renewcommand\isacharverbatimclose{\isacharasterisk\isacharbraceright}
    4.58 +\renewcommand{\isasyminverse}{\isamath{{}^{-}}}
    4.59 +
    4.60 +\hyphenation{isa-belle}
    4.61 +
    4.62 +\isadroptag{theory}
    4.63 +
    4.64 +\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
    4.65 +Defining Nonprimitively (Co)recursive Functions in Isabelle/HOL}
    4.66 +\author{Jasmin Christian Blanchette, Aymeric Bouzy, \\
    4.67 +Andreas Lochbihler, Andrei Popescu, and \\
    4.68 +Dmitriy Traytel}
    4.69 +
    4.70 +\urlstyle{tt}
    4.71 +
    4.72 +\begin{document}
    4.73 +
    4.74 +\maketitle
    4.75 +
    4.76 +\begin{sloppy}
    4.77 +\begin{abstract}
    4.78 +\noindent
    4.79 +This tutorial describes the definitional package for nonprimitively corecursive functions
    4.80 +in Isabelle/HOL. The following commands are provided:
    4.81 +\keyw{corec}, \keyw{corecursive}, \keyw{friend\_of\_corec}, and \keyw{coinduction\_upto}.
    4.82 +They complement \keyw{codatatype}, \keyw{primcorec}, and \keyw{primcorecursive}, which
    4.83 +define codatatypes and primitively corecursive functions.
    4.84 +\end{abstract}
    4.85 +\end{sloppy}
    4.86 +
    4.87 +\tableofcontents
    4.88 +
    4.89 +\input{Corec.tex}
    4.90 +
    4.91 +\let\em=\sl
    4.92 +\bibliography{manual}{}
    4.93 +\bibliographystyle{abbrv}
    4.94 +
    4.95 +\end{document}
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Doc/Corec/document/style.sty	Tue Mar 29 09:45:54 2016 +0200
     5.3 @@ -0,0 +1,46 @@
     5.4 +
     5.5 +%% toc
     5.6 +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
     5.7 +\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
     5.8 +
     5.9 +%% paragraphs
    5.10 +\setlength{\parindent}{1em}
    5.11 +
    5.12 +%% references
    5.13 +\newcommand{\secref}[1]{\S\ref{#1}}
    5.14 +\newcommand{\figref}[1]{figure~\ref{#1}}
    5.15 +
    5.16 +%% logical markup
    5.17 +\newcommand{\strong}[1]{{\bfseries {#1}}}
    5.18 +\newcommand{\qn}[1]{\emph{#1}}
    5.19 +
    5.20 +%% typographic conventions
    5.21 +\newcommand{\qt}[1]{``{#1}''}
    5.22 +\newcommand{\ditem}[1]{\item[\isastyletext #1]}
    5.23 +
    5.24 +%% quote environment
    5.25 +\isakeeptag{quote}
    5.26 +\renewenvironment{quote}
    5.27 +  {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
    5.28 +  {\endlist}
    5.29 +\renewcommand{\isatagquote}{\begin{quote}}
    5.30 +\renewcommand{\endisatagquote}{\end{quote}}
    5.31 +\newcommand{\quotebreak}{\\[1.2ex]}
    5.32 +
    5.33 +%% presentation
    5.34 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    5.35 +
    5.36 +%% character detail
    5.37 +\renewcommand{\isadigit}[1]{\isamath{#1}}
    5.38 +\binperiod
    5.39 +\underscoreoff
    5.40 +
    5.41 +%% format
    5.42 +\pagestyle{headings}
    5.43 +\isabellestyle{it}
    5.44 +
    5.45 +
    5.46 +%%% Local Variables: 
    5.47 +%%% mode: latex
    5.48 +%%% TeX-master: "implementation"
    5.49 +%%% End: 
     6.1 --- a/src/Doc/ROOT	Mon Mar 28 12:11:54 2016 +0200
     6.2 +++ b/src/Doc/ROOT	Tue Mar 29 09:45:54 2016 +0200
     6.3 @@ -43,6 +43,22 @@
     6.4      "root.tex"
     6.5      "style.sty"
     6.6  
     6.7 +session Corec (doc) in "Corec" = HOL +
     6.8 +  options [document_variants = "corec"]
     6.9 +  theories [document = false] "../Datatypes/Setup"
    6.10 +  theories Corec
    6.11 +  document_files (in "..")
    6.12 +    "prepare_document"
    6.13 +    "pdfsetup.sty"
    6.14 +    "iman.sty"
    6.15 +    "extra.sty"
    6.16 +    "isar.sty"
    6.17 +    "manual.bib"
    6.18 +  document_files
    6.19 +    "build"
    6.20 +    "root.tex"
    6.21 +    "style.sty"
    6.22 +
    6.23  session Datatypes (doc) in "Datatypes" = HOL +
    6.24    options [document_variants = "datatypes"]
    6.25    theories [document = false] Setup