diff -r 1c17e99f6f66 -r 9da9ba2b095b CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Wed Oct 01 20:42:55 2008 -0400 +++ b/CookBook/FirstSteps.thy Thu Oct 02 04:48:41 2008 -0400 @@ -1,27 +1,10 @@ theory FirstSteps imports Main uses "antiquote_setup.ML" + "antiquote_setup_plus.ML" begin -(*<*) - - -ML {* -local structure O = ThyOutput -in - fun check_exists f = - if File.exists (Path.explode ("~~/src/" ^ f)) then () - else error ("Source file " ^ quote f ^ " does not exist.") - - val _ = O.add_commands - [("ML_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name => - (check_exists name; Pretty.str name))))]; - -end -*} -(*>*) - chapter {* First Steps *} @@ -56,8 +39,9 @@ The expression inside \isacommand{ML} commands is immediately evaluated, like ``normal'' Isabelle proof scripts, 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. However on such ML-commands the - undo operation behaves slightly counter-intuitive, because if you define + can also contain value and function bindings. However on such \isacommand{ML} + commands the undo operation behaves slightly counter-intuitive, because + if you define *} ML {* @@ -69,14 +53,14 @@ @{ML "foo"}. Once a portion of code is relatively stable, one usually wants to - export it to a separate ML-file. Such files can be included in a - theory using @{ML_text "uses"} in the header of the theory. + export it to a separate ML-file. Such files can then be included in a + theory by using \isacommand{uses} in the header of the theory, like \begin{center} \begin{tabular}{@ {}l} \isacommand{theory} CookBook\\ \isacommand{imports} Main\\ - \isacommand{uses} @{text "\"file_to_be_included.ML\""}\\ + \isacommand{uses} @{ML_text "\"file_to_be_included.ML\""} @{text "\"}\\ \isacommand{begin}\\ \ldots \end{tabular} @@ -109,20 +93,18 @@ text {* The funtion warning should only be used for testing purposes, because - the problem with this function is that any output will be - overwritten if an error is raised. For anything more serious - the function @{ML tracing}, which writes all output in a separate - buffer, should be used. - + any output this funtion generated will be overwritten, if an error is raised. + For printing anything more serious and elaborate, the function @{ML tracing} + should be used. This function writes all output in a separate buffer. *} ML {* tracing "foo" *} -text {* (FIXME: complete the comment about redirecting the trace information) +text {* - In Isabelle it is possible to redirect the message channels to a - separate file, e.g. to prevent Proof General from choking on massive - amounts of trace output. + It is also possible to redirect the channel where the @{ML_text "foo"} is + printed to a separate file, e.g. to prevent Proof General from choking on massive + amounts of trace output. This rediretion can be achieved using the code *} @@ -141,6 +123,12 @@ TextIO.flushOut stream)); *} +text {* + Calling the @{ML_text "redirect_tracing"} function with @{ML_text "(TextIO.openOut \"foo.bar\")"} + will cause that all tracing information is printed into the file @{ML_text "foo.bar"}. + +*} + section {* Antiquotations *} @@ -191,7 +179,7 @@ *} -section {* Terms *} +section {* Terms and Types *} text {* One way to construct terms of Isabelle on the ML-level is by using the antiquotation @@ -238,7 +226,7 @@ enough: \end{exercise} *} -ML {* print_depth 50 *} +ML {* print_depth 50 *} text {* @@ -250,21 +238,23 @@ ML {* @{term "P x"} ; @{prop "P x"} *} -text {* which needs the coercion and *} +text {* which inserts the coercion in the latter ase and *} ML {* @{term "P x \ Q x"} ; @{prop "P x \ Q x"} *} text {* which does not. *} -section {* Constructing Terms Manually *} +text {* (FIXME: add something about @{text "@{typ \}"}) *} + +section {* Constructing Terms and Types Manually *} text {* - While antiquotations are very convenient for constructing terms, they can - only construct fixed terms. Unfortunately, one often needs to construct terms + While antiquotations are very convenient for constructing terms (similarly types), + they can only construct fixed terms. Unfortunately, one often needs to construct them dynamically. For example, a function that returns the implication - @{text "\(x::nat). P x \ Q x"} taking @{term P} and @{term Q} as input terms + @{text "\(x::nat). P x \ Q x"} taking @{term P} and @{term Q} as arguments can only be written as *} @@ -281,7 +271,7 @@ text {* The reason is that one cannot pass the arguments @{term P} and @{term Q} into - an antiquotation, like + an antiquotation. For example this following does not work. *} ML {* @@ -290,19 +280,21 @@ text {* - To see the difference apply @{text "@{term S}"} and - @{text "@{term T}"} to the functions. + To see this apply @{text "@{term S}"} and @{text "@{term T}"} to boths functions. - One tricky point in constructing terms by hand is to obtain the fully qualified - names for constants. For example the names for @{text "zero"} or @{text "+"} are - more complex than one first expects, namely @{ML_text "HOL.zero_class.zero"} - and @{ML_text "HOL.plus_class.plus"}. The extra prefixes @{ML_text zero_class} - and @{ML_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 - Isabellle provides the antiquotation @{text "@{const_name \}"} does the expansion - automatically, for example: + name for constants. For example the names for @{text "zero"} or @{text "+"} are + more complex than one first expects, namely + + \begin{center} + @{ML_text "HOL.zero_class.zero"} and @{ML_text "HOL.plus_class.plus"}. + \end{center} + + The extra prefixes @{ML_text zero_class} and @{ML_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 Isabellle provides the antiquotation @{text "@{const_name \}"} which does the + expansion automatically, for example: *} @@ -328,21 +320,8 @@ the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} associates to the left. Try your function on some examples. \end{exercise} -*} -ML {* - fun rev_sum t = - let - fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = - u' :: dest_sum u - | dest_sum u = [u] - in - foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t) - end; -*} - -text {* - \begin{exercise} + \begin{exercise}\label{fun:makesum} Write a function which takes two terms representing natural numbers in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary number representing their sum. @@ -350,19 +329,11 @@ *} -ML {* - fun make_sum t1 t2 = - HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) -*} - - section {* Type Checking *} text {* - (FIXME: Should we say something about types?) - We can freely construct and manipulate terms, since they are just arbitrary unchecked trees. However, we eventually want to see if a term is well-formed, or type checks, relative to a theory.