diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Tue May 14 16:59:53 2019 +0200 +++ b/ProgTutorial/First_Steps.thy Tue May 14 17:10:47 2019 +0200 @@ -2,11 +2,11 @@ imports Base begin -chapter {* First Steps\label{chp:firststeps} *} +chapter \First Steps\label{chp:firststeps}\ -text {* +text \ \begin{flushright} {\em ``The most effective debugging tool is still careful thought,\\ coupled with judiciously placed print statements.''} \\[1ex] @@ -29,20 +29,20 @@ We also generally assume you are working with the logic HOL. The examples that will be given might need to be adapted if you work in a different logic. -*} +\ -section {* Including ML-Code\label{sec:include} *} +section \Including ML-Code\label{sec:include}\ -text {* +text \ The easiest and quickest way to include code in a theory is by using the \isacommand{ML}-command. For example: \begin{isabelle} \begin{graybox} - \isacommand{ML}~@{text "\"}\isanewline + \isacommand{ML}~\\\\isanewline \hspace{5mm}@{ML "3 + 4"}\isanewline - @{text "\"}\isanewline - @{text "> 7"}\smallskip + \\\\isanewline + \> 7\\smallskip \end{graybox} \end{isabelle} @@ -52,8 +52,7 @@ Jedit GUI, then you just have to hover the cursor over the code and you see the evaluated result in the ``Output'' window. - As mentioned in the Introduction, we will drop the \isacommand{ML}~@{text - "\ \ \"} scaffolding whenever we show code. The lines + As mentioned in the Introduction, we will drop the \isacommand{ML}~\\ \ \\ scaffolding whenever we show code. The lines prefixed with @{text [quotes] ">"} are not part of the code, rather they indicate what the response is when the code is evaluated. There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for including @@ -63,9 +62,9 @@ \begin{quote} \begin{isabelle} - \isacommand{lemma}~@{text "test:"}\isanewline + \isacommand{lemma}~\test:\\isanewline \isacommand{shows}~@{text [quotes] "True"}\isanewline - \isacommand{ML\_prf}~@{text "\"}~@{ML "writeln \"Trivial!\""}~@{text "\"}\isanewline + \isacommand{ML\_prf}~\\\~@{ML "writeln \"Trivial!\""}~\\\\isanewline \isacommand{oops} \end{isabelle} \end{quote} @@ -84,15 +83,15 @@ \isacommand{imports} Main\\ \isacommand{begin}\\ \ldots\\ - \isacommand{ML\_file}~@{text "\"file_to_be_included.ML\""}\\ + \isacommand{ML\_file}~\"file_to_be_included.ML"\\\ \ldots \end{tabular} \end{quote} -*} +\ -section {* Printing and Debugging\label{sec:printing} *} +section \Printing and Debugging\label{sec:printing}\ -text {* +text \ During development you might find it necessary to inspect data in your code. This can be done in a ``quick-and-dirty'' fashion using the function @{ML_ind writeln in Output}. For example @@ -103,11 +102,11 @@ This function expects a string as argument. If you develop under PolyML, then there is a convenient, though again ``quick-and-dirty'', method for converting values into strings, namely the antiquotation - @{text "@{make_string}"}: + \@{make_string}\: @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""} - However, @{text "@{make_string}"} only works if the type of what + However, \@{make_string}\ only works if the type of what is converted is monomorphic and not a function. You can print out error messages with the function @{ML_ind error in Library}; @@ -118,12 +117,12 @@ "*** foo ***"} - This function raises the exception @{text ERROR}, which will then + This function raises the exception \ERROR\, which will then be displayed by the infrastructure indicating that it is an error by painting the output red. Note that this exception is meant for ``user-level'' error messages seen by the ``end-user''. For messages where you want to indicate a genuine program error - use the exception @{text Fail}. + use the exception \Fail\. Most often you want to inspect contents of Isabelle's basic data structures, namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp} @@ -132,12 +131,12 @@ we just use the functions @{ML_ind writeln in Pretty} from the structure @{ML_struct Pretty} and @{ML_ind pretty_term in Syntax} from the structure @{ML_struct Syntax}. For more convenience, we bind them to the toplevel. -*} +\ -ML %grayML{*val pretty_term = Syntax.pretty_term -val pwriteln = Pretty.writeln*} +ML %grayML\val pretty_term = Syntax.pretty_term +val pwriteln = Pretty.writeln\ -text {* +text \ They can be used as follows @{ML_response_fake [display,gray] @@ -147,27 +146,27 @@ If there is more than one term to be printed, you can use the function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty} to separate them. -*} +\ -ML %grayML{*fun pretty_terms ctxt trms = - Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*} +ML %grayML\fun pretty_terms ctxt trms = + Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))\ -text {* +text \ To print out terms together with their typing information, set the configuration value @{ML_ind show_types in Syntax} to @{ML true}. -*} +\ -ML %grayML{*val show_types_ctxt = Config.put show_types true @{context}*} +ML %grayML\val show_types_ctxt = Config.put show_types true @{context}\ -text {* +text \ Now by using this context @{ML pretty_term} prints out @{ML_response_fake [display, gray] "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})" "(1::nat, x::'a)"} - where @{text 1} and @{text x} are displayed with their inferred types. + where \1\ and \x\ are displayed with their inferred types. Other configuration values that influence printing of terms include @@ -178,34 +177,34 @@ \end{itemize} A @{ML_type cterm} can be printed with the following function. -*} +\ -ML %grayML %grayML{*fun pretty_cterm ctxt ctrm = - pretty_term ctxt (Thm.term_of ctrm)*} +ML %grayML %grayML\fun pretty_cterm ctxt ctrm = + pretty_term ctxt (Thm.term_of ctrm)\ -text {* +text \ Here the function @{ML_ind term_of in Thm} extracts the @{ML_type term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can be printed again with @{ML commas in Pretty}. -*} +\ -ML %grayML{*fun pretty_cterms ctxt ctrms = - Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))*} +ML %grayML\fun pretty_cterms ctxt ctrms = + Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))\ -text {* +text \ The easiest way to get the string of a theorem is to transform it into a @{ML_type term} using the function @{ML_ind prop_of in Thm}. -*} +\ -ML %grayML{*fun pretty_thm ctxt thm = - pretty_term ctxt (Thm.prop_of thm)*} +ML %grayML\fun pretty_thm ctxt thm = + pretty_term ctxt (Thm.prop_of thm)\ -text {* - Theorems include schematic variables, such as @{text "?P"}, - @{text "?Q"} and so on. They are instantiated by Isabelle when a theorem is applied. +text \ + Theorems include schematic variables, such as \?P\, + \?Q\ and so on. They are instantiated by Isabelle when a theorem is applied. For example, the theorem @{thm [source] conjI} shown below can be used for any (typable) - instantiation of @{text "?P"} and @{text "?Q"}. + instantiation of \?P\ and \?Q\. @{ML_response_fake [display, gray] "pwriteln (pretty_thm @{context} @{thm conjI})" @@ -213,16 +212,16 @@ However, to improve the readability when printing theorems, we can switch off the question marks as follows: -*} +\ -ML %grayML{*fun pretty_thm_no_vars ctxt thm = +ML %grayML\fun pretty_thm_no_vars ctxt thm = let val ctxt' = Config.put show_question_marks false ctxt in pretty_term ctxt' (Thm.prop_of thm) -end*} +end\ -text {* +text \ With this function, theorem @{thm [source] conjI} is now printed as follows: @{ML_response_fake [display, gray] @@ -231,31 +230,31 @@ Again the functions @{ML commas} and @{ML block in Pretty} help with printing more than one theorem. -*} +\ -ML %grayML{*fun pretty_thms ctxt thms = +ML %grayML\fun pretty_thms ctxt thms = Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms)) fun pretty_thms_no_vars ctxt thms = - Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*} + Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))\ -text {* +text \ Printing functions for @{ML_type typ} are -*} +\ -ML %grayML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty +ML %grayML\fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty fun pretty_typs ctxt tys = - Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*} + Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))\ -text {* +text \ respectively @{ML_type ctyp} -*} +\ -ML %grayML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (Thm.typ_of cty) +ML %grayML\fun pretty_ctyp ctxt cty = pretty_typ ctxt (Thm.typ_of cty) fun pretty_ctyps ctxt ctys = - Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))*} + Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))\ -text {* +text \ \begin{readmore} The simple conversion functions from Isabelle's main datatypes to @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. @@ -298,12 +297,12 @@ Most of the basic string functions of Isabelle are defined in @{ML_file "Pure/library.ML"}. \end{readmore} -*} +\ -section {* Combinators\label{sec:combinators} *} +section \Combinators\label{sec:combinators}\ -text {* +text \ For beginners perhaps the most puzzling parts in the existing code of Isabelle are the combinators. At first they seem to greatly obstruct the comprehension of code, but after getting familiar with them and handled with @@ -311,37 +310,37 @@ The simplest combinator is @{ML_ind I in Library}, which is just the identity function defined as -*} +\ -ML %grayML{*fun I x = x*} +ML %grayML\fun I x = x\ -text {* +text \ Another simple combinator is @{ML_ind K in Library}, defined as -*} +\ -ML %grayML{*fun K x = fn _ => x*} +ML %grayML\fun K x = fn _ => x\ -text {* - @{ML K} ``wraps'' a function around @{text "x"} that ignores its argument. As a - result, @{ML K} defines a constant function always returning @{text x}. +text \ + @{ML K} ``wraps'' a function around \x\ that ignores its argument. As a + result, @{ML K} defines a constant function always returning \x\. The next combinator is reverse application, @{ML_ind "|>" in Basics}, defined as: -*} +\ -ML %grayML{*fun x |> f = f x*} +ML %grayML\fun x |> f = f x\ -text {* While just syntactic sugar for the usual function application, +text \While just syntactic sugar for the usual function application, the purpose of this combinator is to implement functions in a - ``waterfall fashion''. Consider for example the function *} + ``waterfall fashion''. Consider for example the function\ -ML %linenosgray{*fun inc_by_five x = +ML %linenosgray\fun inc_by_five x = x |> (fn x => x + 1) |> (fn x => (x, x)) |> fst - |> (fn x => x + 4)*} + |> (fn x => x + 4)\ -text {* - which increments its argument @{text x} by 5. It does this by first +text \ + which increments its argument \x\ by 5. It does this by first incrementing the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking the first component of the pair (Line 4) and finally incrementing the first component by 4 (Line 5). This kind of cascading @@ -350,42 +349,42 @@ manner. This kind of coding should be familiar, if you have been exposed to Haskell's {\it do}-notation. Writing the function @{ML inc_by_five} using the reverse application is much clearer than writing -*} +\ -ML %grayML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*} +ML %grayML\fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4\ -text {* or *} +text \or\ -ML %grayML{*fun inc_by_five x = - ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*} +ML %grayML\fun inc_by_five x = + ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x\ -text {* and typographically more economical than *} +text \and typographically more economical than\ -ML %grayML{*fun inc_by_five x = +ML %grayML\fun inc_by_five x = let val y1 = x + 1 val y2 = (y1, y1) val y3 = fst y2 val y4 = y3 + 4 -in y4 end*} +in y4 end\ -text {* +text \ Another reasons to avoid the let-bindings in the code above: it is easy to get the intermediate values wrong and the resulting code is difficult to maintain. In Isabelle a ``real world'' example for a function written in the waterfall fashion might be the following code: -*} +\ -ML %linenosgray{*fun apply_fresh_args f ctxt = +ML %linenosgray\fun apply_fresh_args f ctxt = f |> fastype_of |> binder_types |> map (pair "z") |> Variable.variant_frees ctxt [f] |> map Free - |> curry list_comb f *} + |> curry list_comb f\ -text {* +text \ This function takes a term and a context as arguments. If the term is of function type, then @{ML "apply_fresh_args"} returns the term with distinct variables applied to it. For example, below three variables are applied to the term @@ -405,10 +404,10 @@ You can read off this behaviour from how @{ML apply_fresh_args} is coded: in Line 2, the function @{ML_ind fastype_of in Term} calculates the type of the term; @{ML_ind binder_types in Term} in the next line produces the list of - argument types (in the case above the list @{text "[nat, int, unit]"}); Line - 4 pairs up each type with the string @{text "z"}; the function @{ML_ind - variant_frees in Variable} generates for each @{text "z"} a unique name - avoiding the given @{text f}; the list of name-type pairs is turned into a + argument types (in the case above the list \[nat, int, unit]\); Line + 4 pairs up each type with the string \z\; the function @{ML_ind + variant_frees in Variable} generates for each \z\ a unique name + avoiding the given \f\; the list of name-type pairs is turned into a list of variable terms in Line 6, which in the last line is applied by the function @{ML_ind list_comb in Term} to the original term. In this last step we have to use the function @{ML_ind curry in Library}, because @{ML list_comb} @@ -429,18 +428,18 @@ end" "za z zb"} - where the @{text "za"} is correctly avoided. + where the \za\ is correctly avoided. The combinator @{ML_ind "#>" in Basics} is the reverse function composition. It can be used to define the following function -*} +\ -ML %grayML{*val inc_by_six = +ML %grayML\val inc_by_six = (fn x => x + 1) #> (fn x => x + 2) #> - (fn x => x + 3)*} + (fn x => x + 3)\ -text {* +text \ which is the function composed of first the increment-by-one function and then increment-by-two, followed by increment-by-three. Again, the reverse function composition allows you to read the code top-down. This combinator @@ -451,18 +450,18 @@ can be composed with @{ML "#>"}. Consider for example the following code, where we store the theorems @{thm [source] conjI}, @{thm [source] conjunct1} and @{thm [source] conjunct2} under alternative names. -*} +\ -local_setup %graylinenos {* +local_setup %graylinenos \ let fun my_note name thm = Local_Theory.note ((name, []), [thm]) #> snd in my_note @{binding "foo_conjI"} @{thm conjI} #> my_note @{binding "bar_conjunct1"} @{thm conjunct1} #> my_note @{binding "bar_conjunct2"} @{thm conjunct2} -end *} +end\ -text {* +text \ The function @{ML_text "my_note"} in line 3 is just a wrapper for the function @{ML_ind note in Local_Theory} in the structure @{ML_struct Local_Theory}; it stores a theorem under a name. @@ -474,15 +473,15 @@ in Basics} allows you to get hold of an intermediate result (to do some side-calculations or print out an intermediate result, for instance). The function - *} +\ -ML %linenosgray{*fun inc_by_three x = +ML %linenosgray\fun inc_by_three x = x |> (fn x => x + 1) |> tap (fn x => pwriteln (Pretty.str (@{make_string} x))) - |> (fn x => x + 2)*} + |> (fn x => x + 2)\ -text {* - increments the argument first by @{text "1"} and then by @{text "2"}. In the +text \ + increments the argument first by \1\ and then by \2\. In the middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one'' intermediate result. The function @{ML tap} can only be used for side-calculations, because any value that is computed cannot be merged back @@ -491,102 +490,102 @@ The combinator @{ML_ind "`" in Basics} (a backtick) is similar to @{ML tap}, but applies a function to the value and returns the result together with the value (as a pair). It is defined as -*} +\ -ML %grayML{*fun `f = fn x => (f x, x)*} +ML %grayML\fun `f = fn x => (f x, x)\ -text {* +text \ An example for this combinator is the function -*} +\ -ML %grayML{*fun inc_as_pair x = +ML %grayML\fun inc_as_pair x = x |> `(fn x => x + 1) - |> (fn (x, y) => (x, y + 1))*} + |> (fn (x, y) => (x, y + 1))\ -text {* - which takes @{text x} as argument, and then increments @{text x}, but also keeps - @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)" +text \ + which takes \x\ as argument, and then increments \x\, but also keeps + \x\. The intermediate result is therefore the pair @{ML "(x + 1, x)" for x}. After that, the function increments the right-hand component of the pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}. The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are defined for functions manipulating pairs. The first applies the function to the first component of the pair, defined as -*} +\ -ML %grayML{*fun (x, y) |>> f = (f x, y)*} +ML %grayML\fun (x, y) |>> f = (f x, y)\ -text {* +text \ and the second combinator to the second component, defined as -*} +\ -ML %grayML{*fun (x, y) ||> f = (x, f y)*} +ML %grayML\fun (x, y) ||> f = (x, f y)\ -text {* - These two functions can, for example, be used to avoid explicit @{text "lets"} for +text \ + These two functions can, for example, be used to avoid explicit \lets\ for intermediate values in functions that return pairs. As an example, suppose you want to separate a list of integers into two lists according to a threshold. If the threshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"} should be separated as @{ML "([1,2,3,4], [6,5])"}. Such a function can be implemented as -*} +\ -ML %grayML{*fun separate i [] = ([], []) +ML %grayML\fun separate i [] = ([], []) | separate i (x::xs) = let val (los, grs) = separate i xs in if i <= x then (los, x::grs) else (x::los, grs) - end*} + end\ -text {* +text \ where the return value of the recursive call is bound explicitly to the pair @{ML "(los, grs)" for los grs}. However, this function can be implemented more concisely as -*} +\ -ML %grayML{*fun separate _ [] = ([], []) +ML %grayML\fun separate _ [] = ([], []) | separate i (x::xs) = if i <= x then separate i xs ||> cons x - else separate i xs |>> cons x*} + else separate i xs |>> cons x\ -text {* - avoiding the explicit @{text "let"}. While in this example the gain in +text \ + avoiding the explicit \let\. While in this example the gain in conciseness is only small, in more complicated situations the benefit of - avoiding @{text "lets"} can be substantial. + avoiding \lets\ can be substantial. With the combinator @{ML_ind "|->" in Basics} you can re-combine the elements from a pair. This combinator is defined as -*} +\ -ML %grayML{*fun (x, y) |-> f = f x y*} +ML %grayML\fun (x, y) |-> f = f x y\ -text {* +text \ and can be used to write the following roundabout version - of the @{text double} function: -*} + of the \double\ function: +\ -ML %grayML{*fun double x = +ML %grayML\fun double x = x |> (fn x => (x, x)) - |-> (fn x => fn y => x + y)*} + |-> (fn x => fn y => x + y)\ -text {* +text \ The combinator @{ML_ind ||>> in Basics} plays a central role whenever your task is to update a theory and the update also produces a side-result (for example a theorem). Functions for such tasks return a pair whose second component is the theory and the fist component is the side-result. Using @{ML ||>>}, you can do conveniently the update and also accumulate the side-results. Consider the following simple function. -*} +\ -ML %linenosgray{*fun acc_incs x = +ML %linenosgray\fun acc_incs x = x |> (fn x => ("", x)) ||>> (fn x => (x, x + 1)) ||>> (fn x => (x, x + 1)) - ||>> (fn x => (x, x + 1))*} + ||>> (fn x => (x, x + 1))\ -text {* +text \ The purpose of Line 2 is to just pair up the argument with a dummy value (since @{ML ||>>} operates on pairs). Each of the next three lines just increment the value by one, but also nest the intermediate results to the left. For example @@ -626,15 +625,15 @@ obtained by previous calls. A more realistic example for this combinator is the following code -*} +\ -ML %grayML{*val ((([one_def], [two_def]), [three_def]), ctxt') = +ML %grayML\val ((([one_def], [two_def]), [three_def]), ctxt') = @{context} |> Local_Defs.define [((@{binding "One"}, NoSyn), (Binding.empty_atts, @{term "1::nat"}))] ||>> Local_Defs.define [((@{binding "Two"}, NoSyn), (Binding.empty_atts,@{term "2::nat"}))] - ||>> Local_Defs.define [((@{binding "Three"}, NoSyn), (Binding.empty_atts,@{term "3::nat"}))]*} + ||>> Local_Defs.define [((@{binding "Three"}, NoSyn), (Binding.empty_atts,@{term "3::nat"}))]\ -text {* +text \ where we make three definitions, namely @{term "One \ 1::nat"}, @{term "Two \ 2::nat"} and @{term "Three \ 3::nat"}. The point of this code is that we augment the initial context with the definitions. The result we are interested in is the @@ -658,15 +657,15 @@ described above have related combinators for function composition, namely @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the - function @{text double} can also be written as: -*} + function \double\ can also be written as: +\ -ML %grayML{*val double = +ML %grayML\val double = (fn x => (x, x)) #-> - (fn x => fn y => x + y)*} + (fn x => fn y => x + y)\ -text {* +text \ When using combinators for writing functions in waterfall fashion, it is sometimes necessary to do some ``plumbing'' in order to fit functions together. We have already seen such plumbing in the function @{ML @@ -687,11 +686,11 @@ |> pwriteln end" "m + n, m * n, m - n"} -*} +\ -text {* +text \ In this example we obtain three terms (using the function - @{ML_ind parse_term in Syntax}) whose variables @{text m} and @{text n} + @{ML_ind parse_term in Syntax}) whose variables \m\ and \n\ are of type @{typ "nat"}. If you have only a single term, then @{ML check_terms in Syntax} needs plumbing. This can be done with the function @{ML_ind singleton in Library}.\footnote{There is already a function @{ML check_term in @@ -722,12 +721,12 @@ \begin{exercise} Find out what the combinator @{ML "K I"} does. \end{exercise} -*} +\ -section {* ML-Antiquotations\label{sec:antiquote} *} +section \ML-Antiquotations\label{sec:antiquote}\ -text {* +text \ Recall from Section \ref{sec:include} that code in Isabelle is always embedded in a theory. The main advantage of this is that the code can contain references to entities defined on the logical level of Isabelle. By @@ -744,33 +743,32 @@ user level and therefore we are not interested in them in this Tutorial, except in Appendix \ref{rec:docantiquotations} where we show how to implement your own document antiquotations.} Syntactically antiquotations - are indicated by the @{ML_text @}-sign followed by text wrapped in @{text - "{\}"}. For example, one can print out the name of the current theory with + are indicated by the @{ML_text @}-sign followed by text wrapped in \{\}\. For example, one can print out the name of the current theory with the code @{ML_response [display,gray] "Context.theory_name @{theory}" "\"First_Steps\""} - where @{text "@{theory}"} is an antiquotation that is substituted with the + where \@{theory}\ is an antiquotation that is substituted with the current theory (remember that we assumed we are inside the theory - @{text First_Steps}). The name of this theory can be extracted using + \First_Steps\). The name of this theory can be extracted using the function @{ML_ind theory_name in Context}. Note, however, that antiquotations are statically linked, that is their value is determined at ``compile-time'', not at ``run-time''. For example the function -*} +\ -ML %grayML{*fun not_current_thyname () = Context.theory_name @{theory} *} +ML %grayML\fun not_current_thyname () = Context.theory_name @{theory}\ -text {* +text \ does \emph{not} return the name of the current theory, if it is run in a different theory. Instead, the code above defines the constant function that always returns the string @{text [quotes] "First_Steps"}, no matter where the - function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is + function is called. Operationally speaking, the antiquotation \@{theory}\ is \emph{not} replaced with code that will look up the current theory in some data structure and return it. Instead, it is literally replaced with the value representing the theory. - Another important antiquotation is @{text "@{context}"}. (What the + Another important antiquotation is \@{context}\. (What the difference between a theory and a context is will be described in Chapter \ref{chp:advanced}.) A context is for example needed to use the function @{ML print_abbrevs in Proof_Context} that list of all currently @@ -786,11 +784,11 @@ The precise output of course depends on the abbreviations that are currently defined; this can change over time. You can also use antiquotations to refer to proved theorems: - @{text "@{thm \}"} for a single theorem + \@{thm \}\ for a single theorem @{ML_response_fake [display,gray] "@{thm allI}" "(\x. ?P x) \ \x. ?P x"} - and @{text "@{thms \}"} for more than one + and \@{thms \}\ for more than one @{ML_response_fake [display,gray] "@{thms conj_ac}" @@ -811,14 +809,14 @@ under this name (this becomes especially important when you deal with theorem lists; see Section \ref{sec:storing}). - It is also possible to prove lemmas with the antiquotation @{text "@{lemma \ by \}"} - whose first argument is a statement (possibly many of them separated by @{text "and"}) + It is also possible to prove lemmas with the antiquotation \@{lemma \ by \}\ + whose first argument is a statement (possibly many of them separated by \and\) and the second is a proof. For example -*} +\ -ML %grayML{*val foo_thms = @{lemma "True" and "False \ P" by simp_all} *} +ML %grayML\val foo_thms = @{lemma "True" and "False \ P" by simp_all}\ -text {* +text \ The result can be printed out as follows. @{ML_response_fake [gray,display] @@ -829,17 +827,17 @@ You can also refer to the current simpset via an antiquotation. To illustrate this we implement the function that extracts the theorem names stored in a simpset. -*} +\ -ML %grayML{*fun get_thm_names_from_ss ctxt = +ML %grayML\fun get_thm_names_from_ss ctxt = let val simpset = Raw_Simplifier.simpset_of ctxt val {simps,...} = Raw_Simplifier.dest_ss simpset in map #1 simps -end*} +end\ -text {* +text \ The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all information stored in the simpset, but here we are only interested in the names of the simp-rules. Now you can feed in the current simpset into this function. @@ -856,15 +854,15 @@ It is also possible to define your own antiquotations. But you should exercise care when introducing new ones, as they can also make your code difficult to read. In the next chapter we describe how to construct - terms with the (built-in) antiquotation @{text "@{term \}"}. A restriction + terms with the (built-in) antiquotation \@{term \}\. A restriction of this antiquotation is that it does not allow you to use schematic variables in terms. If you want to have an antiquotation that does not have this restriction, you can implement your own using the function @{ML_ind inline in ML_Antiquotation} from the structure @{ML_struct ML_Antiquotation}. The code - for the antiquotation @{text "term_pat"} is as follows. -*} + for the antiquotation \term_pat\ is as follows. +\ -ML %linenosgray{*val term_pat_setup = +ML %linenosgray\val term_pat_setup = let val parser = Args.context -- Scan.lift Args.embedded_inner_syntax @@ -874,15 +872,15 @@ |> ML_Syntax.atomic in ML_Antiquotation.inline @{binding "term_pat"} (parser >> term_pat) -end*} +end\ -text {* +text \ To use it you also have to install it using \isacommand{setup} like so -*} +\ -setup %gray {* term_pat_setup *} +setup %gray \term_pat_setup\ -text {* +text \ The parser in Line 2 provides us with a context and a string; this string is transformed into a term using the function @{ML_ind read_term_pattern in Proof_Context} (Line 5); the next two lines transform the term into a string @@ -893,11 +891,11 @@ "@{term_pat \"Suc (?x::nat)\"}" "Const (\"Suc\", \"nat \ nat\") $ Var ((\"x\", 0), \"nat\")"} - which shows the internal representation of the term @{text "Suc ?x"}. Similarly + which shows the internal representation of the term \Suc ?x\. Similarly we can write an antiquotation for type patterns. Its code is -*} +\ -ML %grayML{*val type_pat_setup = +ML %grayML\val type_pat_setup = let val parser = Args.context -- Scan.lift Args.embedded_inner_syntax @@ -911,15 +909,15 @@ end in ML_Antiquotation.inline @{binding "typ_pat"} (parser >> typ_pat) -end*} +end\ -text {* +text \ which can be installed with -*} +\ -setup %gray {* type_pat_setup *} +setup %gray \type_pat_setup\ -text {* +text \ However, a word of warning is in order: new antiquotations should be introduced only after careful deliberations. They can potentially make your code harder, rather than easier, to read. @@ -928,11 +926,11 @@ contain the infrastructure and definitions for most antiquotations. Most of the basic operations on ML-syntax are implemented in @{ML_file "Pure/ML/ml_syntax.ML"}. \end{readmore} -*} +\ -section {* Storing Data in Isabelle\label{sec:storing} *} +section \Storing Data in Isabelle\label{sec:storing}\ -text {* +text \ Isabelle provides mechanisms for storing (and retrieving) arbitrary data. Before we delve into the details, let us digress a bit. Conventional wisdom has it that the type-system of ML ensures that an @@ -956,9 +954,9 @@ We will show the usage of the universal type by storing an integer and a boolean into a single list. Let us first define injection and projection functions for booleans and integers into and from the type @{ML_type Universal.universal}. -*} +\ -ML %grayML{*local +ML %grayML\local val fn_int = Universal.tag () : int Universal.tag val fn_bool = Universal.tag () : bool Universal.tag in @@ -966,23 +964,23 @@ val inject_bool = Universal.tagInject fn_bool; val project_int = Universal.tagProject fn_int; val project_bool = Universal.tagProject fn_bool -end*} +end\ -text {* +text \ Using the injection functions, we can inject the integer @{ML_text "13"} and the boolean value @{ML_text "true"} into @{ML_type Universal.universal}, and then store them in a @{ML_type "Universal.universal list"} as follows: -*} +\ -ML %grayML{*val foo_list = +ML %grayML\val foo_list = let val thirteen = inject_int 13 val truth_val = inject_bool true in [thirteen, truth_val] -end*} +end\ -text {* +text \ The data can be retrieved with the projection functions defined above. @{ML_response_fake [display, gray] @@ -1023,15 +1021,15 @@ and therefore it makes sense to store this data inside a theory. Consequently we use the functor @{ML_funct Theory_Data}. The code for the table is: -*} +\ -ML %linenosgray{*structure Data = Theory_Data +ML %linenosgray\structure Data = Theory_Data (type T = thm Symtab.table val empty = Symtab.empty val extend = I - val merge = Symtab.merge (K true))*} + val merge = Symtab.merge (K true))\ -text {* +text \ In order to store data in a theory, we have to specify the type of the data (Line 2). In this case we specify the type @{ML_type "thm Symtab.table"}, which stands for a table in which @{ML_type string}s can be looked up @@ -1046,23 +1044,23 @@ it (@{ML Data.map}). There is also the function @{ML Data.put}, but it is not relevant here. Below we define two auxiliary functions, which help us with accessing the table. -*} +\ -ML %grayML{*val lookup = Symtab.lookup o Data.get -fun update k v = Data.map (Symtab.update (k, v))*} +ML %grayML\val lookup = Symtab.lookup o Data.get +fun update k v = Data.map (Symtab.update (k, v))\ -text {* +text \ Since we want to store introduction rules associated with their logical connective, we can fill the table as follows. -*} +\ -setup %gray {* +setup %gray \ update "conj" @{thm conjI} #> update "imp" @{thm impI} #> update "all" @{thm allI} -*} +\ -text {* +text \ The use of the command \isacommand{setup} makes sure the table in the \emph{current} theory is updated (this is explained further in Section~\ref{sec:theories}). The lookup can now be performed as follows. @@ -1074,11 +1072,11 @@ An important point to note is that these tables (and data in general) need to be treated in a purely functional fashion. Although we can update the table as follows -*} +\ -setup %gray {* update "conj" @{thm TrueI} *} +setup %gray \update "conj" @{thm TrueI}\ -text {* +text \ and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"} @{ML_response_fake [display, gray] @@ -1091,15 +1089,15 @@ defeat its undo-mechanism. To see the latter, consider the following data container where we maintain a reference to a list of integers. -*} +\ -ML %grayML{*structure WrongRefData = Theory_Data +ML %grayML\structure WrongRefData = Theory_Data (type T = (int list) Unsynchronized.ref val empty = Unsynchronized.ref [] val extend = I - val merge = fst)*} + val merge = fst)\ -text {* +text \ We initialise the reference with the empty list. Consequently a first lookup produces @{ML "ref []" in Unsynchronized}. @@ -1108,20 +1106,20 @@ "ref []"} For updating the reference we use the following function -*} +\ -ML %grayML{*fun ref_update n = WrongRefData.map - (fn r => let val _ = r := n::(!r) in r end)*} +ML %grayML\fun ref_update n = WrongRefData.map + (fn r => let val _ = r := n::(!r) in r end)\ -text {* +text \ which takes an integer and adds it to the content of the reference. As before, we update the reference with the command \isacommand{setup}. -*} +\ -setup %gray {* ref_update 1 *} +setup %gray \ref_update 1\ -text {* +text \ A lookup in the current theory gives then the expected list @{ML "ref [1]" in Unsynchronized}. @@ -1159,30 +1157,30 @@ Storing data in a proof context is done in a similar fashion. As mentioned before, the corresponding functor is @{ML_funct_ind Proof_Data}. With the following code we can store a list of terms in a proof context. -*} +\ -ML %grayML{*structure Data = Proof_Data +ML %grayML\structure Data = Proof_Data (type T = term list - fun init _ = [])*} + fun init _ = [])\ -text {* +text \ The init-function we have to specify must produce a list for when a context is initialised (possibly taking the theory into account from which the context is derived). We choose here to just return the empty list. Next we define two auxiliary functions for updating the list with a given term and printing the list. -*} +\ -ML %grayML{*fun update trm = Data.map (fn trms => trm::trms) +ML %grayML\fun update trm = Data.map (fn trms => trm::trms) fun print ctxt = case (Data.get ctxt) of [] => pwriteln (Pretty.str "Empty!") - | trms => pwriteln (pretty_terms ctxt trms)*} + | trms => pwriteln (pretty_terms ctxt trms)\ -text {* +text \ Next we start with the context generated by the antiquotation - @{text "@{context}"} and update it in various ways. + \@{context}\ and update it in various ways. @{ML_response_fake [display,gray] "let @@ -1216,63 +1214,63 @@ For convenience there is an abstract layer, namely the type @{ML_type Context.generic}, for treating theories and proof contexts more uniformly. This type is defined as follows -*} +\ -ML_val %grayML{*datatype generic = +ML_val %grayML\datatype generic = Theory of theory -| Proof of proof*} +| Proof of proof\ -text {* +text \ \footnote{\bf FIXME: say more about generic contexts.} There are two special instances of the data storage mechanism described above. The first instance implements named theorem lists using the functor @{ML_funct_ind Named_Thms}. This is because storing theorems in a list is such a common task. To obtain a named theorem list, you just declare -*} +\ -ML %grayML{*structure FooRules = Named_Thms +ML %grayML\structure FooRules = Named_Thms (val name = @{binding "foo"} - val description = "Theorems for foo") *} + val description = "Theorems for foo")\ -text {* +text \ and set up the @{ML_struct FooRules} with the command -*} +\ -setup %gray {* FooRules.setup *} +setup %gray \FooRules.setup\ -text {* +text \ This code declares a data container where the theorems are stored, - an attribute @{text foo} (with the @{text add} and @{text del} options + an attribute \foo\ (with the \add\ and \del\ options for adding and deleting theorems) and an internal ML-interface for retrieving and modifying the theorems. Furthermore, the theorems are made available on the user-level under the name - @{text foo}. For example you can declare three lemmas to be a member of the - theorem list @{text foo} by: -*} + \foo\. For example you can declare three lemmas to be a member of the + theorem list \foo\ by: +\ lemma rule1[foo]: "A" sorry lemma rule2[foo]: "B" sorry lemma rule3[foo]: "C" sorry -text {* and undeclare the first one by: *} +text \and undeclare the first one by:\ declare rule1[foo del] -text {* You can query the remaining ones with: +text \You can query the remaining ones with: \begin{isabelle} - \isacommand{thm}~@{text "foo"}\\ - @{text "> ?C"}\\ - @{text "> ?B"} + \isacommand{thm}~\foo\\\ + \> ?C\\\ + \> ?B\ \end{isabelle} On the ML-level, we can add theorems to the list with @{ML FooRules.add_thm}: -*} +\ -setup %gray {* Context.theory_map (FooRules.add_thm @{thm TrueI}) *} +setup %gray \Context.theory_map (FooRules.add_thm @{thm TrueI})\ -text {* +text \ The rules in the list can be retrieved using the function @{ML FooRules.get}: @@ -1293,24 +1291,23 @@ The second special instance of the data storage mechanism are configuration values. They are used to enable users to configure tools without having to resort to the ML-level (and also to avoid references). Assume you want the - user to control three values, say @{text bval} containing a boolean, @{text - ival} containing an integer and @{text sval} containing a string. These + user to control three values, say \bval\ containing a boolean, \ival\ containing an integer and \sval\ containing a string. These values can be declared by -*} +\ -ML %grayML{*val bval = Attrib.setup_config_bool @{binding "bval"} (K false) +ML %grayML\val bval = Attrib.setup_config_bool @{binding "bval"} (K false) val ival = Attrib.setup_config_int @{binding "ival"} (K 0) -val sval = Attrib.setup_config_string @{binding "sval"} (K "some string") *} +val sval = Attrib.setup_config_string @{binding "sval"} (K "some string")\ -text {* +text \ where each value needs to be given a default. The user can now manipulate the values from the user-level of Isabelle with the command -*} +\ declare [[bval = true, ival = 3]] -text {* +text \ On the ML-level these values can be retrieved using the function @{ML_ind get in Config} from a proof context @@ -1343,7 +1340,7 @@ A concrete example for a configuration value is @{ML_ind simp_trace in Raw_Simplifier}, which switches on trace information in the simplifier. This can be used for example in the following proof -*} +\ lemma @@ -1354,7 +1351,7 @@ show "True" by simp qed -text {* +text \ in order to inspect how the simplifier solves the first subgoal. \begin{readmore} @@ -1362,11 +1359,11 @@ the files @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}. \end{readmore} -*} +\ -section {* Summary *} +section \Summary\ -text {* +text \ This chapter describes the combinators that are used in Isabelle, as well as a simple printing infrastructure for @{ML_type term}, @{ML_type cterm} and @{ML_type thm}. The section on ML-antiquotations shows how to refer @@ -1381,5 +1378,5 @@ \end{itemize} \end{conventions} -*} +\ end