# HG changeset patch # User Christian Urban # Date 1340034398 -3600 # Node ID 0ed6f49277c4dd54da19eea197ff684847c375b1 # Parent 9728b0432fb277b609d89f86c2de2c0506d9c8ba updated diff -r 9728b0432fb2 -r 0ed6f49277c4 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Mon Jun 18 15:04:34 2012 +0100 +++ b/ProgTutorial/Intro.thy Mon Jun 18 16:46:38 2012 +0100 @@ -293,9 +293,6 @@ \item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing} about parsing. - \item {\bf Dmitriy Traytel} suggested to use the ML-antiquotation - @{text "command_spec"} in section~\ref{sec:newcommand}, which simplified the code. - \item {\bf Armin Heller} helped with recipe \ref{rec:sat}. \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' @@ -310,6 +307,9 @@ \item {\bf Christian Sternagel} proofread the tutorial and made many improvemets to the text. + + \item {\bf Dmitriy Traytel} suggested to use the ML-antiquotation + @{text "command_spec"} in section~\ref{sec:newcommand}, which simplified the code. \end{itemize} Please let me know of any omissions. Responsibility for any remaining diff -r 9728b0432fb2 -r 0ed6f49277c4 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Mon Jun 18 15:04:34 2012 +0100 +++ b/ProgTutorial/Parsing.thy Mon Jun 18 16:46:38 2012 +0100 @@ -980,21 +980,21 @@ the name for the command, a kind indicator, a short description and a parser producing a local theory transition (explained later). For the name and the kind, you can use the ML-antiquotation @{text "@{command_spec ...}"}. - After this, you can write in your theory + You can now write in your theory *} foobar text {* - but of course you will not see ``anything''. - Remember that this only works in jEdit. In order to enable also Proof-General - recognise this command, a keyword file needs to be generated (see next - section). + but of course you will not see anything since \isacommand{foobar} is + not intended to do anything. Remember, however, that this only + works in jEdit. In order to enable also Proof-General recognise this + command, a keyword file needs to be generated (see next section). - At the moment the command \isacommand{foobar} is not very useful. Let us - refine it a bit next by letting it take a proposition as argument and - printing this proposition inside the tracing buffer. We announce the - command in the theory header as + As it stands, the command \isacommand{foobar} is not very useful. Let + us refine it a bit next by letting it take a proposition as argument + and printing this proposition inside the tracing buffer. We announce + the command \isacommand{foobar\_trace} in the theory header as \begin{graybox} \isacommand{keywords} @{text [quotes] "foobar_trace"} @{text "::"} @{text "thy_decl"} @@ -1091,31 +1091,33 @@ text {* The last command we describe here is - \isacommand{foobar\_proof}. Like \isacommand{lemma}, its purpose is + \isacommand{foobar\_proof}. Like \isacommand{foobar\_goal}, its purpose is to take a proposition and open a corresponding proof-state that allows us to give a proof for it. However, unlike - \isacommand{lemma}, the proposition will be given as a + \isacommand{foobar\_goal}, the proposition will be given as a ML-value. Such a command is quite useful during development when you generate a goal on the ML-level and want to see - whether it is provable. In addition allow the proved + whether it is provable. In addition we want to allow the proved proposition to have a name that can be referenced later on. - The first problem for this command is to parse some text as - ML-source and then interpret it as an Isabelle term. For the parsing we can - use the function @{ML_ind "ML_source" in Parse} in the structure - @{ML_struct Parse}. For running the ML-interpreter we need the - following scaffolding code. + The first problem for \isacommand{foobar\_proof} is to parse some + text as ML-source and then interpret it as an Isabelle term using + the ML-runtime. For the parsing part, we can use the function + @{ML_ind "ML_source" in Parse} in the structure @{ML_struct + Parse}. For running the ML-interpreter we need the following + scaffolding code. *} ML %grayML{* -structure Result = Proof_Data ( - type T = unit -> term - fun init thy () = error "Result") +structure Result = + Proof_Data (type T = unit -> term + fun init thy () = error "Result") val result_cookie = (Result.get, Result.put, "Result.put") *} text {* - With this in place, we can write the code for \isacommand{foobar\_prove}. + With this in place, we can implement the code for \isacommand{foobar\_prove} + as follows. *} ML %linenosgray{*let @@ -1142,8 +1144,8 @@ and lets the ML-runtime evaluate it using the function @{ML_ind value in Code_Runtime} in the structure @{ML_struct Code_Runtime}. Once the ML-text has been turned into a term, the function @{ML theorem in Proof} opens a corresponding proof-state. This function takes the - function @{ML_text "after_qed"} as argument, whose purpose is to store the theorem, - once it is proven, under the given name @{text "thm_name"}. + function @{text "after_qed"} as argument, whose purpose is to store the theorem + (once it is proven) under the given name @{text "thm_name"}. You can now define a term, for example *} @@ -1159,7 +1161,7 @@ done text {* - Finally we can test whether the lemma has been stored under the given name. + Finally you can test whether the lemma has been stored under the given name. \begin{isabelle} \isacommand{thm}~@{text "test"}\\ @@ -1313,12 +1315,13 @@ @{text "thy_goal"} say, you need to recreate the keyword file. *} + + + text {* {\bf TBD below} - (FIXME: read a name and show how to store theorems; see @{ML_ind note in Local_Theory}) - -*} + *} diff -r 9728b0432fb2 -r 0ed6f49277c4 progtutorial.pdf Binary file progtutorial.pdf has changed