# HG changeset patch # User Christian Urban # Date 1222937321 14400 # Node ID 9da9ba2b095bc566176a1e8d947539fee1a90d3e # Parent 1c17e99f6f669759d0aee1e1944c0fb1f5f360ec added a solution section and some other minor additions 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. diff -r 1c17e99f6f66 -r 9da9ba2b095b CookBook/ROOT.ML --- a/CookBook/ROOT.ML Wed Oct 01 20:42:55 2008 -0400 +++ b/CookBook/ROOT.ML Thu Oct 02 04:48:41 2008 -0400 @@ -6,4 +6,6 @@ use_thy "Appendix"; use_thy "Recipes/NamedThms"; -use_thy "Recipes/Transformation"; \ No newline at end of file +use_thy "Recipes/Transformation"; + +use_thy "Solutions"; \ No newline at end of file diff -r 1c17e99f6f66 -r 9da9ba2b095b CookBook/Recipes/NamedThms.thy --- a/CookBook/Recipes/NamedThms.thy Wed Oct 01 20:42:55 2008 -0400 +++ b/CookBook/Recipes/NamedThms.thy Thu Oct 02 04:48:41 2008 -0400 @@ -1,9 +1,10 @@ theory NamedThms imports Main +uses "antiquote_setup.ML" + "antiquote_setup_plus.ML" begin - section {* Accumulate a List of Theorems under a Name *} @@ -53,6 +54,12 @@ \end{readmore} *} +text {* + (FIXME: maybe add a comment about the case when the theorems + to be added need to satisfy certain properties) + +*} + end diff -r 1c17e99f6f66 -r 9da9ba2b095b CookBook/Solutions.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/Solutions.thy Thu Oct 02 04:48:41 2008 -0400 @@ -0,0 +1,29 @@ +theory Solutions +imports Main +uses "antiquote_setup.ML" + "antiquote_setup_plus.ML" +begin + +chapter {* Solutions to Most Exercises *} + +text {* \solution{fun:revsum} *} + +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 {* \solution{fun:makesum} *} + +ML {* + fun make_sum t1 t2 = + HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) +*} + +end \ No newline at end of file diff -r 1c17e99f6f66 -r 9da9ba2b095b CookBook/antiquote_setup_plus.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/antiquote_setup_plus.ML Thu Oct 02 04:48:41 2008 -0400 @@ -0,0 +1,16 @@ +(* +Auxiliary antiquotations for the Cookbook. + +*) + +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 \ No newline at end of file diff -r 1c17e99f6f66 -r 9da9ba2b095b CookBook/document/root.tex --- a/CookBook/document/root.tex Wed Oct 01 20:42:55 2008 -0400 +++ b/CookBook/document/root.tex Thu Oct 02 04:48:41 2008 -0400 @@ -22,7 +22,6 @@ % sane default for proof documents \parindent 0pt\parskip 0.6ex - % for comments on the margin \newcommand{\readmoremarginpar}[1]% {\marginpar[\raggedleft\small{#1}]{\raggedright\small{#1}}} @@ -30,8 +29,9 @@ \newenvironment{readmore}% {\hspace{-3pt}\readmoremarginpar{\fbox{\textbf{Read More}}}\it}{} +% for exercises and comments \newtheorem{exercise}{Exercise}[section] - +\newcommand{\solution}[1]{{\bf Solution for Exercise~\ref{#1}.}} \begin{document} diff -r 1c17e99f6f66 -r 9da9ba2b095b cookbook.pdf Binary file cookbook.pdf has changed