# HG changeset patch # User Christian Urban # Date 1231951567 0 # Node ID e7519207c2b7adaf9ae4e750ce26e62b1aca7de2 # Parent 5fbeeac2901b1328733b4ff9fe4742e430e037d2 added more to the "new command section" and tuning diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Mon Jan 12 16:49:15 2009 +0000 +++ b/CookBook/FirstSteps.thy Wed Jan 14 16:46:07 2009 +0000 @@ -226,17 +226,17 @@ The antiquotation @{text "@{prop \}"} constructs terms of propositional type, inserting the invisible @{text "Trueprop"}-coercions whenever necessary. - Consider for example + Consider for example the pairs @{ML_response [display] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \) $ Free (\"x\", \), Const (\"Trueprop\", \) $ (Free (\"P\", \) $ Free (\"x\", \)))"} - which inserts the coercion in the second component and + where an coercion is inserted in the second component and @{ML_response [display] "(@{term \"P x \ Q x\"}, @{prop \"P x \ Q x\"})" "(Const (\"==>\", \) $ \ $ \, Const (\"==>\", \) $ \ $ \)"} - which does not (since it is already constructed using the meta-implication). + where it is not (since it is already constructed using the meta-implication). Types can be constructed using the antiquotation @{text "@{typ \}"}. For example @@ -281,36 +281,39 @@ text {* To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} - to both functions: + to both functions. With @{ML make_imp} we obtain the correct term involving + @{term "S"}, @{text "T"} and @{text "@{typ nat}"} @{ML_response [display] "make_imp @{term S} @{term T} @{typ nat}" "Const \ $ Abs (\"x\", Type (\"nat\",[]), Const \ $ (Free (\"S\",\) $ \) $ (Free (\"T\",\) $ \))"} + + With @{ML make_wrong_imp} we obtain an incorrect term involving the @{term "P"} + and @{text "Q"} from the antiquotation. + @{ML_response [display] "make_wrong_imp @{term S} @{term T} @{typ nat}" "Const \ $ Abs (\"x\", \, Const \ $ (Const \ $ (Free (\"P\",\) $ \)) $ (Const \ $ (Free (\"Q\",\) $ \)))"} - As can be seen, in the first case the arguments are correctly used, while the - second generates a term involving the @{term "P"} and @{text "Q"} from the - antiquotation. + One tricky point in constructing terms by hand is to obtain the fully + qualified name for constants. For example the names for @{text "zero"} and + @{text "+"} are more complex than one first expects, namely - One tricky point in constructing terms by hand is to obtain the - fully qualified name for constants. For example the names for @{text "zero"} and - @{text "+"} are more complex than one first expects, namely \begin{center} @{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}. \end{center} - The extra prefixes @{text zero_class} and @{text plus_class} are present because - these constants are defined within type classes; the prefix @{text "HOL"} indicates in - which theory they are defined. Guessing such internal names can sometimes be quite hard. - Therefore Isabelle provides the antiquotation @{text "@{const_name \}"} which does the - expansion automatically, for example: + The extra prefixes @{text zero_class} and @{text plus_class} are present + because these constants are defined within type classes; the prefix @{text + "HOL"} indicates in which theory they are defined. Guessing such internal + names can sometimes be quite hard. Therefore Isabelle provides the + antiquotation @{text "@{const_name \}"} which does the expansion + automatically, for example: @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"} @@ -575,6 +578,11 @@ section {* Theorem Attributes *} +section {* Combinators *} +text {* + @{text I}, @{text K} + +*} end \ No newline at end of file diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/Intro.thy --- a/CookBook/Intro.thy Mon Jan 12 16:49:15 2009 +0000 +++ b/CookBook/Intro.thy Wed Jan 14 16:46:07 2009 +0000 @@ -64,5 +64,12 @@ *} +section {* Conventions *} + +text {* + We use @{text "$"} to indicate a command needs to be run on the Unix-command + line. +*} + end \ No newline at end of file diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Mon Jan 12 16:49:15 2009 +0000 +++ b/CookBook/Parsing.thy Wed Jan 14 16:46:07 2009 +0000 @@ -1,5 +1,5 @@ theory Parsing -imports Base +imports Base begin @@ -556,70 +556,78 @@ section {* New Commands and Creating Keyword Files *} text {* - Often new commands, for example for providing a new definitional principle, - need to be programmed. While this is not difficult to do on the ML-level, + Often new commands, for example for providing new definitional principles, + need to be implemented. While this is not difficult on the ML-level, new commands, in order to be useful, need to be recognised by ProofGeneral. This results in some subtle configuration issues, which we will explain in this section. - Let us start with a ``silly'' command, which we call \isacommand{foo} in what follows. + Let us start with a ``silly'' command, which we call \isacommand{foobar} in what follows. To keep things simple this command does nothing at all. On the ML-level it can be defined as +*} -@{ML [display] -"let - val do_nothing = Scan.succeed (Toplevel.theory (fn x => x)) - val flag = OuterKeyword.thy_decl +ML {* +let + val do_nothing = Scan.succeed (Toplevel.theory I) + val kind = OuterKeyword.thy_decl in - OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing -end"} + OuterSyntax.command "foobar" "description of foobar" kind do_nothing +end +*} +text {* The function @{ML OuterSyntax.command} expects a name for the command, a - short description, a flag (which we will explain later on more thoroughly) and a + short description, a kind indicator (which we will explain later on more thoroughly) and a parser for a top-level transition function (its purpose will also explained later). - While this is everything we have to do on the ML-level, we need - now a keyword file that can be loaded by ProofGeneral. This is to enable ProofGeneral - to recognise \isacommand{foo} as a command. Such a keyword file can be generated with - the command-line + While this is everything we have to do on the ML-level, we need a keyword + file that can be loaded by ProofGeneral. This is to enable ProofGeneral to + recognise \isacommand{foobar} as a command. Such a keyword file can be + generated with the command-line + + + @{text [display] "$ isabelle keywords -k foobar some-log-files"} - @{text [display] "$ isabelle keywords -k foo "} + The option @{text "-k foobar"} indicates which postfix the keyword file will + obtain. In the case above the generated file will be named @{text + "isar-keywords-foobar.el"}. However, this command requires log files to be + present (in order to extract the keywords from them). To generate these log + files, we first package the code above into a separate theory file named + @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the + complete code. - The option @{text "-k foo"} indicates which postfix the keyword file will obtain. In - the case above the generated file will be named @{text "isar-keywords-foo.el"}. This command - requires log files to be present (in order to extract the keywords from them). - To generate these log files, we first package the code above into a separate theory file - named @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the complete code. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{figure}[t] - \begin{boxedminipage}{\textwidth} + \begin{boxedminipage}{\textwidth}\small \isacommand{theory}~@{text Command}\\ \isacommand{imports}~@{text Main}\\ \isacommand{begin}\\ \isacommand{ML}~\isa{\isacharverbatimopen}\\ @{ML "let - val do_nothing = Scan.succeed (Toplevel.theory (fn x => x)) - val flag = OuterKeyword.thy_decl + val do_nothing = Scan.succeed (Toplevel.theory I) + val kind = OuterKeyword.thy_decl in - OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing + OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing end"}\\ \isa{\isacharverbatimclose}\\ \isacommand{end} \end{boxedminipage} \caption{The file @{text "Command.thy"} is necessary for generating a log file. This log file enables Isabelle to generate a keyword file containing - the command \isacommand{foo}.\label{fig:commandtheory}} + the command \isacommand{foobar}.\label{fig:commandtheory}} \end{figure} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - For - our purposes it is sufficient to use the log files for the theories @{text "Pure"}, - @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as the theory @{text "Command.thy"} - containing the new \isacommand{foo}-command. @{text Pure} and @{text HOL} are usually compiled during the - installation of Isabelle. So log files for them are already available. If not, then they - can be conveniently compiled using build-script from the distribution + For our purposes it is sufficient to use the log files for the theories + @{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as + the theory @{text "Command.thy"} containing the new + \isacommand{foobar}-command. @{text Pure} and @{text HOL} are usually + compiled during the installation of Isabelle. So log files for them should be + already available. If not, then they can be conveniently compiled using + build-script from the Isabelle distribution @{text [display] "$ ./build -m \"Pure\" @@ -632,23 +640,23 @@ For the theory @{text "Command.thy"}, we first create a ``managed'' subdirectory with - @{text [display] "$ isabelle mkdir FooCommand"} + @{text [display] "$ isabelle mkdir FoobarCommand"} This creates a directory containing the files @{text [display] "./IsaMakefile -./FooCommand/ROOT.ML -./FooCommand/document -./FooCommand/document/root.tex"} +./FoobarCommand/ROOT.ML +./FoobarCommand/document +./FoobarCommand/document/root.tex"} - We need to copy the file @{text "Command.thy"} into the directory @{text "FooCommand"} + We need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"} and add the line @{text [display] "use_thy \"Command\";"} - to the file @{text "./FooCommand/ROOT.ML"}. We can now compile the theory by just typing + to the file @{text "./FoobarCommand/ROOT.ML"}. We can now compile the theory by just typing @{text [display] "$ isabelle make"} @@ -663,50 +671,139 @@ @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"} - In this directory are the files + on the Unix prompt. This directory should include the files @{text [display] "Pure.gz HOL.gz Pure-ProofGeneral.gz -HOL-FooCommand.gz"} +HOL-FoobarCommand.gz"} - They are used for creating the keyword files with the command + They are the ones we use for creating the keyword files. The corresponding Unix command + is @{text [display] -"$ isabelle keywords -k foo - $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FooCommand.gz}"} +"$ isabelle keywords -k foobar + $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"} - The result is the file @{text "isar-keywords-foo.el"}. This file needs to be - copied to the directory @{text "~/.isabelle/etc"}. To make Isabelle use - this keyword file, we have to start it with the option @{text "-k foo"}, i.e. + The result is the file @{text "isar-keywords-foobar.el"}. It should contain the + string @{text "foobar"} twice (check for example that @{text [quotes] "grep foobar + isar-keywords-foobar.el"} returns something non-empty). This keyword file + needs to be copied into the directory @{text "~/.isabelle/etc"}. To make + Isabelle use this keyword file, we have to start it with the option @{text + "-k foobar"}, i.e. - @{text [display] "isabelle -k foo "} + @{text [display] "$ isabelle -k foobar a-theory-file"} If we now run the original code +*} - @{ML [display] -"let - val do_nothing = Scan.succeed (Toplevel.theory (fn x => x)) - val flag = OuterKeyword.thy_decl +ML {* +let + val do_nothing = Scan.succeed (Toplevel.theory I) + val kind = OuterKeyword.thy_decl in - OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing -end"} + OuterSyntax.command "foobar" "description of foobar" kind do_nothing +end +*} - then we can make use of \isacommand{foo}! Similarly with any other new command. +text {* + then we can make use of \isacommand{foobar}! Similarly with any other new command. In the example above, we built the theories on top of the HOL-logic. If you - target other logics, such as Nominal or ZF, then you need to change the + target other logics, such as Nominal or ZF, then you need to adapt the log files appropriately. + At the moment, \isacommand{foobar} is not very useful. Let us refine it a bit + by taking a proposition as argument and printing this proposition inside + the tracing buffer. + + The crucial part of a command is the function that determines + the behaviour of the command. In the code above we used the the + @{text do_nothing}-function, which because of @{ML Scan.succeed} does not parse + any argument, but immediately returns the simple toplevel function + @{ML "Toplevel.theory I"}. We can replace this code by a function that first + parses a proposition (using the parser @{ML OuterParse.prop}), then prints out + the tracing information and finally does nothing. For this we can write +*} + +ML {* +let + val trace_prop = + OuterParse.prop >> (fn str => (tracing str; (Toplevel.theory I))) + val kind = OuterKeyword.thy_decl +in + OuterSyntax.command "foobar" "traces a proposition" kind trace_prop +end +*} + +text {* + Now we can type for example + + @{ML_response_fake_both [display] "foobar \"True \ False\"" "True \ False"} + + and see the proposition in the tracing buffer. + + Note that so far we used @{ML thy_decl in OuterKeyword} as kind indicator + for the command. This means that the command finishes as soon as the + arguments are processed. Examples of this kind of commands are + \isacommand{definition} and \isacommand{declare}. In other cases, however, + commands are expected to parse some arguments, for example a proposition, + and then ``open up'' a proof in order to prove the proposition (think of + \isacommand{lemma}) or prove some other properties (for example in + \isacommand{function}). To achieve this behaviour we have to use the kind + indicator @{ML thy_goal in OuterKeyword}. + + Below we change \isacommand{foobar} is such a way that an proposition as + argument and then start a proof in order to prove it. Therefore in Line 13 + below, we set the kind indicator to @{ML thy_goal in OuterKeyword}. +*} + +ML %linenumbers {*let + fun set_up_thm str ctxt = + let + val prop = Syntax.read_prop ctxt str + in + Proof.theorem_i NONE (K I) [[(Syntax.read_prop ctxt str,[])]] ctxt + end; + + val prove_prop = OuterParse.prop >> + (fn str => Toplevel.print o + Toplevel.local_theory_to_proof NONE (set_up_thm str)) + + val kind = OuterKeyword.thy_goal +in + OuterSyntax.command "foobar" "proving a proposition" kind prove_prop +end +*} + +text {* + The function @{text set_up_thm} takes a string (the proposition) and a context. + The context is necessary in order to convert the string into a proper proposition + using the function @{ML Syntax.read_prop}. In Line 6 we use the function + @{ML Proof.theorem_i} to start the proof for the proposition. In Lines 9 to + 11 contain the parser for the proposition. + + If we now type @{text "foobar \"True \ True\""}, we obtain the following + proof state: + + @{ML_response_fake_both [display] "foobar \"True \ True\"" +"goal (1 subgoal): +1. True \ True"} + + and we can build the proof + + @{text [display] "foobar \"True \ True\" +apply(rule conjI) +apply(rule TrueI)+ +done"} + + (FIXME What does @{text "Toplevel.theory"}?) + (FIXME Explain @{text "OuterKeyword.thy_decl"} and parser) - *} - - - chapter {* Parsing *} text {* diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/ROOT.ML --- a/CookBook/ROOT.ML Mon Jan 12 16:49:15 2009 +0000 +++ b/CookBook/ROOT.ML Wed Jan 14 16:46:07 2009 +0000 @@ -23,3 +23,4 @@ use_thy "Solutions"; use_thy "Readme"; + diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/Recipes/Config.thy --- a/CookBook/Recipes/Config.thy Mon Jan 12 16:49:15 2009 +0000 +++ b/CookBook/Recipes/Config.thy Wed Jan 14 16:46:07 2009 +0000 @@ -75,16 +75,14 @@ Config.get ctxt ival end" "4"} -\begin{readmore} + \begin{readmore} For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}. -\end{readmore} + \end{readmore} -*} - - -text {* - - Note: Avoid to use references for this purpose! + There are many good reasons to control parameters in this way. One is + that it avoid global references, which cause many headaches with the + multithreaded execution of Isabelle. + *} end \ No newline at end of file diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/Recipes/NamedThms.thy --- a/CookBook/Recipes/NamedThms.thy Mon Jan 12 16:49:15 2009 +0000 +++ b/CookBook/Recipes/NamedThms.thy Wed Jan 14 16:46:07 2009 +0000 @@ -22,13 +22,14 @@ val name = "foo" val description = "Rules for foo"); *} -(*<*)setup FooRules.setup(*>*) text {* and the command +*} - @{text [display] "setup FooRules.setup"} +setup {* FooRules.setup *} +text {* This code declares a context data slot where the theorems are stored, an attribute @{text foo} (with the usual @{text add} and @{text del} options for adding and deleting theorems) and an internal ML interface to retrieve and diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/Recipes/StoringData.thy --- a/CookBook/Recipes/StoringData.thy Mon Jan 12 16:49:15 2009 +0000 +++ b/CookBook/Recipes/StoringData.thy Wed Jan 14 16:46:07 2009 +0000 @@ -7,7 +7,7 @@ text {* {\bf Problem:} - Your tool needs to keep complex data.\smallskip + Your tool needs to manage data.\smallskip {\bf Solution:} This can be achieved using a generic data slot.\smallskip @@ -16,15 +16,15 @@ *} -ML {* local +ML {* +local structure Data = GenericDataFun -( - type T = int Symtab.table - val empty = Symtab.empty - val extend = I - fun merge _ = Symtab.merge (K true) -) + ( type T = int Symtab.table + val empty = Symtab.empty + val extend = I + fun merge _ = Symtab.merge (K true) + ) in @@ -36,7 +36,12 @@ setup {* Context.theory_map (update "foo" 1) *} -ML {* lookup (Context.Proof @{context}) "foo" *} +text {* + + @{ML_response [display] "lookup (Context.Proof @{context}) \"foo\"" "SOME 1"} + + +*} text {* alternatives: TheoryDataFun, ProofDataFun diff -r 5fbeeac2901b -r e7519207c2b7 CookBook/Recipes/TimeLimit.thy --- a/CookBook/Recipes/TimeLimit.thy Mon Jan 12 16:49:15 2009 +0000 +++ b/CookBook/Recipes/TimeLimit.thy Wed Jan 14 16:46:07 2009 +0000 @@ -11,7 +11,7 @@ {\bf Solution:} This can be achieved using the function @{ML timeLimit in TimeLimit}.\smallskip - Assume the following infamous function: + Assume you defined the Ackermann function: *} @@ -27,7 +27,7 @@ @{ML_response_fake [display] "ackermann (4, 12)" "\"} - takes a bit of time to finish. To avoid this, the call can be encapsulated + takes a bit of time before it finishes. To avoid this, the call can be encapsulated in a time limit of five seconds. For this you have to write: @{ML_response [display] diff -r 5fbeeac2901b -r e7519207c2b7 cookbook.pdf Binary file cookbook.pdf has changed