# HG changeset patch # User Christian Urban # Date 1234617621 0 # Node ID 5f003fdf2653bd4943e64da4b7f1b655f2e1eb3c # Parent 796c6ea633b33e76580775a85a5c74ab9d369dcd polished and added more material to the package chapter diff -r 796c6ea633b3 -r 5f003fdf2653 CookBook/FirstSteps.thy --- 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} *} diff -r 796c6ea633b3 -r 5f003fdf2653 CookBook/Package/Ind_Code.thy --- 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} *} diff -r 796c6ea633b3 -r 5f003fdf2653 CookBook/Package/Ind_Interface.thy --- 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 diff -r 796c6ea633b3 -r 5f003fdf2653 CookBook/Package/simple_inductive_package.ML --- 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; diff -r 796c6ea633b3 -r 5f003fdf2653 CookBook/Tactical.thy --- 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 "\A; B\ \ A \ B"}} the theorem is + @{text "(\A; B\ \ A \ B) \ (\A; B\ \ A \ B)"}; when we finish the proof the + theorem is @{text "\A; B\ \ A \ B"}.\label{fig:goalstates}} \end{figure} *} @@ -443,7 +447,7 @@ *} lemma shows "\x\A. P x \ 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: diff -r 796c6ea633b3 -r 5f003fdf2653 CookBook/chunks.ML --- 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)) diff -r 796c6ea633b3 -r 5f003fdf2653 CookBook/document/root.tex --- 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} diff -r 796c6ea633b3 -r 5f003fdf2653 cookbook.pdf Binary file cookbook.pdf has changed