isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:26e5b41faa74
+:79696161ae16
 Calling @{ML "redirect_tracing"} with @{ML "(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 error}; for example:
-@{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
+@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")"
+"Exception- ERROR \"foo\" raised
+At command \"ML\"."}
 Section~\ref{sec:printing} will give more information about printing
 the main data structures of Isabelle, namely @{ML_type term}, @{ML_type cterm}
 and @{ML_type thm}.
 *}
 section {* Antiquotations *}
 text {*
 In a similar way you can use antiquotations to refer to proved theorems:
 @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
-and simpsets:
+and current simpsets:
 @{ML_response_fake [display,gray]
 "let
 val ({rules,...}, _) = MetaSimplifier.rep_ss @{simpset}
 in
 map #name (Net.entries rules)
 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 The code about simpsets extracts the theorem names stored in the
-current simpset.  You can get hold of the current simpset with the antiquotation
+simpset.  You can get hold of the current simpset with the antiquotation
 @{text "@{simpset}"}.  The function @{ML rep_ss in MetaSimplifier} returns a record
 containing all information about the simpset. The rules of a simpset are
 stored in a \emph{discrimination net} (a data structure for fast
 indexing). From this net you can extract the entries using the function @{ML
 Net.entries}.
 These bindings are difficult to maintain and also can be accidentally
 overwritten by the user. This often breakes Isabelle
 packages. Antiquotations solve this problem, since they are ``linked''
 statically at compile-time.  However, this static linkage also limits their
 usefulness in cases where data needs to be build up dynamically. In the
-course of this introduction, we will learn more about these antiquotations:
+course of this introduction, you will learn more about these antiquotations:
-they greatly simplify Isabelle programming since one can directly access all
+they can simplify Isabelle programming since one can directly access all
 kinds of logical elements from th ML-level.
 *}
 section {* Terms and Types *}
 text {*
-One way to construct terms of Isabelle on the ML-level is by using the antiquotation
+One way to construct terms of Isabelle is by using the antiquotation
 \mbox{@{text "@{term \<dots>}"}}. For example:
 @{ML_response [display,gray]
 "@{term \"(a::nat) + b = c\"}"
 "Const (\"op =\", \<dots>) $
 \item @{term "{ [x::int] | x. x \<le> -2 }"}
 \end{itemize}
 Hint: The third term is already quite big, and the pretty printer
 may omit parts of it by default. If you want to see all of it, you
-can use the following ML-function to set the limit to a value high
+can use the following ML-function to set the printing depth to a higher
-enough:
+value:
 @{ML [display,gray] "print_depth 50"}
 \end{exercise}
 The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type,
 "Const \<dots> $
 Abs (\"x\", \<dots>,
 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
-(FIXME: expand the following point)
-One tricky point in constructing terms by hand is to obtain the fully
-qualified name for constants. For example the names for @{text "zero"} and
-@{text "+"} are more complex than one first expects, namely
-\begin{center}
-@{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}.
-\end{center}
-The extra prefixes @{text zero_class} and @{text plus_class} are present
-because these constants are defined within type classes; the prefix @{text
-"HOL"} indicates in which theory they are defined. Guessing such internal
-names can sometimes be quite hard. Therefore Isabelle provides the
-antiquotation @{text "@{const_name \<dots>}"} which does the expansion
-automatically, for example:
-@{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"}
-(FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
 Although types of terms can often be inferred, there are many
 situations where you need to construct types manually, especially
 when defining constants. For example the function returning a function
 type is as follows:
 text {* This can be equally written as: *}
 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 text {*
 \begin{readmore}
 There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
 @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms
 and types easier.\end{readmore}
 Have a look at these files and try to solve the following two exercises:
 *}
 text {*
 \begin{exercise}\label{fun:revsum}
 Write a function @{text "rev_sum : term -> term"} that takes a
-term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero)
+term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero)
 and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}
 associates to the left. Try your function on some examples.
 \end{exercise}
 number representing their sum.
 \end{exercise}
 A handy function for manipulating terms is @{ML map_types}: it takes a
 function and applies it to every type in the term. You can, for example,
-change every @{typ nat} in a term into an @{typ int} using the function
+change every @{typ nat} in a term into an @{typ int} using the function:
 *}
 ML{*fun nat_to_int t =
 (case t of
 @{typ nat} => @{typ int}
 | Type (s, ts) => Type (s, map nat_to_int ts)
 | _ => t)*}
 text {*
-an then apply it as follows:
+An example as follows:
 @{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: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT})
 *}
+section {* Constants *}
+text {*
+There are a few subtle issues with constants. They usually crop up when
+pattern matching terms or constructing term. While it is perfectly ok
+to write the function @{text is_true} as follows
+*}
+ML{*fun is_true @{term True} = true
+| is_true _ = false*}
+text {*
+this does not work for picking out @{text "\<forall>"}-quantified terms. Because
+the function
+*}
+ML{*fun is_all (@{term All} $ _) = true
+| is_all _ = false*}
+text {*
+will not correctly match:
+@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
+The problem is that the @{text "@term"}-antiquotation in the pattern
+fixes the type of @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for
+an arbitrary, but fixed type @{typ "'a"}. A properly working alternative
+for this function is
+*}
+ML{*fun is_all (Const ("All", _) $ _) = true
+| is_all _ = false*}
+text {*
+because now
+@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
+matches correctly.
+However there is still a problem: consider the function that attempts to
+pick out a @{text "Nil"}-term:
+*}
+ML{*fun is_nil (Const ("Nil", _)) = true
+| is_nil _ = false *}
+text {*
+Unfortunately, also this one does not return the expected result, since
+@{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
+The problem is that on the ML-level the name of constants is not
+immediately clear. If you look at
+@{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
+the name of the constant depends on the theory in which the term constructor
+@{text "Nil"} is defined and also in which datatype. Even worse, some
+constants have an even more complex name involving type-classes. Consider
+for example
+@{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})"
+"(Const (\"HOL.zero_class.zero\", \<dots>),
+Const (\"HOL.times_class.times\", \<dots>))"}
+While you could always use the complete name, for example
+@{ML "Const (\"List.list.Nil\", @{typ \"nat list\"})"}, for referring to or
+matching against @{text "Nil"}, this would make the code rather brittle.
+The reason is that the theory and the name of the datatype can easily change.
+To make the code more robust it is better to use the antiquotation
+@{text "@{const_name \<dots>}"}. With this antiquotation you can harness the
+variable parts of the constant's name. Therefore the functions for
+matching against constants should be written as follows.
+*}
+ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
+| is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
+| is_nil_or_all _ = false *}
+text {*
+Having said this, you also frequently have to calculate what the
+``base''  name of a constant is. For this you can use the function
+@{ML Sign.base_name}. For example:
+(FIXME is there an example for that statement?)
+@{ML_response [display,gray] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
+(FIXME authentic syntax?)
+\begin{readmore}
+FIXME
+\end{readmore}
+*}
 section {* Theorems *}
 text {*
 Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
-that can only be built by going through interfaces. As a consequence, every proof
+that can only be build by going through interfaces. As a consequence, every proof
 in Isabelle is correct by construction.
 (FIXME reference LCF-philosophy)
 To see theorems in ``action'', let us give a proof on the ML-level for the following
 ML{*fun str_of_thms ctxt thms =
 commas (map (str_of_thm ctxt) thms)*}
-section {* Operations on Constants (Names) *}
-text {*
-@{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""}
-authentic syntax?
-*}
-ML {* @{const_name lfp} *}
-text {*
-constants in case-patterns?
-In the meantime, lfp has been moved to the Inductive theory, so it is
-no longer called Lfp.lfp. If a @{text "@{const_name}"} antiquotation had been
-used, we would have gotten an error for this. Another advantage of the
-antiquotation is that we can then just write @{text "@{const_name lfp}"} rather
-than @{text "@{const_name Lfp.lfp}"} or whatever, and it expands to the correct
-name.
-*}
 section {* Combinators\label{sec:combinators} *}
 text {*
 For beginners, perhaps the most puzzling parts in the existing code of Isabelle are
 the combinators. At first they seem to greatly obstruct the

changeset 122	79696161ae16
parent 120	c39f83d8daeb
child 123	460bc2ee14e9