# HG changeset patch # User Christian Urban # Date 1223231353 14400 # Node ID 34b93dbf8c3cfac822d05f45e61d3844e5b1c823 # Parent b4c31af6af26d38cf2f0e4aacb8e38752290db81 some tuning in the FirstSteps section diff -r b4c31af6af26 -r 34b93dbf8c3c CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Thu Oct 02 05:30:46 2008 -0400 +++ b/CookBook/FirstSteps.thy Sun Oct 05 14:29:13 2008 -0400 @@ -36,7 +36,7 @@ *} text {* - The expression inside \isacommand{ML} commands is immediately evaluated, + Expressions inside \isacommand{ML} commands are 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 \isacommand{ML} @@ -80,22 +80,24 @@ text {* will print out @{ML "\"any string\""} inside the response buffer of Isabelle. - PolyML provides a convenient, though again ``quick-and-dirty'', method for - converting arbitrary values into strings, for example: + If you develop under PolyML, then there is a convenient, though again + ``quick-and-dirty'', method for converting values into strings, + for example: *} ML {* warning (makestring 1) *} text {* - However this only works if the type of what is printed is monomorphic and not + However this only works if the type of what is converted is monomorphic and not a function. *} text {* The funtion warning should only be used for testing purposes, because - 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. + any output this funtion generates will be overwritten, as soon as an error + is raised. + Therefore for printing anything more serious and elaborate, the function @{ML tracing} + should be used. This function writes all output into a separate buffer. *} ML {* tracing "foo" *} @@ -124,7 +126,7 @@ *} text {* - Calling the @{ML_text "redirect_tracing"} function with @{ML_text "(TextIO.openOut \"foo.bar\")"} + Calling @{ML_text "redirect_tracing"} with @{ML_text "(TextIO.openOut \"foo.bar\")"} will cause that all tracing information is printed into the file @{ML_text "foo.bar"}. *} @@ -154,7 +156,7 @@ *} ML {* - fun current_thyname () = Context.theory_name @{theory} + fun not_current_thyname () = Context.theory_name @{theory} *} text {* @@ -166,10 +168,9 @@ some data structure and return it. Instead, it is literally replaced with the value representing the theory name. - In a similar way you can use antiquotations to refer to types and theorems: + In a similar way you can use antiquotations to refer to theorems: *} -ML {* @{typ "(int * nat) list"} *} ML {* @{thm allI} *} text {* @@ -238,31 +239,51 @@ ML {* @{term "P x"} ; @{prop "P x"} *} -text {* which inserts the coercion in the latter ase and *} +text {* which inserts the coercion in the latter case and *} ML {* @{term "P x \ Q x"} ; @{prop "P x \ Q x"} *} -text {* which does not. *} +text {* + which does not. + + Types can be constructed using the antiquotation @{text "@{typ \}"}. For example + + *} + +ML {* @{typ "bool \ nat"} *} -text {* (FIXME: add something about @{text "@{typ \}"}) *} +text {* + (FIXME: Unlike the term antiquotation, @{text "@{typ \}"} does not print the + internal representation. Is there a reason for this, that needs to be explained + here?) + + \begin{readmore} + Types are described in detail in \isccite{sec:types}. Their + definition and many useful operations can be found in @{ML_file "Pure/type.ML"}. + \end{readmore} + + *} + + + section {* Constructing Terms and Types Manually *} text {* - While antiquotations are very convenient for constructing terms (similarly types), + While antiquotations are very convenient for constructing terms and 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 arguments - can only be written as + @{text "\(x::\). P x \ Q x"} taking @{term P}, @{term Q} and the typ @{term "\"} + as arguments can only be written as *} ML {* - fun make_imp P Q = + fun make_imp P Q tau = let - val x = @{term "x::nat"} + val x = Free ("x",tau) in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x), HOLogic.mk_Trueprop (Q $ x))) end @@ -270,21 +291,22 @@ text {* - The reason is that one cannot pass the arguments @{term P} and @{term Q} into - an antiquotation. For example this following does not work. + The reason is that one cannot pass the arguments @{term P}, @{term Q} and + @{term "tau"} into an antiquotation. For example this following does not work. *} ML {* - fun make_imp_wrong P Q = @{prop "\x. P x \ Q x"} + fun make_wrong_imp P Q tau = @{prop "\x. P x \ Q x"} *} text {* - 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 - name for constants. For example the names for @{text "zero"} or @{text "+"} are - more complex than one first expects, namely + To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} + to both functions. + + One tricky point in constructing terms by hand is to obtain the + fully qualified 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"}. @@ -295,12 +317,11 @@ 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: - *} + +text {* -ML {* @{const_name HOL.zero}; @{const_name plus} *} - -text {* + (FIXME: Is it useful to explain @{text "@{const_syntax}"}?) \begin{readmore} There are many functions in @{ML_file "Pure/logic.ML"} and diff -r b4c31af6af26 -r 34b93dbf8c3c cookbook.pdf Binary file cookbook.pdf has changed