# HG changeset patch # User Christian Urban # Date 1231969564 0 # Node ID 14c3dd5ee2ad8091b679834e5d03bf235edfe9af # Parent bbb2d5f1d58d0036df79f219dd266b19412001d9 removed mytable from root-file diff -r bbb2d5f1d58d -r 14c3dd5ee2ad CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Wed Jan 14 18:30:41 2009 +0000 +++ b/CookBook/FirstSteps.thy Wed Jan 14 21:46:04 2009 +0000 @@ -157,10 +157,11 @@ map #name (Net.entries rules) end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \]"} - In the second example, the function @{ML rep_ss in MetaSimplifier} returns a record - containing information about the simpset. The rules of a simpset are stored in a - discrimination net (a datastructure for fast indexing). From this net we can extract - the entries using the function @{ML Net.entries}. + The second example extracts the theorem names that are stored in a simpset. + For this the function @{ML rep_ss in MetaSimplifier} returns a record + containing information about the simpset. The rules of a simpset are stored + in a discrimination net (a datastructure for fast indexing). From this net + we can extract the entries using the function @{ML Net.entries}. While antiquotations have many applications, they were originally introduced to avoid explicit bindings for theorems such as @@ -185,8 +186,9 @@ One way to construct terms of Isabelle on the ML-level is by using the antiquotation \mbox{@{text "@{term \}"}}. For example - @{ML_response [display] "@{term \"(a::nat) + b = c\"}" - "Const (\"op =\", \) $ (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} + @{ML_response [display] + "@{term \"(a::nat) + b = c\"}" + "Const (\"op =\", \) $ (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} This will show the term @{term "(a::nat) + b = c"}, but printed using the internal representation of this term. This internal representation corresponds to the diff -r bbb2d5f1d58d -r 14c3dd5ee2ad CookBook/Package/Ind_Interface.thy --- a/CookBook/Package/Ind_Interface.thy Wed Jan 14 18:30:41 2009 +0000 +++ b/CookBook/Package/Ind_Interface.thy Wed Jan 14 21:46:04 2009 +0000 @@ -301,7 +301,8 @@ structure of the tokens used, the second part of the library consists of combinators for dealing with specific token types. The following is an excerpt from the signature of @{ML_struct Scan}: -\begin{mytable} + +\begin{table} @{ML "|| : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b"} \\ @{ML "-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e"} \\ @{ML "|-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e"} \\ @@ -311,7 +312,7 @@ @{ML "repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\ @{ML ">> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c"} \\ @{ML "!! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b"} -\end{mytable} +\end{table} Interestingly, the functions shown above are so generic that they do not even rely on the input and output of the parser being a list of tokens. If \texttt{p} succeeds, i.e.\ does not raise an exception, the parser @@ -348,10 +349,12 @@ from simpler parsers. In order for these combinators to be useful, we also need some basic parsers. As an example, we consider the following two parsers defined in @{ML_struct Scan}: -\begin{mytable} + +\begin{table} @{ML "one: ('a -> bool) -> 'a list -> 'a * 'a list" in Scan} \\ @{ML "$$ : string -> string list -> string * string list"} -\end{mytable} +\end{table} + The parser @{ML "one pred" for pred in Scan} parses exactly one token that satisfies the predicate \texttt{pred}, whereas @{ML "$$ s" for s} only accepts a token that equals the string \texttt{s}. Note that we can easily @@ -371,7 +374,8 @@ The parser functions for the theory syntax are contained in the structure @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}. In our parser, we will use the following functions: -\begin{mytable} + +\begin{table} @{ML "$$$ : string -> token list -> string * token list" in OuterParse} \\ @{ML "enum1: string -> (token list -> 'a * token list) -> token list -> 'a list * token list" in OuterParse} \\ @@ -382,7 +386,8 @@ @{ML "for_fixes: token list -> (Binding.T * string option * mixfix) list * token list" in OuterParse} \\ @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse} -\end{mytable} +\end{table} + The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from @{ML_struct Scan}. @@ -400,10 +405,12 @@ and @{ML for_fixes in OuterParse}, respectively. In addition, the following function from @{ML_struct SpecParse} for parsing an optional theorem name and attribute, followed by a delimiter, will be useful: -\begin{mytable} + +\begin{table} @{ML "opt_thm_name: string -> token list -> Attrib.binding * token list" in SpecParse} -\end{mytable} +\end{table} + We now have all the necessary tools to write the parser for our \isa{\isacommand{simple{\isacharunderscore}inductive}} command: @{ML_chunk [display] syntax} diff -r bbb2d5f1d58d -r 14c3dd5ee2ad CookBook/document/root.tex --- a/CookBook/document/root.tex Wed Jan 14 18:30:41 2009 +0000 +++ b/CookBook/document/root.tex Wed Jan 14 21:46:04 2009 +0000 @@ -21,7 +21,7 @@ \renewcommand{\isastyle}{\small\tt\slshape}% \isadroptag{theory} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % For cross references to the other manuals: \usepackage{xr} \externaldocument[I-]{implementation} @@ -33,21 +33,18 @@ \newcommand{\rchcite}[1]{[Isar Ref.\,Man., Ch.~\isarref{#1}]} \newcommand{\rsccite}[1]{[Isar Ref.\,Man., Sec.~\isarref{#1}]} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % sane default for proof documents -\parindent 0pt\parskip 0.6ex +\parindent 0pt\parskip 0.7ex -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +\hyphenation{Isabelle} + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % to work around a problem with \isanewline \renewcommand{\isanewline}{{\parindent0pt\parskip0pt\mbox{}\par\mbox{}}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% FIXME: WHAT DOES THIS DO? -\renewenvironment{isabelle} -{\begin{trivlist}\begin{isabellebody}\small\item\relax} -{\end{isabellebody}\end{trivlist}} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % for exercises, comments and readmores \newtheorem{exercise}{Exercise}[section] \newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}} @@ -58,17 +55,15 @@ \newenvironment{readmore}% {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% FIXME: THIS SHOULD NOT BE USED ANYMORE -% a table environment with proper indentation -\newenvironment{mytable} -{\begin{trivlist}\item\begin{tabular}{@{\hspace{2ex}}l}} -{\end{tabular}\end{trivlist}} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\hyphenation{Isabelle} +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% this is to draw a gray box around code +\makeatletter\newenvironment{graybox}{% + \begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}% + \colorbox{gray!10}{\usebox{\@tempboxa}} +}\makeatother -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % this hack is for getting rid of the ML {* ... *} % scaffolding around function definitions \newenvironment{vanishML}{% @@ -76,31 +71,27 @@ \renewcommand{\isacharverbatimopen}{}% \renewcommand{\isacharverbatimclose}{}}{} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\makeatletter\newenvironment{graybox}{% - \begin{lrbox}{\@tempboxa}\begin{minipage}{\textwidth}}{\end{minipage}\end{lrbox}% - \colorbox{gray!5}{\usebox{\@tempboxa}} -}\makeatother - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \isakeeptag{CookBookML} \renewcommand{\isatagCookBookML}{\begin{vanishML}\begin{graybox}} \renewcommand{\endisatagCookBookML}{\end{graybox}\end{vanishML}\smallskip} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % for line numbers \isakeeptag{linenumbers} \renewcommand{\isataglinenumbers} {\begin{vanishML}\begingroup\begin{graybox}\resetlinenumber\internallinenumbers} \renewcommand{\endisataglinenumbers}{\end{graybox}\endgroup\end{vanishML}\smallskip} -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + + +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{document} \title{\mbox{}\\[-10ex] \includegraphics[scale=0.5]{cookbook-logo.jpg}\\[3ex] The Isabelle Programmer's Cookbook (fragment)} + \author{with contributions by:\\[2ex] \begin{tabular}{r@{\hspace{1.8mm}}l} Stefan & Berghofer\\ @@ -108,8 +99,8 @@ Jeremy & Dawson\\ Alexander & Krauss\\ \end{tabular}} + \maketitle - \tableofcontents % generated text of all theories diff -r bbb2d5f1d58d -r 14c3dd5ee2ad cookbook.pdf Binary file cookbook.pdf has changed