diff -r f4fa6540e280 -r c90f4ec30d43 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Thu Aug 13 21:32:10 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Sun Aug 16 21:54:47 2009 +0200 @@ -194,11 +194,13 @@ *) text {* - Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} - or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing - them (see Section \ref{sec:pretty}), - but for quick-and-dirty solutions they are far too unwieldy. One way to transform - a term into a string is to use the function @{ML [index] string_of_term in Syntax}. + Most often you want to inspect data of Isabelle's most basic datastructures, + namely @{ML_type term}, @{ML_type cterm} or @{ML_type thm}. Isabelle + contains elaborate pretty-printing functions for printing them (see Section + \ref{sec:pretty}), but for quick-and-dirty solutions they are far too + unwieldy. One way to transform a term into a string is to use the function + @{ML [index] string_of_term in Syntax}. + @{ML_response_fake [display,gray] "Syntax.string_of_term @{context} @{term \"1::nat\"}" @@ -206,17 +208,23 @@ This produces a string with some additional information encoded in it. The string can be properly printed by using either the function @{ML [index] writeln} or - @{ML [index] tracing}. + @{ML [index] tracing}: @{ML_response_fake [display,gray] "writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})" "\"1\""} + or + + @{ML_response_fake [display,gray] + "tracing (Syntax.string_of_term @{context} @{term \"1::nat\"})" + "\"1\""} + A @{ML_type cterm} can be transformed into a string by the following function. *} ML{*fun string_of_cterm ctxt t = - Syntax.string_of_term ctxt (term_of t)*} + Syntax.string_of_term ctxt (term_of t)*} text {* In this example the function @{ML [index] term_of} extracts the @{ML_type term} from @@ -225,7 +233,7 @@ *} ML{*fun string_of_cterms ctxt ts = - commas (map (string_of_cterm ctxt) ts)*} + commas (map (string_of_cterm ctxt) ts)*} text {* The easiest way to get the string of a theorem is to transform it @@ -245,7 +253,8 @@ In order to improve the readability of theorems we convert these schematic variables into free variables using the - function @{ML [index] import in Variable}. + function @{ML [index] import in Variable}. This is similar + to the attribute @{text "[no_vars]"} from Isabelle's user-level. *} ML{*fun no_vars ctxt thm = @@ -495,6 +504,39 @@ ML{*fun (x, y) ||> f = (x, f y)*} text {* + These two functions can be used to avoid explicit @{text "lets"} for + intermediate values in functions that return pairs. Suppose for example you + want to separate a list of integers into two lists according to a + treshold. For example if the treshold is @{ML "5"}, the list @{ML + "[1,6,2,5,3,4]"} should be separated to @{ML "([1,2,3,4], [6,5])"}. You + can implement this function more concisely as +*} + +ML{*fun separate i [] = ([], []) + | separate i (x::xs) = + let + val (los, grs) = separate i xs + in + if i <= x then (los, x::grs) else (x::los, grs) + end*} + +text {* + where however the return value of the recursive + call is bound explicitly to the pair @{ML "(los, grs)" for los grs}. + This function can equally be written as +*} + +ML{*fun separate i [] = ([], []) + | separate i (x::xs) = + if i <= x + then separate i xs ||> cons x + else separate i xs |>> cons x*} + +text {* + where no explicit @{text "let"} is needed. While in this example the gain is + only small, in more complicated situations the benefit of avoiding @{text "lets"} + can be substantial. + With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair. This combinator is defined as *} @@ -569,6 +611,8 @@ \end{readmore} (FIXME: say something about calling conventions) + + (FIXME: say something about singleton) *} @@ -685,7 +729,7 @@ code also difficult to read. In the next section we will see how the (build in) antiquotation @{text "@{term \}"} can be used to construct terms. A restriction of this antiquotation is that it does not allow you to - use schematic variables. If you want an antiquotation that does not + use schematic variables. If you want to have an antiquotation that does not have this restriction, you can implement your own using the function @{ML [index] ML_Antiquote.inline}. The code is as follows. *} @@ -698,11 +742,11 @@ |> ML_Syntax.atomic))*} text {* - We call the new antiquotation @{text "term_pat"} (Line 1); the parser in Line - 2 provides us with a context and a string; this string is transformed into a - term using the function @{ML [index] read_term_pattern in ProofContext} (Line 4); - the next two lines print the term so that the ML-system can understand - them. An example of this antiquotation is as follows. + The parser in Line 2 provides us with a context and a string; this string is + transformed into a term using the function @{ML [index] read_term_pattern in + ProofContext} (Line 4); the next two lines print the term so that the + ML-system can understand them. An example of this antiquotation is as + follows. @{ML_response_fake [display,gray] "@{term_pat \"Suc (?x::nat)\"}" @@ -774,10 +818,12 @@ @{ML $}. - Isabelle makes a distinction between \emph{free} variables (term-constructor @{ML Free}) - and variables (term-constructor @{ML Var}). The latter correspond to the schematic - variables that when printed show up with a question mark in front of them. Consider - the following two examples + Isabelle makes a distinction between \emph{free} variables (term-constructor + @{ML Free} and written in blue colour) and \emph{schematic} variables + (term-constructor @{ML Var} and written with a leading question mark). The + latter correspond to the schematic variables that when printed show up with + a question mark in front of them. Consider the following two examples + @{ML_response_fake [display, gray] "let @@ -986,10 +1032,10 @@ of Church-style typing, where variables with the same name still differ, if they have different type. - There is also the function @{ML [index] subst_free} with which terms can - be replaced by other terms. For example below, we will replace in - @{term "(f::nat \ nat \ nat) 0 x"} - the subterm @{term "(f::nat \ nat \ nat) 0"} by @{term y}, and @{term x} by @{term True}. + There is also the function @{ML [index] subst_free} with which terms can be + replaced by other terms. For example below, we will replace in @{term + "(f::nat \ nat \ nat) 0 x"} the subterm @{term "(f::nat \ nat \ nat) 0"} by + @{term y}, and @{term x} by @{term True}. @{ML_response_fake [display,gray] "let @@ -1013,6 +1059,48 @@ end" "Free (\"x\", \"nat\")"} + Similarly the function @{ML [index] subst_bounds}, replaces lose bound + variables with terms. To see how this function works, let us implement a + function that strips off the outermost quantifiers in a term. +*} + +ML {* +subst_bounds ([Free ("x", @{typ nat}), Free ("y", @{typ bool})], + (Bound 1 $ Bound 0)) +*} + + +ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) = + strip_alls t |>> cons (Free (n, T)) + | strip_alls t = ([], t) *} + +text {* + The function returns a pair consisting of the stripped off variables and + the body of the universal quantifications. For example + + @{ML_response_fake [display, gray] + "strip_alls @{term \"\x y. x = (y::bool)\"}" +"([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")], + Const (\"op =\", \) $ Bound 1 $ Bound 0)"} + + With the function @{ML subst_bounds}, you can replace the lose + @{ML [index] Bound}s with the stripped off variables. + + @{ML_response_fake [display, gray, linenos] + "let + val (vrs, trm) = strip_alls @{term \"\x y. x = (y::bool)\"} +in + subst_bounds (rev vrs, trm) + |> Syntax.string_of_term @{context} + |> tracing +end" + "x = y"} + + Note that in Line 4 we had to reverse the list of variables that @{ML strip_alls} + returned. The reason is that the head of the list the function @{ML subst_bounds} + takes is the replacement for @{ML "Bound 0"}, the next element for @{ML "Bound 1"} + and so on. + There are many convenient functions that construct specific HOL-terms. For example @{ML [index] mk_eq in HOLogic} constructs an equality out of two terms. The types needed in this equality are calculated from the type of the