isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:077c764c8d8b
+:41a802bbb7df
 @{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)"}
-You can also refer to the current simpset. To illustrate this we implement the
+The point of these antiquotations is that referring to theorems in this way
-function that extracts the theorem names stored in a simpset.
+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:attributes}).
+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.
 *}
 ML{*fun get_thm_names_from_ss simpset =
 let
 val {simps,...} = MetaSimplifier.dest_ss 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 that potentially cause loops.
+of lemmas to the simpset by the user that 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>}"}.
+@{text "@{binding \<dots>}"}. For example
 @{ML_response [display,gray]
 "@{binding \"name\"}"
 "name"}
-An example where a binding is needed is the function @{ML [index] define in
+An example where a qualified name is needed is the function
-LocalTheory}.  This function is below used to define the constant @{term
+@{ML [index] define in LocalTheory}.  This function is used below to define
-"TrueConj"} as the conjunction
+the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
-@{term "True \<and> True"}.
 *}
 local_setup %gray {*
 snd o LocalTheory.define Thm.internalK
 ((@{binding "TrueConj"}, NoSyn),
 (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)
-While antiquotations have many applications, they were originally introduced
+It is also possible to define your own antiquotations. But you should
-in order to avoid explicit bindings of theorems such as:
+exercise care when introducing new one, as they can also make your
-*}
+code unreadable. In the next section we will see how the (build in)
+antiquotation @{text "@{term \<dots>}"} can be used to construct terms.
-ML{*val allI = thm "allI" *}
+A restriction of this antiquotation is that it does not allow you to
+use schematic variables. If you want a antiquotation that does not
-text {*
+have this restriction, you can implement your own using the
-Such bindings are difficult to maintain and can be overwritten by the
+function @{ML [index] ML_Antiquote.inline}.
-user accidentally. This often broke Isabelle
+*}
-packages. Antiquotations solve this problem, since they are ``linked''
-statically at compile-time.  However, this static linkage also limits their
+ML %linenosgray{*ML_Antiquote.inline "term_pat"
-usefulness in cases where data needs to be built up dynamically. In the
-course of this chapter you will learn more about antiquotations:
-they can simplify Isabelle programming since one can directly access all
-kinds of logical elements from the ML-level.
-*}
-text {* FIXME: give an example of a user defined antiquotation *}
-ML{*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))*}
-ML{*@{term_pat "?x + ?y"}*}
+text {*
+We call the antiquotation @{text "term_pat"} (Line 1); the parser in Line
-text {*
+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);
+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\")"}
 \begin{readmore}
-@{ML_file "Pure/ML/ml_antiquote.ML"}
+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
+very different infrastructures. The first kind, described in this section,
+is sometimes called \emph{ML-antiquotations}. They are used to refer to
+entities (like terms, types etc) from Isabelle's logic layer inside ML-code.
+They are ``linked'' statically at compile-time, which  limits sometimes
+their usefulness in  cases where, for example, terms needs to be built up
+dynamically.
+The other kind of antiquotations are called \emph{document antiquotations}.
+They are used only in the text parts of Isabelle and help with printing logical
+entities inside \LaTeX-documents. In this Tutorial we are not interested
+in these antiquotations, except in Appendix \ref{rec:docantiquotations} where
+we show how to implement your own document antiquotations.
 *}
 section {* Terms and Types *}
 text {*
 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\"}"
+"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"}),
 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
 @{ML_response_fake [display,gray]
-"lambda @{term \"x::nat\"} @{term \"(P::bool\<Rightarrow>bool) x\"}"
+"lambda @{term \"x::nat\"} @{term \"(P::bool \<Rightarrow> bool) x\"}"
 "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Free (\"x\", \"bool\"))"}
 then the variable @{text "Free (\"x\", \"bool\")"} is \emph{not} abstracted.
 This is a fundamental principle
 of Church-style typing, where variables with the same name still differ, if they
 have different type.
 There is also the function @{ML [index] subst_free} with which terms can
 be replaced by other terms. For example below, we will replace in
-@{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0 x"}
+@{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"}
-the subterm @{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0"} by @{term y}, and @{term x} by @{term True}.
+the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by @{term y}, and @{term x} by @{term True}.
 @{ML_response_fake [display,gray]
-"subst_free [(@{term \"(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0\"}, @{term \"y::nat\<Rightarrow>nat\"}),
+"let
-(@{term \"x::nat\"}, @{term \"True\"})]
+val s1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
-@{term \"((f::nat\<Rightarrow>nat\<Rightarrow>nat) 0) x\"}"
+val s2 = (@{term \"x::nat\"}, @{term \"True\"})
+val trm =  @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
+in
+subst_free [s1, s2] trm
+end"
 "Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}
 As can be seen, @{ML subst_free} does not take typability into account.
 However it takes alpha-equivalence into account:
 @{ML_response_fake [display, gray]
-"subst_free [(@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})]
+"let
-@{term \"(\<lambda>x::nat. x)\"}"
+val s = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})
+val trm = @{term \"(\<lambda>x::nat. x)\"}
+in
+subst_free [s] trm
+end"
 "Free (\"x\", \"nat\")"}
 There are many convenient functions that construct specific HOL-terms. For
 example @{ML [index] mk_eq in HOLogic} constructs an equality out of two terms.
 The types needed in this equality are calculated from the type of the
 @{ML_response_fake [gray,display]
 "writeln (Syntax.string_of_term @{context}
 (HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})))"
 "True = False"}
+*}
+text {*
+\begin{readmore}
+Most of the HOL-specific operations on terms and types are defined
+in @{ML_file "HOL/Tools/hologic.ML"}.
+\end{readmore}
 *}
 section {* Constants *}
 text {*
 use the commands \isacommand{method\_setup} for installing methods in the
 current theory and \isacommand{simproc\_setup} for adding new simprocs to
 the current simpset.
 *}
-section {* Theorem Attributes *}
+section {* Theorem Attributes\label{sec:attributes} *}
 text {*
 Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text
 "[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
 annotated to theorems, but functions that do further processing once a

changeset 292	41a802bbb7df
parent 290	6af069ab43d4
child 293	0a567f923b42