author | wenzelm |
Tue, 09 Mar 2021 18:44:43 +0100 | |
changeset 73401 | 8b464825d2b5 |
parent 59005 | 1c54ebc68394 |
child 73404 | 299f6a8faccc |
permissions | -rw-r--r-- |
21212 | 1 |
|
25092 | 2 |
\documentclass[a4paper,fleqn]{article} |
23003 | 3 |
|
73401 | 4 |
\usepackage{graphicx} |
21212 | 5 |
\usepackage[refpage]{nomencl} |
48948
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
6 |
\usepackage{iman,extra,isar} |
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
7 |
\usepackage{isabelle,isabellesym} |
21212 | 8 |
\usepackage{style} |
23003 | 9 |
\usepackage{mathpartir} |
10 |
\usepackage{amsthm} |
|
48948
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
11 |
\usepackage{pdfsetup} |
21212 | 12 |
|
13 |
\newcommand{\cmd}[1]{\isacommand{#1}} |
|
14 |
||
15 |
\newcommand{\isasymINFIX}{\cmd{infix}} |
|
16 |
\newcommand{\isasymLOCALE}{\cmd{locale}} |
|
17 |
\newcommand{\isasymINCLUDES}{\cmd{includes}} |
|
18 |
\newcommand{\isasymDATATYPE}{\cmd{datatype}} |
|
19 |
\newcommand{\isasymDEFINES}{\cmd{defines}} |
|
20 |
\newcommand{\isasymNOTES}{\cmd{notes}} |
|
21 |
\newcommand{\isasymCLASS}{\cmd{class}} |
|
22 |
\newcommand{\isasymINSTANCE}{\cmd{instance}} |
|
23 |
\newcommand{\isasymLEMMA}{\cmd{lemma}} |
|
24 |
\newcommand{\isasymPROOF}{\cmd{proof}} |
|
25 |
\newcommand{\isasymQED}{\cmd{qed}} |
|
26 |
\newcommand{\isasymFIX}{\cmd{fix}} |
|
27 |
\newcommand{\isasymASSUME}{\cmd{assume}} |
|
28 |
\newcommand{\isasymSHOW}{\cmd{show}} |
|
29 |
\newcommand{\isasymNOTE}{\cmd{note}} |
|
30 |
\newcommand{\isasymCODEGEN}{\cmd{code\_gen}} |
|
31 |
\newcommand{\isasymPRINTCODETHMS}{\cmd{print\_codethms}} |
|
32 |
\newcommand{\isasymFUN}{\cmd{fun}} |
|
33 |
\newcommand{\isasymFUNCTION}{\cmd{function}} |
|
34 |
\newcommand{\isasymPRIMREC}{\cmd{primrec}} |
|
35 |
\newcommand{\isasymRECDEF}{\cmd{recdef}} |
|
36 |
||
37 |
\newcommand{\qt}[1]{``#1''} |
|
38 |
\newcommand{\qtt}[1]{"{}{#1}"{}} |
|
39 |
\newcommand{\qn}[1]{\emph{#1}} |
|
40 |
\newcommand{\strong}[1]{{\bfseries #1}} |
|
41 |
\newcommand{\fixme}[1][!]{\strong{FIXME: #1}} |
|
42 |
||
23003 | 43 |
\newtheorem{exercise}{Exercise}{\bf}{\itshape} |
44 |
%\newtheorem*{thmstar}{Theorem}{\bf}{\itshape} |
|
21212 | 45 |
|
46 |
\hyphenation{Isabelle} |
|
47 |
\hyphenation{Isar} |
|
48 |
||
49 |
\isadroptag{theory} |
|
23003 | 50 |
\title{Defining Recursive Functions in Isabelle/HOL} |
51 |
\author{Alexander Krauss} |
|
21212 | 52 |
|
53 |
\isabellestyle{tt} |
|
54 |
||
55 |
\begin{document} |
|
56 |
||
23805 | 57 |
\date{\ \\} |
21212 | 58 |
\maketitle |
59 |
||
60 |
\begin{abstract} |
|
52791
9e4bb60f8007
tuned docs (the function package isn't so new anymore)
blanchet
parents:
48985
diff
changeset
|
61 |
This tutorial describes the use of the \emph{function} package, |
23003 | 62 |
which provides general recursive function definitions for Isabelle/HOL. |
23188 | 63 |
We start with very simple examples and then gradually move on to more |
64 |
advanced topics such as manual termination proofs, nested recursion, |
|
23805 | 65 |
partiality, tail recursion and congruence rules. |
21212 | 66 |
\end{abstract} |
67 |
||
23003 | 68 |
%\thispagestyle{empty}\clearpage |
21212 | 69 |
|
23003 | 70 |
%\pagenumbering{roman} |
71 |
%\clearfirst |
|
21212 | 72 |
|
23003 | 73 |
\input{intro.tex} |
48948
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
74 |
\input{Functions.tex} |
23805 | 75 |
%\input{conclusion.tex} |
21212 | 76 |
|
77 |
\begingroup |
|
78 |
%\tocentry{\bibname} |
|
79 |
\bibliographystyle{plain} \small\raggedright\frenchspacing |
|
48948
fa49f8890ef3
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
80 |
\bibliography{manual} |
21212 | 81 |
\endgroup |
82 |
||
83 |
\end{document} |
|
84 |
||
85 |
||
86 |
%%% Local Variables: |
|
87 |
%%% mode: latex |
|
88 |
%%% TeX-master: t |
|
89 |
%%% End: |