--- a/doc/Contents Mon Mar 28 12:11:54 2016 +0200
+++ b/doc/Contents Tue Mar 29 09:45:54 2016 +0200
@@ -4,6 +4,7 @@
classes Tutorial on Type Classes
datatypes Tutorial on (Co)datatype Definitions
functions Tutorial on Function Definitions
+ corec Tutorial on Nonprimitively Corecursive Definitions
codegen Tutorial on Code Generation
nitpick User's Guide to Nitpick
sledgehammer User's Guide to Sledgehammer
@@ -22,4 +23,3 @@
intro Old Introduction to Isabelle
logics Isabelle's Logics: HOL and misc logics
logics-ZF Isabelle's Logics: FOL and ZF
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Corec/Corec.thy Tue Mar 29 09:45:54 2016 +0200
@@ -0,0 +1,111 @@
+(* Title: Doc/Corec/Corec.thy
+ Author: Jasmin Blanchette, Inria, LORIA, MPII
+ Author: Aymeric Bouzy, Ecole polytechnique
+ Author: Andreas Lochbihler, ETH Zuerich
+ Author: Andrei Popescu, Middlesex University
+ Author: Dmitriy Traytel, ETH Zuerich
+
+Tutorial for nonprimitively corecursive definitions.
+*)
+
+theory Corec
+imports
+ "../Datatypes/Setup"
+ "~~/src/HOL/Library/BNF_Corec"
+begin
+
+section \<open>Introduction
+ \label{sec:introduction}\<close>
+
+text \<open>
+...
+\cite{isabelle-datatypes}
+\<close>
+
+
+section \<open>Introductory Examples
+ \label{sec:introductory-examples}\<close>
+
+
+subsection \<open>Simple Corecursion
+ \label{ssec:simple-corecursion}\<close>
+
+
+subsection \<open>Nested Corecursion
+ \label{ssec:nested-corecursion}\<close>
+
+
+subsection \<open>Polymorphism
+ \label{ssec:polymorphism}\<close>
+
+
+subsection \<open>Coinduction
+ \label{ssec:coinduction}\<close>
+
+
+subsection \<open>Uniqueness Reasoning
+ \label{ssec:uniqueness-reasoning}\<close>
+
+
+section \<open>Command Syntax
+ \label{sec:command-syntax}\<close>
+
+
+subsection \<open>corec and corecursive
+ \label{ssec:corec-and-corecursive}\<close>
+
+
+subsection \<open>friend_of_corec
+ \label{ssec:friend-of-corec}\<close>
+
+
+subsection \<open>coinduction_upto
+ \label{ssec:coinduction-upto}\<close>
+
+
+section \<open>Generated Theorems
+ \label{sec:generated-theorems}\<close>
+
+
+subsection \<open>corec and corecursive
+ \label{ssec:corec-and-corecursive}\<close>
+
+
+subsection \<open>friend_of_corec
+ \label{ssec:friend-of-corec}\<close>
+
+
+subsection \<open>coinduction_upto
+ \label{ssec:coinduction-upto}\<close>
+
+
+section \<open>Proof Method
+ \label{sec:proof-method}\<close>
+
+
+subsection \<open>corec_unique
+ \label{ssec:corec-unique}\<close>
+
+
+section \<open>Known Bugs and Limitations
+ \label{sec:known-bugs-and-limitations}\<close>
+
+text \<open>
+This section lists the known bugs and limitations of the corecursion package at
+the time of this writing.
+
+\begin{enumerate}
+\setlength{\itemsep}{0pt}
+
+\item
+\emph{TODO.} TODO.
+
+ * no mutual types
+ * limitation on type of friend
+ * unfinished tactics
+ * polymorphism of corecUU_transfer
+
+\end{enumerate}
+\<close>
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Corec/document/build Tue Mar 29 09:45:54 2016 +0200
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+set -e
+
+FORMAT="$1"
+VARIANT="$2"
+
+"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Corec/document/root.tex Tue Mar 29 09:45:54 2016 +0200
@@ -0,0 +1,92 @@
+\documentclass[12pt,a4paper]{article} % fleqn
+\usepackage{lmodern}
+\usepackage[T1]{fontenc}
+\usepackage{amsmath}
+\usepackage{cite}
+\usepackage{enumitem}
+\usepackage{footmisc}
+\usepackage{latexsym}
+\usepackage{graphicx}
+\usepackage{iman}
+\usepackage{extra}
+\usepackage{isar}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{style}
+\usepackage{pdfsetup}
+\usepackage{railsetup}
+\usepackage{framed}
+\usepackage{regexpatch}
+
+\makeatletter
+\xpatchcmd{\chaptermark}{\MakeUppercase}{}{}{}%
+\xpatchcmd{\sectionmark}{\MakeUppercase}{}{}{}%
+\xpatchcmd*{\tableofcontents}{\MakeUppercase}{}{}{}%
+\makeatother
+
+\setcounter{secnumdepth}{3}
+\setcounter{tocdepth}{3}
+
+\renewcommand\_{\hbox{\textunderscore\kern-.05ex}}
+
+\newbox\boxA
+\setbox\boxA=\hbox{\ }
+\parindent=4\wd\boxA
+
+\newcommand\blankline{\vskip-.25\baselineskip}
+
+\newenvironment{indentblock}{\list{}{\setlength{\leftmargin}{\parindent}}\item[]}{\endlist}
+
+\newcommand{\keyw}[1]{\textbf{#1}}
+\newcommand{\synt}[1]{\textit{#1}}
+\newcommand{\hthm}[1]{\textbf{\textit{#1}}}
+
+%\renewcommand{\isactrlsub}[1]{\/$\sb{\mathrm{#1}}$}
+\renewcommand\isactrlsub[1]{\/$\sb{#1}$}
+\renewcommand\isadigit[1]{\/\ensuremath{\mathrm{#1}}}
+\renewcommand\isacharprime{\isamath{{'}\mskip-2mu}}
+\renewcommand\isacharunderscore{\mbox{\_}}
+\renewcommand\isacharunderscorekeyword{\mbox{\_}}
+\renewcommand\isachardoublequote{\mbox{\upshape{``}}}
+\renewcommand\isachardoublequoteopen{\mbox{\upshape{``}\kern.1ex}}
+\renewcommand\isachardoublequoteclose{\/\kern.15ex\mbox{\upshape{''}}}
+\renewcommand\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
+\renewcommand\isacharverbatimclose{\isacharasterisk\isacharbraceright}
+\renewcommand{\isasyminverse}{\isamath{{}^{-}}}
+
+\hyphenation{isa-belle}
+
+\isadroptag{theory}
+
+\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
+Defining Nonprimitively (Co)recursive Functions in Isabelle/HOL}
+\author{Jasmin Christian Blanchette, Aymeric Bouzy, \\
+Andreas Lochbihler, Andrei Popescu, and \\
+Dmitriy Traytel}
+
+\urlstyle{tt}
+
+\begin{document}
+
+\maketitle
+
+\begin{sloppy}
+\begin{abstract}
+\noindent
+This tutorial describes the definitional package for nonprimitively corecursive functions
+in Isabelle/HOL. The following commands are provided:
+\keyw{corec}, \keyw{corecursive}, \keyw{friend\_of\_corec}, and \keyw{coinduction\_upto}.
+They complement \keyw{codatatype}, \keyw{primcorec}, and \keyw{primcorecursive}, which
+define codatatypes and primitively corecursive functions.
+\end{abstract}
+\end{sloppy}
+
+\tableofcontents
+
+\input{Corec.tex}
+
+\let\em=\sl
+\bibliography{manual}{}
+\bibliographystyle{abbrv}
+
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Corec/document/style.sty Tue Mar 29 09:45:54 2016 +0200
@@ -0,0 +1,46 @@
+
+%% toc
+\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
+\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
+
+%% paragraphs
+\setlength{\parindent}{1em}
+
+%% references
+\newcommand{\secref}[1]{\S\ref{#1}}
+\newcommand{\figref}[1]{figure~\ref{#1}}
+
+%% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+%% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+\newcommand{\ditem}[1]{\item[\isastyletext #1]}
+
+%% quote environment
+\isakeeptag{quote}
+\renewenvironment{quote}
+ {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
+ {\endlist}
+\renewcommand{\isatagquote}{\begin{quote}}
+\renewcommand{\endisatagquote}{\end{quote}}
+\newcommand{\quotebreak}{\\[1.2ex]}
+
+%% presentation
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+%% character detail
+\renewcommand{\isadigit}[1]{\isamath{#1}}
+\binperiod
+\underscoreoff
+
+%% format
+\pagestyle{headings}
+\isabellestyle{it}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "implementation"
+%%% End:
--- a/src/Doc/ROOT Mon Mar 28 12:11:54 2016 +0200
+++ b/src/Doc/ROOT Tue Mar 29 09:45:54 2016 +0200
@@ -43,6 +43,22 @@
"root.tex"
"style.sty"
+session Corec (doc) in "Corec" = HOL +
+ options [document_variants = "corec"]
+ theories [document = false] "../Datatypes/Setup"
+ theories Corec
+ document_files (in "..")
+ "prepare_document"
+ "pdfsetup.sty"
+ "iman.sty"
+ "extra.sty"
+ "isar.sty"
+ "manual.bib"
+ document_files
+ "build"
+ "root.tex"
+ "style.sty"
+
session Datatypes (doc) in "Datatypes" = HOL +
options [document_variants = "datatypes"]
theories [document = false] Setup