# HG changeset patch # User Christian Urban # Date 1234008302 0 # Node ID 5e309df5855798e9b2017ed6977477bd055bba31 # Parent 123401a5c8e9befef2c9f30f5206cab477b35f45 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution diff -r 123401a5c8e9 -r 5e309df58557 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Fri Feb 06 06:19:52 2009 +0000 +++ b/CookBook/FirstSteps.thy Sat Feb 07 12:05:02 2009 +0000 @@ -37,17 +37,18 @@ \end{graybox} \end{isabelle} - Like normal Isabelle proof scripts, - \isacommand{ML}-commands can be evaluated by using the advance and undo buttons of - your Isabelle environment. The code inside the \isacommand{ML}-command - can also contain value and function bindings, and even those can be - undone when the proof script is retracted. As mentioned earlier, we will - drop the \isacommand{ML}~@{text "\ \ \"} - scaffolding whenever we show code. + Like normal Isabelle proof scripts, \isacommand{ML}-commands can be + evaluated by using the advance and undo buttons of your Isabelle + environment. The code inside the \isacommand{ML}-command can also contain + value and function bindings, and even those can be undone when the proof + script is retracted. As mentioned earlier, we will drop the + \isacommand{ML}~@{text "\ \ \"} scaffolding whenever we + show code. The lines prefixed with @{text ">"} are not part of the + code, rather they indicate what the response is when the code is evaluated. - Once a portion of code is relatively stable, one usually wants to - export it to a separate ML-file. Such files can then be included in a - theory by using the \isacommand{uses}-command in the header of the theory, like: + Once a portion of code is relatively stable, you usually want to export it + to a separate ML-file. Such files can then be included in a theory by using + the \isacommand{uses}-command in the header of the theory, like: \begin{center} \begin{tabular}{@ {}l} @@ -115,6 +116,8 @@ @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""} + See leter on in Section~\ref{sec:printing} for information about printing + out data of type @{ML_type term}, @{ML_type cterm} and @{ML_type thm}. *} @@ -277,13 +280,12 @@ text {* While antiquotations are very convenient for constructing terms, they can - only construct fixed terms (remember they are ``linked'' at - compile-time). See Recipe~\ref{rec:external} on Page~\pageref{rec:external} - for a function that pattern-matches over terms and where the patterns are - constructed using antiquotations. However, one often needs to construct - terms dynamically. For example, a function that returns the implication - @{text "\(x::\). P x \ Q x"} taking @{term P}, @{term Q} and the type @{term - "\"} as arguments can only be written as: + only construct fixed terms (remember they are ``linked'' at compile-time). + However, you often need to construct terms dynamically. For example, a + function that returns the implication @{text "\(x::\). P x \ Q x"} taking + @{term P}, @{term Q} and the type @{term "\"} as arguments can only be + written as: + *} ML{*fun make_imp P Q tau = @@ -294,7 +296,7 @@ end *} text {* - The reason is that one cannot pass the arguments @{term P}, @{term Q} and + The reason is that you cannot pass the arguments @{term P}, @{term Q} and @{term "tau"} into an antiquotation. For example the following does \emph{not} work: *} @@ -303,7 +305,7 @@ text {* To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} to both functions. With @{ML make_imp} we obtain the intended term involving - @{term "S"}, @{text "T"} and @{text "@{typ nat}"} + the given arguments @{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}" "Const \ $ @@ -342,8 +344,8 @@ (FIXME: Is it useful to explain @{text "@{const_syntax}"}?) - Similarly, one can construct types manually. For example the function returning - a function type is as follows: + Similarly, you occasionally need to construct types manually. For example + the function returning a function type is as follows: *} @@ -357,7 +359,7 @@ \begin{readmore} There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and - @{ML_file "HOL/hologic.ML"} that make such manual constructions of terms + @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms and types easier.\end{readmore} Have a look at these files and try to solve the following two exercises: @@ -403,8 +405,8 @@ text {* - We can freely construct and manipulate terms, since they are just - arbitrary unchecked trees. However, we eventually want to see if a + You can freely construct and manipulate terms, since they are just + arbitrary unchecked trees. However, you eventually want to see if a term is well-formed, or type-checks, relative to a theory. Type-checking is done via the function @{ML cterm_of}, which converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term. @@ -415,11 +417,11 @@ Type-checking is always relative to a theory context. For now we use the @{ML "@{theory}"} antiquotation to get hold of the current theory. - For example we can write + For example you can write: @{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"} - This can also be wirtten with an antiquotation + This can also be wirtten with an antiquotation: @{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"} @@ -428,8 +430,7 @@ @{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \"} yields an error (since the term is not typable). A slightly more elaborate - example that type-checks is - + example that type-checks is: @{ML_response_fake [display,gray] "let @@ -503,6 +504,9 @@ } \] + However, while we obtained a theorem as result, this theorem is not + yet stored in Isabelle's theorem database. So it cannot be referenced later + on. How to store theorems will be explained in the next section. \begin{readmore} For the functions @{text "assume"}, @{text "forall_elim"} etc @@ -519,8 +523,8 @@ section {* Printing Terms, CTerms and Theorems\label{sec:printing} *} text {* - You will occationally feel the need to inspect terms, cterms or theorems during - development. Isabelle contains elaborate pretty-printing functions for that, but + During development, you will occationally feel the need to inspect terms, cterms + or theorems. Isabelle contains elaborate pretty-printing functions for that, but for quick-and-dirty solutions they are way too unwieldy. A simple way to transform a term into a string is to use the function @{ML Syntax.string_of_term}. @@ -542,12 +546,12 @@ Syntax.string_of_term ctxt (term_of t)*} text {* - If there are more than one @{ML_type cterm} to be printed, you can use the function - @{ML commas} to conveniently separate them. + If there are more than one @{ML_type cterm}s to be printed, you can use the + function @{ML commas} to separate them. *} ML{*fun str_of_cterms ctxt ts = - commas (map (str_of_cterm ctxt) ts)*} + commas (map (str_of_cterm ctxt) ts)*} text {* The easiest way to get the string of a theorem is to transform it @@ -722,7 +726,7 @@ The combinators @{ML "|>>"} and @{ML "||>"} are defined for functions manipulating pairs. The first applies the function to - the first component of the pair, defined as: + the first component of the pair, defined as *} ML{*fun (x, y) |>> f = (f x, y)*} diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Intro.thy --- a/CookBook/Intro.thy Fri Feb 06 06:19:52 2009 +0000 +++ b/CookBook/Intro.thy Sat Feb 07 12:05:02 2009 +0000 @@ -96,7 +96,7 @@ The usual user-level commands of Isabelle are written in bold, for example \isacommand{lemma}, \isacommand{foobar} and so on. We use @{text "$"} to indicate that a command needs to be run - in the Unix-shell, for example + in a Unix-shell, for example @{text [display] "$ ls -la"} @@ -104,7 +104,7 @@ italic and highlighted as follows: \begin{readmore} - Further information or pointer to file. + Further information or pointers to files. \end{readmore} *} diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Package/Ind_Examples.thy --- a/CookBook/Package/Ind_Examples.thy Fri Feb 06 06:19:52 2009 +0000 +++ b/CookBook/Package/Ind_Examples.thy Sat Feb 07 12:05:02 2009 +0000 @@ -128,12 +128,15 @@ apply (unfold trcl_def) apply (rule allI impI)+ proof - - case goal1 + case (goal1 P) + have g1: "R x y" by fact + have g2: "\P. (\x. P x x) \ (\x y z. R x y \ P y z \ P x z) \ P y z" by fact + have g3: "\x. P x x" by fact + have g4: "\x y z. R x y \ P y z \ P x z" by fact show ?case - apply (rule goal1(4) [rule_format]) - apply (rule goal1(1)) - apply (rule goal1(2) [THEN spec [where x=P], THEN mp, THEN mp, - OF goal1(3-4)]) + apply (rule g4 [rule_format]) + apply (rule g1) + apply (rule g2 [THEN spec [where x=P], THEN mp, THEN mp, OF g3, OF g4]) done qed diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Package/Ind_Interface.thy --- a/CookBook/Package/Ind_Interface.thy Fri Feb 06 06:19:52 2009 +0000 +++ b/CookBook/Package/Ind_Interface.thy Sat Feb 07 12:05:02 2009 +0000 @@ -250,11 +250,6 @@ thm rel.accpartI' thm rel.accpart'.induct -ML{*val (result, lthy) = SimpleInductivePackage.add_inductive - [(Binding.name "trcl'", NONE, NoSyn)] [(Binding.name "r", SOME "'a \ 'a \ bool", NoSyn)] - [((Binding.name "base", []), "\x. trcl' r x x"), ((Binding.name "step", []), "\x y z. trcl' r x y \ r y z \ trcl' r x z")] - (TheoryTarget.init NONE @{theory}) -*} (*>*) text {* @@ -460,11 +455,11 @@ {\it The whole parser for our command has type - @{ML_text [display] "OuterLex.token list -> + @{text [display] "OuterLex.token list -> (Toplevel.transition -> Toplevel.transition) * OuterLex.token list"} - which is abbreviated by @{ML_text OuterSyntax.parser_fn}. The new command can be added + which is abbreviated by @{text OuterSyntax.parser_fn}. The new command can be added to the system via the function - @{ML_text [display] "OuterSyntax.command : + @{text [display] "OuterSyntax.command : string -> string -> OuterKeyword.T -> OuterSyntax.parser_fn -> unit"} which imperatively updates the parser table behind the scenes. } diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Package/simple_inductive_package.ML --- a/CookBook/Package/simple_inductive_package.ML Fri Feb 06 06:19:52 2009 +0000 +++ b/CookBook/Package/simple_inductive_package.ML Sat Feb 07 12:05:02 2009 +0000 @@ -9,14 +9,22 @@ val add_inductive: (Binding.binding * string option * mixfix) list -> (*{predicates}*) (Binding.binding * string option * mixfix) list -> (*{parameters}*) - (Attrib.binding * string) list -> (*{rules}*) - local_theory -> (thm list * thm list) * local_theory + (Attrib.binding * string list) list list -> (*{rules}*) + local_theory -> local_theory end; (* @end *) structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE = struct +fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P + +fun inst_spec ct = Drule.instantiate' + [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}; + +val all_elims = fold (fn ct => fn th => th RS inst_spec ct); +val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp}); + fun add_inductive_i preds_syn params intrs lthy = let val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params; @@ -29,8 +37,6 @@ val intrs' = map (ObjectLogic.atomize_term (ProofContext.theory_of lthy) o snd) intrs; - fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P; - val (defs, lthy1) = fold_map (fn ((((R, _), syn), pred), Ts) => let val zs = map Free (Variable.variant_frees lthy intrs' (map (pair "z") Ts)) @@ -53,9 +59,6 @@ val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; val intrs'' = map (subst_free (preds ~~ Ps) o snd) intrs; - fun inst_spec ct = Drule.instantiate' - [SOME (ctyp_of_term ct)] [NONE, SOME ct] spec; - fun prove_indrule ((R, P), Ts) = let val (znames, lthy4) = @@ -80,9 +83,6 @@ (* proving the introduction rules *) (* @chunk intro_rules *) - val all_elims = fold (fn ct => fn th => th RS inst_spec ct); - val imp_elims = fold (fn th => fn th' => [th', th] MRS mp); - fun prove_intr (i, (_, r)) = Goal.prove lthy2 [] [] r (fn {prems, context = ctxt} => EVERY @@ -136,36 +136,39 @@ end; (* @chunk add_inductive *) -fun add_inductive preds_syn params_syn intro_srcs lthy = - let - val ((vars, specs), _) = Specification.read_specification - (preds_syn @ params_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs) - lthy; - val (preds_syn', params_syn') = chop (length preds_syn) vars; - val intrs = map (apsnd the_single) specs - in - add_inductive_i preds_syn' (map fst params_syn') intrs lthy - end; +fun add_inductive preds params specs lthy = + let + val ((vars, specs'), _) = Specification.read_specification (preds @ params) specs lthy; + val (preds', params') = chop (length preds) vars; + val specs'' = map (apsnd the_single) specs' + val params'' = map fst params' + in + snd (add_inductive_i preds' params'' specs'' lthy) + end; (* @end *) (* outer syntax *) +(* @chunk syntax *) +val parser = + OuterParse.opt_target -- + OuterParse.fixes -- + OuterParse.for_fixes -- + Scan.optional + (OuterParse.$$$ "where" |-- + OuterParse.!!! + (OuterParse.enum1 "|" + ((SpecParse.opt_thm_name ":" -- + (OuterParse.prop >> single)) >> single))) [] -(* @chunk syntax *) -local structure P = OuterParse and K = OuterKeyword in val ind_decl = - P.opt_target -- - P.fixes -- P.for_fixes -- - Scan.optional (P.$$$ "where" |-- - P.!!! (P.enum1 "|" (SpecParse.opt_thm_name ":" -- P.prop))) [] >> - (fn (((loc, preds), params), specs) => - Toplevel.local_theory loc (add_inductive preds params specs #> snd)); + parser >> + (fn (((loc, preds), params), specs) => + Toplevel.local_theory loc (add_inductive preds params specs)); val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" - K.thy_decl ind_decl; - -end; + OuterKeyword.thy_decl ind_decl; (* @end *) end; diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Parsing.thy --- a/CookBook/Parsing.thy Fri Feb 06 06:19:52 2009 +0000 +++ b/CookBook/Parsing.thy Sat Feb 07 12:05:02 2009 +0000 @@ -86,14 +86,14 @@ Two parser can be connected in sequence by using the function @{ML "(op --)"}. For example parsing @{text "h"}, @{text "e"} and @{text "l"} in this - sequence can be achieved by + sequence you can achieve by: @{ML_response [display,gray] "(($$ \"h\") -- ($$ \"e\") -- ($$ \"l\")) (explode \"hello\")" "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"} Note how the result of consumed strings builds up on the left as nested pairs. - If, as in the previous example, one wants to parse a particular string, + If, as in the previous example, you want to parse a particular string, then one should use the function @{ML Scan.this_string}: @{ML_response [display,gray] "Scan.this_string \"hell\" (explode \"hello\")" @@ -102,7 +102,7 @@ Parsers that explore alternatives can be constructed using the function @{ML "(op ||)"}. For example, the parser @{ML "(p || q)" for p q} returns the result of @{text "p"}, in case it succeeds, otherwise it returns the - result of @{text "q"}. For example + result of @{text "q"}. For example: @{ML_response [display,gray] @@ -117,7 +117,7 @@ The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing function for parsers, except that they discard the item being parsed by the first (respectively second) - parser. For example + parser. For example: @{ML_response [display,gray] "let @@ -156,24 +156,25 @@ end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"} The function @{ML "(op !!)"} helps to produce appropriate error messages - during parsing. For example if one wants to parse that @{text p} is immediately + during parsing. For example if you want to parse that @{text p} is immediately followed by @{text q}, or start a completely different parser @{text r}, - one might write + you might write @{ML [display,gray] "(p -- q) || r" for p q r} - However, this parser is problematic for producing an appropriate error message, in case - the parsing of @{ML "(p -- q)" for p q} fails. Because in that case one loses the information - that @{text p} should be followed by @{text q}. To see this consider the case in - which @{text p} - is present in the input, but not @{text q}. That means @{ML "(p -- q)" for p q} will fail - and the - alternative parser @{text r} will be tried. However in many circumstance this will be the wrong - parser for the input ``p-followed-by-q'' and therefore will also fail. The error message is then - caused by the - failure of @{text r}, not by the absence of @{text q} in the input. This kind of situation - can be avoided when using the function @{ML "(op !!)"}. This function aborts the whole process of - parsing in case of a failure and prints an error message. For example if we invoke the parser + However, this parser is problematic for producing an appropriate error + message, in case the parsing of @{ML "(p -- q)" for p q} fails. Because in + that case you lose the information that @{text p} should be followed by + @{text q}. To see this consider the case in which @{text p} is present in + the input, but not @{text q}. That means @{ML "(p -- q)" for p q} will fail + and the alternative parser @{text r} will be tried. However in many + circumstance this will be the wrong parser for the input ``p-followed-by-q'' + and therefore will also fail. The error message is then caused by the + failure of @{text r}, not by the absence of @{text q} in the input. This + kind of situation can be avoided when using the function @{ML "(op + !!)"}. This function aborts the whole process of parsing in case of a + failure and prints an error message. For example if you invoke the parser + @{ML [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\"))"} @@ -183,24 +184,24 @@ "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"} - but if we invoke it on @{text [quotes] "world"} + but if you invoke it on @{text [quotes] "world"} @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")" "Exception ABORT raised"} then the parsing aborts and the error message @{text "foo"} is printed out. In order to see the error message, we need to prefix the parser with the function - @{ML "Scan.error"}. For example + @{ML "Scan.error"}. For example: @{ML_response_fake [display,gray] "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))" "Exception Error \"foo\" raised"} This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"} - (FIXME: give reference to later place). + (see Section~\ref{sec:newcommand} which explains this function in more detail). - Let us now return to our example of parsing @{ML "(p -- q) || r" for p q r}. If we want - to generate the correct error message for p-followed-by-q, then - we have to write: + Let us now return to our example of parsing @{ML "(p -- q) || r" for p q + r}. If you want to generate the correct error message for p-followed-by-q, + then you have to write: *} ML{*fun p_followed_by_q p q r = @@ -226,7 +227,7 @@ yields the expected parsing. The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as - often as it succeeds. For example + often as it succeeds. For example: @{ML_response [display,gray] "Scan.repeat ($$ \"h\") (explode \"hhhhello\")" "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"} @@ -236,15 +237,15 @@ succeeds at least once. Also note that the parser would have aborted with the exception @{text MORE}, if - we had run it only on just @{text [quotes] "hhhh"}. This can be avoided by using + you had run it only on just @{text [quotes] "hhhh"}. This can be avoided by using the wrapper @{ML Scan.finite} and the ``stopper-token'' @{ML Symbol.stopper}. With - them we can write + them you can write: @{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (explode \"hhhh\")" "([\"h\", \"h\", \"h\", \"h\"], [])"} @{ML Symbol.stopper} is the ``end-of-input'' indicator for parsing strings; - other stoppers need to be used when parsing token, for example. However, this kind of + other stoppers need to be used when parsing tokens, for example. However, this kind of manually wrapping is often already done by the surrounding infrastructure. The function @{ML Scan.repeat} can be used with @{ML Scan.one} to read any @@ -291,14 +292,14 @@ "(([\"f\", \"o\", \"o\", \"o\", \"o\", \"o\"], []), ([\"f\", \"o\", \"o\"], [\"*\", \"o\", \"o\", \"o\"]))"} - After parsing is done, one nearly always wants to apply a function on the parsed + After parsing is done, you nearly always want to apply a function on the parsed items. To do this the function @{ML "(p >> f)" for p f} can be employed, which runs first the parser @{text p} and upon successful completion applies the function @{text f} to the result. For example @{ML_response [display,gray] "let - fun double (x,y) = (x^x,y^y) + fun double (x,y) = (x ^ x, y ^ y) in (($$ \"h\") -- ($$ \"e\") >> double) (explode \"hello\") end" @@ -323,7 +324,7 @@ inside @{text "(*\*)"} is replaced by a the same comment but enclosed inside @{text "(**\**)"} in the output string. To enclose a string, you can use the function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML - "s1^s^s2" for s1 s2 s}. + "s1 ^ s ^ s2" for s1 s2 s}. \end{exercise} @@ -341,11 +342,12 @@ section {* Parsing Theory Syntax *} text {* - Most of the time, however, Isabelle developers have to deal with parsing tokens, not strings. - This is because the parsers for the theory syntax, as well as the parsers for the - argument syntax of proof methods and attributes use the type - @{ML_type OuterLex.token} (which is identical to the type @{ML_type OuterParse.token}). - There are also parsers for ML-expressions and ML-files. + Most of the time, however, Isabelle developers have to deal with parsing + tokens, not strings. This is because the parsers for the theory syntax, as + well as the parsers for the argument syntax of proof methods and attributes + use the type @{ML_type OuterLex.token} (which is identical to the type + @{ML_type OuterParse.token}). There are also parsers for ML-expressions and + ML-files, which can be sometimes handy. \begin{readmore} The parser functions for the theory syntax are contained in the structure @@ -360,11 +362,10 @@ *} text {* - For the examples below, we can generate a token list out of a string using - the function @{ML "OuterSyntax.scan"}, which we give below @{ML - "Position.none"} as argument since, at the moment, we are not interested in - generating precise error messages. The following code - + With the examples below, you can generate a token list out of a string using + the function @{ML "OuterSyntax.scan"}, which is given @{ML "Position.none"} + as argument since, at the moment, we are not interested in generating + precise error messages. The following code @{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\"" "[Token (\,(Ident, \"hello\"),\), @@ -374,13 +375,12 @@ produces three tokens where the first and the last are identifiers, since @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any other syntactic category.\footnote{Note that because of a possible a bug in - the PolyML runtime system the result is printed as @{text "?"}, instead of + the PolyML runtime system the result is printed as @{text [quotes] "?"}, instead of the tokens.} The second indicates a space. Many parsing functions later on will require spaces, comments and the like to have already been filtered out. So from now on we are going to use the - functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example - + functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example: @{ML_response_fake [display,gray] "let @@ -390,7 +390,7 @@ end" "[Token (\,(Ident, \"hello\"), \), Token (\,(Ident, \"world\"), \)]"} - For convenience we define the function + For convenience we define the function: *} @@ -399,7 +399,7 @@ text {* - If we parse + If you now parse @{ML_response_fake [display,gray] "filtered_input \"inductive | for\"" @@ -407,7 +407,7 @@ Token (\,(Keyword, \"|\"),\), Token (\,(Keyword, \"for\"),\)]"} - we obtain a list consisting of only a command and two keyword tokens. + you obtain a list consisting of only a command and two keyword tokens. If you want to see which keywords and commands are currently known, type in the following code (you might have to adjust the @{ML print_depth} in order to see the complete list): @@ -420,7 +420,7 @@ end" "([\"}\",\"{\",\],[\"\\",\"\\",\])"} - Now the parser @{ML "OuterParse.$$$"} parses a single keyword. For example + The parser @{ML "OuterParse.$$$"} parses a single keyword. For example: @{ML_response [display,gray] "let @@ -431,7 +431,7 @@ end" "((\"where\",\),(\"|\",\))"} - Like before, we can sequentially connect parsers with @{ML "(op --)"}. For example + Like before, you can sequentially connect parsers with @{ML "(op --)"}. For example: @{ML_response [display,gray] "let @@ -443,7 +443,7 @@ The parser @{ML "OuterParse.enum s p" for s p} parses a possibly empty list of items recognised by the parser @{text p}, where the items being parsed - are separated by the string @{text s}. For example + are separated by the string @{text s}. For example: @{ML_response [display,gray] "let @@ -454,12 +454,12 @@ "([\"in\",\"in\",\"in\"],[\])"} @{ML "OuterParse.enum1"} works similarly, except that the parsed list must - be non-empty. Note that we had to add a string @{text [quotes] "foo"} at the end - of the parsed string, otherwise the parser would have consumed all tokens - and then failed with the exception @{text "MORE"}. Like in the previous - section, we can avoid this exception using the wrapper @{ML + be non-empty. Note that we had to add a string @{text [quotes] "foo"} at the + end of the parsed string, otherwise the parser would have consumed all + tokens and then failed with the exception @{text "MORE"}. Like in the + previous section, we can avoid this exception using the wrapper @{ML Scan.finite}. This time, however, we have to use the ``stopper-token'' @{ML - OuterLex.stopper}. We can write + OuterLex.stopper}. We can write: @{ML_response [display,gray] "let @@ -528,9 +528,9 @@ section {* Parsing Specifications *} text {* - There are a number of special purpose parsers that help for parsing specifications. - For example the function @{ML OuterParse.target} reads a target in order to indicate - a locale. + There are a number of special purpose parsers that help with parsing specifications + of functions, inductive definitions and so on. For example the function + @{ML OuterParse.target} reads a target in order to indicate a locale. @{ML_response [display,gray] "let @@ -539,12 +539,13 @@ parse OuterParse.target input end" "(\"test\",[])"} - The function @{ML OuterParse.opt_target} makes this parser ``optional''. + The function @{ML OuterParse.opt_target} makes this parser ``optional'', that + is wrapping the result into an option type and returning @{ML NONE} if no + target is present. The function @{ML OuterParse.fixes} reads a list of constants - which can include a type annotation and a syntax translation. - The list needs to be separated by \isacommand{and}. - + that can include type annotations and syntax translations. + The list is separated by \isacommand{and}. For example: *} text {* @@ -560,14 +561,28 @@ (bar, SOME \, NoSyn), (blonk, NONE, NoSyn)],[])"} - The types of the constants is stored in the @{ML SOME}s. - We need to write @{text "\\\"int \ bool\\\""} to properly - escape the type. + Whenever types are given, then they are stored in the @{ML SOME}s. + Note that we had to write @{text "\\\"int \ bool\\\""} to properly escape + the double quotes in the compound type. @{ML OuterParse.for_fixes} is an ``optional'' that prefixes @{ML OuterParse.fixes} with the comman \isacommand{for}. + (FIXME give an example and explain more) + +@{ML_response [display,gray] +"let + val input = filtered_input + \"for foo::\\\"int \ bool\\\" (\\\"FOO\\\" [100] 100) and bar::nat and blonk\" +in + parse OuterParse.for_fixes input +end" +"([(foo, SOME \, Mixfix (\"FOO\",[100],100)), + (bar, SOME \, NoSyn), + (blonk, NONE, NoSyn)],[])"} + *} + ML{*let val input = filtered_input "test_lemma[intro,foo,elim,dest!,bar]:" in @@ -614,7 +629,7 @@ and a list of rules where each rule has optionally a name and an attribute. *} -section {* New Commands and Keyword Files *} +section {* New Commands and Keyword Files\label{sec:newcommand} *} text {* Often new commands, for example for providing new definitional principles, @@ -625,7 +640,7 @@ To keep things simple, let us start with a ``silly'' command that does nothing at all. We shall name this command \isacommand{foobar}. On the ML-level it can be - defined as + defined as: *} ML{*let @@ -688,23 +703,22 @@ @{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 with the help of the build-script from the Isabelle - distribution - + distribution. @{text [display] "$ ./build -m \"Pure\" $ ./build -m \"HOL\""} - The @{text "Pure-ProofGeneral"} theory needs to be compiled with + The @{text "Pure-ProofGeneral"} theory needs to be compiled with: @{text [display] "$ ./build -m \"Pure-ProofGeneral\" \"Pure\""} For the theory @{text "Command.thy"}, you first need to create a ``managed'' subdirectory - with + with: @{text [display] "$ isabelle mkdir FoobarCommand"} - This generates a directory containing the files + This generates a directory containing the files: @{text [display] "./IsaMakefile @@ -718,7 +732,7 @@ @{text [display] "use_thy \"Command\";"} - to the file @{text "./FoobarCommand/ROOT.ML"}. You can now compile the theory by just typing + to the file @{text "./FoobarCommand/ROOT.ML"}. You can now compile the theory by just typing: @{text [display] "$ isabelle make"} @@ -732,7 +746,7 @@ @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"} - on the Unix prompt. The directory should include the files + on the Unix prompt. The directory should include the files: @{text [display] "Pure.gz @@ -754,10 +768,10 @@ non-empty.} This keyword file needs to be copied into the directory @{text "~/.isabelle/etc"}. To make Isabelle aware of this keyword file, you have to start Isabelle with the option @{text - "-k foobar"}, i.e. + "-k foobar"}, that is: - @{text [display] "$ isabelle -k foobar a_theory_file"} + @{text [display] "$ isabelle emacs -k foobar a_theory_file"} If you now build a theory on top of @{text "Command.thy"}, then the command \isacommand{foobar} can be used. @@ -765,8 +779,8 @@ At the moment \isacommand{foobar} is not very useful. Let us refine it a bit - next by taking a proposition as argument and printing this proposition inside - the tracing buffer. + next by letting it take 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 a ``do-nothing''-function, which @@ -775,7 +789,7 @@ replace this code by a function that first parses a proposition (using the parser @{ML OuterParse.prop}), then prints out the tracing information (using a new top-level function @{text trace_top_lvl}) and - finally does nothing. For this we can write + finally does nothing. For this you can write: *} ML{*let @@ -790,7 +804,7 @@ end *} text {* - Now we can type + Now you can type \begin{isabelle} \isacommand{foobar}~@{text [quotes] "True \ False"}\\ @@ -810,8 +824,8 @@ indicator @{ML thy_goal in OuterKeyword}. Below we change \isacommand{foobar} so that it takes a proposition as - argument and then starts a proof in order to prove it. Therefore in Line 13 - below, we set the kind indicator to @{ML thy_goal in OuterKeyword}. + argument and then starts a proof in order to prove it. Therefore in Line 13, + we set the kind indicator to @{ML thy_goal in OuterKeyword}. *} ML%linenumbers{*let @@ -833,24 +847,26 @@ text {* The function @{text set_up_thm} in Lines 2 to 7 takes a string (the proposition to be - proved) and a context. The context is necessary in order to be able to use + proved) and a context as argument. The context is necessary in order to be able to use @{ML Syntax.read_prop}, which converts a string into a proper proposition. In Line 6 the function @{ML Proof.theorem_i} starts the proof for the proposition. Its argument @{ML NONE} stands for a locale (which we chose to omit); the argument @{ML "(K I)"} stands for a function that determines what should be done with the theorem once it is proved (we chose to just forget - about it). In Lines 9 to 11 contain the parser for the proposition. + about it). Lines 9 to 11 contain the parser for the proposition. + + (FIXME: explain @{ML Toplevel.print} etc) - If we now type \isacommand{foobar}~@{text [quotes] "True \ True"}, we obtain the following + If you now type \isacommand{foobar}~@{text [quotes] "True \ True"}, you obtain the following proof state: - + \begin{isabelle} \isacommand{foobar}~@{text [quotes] "True \ True"}\\ - @{text "goal (1 subgoal)"}\\ + @{text "goal (1 subgoal):"}\\ @{text "1. True \ True"} \end{isabelle} - and we can build the proof + and you can build the proof \begin{isabelle} \isacommand{foobar}~@{text [quotes] "True \ True"}\\ @@ -866,11 +882,8 @@ @{ML "Toplevel.print"} @{ML Toplevel.local_theory}?) - - (FIXME read a name and show how to store theorems) - (FIXME possibly also read a locale) *} (*<*) diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Recipes/Config.thy --- a/CookBook/Recipes/Config.thy Fri Feb 06 06:19:52 2009 +0000 +++ b/CookBook/Recipes/Config.thy Sat Feb 07 12:05:02 2009 +0000 @@ -12,8 +12,8 @@ {\bf Solution:} This can be achieved using configuration values.\smallskip - Assume you want to control three values, namely @{ML_text bval} containing a - boolean, @{ML_text ival} containing an integer and @{ML_text sval} + Assume you want to control three values, namely @{text bval} containing a + boolean, @{text ival} containing an integer and @{text sval} containing a string. These values can be declared on the ML-level with *} diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Recipes/ExternalSolver.thy --- a/CookBook/Recipes/ExternalSolver.thy Fri Feb 06 06:19:52 2009 +0000 +++ b/CookBook/Recipes/ExternalSolver.thy Sat Feb 07 12:05:02 2009 +0000 @@ -73,8 +73,8 @@ \begin{readmore} A short introduction to oracles can be found in [isar-ref: no suitable label for section 3.11]. A simple example, which we will slightly extend here, - is given in @{ML_file "FOL/ex/IffOracle"}. The raw interface for adding - oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm"}. + is given in @{ML_file "FOL/ex/IffOracle.thy"}. The raw interface for adding + oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm.ML"}. \end{readmore} For our explanation here, we restrict ourselves to decide propositional diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Recipes/TimeLimit.thy --- a/CookBook/Recipes/TimeLimit.thy Fri Feb 06 06:19:52 2009 +0000 +++ b/CookBook/Recipes/TimeLimit.thy Sat Feb 07 12:05:02 2009 +0000 @@ -33,7 +33,7 @@ handle TimeLimit.TimeOut => ~1" "~1"} - where @{ML_text TimeOut} is the exception raised when the time limit + where @{text TimeOut} is the exception raised when the time limit is reached. Note that @{ML "timeLimit" in TimeLimit} is only meaningful when you use PolyML, diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Fri Feb 06 06:19:52 2009 +0000 +++ b/CookBook/Tactical.thy Sat Feb 07 12:05:02 2009 +0000 @@ -6,20 +6,22 @@ text {* - The main reason for descending to the ML-level of Isabelle is to be able to - implement automatic proof procedures. Such proof procedures usually lessen - considerably the burden of manual reasoning, for example, when introducing - new definitions. These proof procedures are centred around refining a goal - state using tactics. This is similar to the @{text apply}-style reasoning at - the user level, where goals are modified in a sequence of proof steps until - all of them are solved. However, there are also more structured operations - that help with handling of variables and assumptions. + The main reason for descending to the ML-level of Isabelle is to be + able to implement automatic proof procedures. Such proof procedures usually + lessen considerably the burden of manual reasoning, for example, when + introducing new definitions. These proof procedures are centred around + refining a goal state using tactics. This is similar to the @{text + apply}-style reasoning at the user level, where goals are modified in a + sequence of proof steps until all of them are solved. However, there are + also more structured operations available on the ML-level that help with + the handling of variables and assumptions. + *} -section {* Tactical Reasoning *} +section {* Basics of Reasoning with Tactics*} text {* - To see how tactics work, let us first transcribe a simple @{text apply}-style proof + To see how tactics work, let us first transcribe a simple \isacommand{apply}-style proof into ML. Consider the following proof. *} @@ -57,7 +59,10 @@ it can make use of the local assumptions (there are none in this example). The functions @{ML etac}, @{ML rtac} and @{ML atac} correspond to @{text erule}, @{text rule} and @{text assumption}, respectively. - The operator @{ML THEN} strings the tactics together. + The operator @{ML THEN} strings the tactics together. A difference + between the \isacommand{apply}-script and the ML-code is that the + former causes the lemma to be stored under the name @{text "disj_swap"}, + whereas the latter does not include any code for this. \begin{readmore} To learn more about the function @{ML Goal.prove} see \isccite{sec:results} @@ -75,8 +80,8 @@ actually applied. This problem is nicely prevented by using antiquotations, because then the theorems are fixed statically at compile-time. - During the development of automatic proof procedures, it will often be necessary - to test a tactic on examples. This can be conveniently + During the development of automatic proof procedures, you will often find it + necessary to test a tactic on examples. This can be conveniently done with the command \isacommand{apply}@{text "(tactic \ \ \)"}. Consider the following sequence of tactics *} @@ -96,13 +101,15 @@ text {* By using @{text "tactic \ \ \"} in the apply-step, - you can call @{ML foo_tac} or any function that returns a tactic from the - user level of Isabelle. + you can call from the user level of Isabelle the tactic @{ML foo_tac} or + any other function that returns a tactic. - As can be seen, each tactic in @{ML foo_tac} has a hard-coded number that - stands for the subgoal analysed by the tactic. In our case, we only focus on the first - subgoal. This is sometimes wanted, but usually not. To avoid the explicit numbering in the - tactic, you can write + The tactic @{ML foo_tac} is just a sequence of simple tactics stringed + together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac} + has a hard-coded number that stands for the subgoal analysed by the + tactic (@{text "1"} stands for the first, or top-most, subgoal). This is + sometimes wanted, but usually not. To avoid the explicit numbering in + the tactic, you can write *} ML{*val foo_tac' = @@ -114,9 +121,9 @@ text {* and then give the number for the subgoal explicitly when the tactic is - called. For every operator that combines tactics, such a primed version - exists. So in the next proof we can first discharge the second subgoal, - and after that the first. + called. For every operator that combines tactics (@{ML THEN} is only one + such operator), a primed version exists. So in the next proof you + can first discharge the second subgoal, and after that the first. *} lemma "P1 \ Q1 \ Q1 \ P1" @@ -126,11 +133,11 @@ done text {* - (FIXME: maybe add something about how each goal state is interpreted - as a theorem) + This kind of addressing is more difficult to achieve when the goal is + hard-coded inside the tactic. - The tactic @{ML foo_tac} (and @{ML foo_tac'}) are very specific for - analysing goals only of the form @{prop "P \ Q \ Q \ P"}. If the goal is not + The tactics @{ML foo_tac} and @{ML foo_tac'} are very specific for + analysing goals being only of the form @{prop "P \ Q \ Q \ P"}. If the goal is not of this form, then @{ML foo_tac} throws the error message: \begin{isabelle} @@ -140,12 +147,29 @@ Meaning the tactic failed. The reason for this error message is that tactics are functions that map a goal state to a (lazy) sequence of successor states, - hence the type of a tactic is + hence the type of a tactic is: @{text [display, gray] "type tactic = thm -> thm Seq.seq"} It is custom that if a tactic fails, it should return the empty sequence: - tactics should not raise exceptions willy-nilly. + your own tactics should not raise exceptions willy-nilly. + + The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns + the empty sequence and is defined as +*} + +ML{*fun no_tac thm = Seq.empty*} + +text {* + which means @{ML no_tac} always fails. The second returns the given theorem wrapped + as a single member sequence. It is defined as +*} + +ML{*fun all_tac thm = Seq.single thm*} + +text {* + which means @{ML all_tac} always succeeds (but also does not make any progress + with the proof). The lazy list of possible successor states shows through to the user-level of Isabelle when using the command \isacommand{back}. For instance in the @@ -158,10 +182,12 @@ back done + text {* By using \isacommand{back}, we construct the proof that uses the - second assumption to complete the proof. In more interesting - situations, different possibilities can lead to different proofs. + second assumption. In more interesting situations, different possibilities + can lead to different proofs and even often need to be explored when + a first proof attempt is unsuccessful. \begin{readmore} See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy @@ -170,9 +196,95 @@ instead. \end{readmore} + For a beginner it might be surprising that tactics, which transform + one proof state to the next, are functions from theorems to theorem + (sequences). The surprise resolves by knowing that every + proof state is indeed a theorem. To shed more light on this, + let us modify the code of @{ML all_tac} to obtain the following + tactic +*} + +ML{*fun my_print_tac ctxt thm = + let + val _ = warning (str_of_thm ctxt thm) + in + Seq.single thm + end*} + +text {* + which prints out the given theorem (using the string-function defined + in Section~\ref{sec:printing}) and then behaves like @{ML all_tac}. We + now can inspect every proof state in the follwing proof. On the left-hand + side we show the goal state as shown by the system; on the right-hand + side the print out from our @{ML my_print_tac}. +*} + +lemma shows "\A; B\ \ A \ B" +apply(tactic {* my_print_tac @{context} *}) + +txt{* \small + \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}} + \begin{minipage}[t]{0.3\textwidth} + @{subgoals [display]} + \end{minipage} & + \hfill@{text "(\A; B\ \ A \ B) \ (\A; B\ \ A \ B)"} + \end{tabular} *} -section {* Basic Tactics *} +apply(rule conjI) +apply(tactic {* my_print_tac @{context} *}) + +txt{* \small + \begin{tabular}{@ {}l@ {}p{0.76\textwidth}@ {}} + \begin{minipage}[t]{0.26\textwidth} + @{subgoals [display]} + \end{minipage} & + \hfill@{text "(\A; B\ \ A) \ (\A; B\ \ B) \ (\A; B\ \ A \ B)"} + \end{tabular} +*} + +apply(assumption) +apply(tactic {* my_print_tac @{context} *}) + +txt{* \small + \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}} + \begin{minipage}[t]{0.3\textwidth} + @{subgoals [display]} + \end{minipage} & + \hfill@{text "(\A; B\ \ B) \ (\A; B\ \ A \ B)"} + \end{tabular} +*} + +apply(assumption) +apply(tactic {* my_print_tac @{context} *}) + +txt{* \small + \begin{tabular}{@ {}l@ {}p{0.7\textwidth}@ {}} + \begin{minipage}[t]{0.3\textwidth} + @{subgoals [display]} + \end{minipage} & + \hfill@{text "\A; B\ \ A \ B"} + \end{tabular} +*} + +done + +text {* + As can be seen, internally every goal state is an implication of the form + + @{text[display] "A\<^isub>1 \ \ \ A\<^isub>n \ (C)"} + + where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the + subgoals. Since the goal @{term C} can potentially be an implication, + there is a protector (invisible in the print out above) wrapped around + it. This prevents that premises are misinterpreted as open subgoals. + While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they + are expected to leave the conclusion @{term C} intact, with the + exception of possibly instantiating schematic variables. + +*} + +section {* Simple Tactics *} text {* As seen above, the function @{ML atac} corresponds to the assumption tactic. @@ -184,7 +296,7 @@ text {* Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond - to @{ML_text rule}, @{ML_text drule}, @{ML_text erule} and @{ML_text frule}, + to @{text rule}, @{text drule}, @{text erule} and @{text frule}, respectively. Below are three examples with the resulting goal state. How they work should therefore be self-explanatory. *} @@ -247,7 +359,7 @@ (*<*)oops(*>*) text {* - Also for useful for debugging, but not exclusively, are the tactics @{ML all_tac} and + Also for useful for debugging purposes are the tactics @{ML all_tac} and @{ML no_tac}. The former always succeeds (but does not change the goal state), and the latter always fails. @@ -274,9 +386,9 @@ val _ = (warning ("params: " ^ str_of_params); warning ("schematics: " ^ str_of_schms); - warning ("asms: " ^ str_of_asms); - warning ("concl: " ^ str_of_concl); - warning ("prems: " ^ str_of_prems)) + warning ("assumptions: " ^ str_of_asms); + warning ("conclusion: " ^ str_of_concl); + warning ("premises: " ^ str_of_prems)) in no_tac end*} @@ -303,11 +415,11 @@ \begin{quote}\small \begin{tabular}{ll} - params: & @{term x}, @{term y}\\ - schematics: & @{term z}\\ - asms: & @{term "A x y"}\\ - concl: & @{term "B y x \ C (z y) x"}\\ - prems: & @{term "A x y"} + params: & @{term x}, @{term y}\\ + schematics: & @{term z}\\ + assumptions: & @{term "A x y"}\\ + conclusion: & @{term "B y x \ C (z y) x"}\\ + premises: & @{term "A x y"} \end{tabular} \end{quote} @@ -335,11 +447,11 @@ \begin{quote}\small \begin{tabular}{ll} - params: & @{term x}, @{term y}\\ - schematics: & @{term z}\\ - asms: & @{term "A x y"}, @{term "B y x"}\\ - concl: & @{term "C (z y) x"}\\ - prems: & @{term "A x y"}, @{term "B y x"} + params: & @{term x}, @{term y}\\ + schematics: & @{term z}\\ + assumptions: & @{term "A x y"}, @{term "B y x"}\\ + conclusion: & @{term "C (z y) x"}\\ + premises: & @{term "A x y"}, @{term "B y x"} \end{tabular} \end{quote} *} @@ -428,35 +540,6 @@ @{ML resolve_tac} *} - - -text {* - - - A goal (or goal state) is a special @{ML_type thm}, which by - convention is an implication of the form: - - @{text[display] "A\<^isub>1 \ \ \ A\<^isub>n \ #(C)"} - - where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are the open - subgoals. - Since the goal @{term C} can potentially be an implication, there is a - @{text "#"} wrapped around it, which prevents that premises are - misinterpreted as open subgoals. The wrapper @{text "# :: prop \ - prop"} is just the identity function and used as a syntactic marker. - - - - - - While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they - are expected to leave the conclusion @{term C} intact, with the - exception of possibly instantiating schematic variables. - - - -*} - section {* Structured Proofs *} lemma True @@ -495,4 +578,5 @@ *} + end \ No newline at end of file diff -r 123401a5c8e9 -r 5e309df58557 CookBook/antiquote_setup.ML --- a/CookBook/antiquote_setup.ML Fri Feb 06 06:19:52 2009 +0000 +++ b/CookBook/antiquote_setup.ML Sat Feb 07 12:05:02 2009 +0000 @@ -53,12 +53,19 @@ let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end -fun check_file_exists ctxt txt = - if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () - else error ("Source file " ^ quote txt ^ " does not exist.") +fun check_file_exists src node = +let + fun check txt = + if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () + else error ("Source file " ^ (quote txt) ^ " does not exist.") +in + ThyOutput.args (Scan.lift Args.name) + (ThyOutput.output (fn _ => fn s => (check s; Pretty.str s))) src node +end -(* to be closer to the actual output *) -fun output_goals main_goal src node = +(* replaces the official subgoal antiquotation with one *) +(* that is closer to the actual output *) +fun output_goals src node = let fun subgoals 0 = "" | subgoals 1 = "goal (1 subgoal):" @@ -70,7 +77,7 @@ | _ => error "No proof state"); val state = proof_state node; - val goals = Proof.pretty_goals main_goal state; + val goals = Proof.pretty_goals false state; val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd); val (As, B) = Logic.strip_horn prop; @@ -88,10 +95,7 @@ (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) (output_ml ml_val_open)), - ("ML_file", ThyOutput.args (Scan.lift Args.name) - (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))), - ("ML_text", ThyOutput.args (Scan.lift Args.name) - (ThyOutput.output (fn _ => fn s => Pretty.str s))), + ("ML_file", check_file_exists), ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) (output_ml_response ml_pat)), ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) @@ -100,6 +104,6 @@ (output_ml_response_fake_both ml_val)), ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type)), - ("subgoals", output_goals false)]; + ("subgoals", output_goals)]; end; diff -r 123401a5c8e9 -r 5e309df58557 cookbook.pdf Binary file cookbook.pdf has changed