isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:2565c87f8db7
+:8057d65607eb
 |> curry list_comb f *}
 text {*
 This function takes a term and a context as argument. If the term is of function
 type, then @{ML "apply_fresh_args"} returns the term with distinct variables
-applied to it. For example:
+applied to it. For example below 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 ctxt = @{context}
 end"
 "P z za zb"}
 You can read off this behaviour from how @{ML apply_fresh_args} is
 coded: in Line 2, the function @{ML [index] fastype_of} calculates the type of the
-function; @{ML [index] binder_types} in the next line produces the list of argument
+term; @{ML [index] binder_types} in the next line produces the list of 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 [index] 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 [index] list_comb} to the function. In this last step we have to
+by the function @{ML [index] list_comb} to the term. In this last step we have to
 use the function @{ML [index] curry}, because @{ML [index] list_comb} expects the
 function and the variables list as a pair. This kind of functions is often needed when
-constructing terms and the infrastructure helps tremendously to avoid
+constructing terms with fresh variables. The infrastructure helps tremendously
-any name clashes. Consider for example:
+to avoid any name clashes. Consider for example:
 @{ML_response_fake [display,gray]
 "let
 val t = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
 val ctxt = @{context}
 @{ML_response [display,gray]
 "acc_incs 1 ||>> (fn x => (x, x + 2))"
 "(((((\"\", 1), 2), 3), 4), 6)"}
-(FIXME: maybe give a ``real world'' example)
+(FIXME: maybe give a ``real world'' example for this combinator)
 *}
 text {*
 Recall that @{ML [index] "|>"} is the reverse function application. Recall also that
 the related
 text {*
 The main advantage of embedding all code in a theory is that the code can
 contain references to entities defined on the logical level of Isabelle. By
 this we mean definitions, theorems, terms and so on. This kind of reference is
-realised with antiquotations.  For example, one can print out the name of the current
+realised with antiquotations, sometimes also referred to as ML-antiquotations.
+For example, one can print out the name of the current
 theory by typing
 @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
 (FIXME give a better example why bindings are important; maybe
 give a pointer to \isacommand{local\_setup}; if not, then explain
 why @{ML snd} is needed)
 It is also possible to define your own antiquotations. But you should
-exercise care when introducing new one, as they can also make your
+exercise care when introducing new ones, as they can also make your
-code unreadable. In the next section we will see how the (build in)
+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 a antiquotation that does not
+use schematic variables. If you want an antiquotation that does not
 have this restriction, you can implement your own using the
-function @{ML [index] ML_Antiquote.inline}.
+function @{ML [index] ML_Antiquote.inline}. The code is as follows.
 *}
 ML %linenosgray{*ML_Antiquote.inline "term_pat"
 (Args.context -- Scan.lift Args.name_source >>
 (fn (ctxt, s) =>
 s |> ProofContext.read_term_pattern ctxt
 |> ML_Syntax.print_term
 |> ML_Syntax.atomic))*}
 text {*
-We call the antiquotation @{text "term_pat"} (Line 1); the parser in Line
+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 read_term_pattern in ProofContext} (Line 4);
+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)\"}"
 "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
+which is the internal representation of the term @{text "Suc ?x"}.
 \begin{readmore}
 The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
 for most antiquotations.
 \end{readmore}
-Note also that in Isabelle there are two kinds of antiquotations, which have
+Note one source of possible confusion about antiquotations. There are two kinds
-very different infrastructures. The first kind, described in this section,
+of them in Isabelle, which have very different purpose and infrastructures. The
-is sometimes called \emph{ML-antiquotations}. They are used to refer to
+first kind, described in this section, are \emph{ML-antiquotations}. They are
-entities (like terms, types etc) from Isabelle's logic layer inside ML-code.
+used to refer to entities (like terms, types etc) from Isabelle's logic layer
-They are ``linked'' statically at compile-time, which  limits sometimes
+inside ML-code. They are ``linked'' statically at compile-time, which  limits
-their usefulness in  cases where, for example, terms needs to be built up
+sometimes their usefulness in  cases where, for example, terms needs to be
-dynamically.
+built up dynamically.
-The other kind of antiquotations are called \emph{document antiquotations}.
+The other kind of antiquotations are \emph{document} antiquotations.
-They are used only in the text parts of Isabelle and help with printing logical
+They are used only in the text parts of Isabelle and their purpose is to print
-entities inside \LaTeX-documents. In this Tutorial we are not interested
+logical entities inside \LaTeX-documents. They are part of the user level and
-in these antiquotations, except in Appendix \ref{rec:docantiquotations} where
+therefore we are not interested in them in this Tutorial, except in
-we show how to implement your own document antiquotations.
+Appendix \ref{rec:docantiquotations} where we show how to implement your
+own document antiquotations.
 *}
 section {* Terms and Types *}
 text {*
 | Bound of int
 | Abs of string * typ * term
 | $ of term * term *}
 text {*
+This datatype implements lambda-terms typed in Church-style.
 As can be seen in Line 5, terms use the usual de Bruijn index mechanism
 for representing bound variables.  For
 example in
 @{ML_response_fake [display, gray]
 "@{term \"\<lambda>x y. x y\"}"
 "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}
-the indices refer to the number of Abstractions (@{ML Abs}) that we need to skip
+the indices refer to the number of Abstractions (@{ML Abs}) that we need to
-until we hit the @{ML Abs} that binds the corresponding variable. Note that
+skip until we hit the @{ML Abs} that binds the corresponding variable. Constructing
-the names of bound variables are kept at abstractions for printing purposes,
+a term with dangling de Bruijn indices is possible, but will be flagged as
-and so should be treated only as ``comments''.  Application in Isabelle is
+ill-formed when you try to typecheck or certify it (see
-realised with the term-constructor @{ML $}.
+Section~\ref{sec:typechecking}). Note that the names of bound variables are kept at
+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})
 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
 @{ML_response_fake [display, gray]
 "let
 val v1 = Var ((\"x\", 3), @{typ bool})
 val v2 = Var ((\"x1\", 3), @{typ bool})
+val v3 = Free (\"x\", @{typ bool})
 in
 writeln (Syntax.string_of_term @{context} v1);
-writeln (Syntax.string_of_term @{context} v2)
+writeln (Syntax.string_of_term @{context} v2);
+writeln (Syntax.string_of_term @{context} v3)
 end"
 "?x3
-?x1.3"}
+?x1.3
+x"}
-This is different from a free variable
+When constructing terms, you are usually concerned with free variables (as mentioned earlier,
-@{ML_response_fake [display, gray]
-"writeln (Syntax.string_of_term @{context} (Free (\"x\", @{typ bool})))"
-"x"}
-When constructing terms, you are usually concerned with free variables (for example
 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).
 \begin{readmore}
 As already seen above, types can be constructed using the antiquotation
 @{text "@{typ \<dots>}"}. For example:
 @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
-Their definition is
+The corresponding datatype is
 *}
 ML_val{*datatype typ =
 Type  of string * typ list
 | TFree of string * sort
 text {*
 Like with terms, there is the distinction between free type
 variables (term-constructor @{ML "TFree"} and schematic
 type variables (term-constructor @{ML "TVar"}). A type constant,
 like @{typ "int"} or @{typ bool}, are types with an empty list
-of argument types.
+of argument types. However, it is a bit difficult to show an
+example, because Isabelle always pretty-prints types (unlike terms).
+Here is a contrived example:
+@{ML_response [display, gray]
+"if Type (\"bool\", []) = @{typ \"bool\"} then true else false"
+"true"}
 \begin{readmore}
 Types are described in detail in \isccite{sec:types}. Their
 definition and many useful operations are implemented
 in @{ML_file "Pure/type.ML"}.
 constructing terms. One is the function @{ML [index] list_comb}, which takes a term
 and a list of terms as arguments, and produces as output the term
 list applied to the term. For example
 @{ML_response_fake [display,gray]
-"list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])"
+"let
+val t = @{term \"P::nat\"}
+val args = [@{term \"True\"}, @{term \"False\"}]
+in
+list_comb (t, args)
+end"
 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
 Another handy function is @{ML [index] lambda}, which abstracts a variable
 in a term. For example
 @{ML_response_fake [display,gray]
 "lambda @{term \"x::nat\"} @{term \"(P::nat \<Rightarrow> bool) x\"}"
 "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
-In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound  0"}),
+In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}),
 and an abstraction. It also records the type of the abstracted
 variable and for printing purposes also its name.  Note that because of the
 typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
 is of the same type as the abstracted variable. If it is of different type,
 as in
 named @{text "add_"}some\_name in @{ML_file "Pure/term.ML"}.
 *}
-section {* Type-Checking *}
+section {* Type-Checking\label{sec:typechecking} *}
 text {*
 You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
 typ}es, since they are just arbitrary unchecked trees. However, you

changeset 298	8057d65607eb
parent 293	0a567f923b42
child 299	d0b81d6e1b28