# HG changeset patch # User blanchet # Date 1459237554 -7200 # Node ID 628c97d39627c0da7c5db8bbefbd41615c2c12eb # Parent fe827c6fa8c51de6fdf92de572414942667b1c64 added sketchy 'corec' documentation diff -r fe827c6fa8c5 -r 628c97d39627 doc/Contents --- 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 - diff -r fe827c6fa8c5 -r 628c97d39627 src/Doc/Corec/Corec.thy --- /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 \Introduction + \label{sec:introduction}\ + +text \ +... +\cite{isabelle-datatypes} +\ + + +section \Introductory Examples + \label{sec:introductory-examples}\ + + +subsection \Simple Corecursion + \label{ssec:simple-corecursion}\ + + +subsection \Nested Corecursion + \label{ssec:nested-corecursion}\ + + +subsection \Polymorphism + \label{ssec:polymorphism}\ + + +subsection \Coinduction + \label{ssec:coinduction}\ + + +subsection \Uniqueness Reasoning + \label{ssec:uniqueness-reasoning}\ + + +section \Command Syntax + \label{sec:command-syntax}\ + + +subsection \corec and corecursive + \label{ssec:corec-and-corecursive}\ + + +subsection \friend_of_corec + \label{ssec:friend-of-corec}\ + + +subsection \coinduction_upto + \label{ssec:coinduction-upto}\ + + +section \Generated Theorems + \label{sec:generated-theorems}\ + + +subsection \corec and corecursive + \label{ssec:corec-and-corecursive}\ + + +subsection \friend_of_corec + \label{ssec:friend-of-corec}\ + + +subsection \coinduction_upto + \label{ssec:coinduction-upto}\ + + +section \Proof Method + \label{sec:proof-method}\ + + +subsection \corec_unique + \label{ssec:corec-unique}\ + + +section \Known Bugs and Limitations + \label{sec:known-bugs-and-limitations}\ + +text \ +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} +\ + +end diff -r fe827c6fa8c5 -r 628c97d39627 src/Doc/Corec/document/build --- /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" + diff -r fe827c6fa8c5 -r 628c97d39627 src/Doc/Corec/document/root.tex --- /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} diff -r fe827c6fa8c5 -r 628c97d39627 src/Doc/Corec/document/style.sty --- /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: diff -r fe827c6fa8c5 -r 628c97d39627 src/Doc/ROOT --- 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