isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:ab9e09076462
+:cccb25ee1309
 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")"
 "Exception- ERROR \"foo\" raised
 At command \"ML\"."}
-(FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling})
+(FIXME Mention how to work with @{ML Toplevel.debug} and @{ML Toplevel.profiling}.)
 *}
 (*
 ML {* reset Toplevel.debug *}
 ML {* Toplevel.program (fn () => innocent ()) *}
 *)
 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,
+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. A simple way to transform
 a term into a string is to use the function @{ML Syntax.string_of_term}.
 @{ML_response_fake [display,gray]
 "Syntax.string_of_term @{context} @{term \"1::nat\"}"
 "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 abou calling conventions)
+(FIXME: say something about calling conventions)
 *}
 section {* Antiquotations *}
 "[\"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 that potentially cause loops.
-On the ML-level of Isabelle, you often have to work with qualified names;
+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
+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>}"}.
 @{ML_response [display,gray]
 "@{binding \"name\"}"
 "name"}
 An example where a binding is needed is the function @{ML define in
-LocalTheory}.  Below, this function is used to define the constant @{term
+LocalTheory}.  This function is below used to define the constant @{term
 "TrueConj"} as the conjunction
 @{term "True \<and> True"}.
 *}
 local_setup %gray {*
 "@{term \"(a::nat) + b = c\"}"
 "Const (\"op =\", \<dots>) $
 (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 will show the term @{term "(a::nat) + b = c"}, but printed using the internal
-representation corresponding to the datatype @{ML_type "term"}. Since Isabelle
+representation corresponding to the datatype @{ML_type "term"} defined as follows:
-uses Church-style terms, the datatype @{ML_type term} must be defined in
-conjunction with types, that is the datatype @{ML_type typ}:
 *}
-ML_val{*datatype typ =
+ML_val{*datatype term =
-Type  of string * typ list
-| TFree of string * sort
-| TVar  of indexname * sort
-datatype term =
 Const of string * typ
 | Free of string * typ
 | Var of indexname * typ
 | Bound of int
 | Abs of string * typ * term
 | $ of term * term *}
 text {*
-The datatype for terms uses the usual de Bruijn index mechanism---where
+Terms use the usual de Bruijn index mechanism---where
-bound variables are represented by the constructor @{ML Bound}.
+bound variables are represented by the constructor @{ML Bound}.  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 index in
+the indices refer to the number of Abstractions (@{ML Abs}) that we need to skip
-@{ML Bound} refers to the number of Abstractions (@{ML Abs}) we have to skip
 until we hit the @{ML Abs} that binds the corresponding variable. 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 show up with a question mark in front of them. Consider the following
+variables that when printed show up with a question mark in front of them. Consider
-two examples
+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 v2 = Var ((\"x1\", 3), @{typ bool})
 in
 writeln (Syntax.string_of_term @{context} v1);
 writeln (Syntax.string_of_term @{context} v2)
 end"
 "?x3
 ?x1.3"}
 This is different from a free variable
 @{ML_response_fake [display, gray]
-"@{term \"x\"}"
+"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 observe the distinction. The same holds
+If you deal with theorems, you have to observe the distinction. A similar
-for types.
+distinction holds for types (see below).
 \begin{readmore}
 Terms and types are described in detail in \isccite{sec:terms}. Their
 definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
 \end{readmore}
 @{ML_response_fake_both [display,gray]
 "@{term \"x x\"}"
 "Type unification failed: Occurs check!"}
 raises a typing error, while it perfectly ok to construct the term
-@{ML [display,gray] "Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})"}
+@{ML_response_fake [display,gray]
+"let
+val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})
+in
+writeln (Syntax.string_of_term @{context} omega)
+end"
+"x x"}
 with the raw ML-constructors.
 Sometimes the internal representation of terms can be surprisingly different
 from what you see at the user-level, because the layers of
 parsing/type-checking/pretty printing can be quite elaborate.
 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
+*}
+ML_val{*datatype typ =
+Type  of string * typ list
+| TFree of string * sort
+| TVar  of indexname * 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.
 \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"}.
 For example
 @{ML_response [display,gray]
 "@{type_name \"list\"}" "\"List.list\""}
+(FIXME: Explain the following better.)
 Occasionally you have to calculate what the ``base'' name of a given
 constant is. For this you can use the function @{ML Sign.extern_const} or
 @{ML Long_Name.base_name}. For example:
 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
 @{ML_response_fake [display,gray]
 "map_types nat_to_int @{term \"a = (1::nat)\"}"
 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
-(FIXME: a readmore about types)
+If you want to obtain the list of free type-variables of a term, you
+can use the function @{ML Term.add_tfrees} (similarly @{ML Term.add_tvars}
-(Explain @{ML Term.add_tvarsT} and @{ML Term.add_tfreesT})
+for the schematic type-variables). One would expect that such functions
+take a term as input and return a list of types. But their type is actually
+@{text[display] "Term.term -> (string * Term.sort) list -> (string * Term.sort) list"}
+that is they take, besides a term, also a list of type-variables as input.
+So in order to obtain the list of type-variables of a term you have to
+call them as follows
+@{ML_response [gray,display]
+"Term.add_tfrees @{term \"(a,b)\"} []"
+"[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
+The reason for this definition is that @{ML Term.add_tfrees} can
+be easily folded over a list of terms. Similarly for all functions
+named @{text "add_"}some\_name in @{ML_file "Pure/term.ML"}.
 *}
 section {* Type-Checking *}

changeset 251	cccb25ee1309
parent 250	ab9e09076462
child 252	f380b13b25a7