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