--- a/ProgTutorial/FirstSteps.thy Mon Jul 27 10:37:28 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Tue Jul 28 08:53:05 2009 +0200
@@ -574,8 +574,14 @@
(?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
- function that extracts the theorem names stored in a simpset.
+ 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: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 =
@@ -596,21 +602,21 @@
"[\"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
- LocalTheory}. This function is below used to define the constant @{term
- "TrueConj"} as the conjunction
- @{term "True \<and> True"}.
+ An example where a qualified name is needed is the function
+ @{ML [index] define in LocalTheory}. This function is used below to define
+ the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
*}
local_setup %gray {*
@@ -630,38 +636,52 @@
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
- in order to avoid explicit bindings of theorems such as:
+ It is also possible to define your own antiquotations. But you should
+ 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.
+ A restriction of this antiquotation is that it does not allow you to
+ use schematic variables. If you want a antiquotation that does not
+ have this restriction, you can implement your own using the
+ function @{ML [index] ML_Antiquote.inline}.
*}
-ML{*val allI = thm "allI" *}
-
-text {*
- Such bindings are difficult to maintain and can be overwritten by the
- 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
- 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"
+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))*}
-ML{*@{term_pat "?x + ?y"}*}
-
text {*
+ We call the 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);
+ 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 *}
@@ -878,7 +898,7 @@
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"}),
@@ -889,7 +909,7 @@
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.
@@ -899,21 +919,29 @@
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"}
- the subterm @{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0"} by @{term y}, and @{term x} by @{term True}.
+ @{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}.
@{ML_response_fake [display,gray]
-"subst_free [(@{term \"(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0\"}, @{term \"y::nat\<Rightarrow>nat\"}),
- (@{term \"x::nat\"}, @{term \"True\"})]
- @{term \"((f::nat\<Rightarrow>nat\<Rightarrow>nat) 0) x\"}"
+"let
+ val s1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
+ 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\"})]
- @{term \"(\<lambda>x::nat. x)\"}"
+"let
+ 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
@@ -927,6 +955,13 @@
"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 {*
@@ -1399,7 +1434,7 @@
the current simpset.
*}
-section {* Theorem Attributes *}
+section {* Theorem Attributes\label{sec:attributes} *}
text {*
Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text
--- a/ProgTutorial/Tactical.thy Mon Jul 27 10:37:28 2009 +0200
+++ b/ProgTutorial/Tactical.thy Tue Jul 28 08:53:05 2009 +0200
@@ -1994,7 +1994,9 @@
variable that is abstracted and a context). The conversion that goes under
an application is @{ML [index] combination_conv in Conv}. It expects two
conversions as arguments, each of which is applied to the corresponding
- ``branch'' of the application.
+ ``branch'' of the application. An abbreviation for this conversion is the
+ function @{ML [index] comb_conv in Conv}, which applies the same conversion
+ to both branches.
We can now apply all these functions in a conversion that recursively
descends a term and applies a ``@{thm [source] true_conj1}''-conversion
@@ -2006,8 +2008,7 @@
@{term "op \<and>"} $ @{term True} $ _ =>
(Conv.arg_conv (all_true1_conv ctxt) then_conv
Conv.rewr_conv @{thm true_conj1}) ctrm
- | _ $ _ => Conv.combination_conv
- (all_true1_conv ctxt) (all_true1_conv ctxt) ctrm
+ | _ $ _ => Conv.comb_conv (all_true1_conv ctxt) ctrm
| Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm
| _ => Conv.all_conv ctrm*}
@@ -2038,8 +2039,7 @@
case Thm.term_of ctrm of
Const (@{const_name If}, _) $ _ =>
Conv.arg_conv (all_true1_conv ctxt) ctrm
- | _ $ _ => Conv.combination_conv
- (if_true1_conv ctxt) (if_true1_conv ctxt) ctrm
+ | _ $ _ => Conv.comb_conv (if_true1_conv ctxt) ctrm
| Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm
| _ => Conv.all_conv ctrm *}