isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:ed797395fab6
+:007922777ff1
 theory FirstSteps
 imports Base
+uses "FirstSteps.ML"
 begin
 chapter {* First Steps *}
 text {*
 Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
 @{ML [display,gray] "redirect_tracing (TextIO.openOut \"foo.bar\")"}
 will cause that all tracing information is printed into the file @{text "foo.bar"}.
 You can print out error messages with the function @{ML [index] error}; for
-example:\footnote{FIXME: unwanted pagebreak}
+example:
 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")"
 "Exception- ERROR \"foo\" raised
 At command \"ML\"."}
 ML {* Toplevel.program (fn () => innocent ()) *}
 *)
 text {*
-Most often you want to inspect data of Isabelle's most basic datastructures,
+Most often you want to inspect data of Isabelle's most basic data
-namely @{ML_type term}, @{ML_type cterm} or @{ML_type thm}. Isabelle
+structures, namely @{ML_type term}, @{ML_type cterm} or @{ML_type
-contains elaborate pretty-printing functions for printing them (see Section
+thm}. Isabelle contains elaborate pretty-printing functions for printing
-\ref{sec:pretty}), but for quick-and-dirty solutions they are far too
+them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
-unwieldy. One way to transform a term into a string is to use the function
+are a bit unwieldy. One way to transform a term into a string is to use the
-@{ML [index] string_of_term in Syntax}.
+function @{ML [index] string_of_term in Syntax} in structure @{ML_struct
+Syntax}, which we bind for more convenience to the toplevel.
+*}
+ML{*val string_of_term = Syntax.string_of_term*}
+text {*
+It can now be used as follows
 @{ML_response_fake [display,gray]
-"Syntax.string_of_term @{context} @{term \"1::nat\"}"
+"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
+This produces a string corrsponding to the term @{term [show_types] "1::nat"} with some
-can be properly printed by using either the function @{ML [index] writeln} or
+additional information encoded in it. The string can be properly printed by
-@{ML [index] tracing}:
+using either the function @{ML [index] writeln} or @{ML [index] tracing}:
 @{ML_response_fake [display,gray]
-"writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})"
+"writeln (string_of_term @{context} @{term \"1::nat\"})"
 "\"1\""}
 or
 @{ML_response_fake [display,gray]
-"tracing (Syntax.string_of_term @{context} @{term \"1::nat\"})"
+"tracing (string_of_term @{context} @{term \"1::nat\"})"
 "\"1\""}
+If there are more than one @{ML_type term}s to be printed, you can use the
+function @{ML [index] commas} to separate them.
+*}
+ML{*fun string_of_terms ctxt ts =
+commas (map (string_of_term ctxt) ts)*}
+text {*
 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)*}
+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
+a @{ML_type cterm}.  More than one @{ML_type cterm}s can again be printed
-printed, you can use the function @{ML [index] commas} to separate them.
+with @{ML [index] commas}.
 *}
-ML{*fun string_of_cterms ctxt ts =
+ML{*fun string_of_cterms ctxt cts =
-commas (map (string_of_cterm ctxt) ts)*}
+commas (map (string_of_cterm ctxt) cts)*}
 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}.
 *}
 @{ML_response_fake [display, gray]
 "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
+In order to improve the readability of theorems we convert these schematic
-these schematic variables into free variables using the
+variables into free variables using the function @{ML [index] import in
-function @{ML [index] import in Variable}. This is similar
+Variable}. This is similar to the theorem attribute @{text "[no_vars]"} from
-to the attribute @{text "[no_vars]"} from Isabelle's user-level.
+Isabelle's user-level.
 *}
 ML{*fun no_vars ctxt thm =
 let
 val ((_, [thm']), _) = Variable.import true [thm] ctxt
 "let
 val t = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
 val ctxt = @{context}
 in
 apply_fresh_args t ctxt
-|> Syntax.string_of_term ctxt
+|> string_of_term ctxt
 |> tracing
 end"
 "P z za zb"}
 You can read off this behaviour from how @{ML apply_fresh_args} is
 "let
 val t = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
 val ctxt = @{context}
 in
 apply_fresh_args t ctxt
-|> Syntax.string_of_term ctxt
+|> string_of_term ctxt
 |> tracing
 end"
 "za z zb"}
 where the @{text "za"} is correctly avoided.
 ML{*val double =
 (fn x => (x, x))
 #-> (fn x => fn y => x + y)*}
-text {*
+text {*
-(FIXME: find a good exercise for combinators)
+When using combinators for writing function in waterfall fashion, it is
+sometimes necessary to do some ``plumbing'' for fitting functions
+together. We have already seen such plumbing in the function @{ML
+apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
+list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such
+plumbing is also needed in situations where a functions operate over lists,
+but one calculates only with a single entity. An example is the function
+@{ML [index] check_terms in Syntax}, whose purpose is to type-check a list
+of terms.
+@{ML_response_fake [display, gray]
+"let
+val ctxt = @{context}
+in
+map (Syntax.parse_term ctxt) [\"m + n\", \"m - (n::nat)\"]
+|> Syntax.check_terms ctxt
+|> string_of_terms ctxt
+|> tracing
+end"
+"m + n, m - n"}
+*}
+text {*
+In this example we obtain two terms with appropriate typing. However, if you
+have only a single term, then @{ML check_terms in Syntax} needs to be
+adapted. This can be done with the ``plumbing'' function @{ML
+singleton}.\footnote{There is in fact alread a function @{ML check_term in Syntax},
+which however is defined in terms of @{ML singleton} and @{ML check_terms in
+Syntax}.} For example
+@{ML_response_fake [display, gray]
+"let
+val ctxt = @{context}
+in
+Syntax.parse_term ctxt \"m - (n::nat)\"
+|> singleton (Syntax.check_terms ctxt)
+|> string_of_term ctxt
+|> tracing
+end"
+"m - n"}
 \begin{readmore}
 The most frequently used combinators are defined in the files @{ML_file
 "Pure/library.ML"}
 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: find a good exercise for combinators)
-(FIXME: say something about singleton)
+(FIXME: say something about calling conventions)
 *}
 section {* Antiquotations *}
 "let
 val v1 = Var ((\"x\", 3), @{typ bool})
 val v2 = Var ((\"x1\", 3), @{typ bool})
 val v3 = Free (\"x\", @{typ bool})
 in
-map (Syntax.string_of_term @{context}) [v1, v2, v3]
+string_of_terms @{context} [v1, v2, v3]
-|> cat_lines
 |> tracing
 end"
-"?x3
+"?x3, ?x1.3, x"}
-?x1.3
-x"}
 When constructing terms, you are usually concerned with free variables (as mentioned earlier,
 you cannot construct schematic variables using the antiquotation @{text "@{term \<dots>}"}).
 If you deal with theorems, you have to, however, observe the distinction. A similar
 distinction holds for types (see below).
 @{ML_response_fake [display,gray]
 "let
 val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})
 in
-tracing (Syntax.string_of_term @{context} omega)
+tracing (string_of_term @{context} omega)
 end"
 "x x"}
 with the raw ML-constructors.
 @{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}
+|> 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}
 @{ML_response_fake [gray,display]
 "let
 val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
 in
-tracing (Syntax.string_of_term @{context} eq)
+tracing (string_of_term @{context} eq)
 end"
 "True = False"}
 *}
 text {*
 let val prems = Logic.strip_imp_prems t in
 if i <= length prems
 then let val (params,t) = strip_assums_all([], nth prems (i - 1))
 in subst_bounds(map Free params, t) end
 else error ("Not enough premises for prem" ^ string_of_int i ^
-" in propositon: " ^ Syntax.string_of_term ctxt t)
+" in propositon: " ^ string_of_term ctxt t)
 end;
 *}
 ML {*
 strip_assums_all ([], @{term "\<And>x y. A x y"})

changeset 310	007922777ff1
parent 309	ed797395fab6
child 311	ee864694315b