--- a/CookBook/FirstSteps.thy Sat Feb 14 00:24:05 2009 +0000
+++ b/CookBook/FirstSteps.thy Sat Feb 14 13:20:21 2009 +0000
@@ -523,6 +523,8 @@
*}
+section {* Theories and Local Theories *}
+
section {* Storing Theorems *}
text {* @{ML PureThy.add_thms_dynamic} *}
--- a/CookBook/Package/Ind_Code.thy Sat Feb 14 00:24:05 2009 +0000
+++ b/CookBook/Package/Ind_Code.thy Sat Feb 14 13:20:21 2009 +0000
@@ -4,6 +4,13 @@
text {*
+ @{ML_chunk [display,gray] definitions_aux}
+ @{ML_chunk [display,gray,linenos] definitions}
+
+*}
+
+text {*
+
@{ML_chunk [display,gray] induction_rules}
*}
--- a/CookBook/Package/Ind_Interface.thy Sat Feb 14 00:24:05 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy Sat Feb 14 13:20:21 2009 +0000
@@ -108,11 +108,23 @@
text {*
The syntax of the \simpleinductive{} command can be described by the
railroad diagram in Figure~\ref{fig:railroad}. This diagram more or less
- translates directly into the parser
+ translates directly into the parser:
+
+ @{ML_chunk [display,gray] parser}
+
+ which we also described in Section~\ref{sec:parsingspecs}. Its return value
+ of this parser is a locale, the predicates, parameters and specifications of
+ the introduction rules. This is all the information we need to call the package.
- @{ML_chunk [display,gray,linenos] parser}
+ @{ML_chunk [display,gray,linenos] syntax}
- which we also described in Section~\ref{sec:parsingspecs}
+ The locale is passed as argument to the function
+ @{ML Toplevel.local_theory}.\footnote{FIXME Is this already described?} The
+ other arguments, i.e.~the predicates, parameters and specifications, are passed
+ to the function @{ML add_inductive in SimpleInductivePackage} (Line 4). The
+ actual command is defined in Lines 6 and 7. We called @{ML OuterSyntax.command}
+ with the kind-indicator @{ML OuterKeyword.thy_decl} since the package does
+ not need to open up any goal state (see Section~\ref{sec:newcommand}).
In order to add a new inductive predicate to a theory with the help of our
package, the user must \emph{invoke} it. For every package, there are
@@ -305,27 +317,6 @@
\isa{\isacommand{simple{\isacharunderscore}inductive}} command:
-
- The definition of the parser \verb!ind_decl! closely follows the railroad
- diagram shown above. In order to make the code more readable, the structures
- @{ML_struct OuterParse} and @{ML_struct OuterKeyword} are abbreviated by
- \texttt{P} and \texttt{K}, respectively. Note how the parser combinator
- @{ML "!!!" in OuterParse} is used: once the keyword \texttt{where}
- has been parsed, a non-empty list of introduction rules must follow.
- Had we not used the combinator @{ML "!!!" in OuterParse}, a
- \texttt{where} not followed by a list of rules would have caused the parser
- to respond with the somewhat misleading error message
-
- \begin{verbatim}
- Outer syntax error: end of input expected, but keyword where was found
- \end{verbatim}
-
- rather than with the more instructive message
-
- \begin{verbatim}
- Outer syntax error: proposition expected, but terminator was found
- \end{verbatim}
-
Once all arguments of the command have been parsed, we apply the function
@{ML add_inductive in SimpleInductivePackage}, which yields a local theory
transformer of type @{ML_type "local_theory -> local_theory"}. Commands in
--- a/CookBook/Package/simple_inductive_package.ML Sat Feb 14 00:24:05 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML Sat Feb 14 13:20:21 2009 +0000
@@ -20,17 +20,21 @@
fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P
-(* @chunk definitions *)
-fun define_aux s ((binding, syn), (attr, trm)) lthy =
+(* @chunk definitions_aux *)
+fun definitions_aux s ((binding, syn), (attr, trm)) lthy =
let
- val ((_, (_ , thm)), lthy) = LocalTheory.define s ((binding, syn), (attr, trm)) lthy
+ val ((_, (_, thm)), lthy) =
+ LocalTheory.define s ((binding, syn), (attr, trm)) lthy
in
(thm, lthy)
end
+(* @end *)
-fun DEFINITION params' rules preds preds' Tss lthy =
+(* @chunk definitions *)
+fun definitions params rules preds preds' Tss lthy =
let
- val rules' = map (ObjectLogic.atomize_term (ProofContext.theory_of lthy)) rules
+ val thy = ProofContext.theory_of lthy
+ val rules' = map (ObjectLogic.atomize_term thy) rules
in
fold_map (fn ((((R, _), syn), pred), Ts) =>
let
@@ -39,9 +43,9 @@
val t0 = list_comb (pred, zs);
val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0;
val t2 = fold_rev mk_all preds' t1;
- val t3 = fold_rev lambda (params' @ zs) t2;
+ val t3 = fold_rev lambda (params @ zs) t2;
in
- define_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3))
+ definitions_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3))
end) (preds ~~ preds' ~~ Tss) lthy
end
(* @end *)
@@ -125,7 +129,7 @@
val Tss = map (binder_types o fastype_of) preds';
val (ass,rules) = split_list specs;
- val (defs, lthy1) = DEFINITION params' rules preds preds' Tss lthy
+ val (defs, lthy1) = definitions params' rules preds preds' Tss lthy
val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2
@@ -190,7 +194,7 @@
Toplevel.local_theory loc (add_inductive preds params specs))
val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
- OuterKeyword.thy_decl ind_decl;
+ OuterKeyword.thy_decl ind_decl
(* @end *)
end;
--- a/CookBook/Tactical.thy Sat Feb 14 00:24:05 2009 +0000
+++ b/CookBook/Tactical.thy Sat Feb 14 13:20:21 2009 +0000
@@ -70,7 +70,7 @@
Note that in the code above we used antiquotations for referencing the theorems. Many theorems
also have ML-bindings with the same name. Therefore, we could also just have
- written @{ML "etac disjE 1"}, or in case there are no ML-binding obtained
+ written @{ML "etac disjE 1"}, or in case where there are no ML-binding obtain
the theorem dynamically using the function @{ML thm}; for example
\mbox{@{ML "etac (thm \"disjE\") 1"}}. Both ways however are considered bad style!
The reason
@@ -284,9 +284,13 @@
done
text_raw {*
\end{isabelle}
- \caption{A proof where we show the goal state as printed
- by the Isabelle system and as represented internally
- (highlighted boxes).\label{fig:goalstates}}
+ \caption{The figure shows a proof where each intermediate goal state is
+ printed by the Isabelle system and by @{ML my_print_tac}. The latter shows
+ the goal state as represented internally (highlighted boxes). This
+ illustrates that every goal state in Isabelle is represented by a theorem:
+ when we start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
+ @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when we finish the proof the
+ theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}
\end{figure}
*}
@@ -443,7 +447,7 @@
*}
lemma shows "\<forall>x\<in>A. P x \<Longrightarrow> Q x"
-apply(drule bspec)
+apply(tactic {* dtac @{thm bspec} 1 *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}*}
@@ -595,7 +599,7 @@
apply(tactic {* SUBPROOF sp_tac @{context} 1 *})?
txt {*
- then tactic prints out
+ then the tactic prints out:
\begin{quote}\small
\begin{tabular}{ll}
@@ -687,7 +691,7 @@
way. The reason is that an antiquotation would fix the type of the
quantified variable. So you really have to construct the pattern using the
basic term-constructors. This is not necessary in other cases, because their type
- is always fixed to function types involving only the type @{typ bool}. The
+ is always fixed to function types involving only the type @{typ bool}. For the
final pattern, we chose to just return @{ML all_tac}. Consequently,
@{ML select_tac} never fails.
@@ -784,7 +788,7 @@
atac, rtac @{thm disjI1}, atac]*}
text {*
- and just call @{ML foo_tac1}.
+ and call @{ML foo_tac1}.
With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be
guaranteed that all component tactics successfully apply; otherwise the
@@ -824,7 +828,7 @@
text {*
Since we like to mimic the behaviour of @{ML select_tac} as closely as possible,
we must include @{ML all_tac} at the end of the list, otherwise the tactic will
- fail if no rule applies (we laso have to wrap @{ML all_tac} using the
+ fail if no rule applies (we also have to wrap @{ML all_tac} using the
@{ML K}-combinator, because it does not take a subgoal number as argument). You can
test the tactic on the same goals:
*}
@@ -992,7 +996,7 @@
\end{minipage} *}
(*<*)oops(*>*)
text {*
- This will combinator prune the search space to just the first successful application.
+ This combinator will prune the search space to just the first successful application.
Attempting to apply \isacommand{back} in this goal states gives the
error message:
--- a/CookBook/chunks.ML Sat Feb 14 00:24:05 2009 +0000
+++ b/CookBook/chunks.ML Sat Feb 14 13:20:21 2009 +0000
@@ -20,8 +20,8 @@
|> (if ! ThyOutput.display then
map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
#> space_implode "\\isasep\\isanewline%\n"
+ #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I)
#> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I)
- #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I)
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
else
map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
--- a/CookBook/document/root.tex Sat Feb 14 00:24:05 2009 +0000
+++ b/CookBook/document/root.tex Sat Feb 14 13:20:21 2009 +0000
@@ -84,16 +84,16 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% for code that has line numbers
-\newenvironment{linenos}{\resetlinenumber\internallinenumbers}{\nolinenumbers}
+\newenvironment{linenos}{\resetlinenumber\internallinenumbers}{\par\nolinenumbers}
\isakeeptag{linenos}
\renewcommand{\isataglinenos}{\begin{linenos}}
-\renewcommand{\endisataglinenos}{\par\end{linenos}}
+\renewcommand{\endisataglinenos}{\end{linenos}}
% should only be used in ML code
\isakeeptag{linenosgray}
\renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\begin{linenos}}
-\renewcommand{\endisataglinenosgray}{\par\end{linenos}\end{graybox}\end{vanishML}}
+\renewcommand{\endisataglinenosgray}{\end{linenos}\end{graybox}\end{vanishML}}
\isakeeptag{small}
\renewcommand{\isatagsmall}{\begingroup\small}
Binary file cookbook.pdf has changed