isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:f4fa6540e280
+:c90f4ec30d43
 ML {* Toplevel.program (fn () => innocent ()) *}
 *)
 text {*
-Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm}
+Most often you want to inspect data of Isabelle's most basic datastructures,
-or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing
+namely @{ML_type term}, @{ML_type cterm} or @{ML_type thm}. Isabelle
-them (see Section \ref{sec:pretty}),
+contains elaborate pretty-printing functions for printing them (see Section
-but  for quick-and-dirty solutions they are far too unwieldy. One way to transform
+\ref{sec:pretty}), but for quick-and-dirty solutions they are far too
-a term into a string is to use the function @{ML [index] string_of_term in Syntax}.
+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\"}"
 "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
 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)*}
 text {*
 In this example the function @{ML [index] term_of} extracts the @{ML_type term} from
 a @{ML_type cterm}.  If there are more than one @{ML_type cterm}s to be
 printed, you can use the function @{ML [index] commas} to separate them.
 *}
 ML{*fun string_of_cterms ctxt ts =
 commas (map (string_of_cterm ctxt) ts)*}
 text {*
 The easiest way to get the string of a theorem is to transform it
 into a @{ML_type cterm} using the function @{ML [index] crep_thm}.
 *}
 "tracing (string_of_thm @{context} @{thm conjI})"
 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 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 =
 let
 val ((_, [thm']), _) = Variable.import true [thm] ctxt
 *}
 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
 *}
 ML{*fun (x, y) |-> f = f x y*}
 and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
 contains further information about combinators.
 \end{readmore}
 (FIXME: say something about calling conventions)
+(FIXME: say something about singleton)
 *}
 section {* Antiquotations *}
 It is also possible to define your own antiquotations. But you should
 exercise care when introducing new ones, as they can also make your
 code also difficult to read. In the next section we will see how the (build in)
 antiquotation @{text "@{term \<dots>}"} 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.
 *}
 ML %linenosgray{*ML_Antiquote.inline "term_pat"
 s |> ProofContext.read_term_pattern ctxt
 |> ML_Syntax.print_term
 |> ML_Syntax.atomic))*}
 text {*
-We call the new antiquotation @{text "term_pat"} (Line 1); the parser in Line
+The parser in Line 2 provides us with a context and a string; this string is
-2 provides us with a context and a string; this string is transformed into a
+transformed into a term using the function @{ML [index] read_term_pattern in
-term using the function @{ML [index] read_term_pattern in ProofContext} (Line 4);
+ProofContext} (Line 4); the next two lines print the term so that the
-the next two lines print the term so that the ML-system can understand
+ML-system can understand them. An example of this antiquotation is as
-them. An example of this antiquotation is as follows.
+follows.
 @{ML_response_fake [display,gray]
 "@{term_pat \"Suc (?x::nat)\"}"
 "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
 abstractions for printing purposes, and so should be treated only as
 ``comments''.  Application in Isabelle is realised with the term-constructor
 @{ML $}.
-Isabelle makes a distinction between \emph{free} variables (term-constructor @{ML Free})
+Isabelle makes a distinction between \emph{free} variables (term-constructor
-and variables (term-constructor @{ML Var}). The latter correspond to the schematic
+@{ML Free} and written in blue colour) and \emph{schematic} variables
-variables that when printed show up with a question mark in front of them. Consider
+(term-constructor @{ML Var} and written with a leading question mark). The
-the following two examples
+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
 val v1 = Var ((\"x\", 3), @{typ bool})
 val v2 = Var ((\"x1\", 3), @{typ bool})
 then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted.
 This is a fundamental principle
 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
+There is also the function @{ML [index] subst_free} with which terms can be
-be replaced by other terms. For example below, we will replace in
+replaced by other terms. For example below, we will replace in @{term
-@{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"}
+"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by
-the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by @{term y}, and @{term x} by @{term True}.
+@{term y}, and @{term x} by @{term True}.
 @{ML_response_fake [display,gray]
 "let
 val s1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
 val s2 = (@{term \"x::nat\"}, @{term \"True\"})
 val trm = @{term \"(\<lambda>x::nat. x)\"}
 in
 subst_free [s] trm
 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 \"\<forall>x y. x = (y::bool)\"}"
+"([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
+Const (\"op =\", \<dots>) $ 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 \"\<forall>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
 arguments. For example

changeset 308	c90f4ec30d43
parent 307	f4fa6540e280
child 309	ed797395fab6