isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:95461cf6fd07
+:5fc2fb34c323
 ML {* Toplevel.program (fn () => innocent ()) *}
 *)
 text {*
-Most often you want to inspect data of Isabelle's basic data
+Most often you want to inspect data of Isabelle's basic data structures,
-structures, namely @{ML_type term}, @{ML_type cterm} and @{ML_type
+namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
-thm}. Isabelle contains elaborate pretty-printing functions for printing
+and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions
-them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
+for printing them (see Section \ref{sec:pretty}), but for quick-and-dirty
-are a bit unwieldy. One way to transform a term into a string is to use the
+solutions they are a bit unwieldy. One way to transform a term into a string
-function @{ML_ind  string_of_term in Syntax} from the structure @{ML_struct
+is to use the function @{ML_ind string_of_term in Syntax} from the structure
-Syntax}. For more convenience, we bind this function to the toplevel.
+@{ML_struct Syntax}. For more convenience, we bind this function to the
+toplevel.
 *}
 ML{*val string_of_term = Syntax.string_of_term*}
 text {*
 fun string_of_thms_no_vars ctxt thms =
 commas (map (string_of_thm_no_vars ctxt) thms) *}
 text {*
+The printing functions for types are
+*}
+ML{*fun string_of_typ ctxt ty = Syntax.string_of_typ ctxt ty
+fun string_of_typs ctxt tys = commas (map (string_of_typ ctxt) tys)*}
+text {*
+respectively ctypes
+*}
+ML{*fun string_of_ctyp ctxt cty = string_of_typ ctxt (typ_of cty)
+fun string_of_ctyps ctxt ctys = commas (map (string_of_ctyp ctxt) ctys)*}
+text {*
 \begin{readmore}
 The simple conversion functions from Isabelle's main datatypes to
 @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}.
 The references that change the printing information are declared in
 @{ML_file "Pure/Syntax/printer.ML"}.
 \end{readmore}
-Note that for printing out several ``parcels'' of information that
+Note that for printing out several ``parcels'' of information that belong
-semantically belong together, like a warning message consisting of
+together, like a warning message consisting of a term and its type, you
-a term and its type, you should try to keep this information together in a
+should try to print these parcels together in a single string. Therefore do
-single string. Therefore do \emph{not} print out information as
+\emph{not} print out information as
 @{ML_response_fake [display,gray]
 "tracing \"First half,\";
 tracing \"and second half.\""
 "First half,
 To ease this kind of string manipulations, there are a number
 of library functions in Isabelle. For example,  the function
 @{ML_ind cat_lines in Library} concatenates a list of strings
 and inserts newlines in between each element.
-@{ML_response [display, gray]
+@{ML_response_fake [display, gray]
-"cat_lines [\"foo\", \"bar\"]"
+"tracing (cat_lines [\"foo\", \"bar\"])"
-"\"foo\\nbar\""}
+"foo
+bar"}
-Section \ref{sec:pretty} will also explain the infrastructure that Isabelle
+Section \ref{sec:pretty} will explain the infrastructure that Isabelle
 provides for more elaborate pretty printing.
 \begin{readmore}
 Most of the basic string functions of Isabelle are defined in
 @{ML_file "Pure/library.ML"}.
 |> (fn x => (x, x))
 |> fst
 |> (fn x => x + 4)*}
 text {*
-which increments its argument @{text x} by 5. It does this by first incrementing
+which increments its argument @{text x} by 5. It does this by first
-the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking
+incrementing the argument by 1 (Line 2); then storing the result in a pair
-the first component of the pair (Line 4) and finally incrementing the first
+(Line 3); taking the first component of the pair (Line 4) and finally
-component by 4 (Line 5). This kind of cascading manipulations of values is quite
+incrementing the first component by 4 (Line 5). This kind of cascading
-common when dealing with theories (for example by adding a definition, followed by
+manipulations of values is quite common when dealing with theories. The
-lemmas and so on). The reverse application allows you to read what happens in
+reverse application allows you to read what happens in a top-down
-a top-down manner. This kind of coding should also be familiar,
+manner. This kind of coding should be familiar, if you have been exposed to
-if you have been exposed to Haskell's {\it do}-notation. Writing the function
+Haskell's {\it do}-notation. Writing the function @{ML inc_by_five} using
-@{ML inc_by_five} using the reverse application is much clearer than writing
+the reverse application is much clearer than writing
 *}
 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
 text {* or *}
 applied to it. For example below three variables are applied to the term
 @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
 @{ML_response_fake [display,gray]
 "let
-val t = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
+val trm = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
 val ctxt = @{context}
 in
-apply_fresh_args t ctxt
+apply_fresh_args trm ctxt
 |> string_of_term ctxt
 |> tracing
 end"
 "P z za zb"}
 argument types (in the case above the list @{text "[nat, int, unit]"}); Line
 4 pairs up each type with the string @{text "z"}; the function @{ML_ind
 variant_frees in Variable} generates for each @{text "z"} a unique name
 avoiding the given @{text f}; the list of name-type pairs is turned into a
 list of variable terms in Line 6, which in the last line is applied by the
-function @{ML_ind list_comb in Term} to the term. In this last step we have
+function @{ML_ind list_comb in Term} to the original term. In this last step we have
 to use the function @{ML_ind curry in Library}, because @{ML list_comb}
 expects the function and the variables list as a pair.
 Functions like @{ML apply_fresh_args} are often needed when constructing
-terms with fresh variables. The
+terms involving fresh variables. For this the infrastructure helps
-infrastructure helps tremendously to avoid any name clashes. Consider for
+tremendously to avoid any name clashes. Consider for example:
-example:
 @{ML_response_fake [display,gray]
 "let
-val t = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
+val trm = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
 val ctxt = @{context}
 in
-apply_fresh_args t ctxt
+apply_fresh_args trm ctxt
 |> string_of_term ctxt
 |> tracing
 end"
 "za z zb"}
 (fn x => x + 1) #>
 (fn x => x + 2) #>
 (fn x => x + 3)*}
 text {*
-which is the function composed of first the increment-by-one function and then
+which is the function composed of first the increment-by-one function and
-increment-by-two, followed by increment-by-three. Again, the reverse function
+then increment-by-two, followed by increment-by-three. Again, the reverse
-composition allows you to read the code top-down. This combinator is often used
+function composition allows you to read the code top-down. This combinator
-for setup function inside the \isacommand{setup}-command. These function have to be
+is often used for setup functions inside the
-of type @{ML_type "theory -> theory"} in order to install, for example, some new
+\isacommand{setup}-command. These functions have to be of type @{ML_type
-data inside the current theory. More than one such setup function can be composed
+"theory -> theory"}. More than one such setup function can be composed with
-with @{ML "#>"}. For example
+@{ML "#>"}. For example
 *}
 setup %gray {* let
 val (ival1, setup_ival1) = Attrib.config_int "ival1" 1
 val (ival2, setup_ival2) = Attrib.config_int "ival2" 2
 text {*
 These two functions can, for example, be used to avoid explicit @{text "lets"} for
 intermediate values in functions that return pairs. As an example, suppose you
 want to separate a list of integers into two lists according to a
 treshold. 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])"}.  This function can be
+should be separated as @{ML "([1,2,3,4], [6,5])"}.  Such a function can be
 implemented as
 *}
 ML{*fun separate i [] = ([], [])
 | separate i (x::xs) =
 if i <= x then (los, x::grs) else (x::los, grs)
 end*}
 text {*
 where the return value of the recursive call is bound explicitly to
-the pair @{ML "(los, grs)" for los grs}. You can implement this function
+the pair @{ML "(los, grs)" for los grs}. However, this function
-more concisely as
+can be implemented more concisely as
 *}
 ML{*fun separate i [] = ([], [])
 | separate i (x::xs) =
 if i <= x
 text {*
 When using combinators for writing functions in waterfall fashion, it is
 sometimes necessary to do some ``plumbing'' in order to fit 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}, which works over pairs to fit with the combinator @{ML "|>"}. Such
+list_comb}, which works over pairs, to fit with the combinator @{ML "|>"}. Such
-plumbing is also needed in situations where a function operate over lists,
+plumbing is also needed in situations where a function operates over lists,
 but one calculates only with a single element. An example is the function
 @{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check
 a list of terms. Consider the code:
 @{ML_response_fake [display, gray]
 *}
 ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
 text {*
 does \emph{not} return the name of the current theory, if it is run in a
 different theory. Instead, the code above defines the constant function
 that always returns the string @{text [quotes] "FirstSteps"}, no matter where the
 function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is
 \emph{not} replaced with code that will look up the current theory in
 some data structure and return it. Instead, it is literally
-replaced with the value representing the theory name.
+replaced with the value representing the theory.
-In a similar way you can use antiquotations to refer to proved theorems:
+Another important antiquotation is @{text "@{context}"}. (What the
+difference between a theory and a context is will be described in Chapter
+\ref{chp:advanced}.) A context is for example needed in order to use the
+function @{ML print_abbrevs in ProofContext} that list of all currently
+defined abbreviations.
+@{ML_response_fake [display, gray]
+"ProofContext.print_abbrevs @{context}"
+"Code_Evaluation.valtermify \<equiv> \<lambda>x. (x, \<lambda>u. Code_Evaluation.termify x)
+INTER \<equiv> INFI
+Inter \<equiv> Inf
+\<dots>"}
+You can also use antiquotations to refer to proved theorems:
 @{text "@{thm \<dots>}"} for a single theorem
 @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
 and @{text "@{thms \<dots>}"} for more than one
-@{ML_response_fake [display,gray] "@{thms conj_ac}"
+@{ML_response_fake [display,gray]
+"@{thms conj_ac}"
 "(?P \<and> ?Q) = (?Q \<and> ?P)
 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}
+The thm-antiquotations can also be used for manipulating theorems. For
+example, if you need the version of te theorem @{thm [source] refl} that
+has a meta-equality instead of an equality, you can write
+@{ML_response_fake [display,gray]
+"@{thm refl[THEN eq_reflection]}"
+"?x \<equiv> ?x"}
 The point of these antiquotations is that referring to theorems in this way
 makes your code independent from what theorems the user might have stored
 under this name (this becomes especially important when you deal with
 theorem lists; see Section \ref{sec:storing}).
 text {*
 The result can be printed out as follows.
 @{ML_response_fake [gray,display]
-"foo_thm |> string_of_thms @{context}
+"foo_thm |> string_of_thms_no_vars @{context}
 |> tracing"
-"True, True"}
+"True, False \<Longrightarrow> P"}
 You can also refer to the current simpset via an antiquotation. To illustrate
 this we implement the function that extracts the theorem names stored in a
 simpset.
 *}
 map #1 simps
 end*}
 text {*
 The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing all
-information stored in the simpset, but we are only interested in the names of the
+information stored in the simpset, but here we are only interested in the names of the
 simp-rules. Now you can feed in the current simpset into this function.
 The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.
 @{ML_response_fake [display,gray]
 "get_thm_names_from_ss @{simpset}"
 "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 Again, this way of referencing simpsets makes you independent from additions
 of lemmas to the simpset by the user, which can potentially cause loops in your
 code.
-On the ML-level of Isabelle, you often have to work with qualified names.
-These are strings with some additional information, such as positional
-information and qualifiers. Such qualified names can be generated with the
-antiquotation @{text "@{binding \<dots>}"}. For example
-@{ML_response [display,gray]
-"@{binding \"name\"}"
-"name"}
-An example where a qualified name is needed is the function
-@{ML_ind define in Local_Theory}.  This function is used below to define
-the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
-*}
-local_setup %gray {*
-Local_Theory.define ((@{binding "TrueConj"}, NoSyn),
-(Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}
-text {*
-Now querying the definition you obtain:
-\begin{isabelle}
-\isacommand{thm}~@{text "TrueConj_def"}\\
-@{text "> "}~@{thm TrueConj_def}
-\end{isabelle}
-\begin{readmore}
-The basic operations on bindings are implemented in
-@{ML_file "Pure/General/binding.ML"}.
-\end{readmore}
-\footnote{\bf FIXME give a better example why bindings are important}
-\footnote{\bf FIXME give a pointer to \isacommand{local\_setup}; if not, then explain
-why @{ML snd} is needed.}
-\footnote{\bf FIXME: There should probably a separate section on binding, long-names
-and sign.}
 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 chapter we describe how to construct
 terms with the (build in) antiquotation @{text "@{term \<dots>}"}.  A restriction
 ML{*structure Data = Proof_Data
 (type T = term list
 fun init _ = [])*}
 text {*
-The function we have to specify has to produce a list once a context
+The init-function we have to specify must produce a list for when a context
 is initialised (possibly taking the theory into account from which the
 context is derived). We choose here to just return the empty list. Next
 we define two auxiliary functions for updating the list with a given
 term and printing the list.
 *}
 True \<and> True, False
 1
 2, 1"}
 Many functions in Isabelle manage and update data in a similar
-fashion. Consequently, such calculation with contexts occur frequently in
+fashion. Consequently, such calculations with contexts occur frequently in
 Isabelle code, although the ``context flow'' is usually only linear.
 Note also that the calculation above has no effect on the underlying
 theory. Once we throw away the contexts, we have no access to their
-associated data. This is different to theories, where the command
+associated data. This is different for theories, where the command
 \isacommand{setup} registers the data with the current and future
 theories, and therefore one can access the data potentially
 indefinitely.
 For convenience there is an abstract layer, namely the type @{ML_type Context.generic},

changeset 414	5fc2fb34c323
parent 413	95461cf6fd07
child 417	5f00958e3c7b