# HG changeset patch # User Christian Urban # Date 1255966273 -7200 # Node ID 544c149005cf892814252b1e1f4edce3a6df3df6 # Parent e73ccbed776ed55db2c659c026dffe08de051407 some slight polishing diff -r e73ccbed776e -r 544c149005cf ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Mon Oct 19 14:10:42 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Mon Oct 19 17:31:13 2009 +0200 @@ -714,9 +714,10 @@ with ML-antiquotations, often just called antiquotations.\footnote{There are two kinds of antiquotations in Isabelle, which have very different purposes and infrastructures. The first kind, described in this section, are - \emph{ML-antiquotations}. They are used to refer to entities (like terms, + \emph{\index*{ML-antiquotations}}. They are used to refer to entities (like terms, types etc) from Isabelle's logic layer inside ML-code. The other kind of - antiquotations are \emph{document} antiquotations. They are used only in the + antiquotations are \emph{document}\index{document antiquotationa} antiquotations. + They are used only in the text parts of Isabelle and their purpose is to print logical entities inside \LaTeX-documents. Document antiquotations are part of the user level and therefore we are not interested in them in this Tutorial, except in Appendix diff -r e73ccbed776e -r 544c149005cf ProgTutorial/General.thy --- a/ProgTutorial/General.thy Mon Oct 19 14:10:42 2009 +0200 +++ b/ProgTutorial/General.thy Mon Oct 19 17:31:13 2009 +0200 @@ -1129,19 +1129,19 @@ proved theorems can be quoted in documents referencing directly their formalisation. This helps tremendously to minimise cut-and-paste errors. However, sometimes the verbatim quoting is not what is wanted or what can be shown to - readers. For such situations Isabelle allows the installation of \emph{theorem - styles}. These are, roughly speaking, functions from terms to terms. The input + readers. For such situations Isabelle allows the installation of \emph{\index*{theorem + styles}}. These are, roughly speaking, functions from terms to terms. The input term stands for the theorem to be presented; the output can be constructed to ones wishes. Let us, for example, assume we want to quote theorems without leading @{text \}-quantifiers. For this we can implement the following function that strips off meta-quantifiers. *} -ML %linenosgray {*fun strip_all_qnt (Const (@{const_name "All"}, _) $ Abs body) = - Term.dest_abs body |> snd |> strip_all_qnt - | strip_all_qnt (Const (@{const_name "Trueprop"}, _) $ t) = - strip_all_qnt t - | strip_all_qnt t = t*} +ML %linenosgray {*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = + Term.dest_abs body |> snd |> strip_allq + | strip_allq (Const (@{const_name "Trueprop"}, _) $ t) = + strip_allq t + | strip_allq t = t*} text {* We use in Line 2 the function @{ML_ind dest_abs in Term} for deconstructing abstractions, @@ -1149,11 +1149,11 @@ a pair consisting of the variable and the body of the abstraction. We are only interested in the body, which we feed into the recursive call. In Line 3 and 4, we also have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can - install this function as the theorem style named @{text "my_strip_all_qnt"}. + install this function as the theorem style named @{text "my_strip_allq"}. *} setup %gray {* - Term_Style.setup "my_strip_all_qnt" (Scan.succeed (K strip_all_qnt)) + Term_Style.setup "my_strip_allq" (Scan.succeed (K strip_allq)) *} text {* @@ -1172,12 +1172,12 @@ @{text ">"}~@{thm style_test} \end{isabelle} - as expected. But with the theorem style @{text "@{thm (my_strip_all_qnt) \}"} + as expected. But with the theorem style @{text "@{thm (my_strip_allq) \}"} we obtain \begin{isabelle} - @{text "@{thm (my_strip_all_qnt) style_test}"}\\ - @{text ">"}~@{thm (my_strip_all_qnt) style_test}\\ + @{text "@{thm (my_strip_allq) style_test}"}\\ + @{text ">"}~@{thm (my_strip_allq) style_test}\\ \end{isabelle} without the leading quantifiers. We can improve this theorem style by explicitly @@ -1186,12 +1186,12 @@ and uses them as name in the outermost abstractions. *} -ML {*fun rename_all [] t = t - | rename_all (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = - Const (@{const_name "All"}, U) $ Abs (x, T, rename_all xs t) - | rename_all xs (Const (@{const_name "Trueprop"}, U) $ t) = - rename_all xs t - | rename_all _ t = t*} +ML {*fun rename_allq [] t = t + | rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = + Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t) + | rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) = + rename_allq xs t + | rename_allq _ t = t*} text {* We can now install a the modified theorem style as follows @@ -1200,18 +1200,21 @@ setup %gray {* let val parser = Scan.repeat Args.name - fun action xs = K (rename_all xs #> strip_all_qnt) + fun action xs = K (rename_allq xs #> strip_allq) in - Term_Style.setup "my_strip_all_qnt2" (parser >> action) + Term_Style.setup "my_strip_allq2" (parser >> action) end *} text {* - We can now suggest, for example, two variables for stripping - off the @{text \}-quantifiers, namely: + The parser reads a list of names. In the function @{ML_text action} we first + call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq} + on the resulting term. We can now suggest, for example, two variables for + stripping off the first two @{text \}-quantifiers. + \begin{isabelle} - @{text "@{thm (my_strip_all_qnt2 x' x'') style_test}"}\\ - @{text ">"}~@{thm (my_strip_all_qnt2 x' x'') style_test} + @{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\ + @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test} \end{isabelle} Such theorem styles allow one to print out theorems in documents formatted to diff -r e73ccbed776e -r 544c149005cf progtutorial.pdf Binary file progtutorial.pdf has changed