--- a/CookBook/FirstSteps.thy Wed Mar 18 03:27:15 2009 +0100
+++ b/CookBook/FirstSteps.thy Wed Mar 18 18:27:48 2009 +0100
@@ -557,32 +557,31 @@
While antiquotations are very convenient for constructing terms, they can
only construct fixed terms (remember they are ``linked'' at compile-time).
However, you often need to construct terms dynamically. For example, a
- function that returns the implication @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking
- @{term P}, @{term Q} and the type @{term "\<tau>"} as arguments can only be
- written as:
+ function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking
+ @{term P} and @{term Q} as arguments can only be written as:
*}
-ML{*fun make_imp P Q tau =
+ML{*fun make_imp P Q =
let
- val x = Free ("x", tau)
+ val x = Free ("x", @{typ nat})
in
Logic.all x (Logic.mk_implies (P $ x, Q $ x))
end *}
text {*
- The reason is that you cannot pass the arguments @{term P}, @{term Q} and
- @{term "tau"} into an antiquotation. For example the following does \emph{not} work.
+ The reason is that you cannot pass the arguments @{term P} and @{term Q}
+ into an antiquotation. For example the following does \emph{not} work.
*}
-ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}
+ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
text {*
- To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"}
+ To see this apply @{text "@{term S}"} and @{text "@{term T}"}
to both functions. With @{ML make_imp} we obtain the intended term involving
the given arguments
- @{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}"
+ @{ML_response [display,gray] "make_imp @{term S} @{term T}"
"Const \<dots> $
Abs (\"x\", Type (\"nat\",[]),
Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}
@@ -590,48 +589,17 @@
whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"}
and @{text "Q"} from the antiquotation.
- @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}"
+ @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}"
"Const \<dots> $
Abs (\"x\", \<dots>,
Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
(Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
(FIXME: handy functions for constructing terms: @{ML list_comb}, @{ML lambda})
-
-
- 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:
+*}
-*}
-
-ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *}
-
-text {* This can be equally written with the combinator @{ML "-->"} as: *}
-
-ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
text {*
- A handy function for manipulating terms is @{ML map_types}: it takes a
- function and applies it to every type in a term. You can, for example,
- 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 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\")"}
-
\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
@@ -752,8 +720,42 @@
\begin{readmore}
Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
functions about signatures in @{ML_file "Pure/sign.ML"}.
-
\end{readmore}
+
+ 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:
+
+*}
+
+ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *}
+
+text {* This can be equally written with the combinator @{ML "-->"} as: *}
+
+ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
+
+text {*
+ A handy function for manipulating terms is @{ML map_types}: it takes a
+ function and applies it to every type in a term. You can, for example,
+ 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 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: readmore about types)
*}
@@ -797,7 +799,7 @@
(Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
end" "0 + 0"}
- In Isabelle not just types need to be certified, but also types. For example,
+ In Isabelle not just terms need to be certified, but also types. For example,
you obtain the certified type for the Isablle type @{typ "nat \<Rightarrow> bool"} on
the ML-level as follows:
@@ -1183,23 +1185,23 @@
text {*
In the previous section we used \isacommand{setup} in order to make
a theorem attribute known to Isabelle. What happens behind the scenes
- is that \isacommand{setup} expects a functions from @{ML_type theory}
- to @{ML_type theory}: the input theory is the current theory and the
+ is that \isacommand{setup} expects a functions of type
+ @{ML_type "theory -> theory"}: the input theory is the current theory and the
output the theory where the theory attribute has been stored.
This is a fundamental principle in Isabelle. A similar situation occurs
for example with declaring constants. The function that declares a
- constant on the ML-level is @{ML Sign.add_consts_i}. Recall that ML-code
- needs to be \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.
- If you write
+ constant on the ML-level is @{ML Sign.add_consts_i}.
+ If you write\footnote{Recall that ML-code needs to be
+ enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
*}
-ML{*Sign.add_consts_i [(Binding.name "BAR", @{typ "nat"}, NoSyn)] @{theory} *}
+ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
text {*
for declaring the constant @{text "BAR"} with type @{typ nat} and
run the code, then you indeed obtain a theory as result. But if you
- query the constant with \isacommand{term}
+ query the constant on the Isabelle level using the command \isacommand{term}
\begin{isabelle}
\isacommand{term}~@{text [quotes] "BAR"}\\
@@ -1212,7 +1214,7 @@
\isacommand{setup} is for. The constant is properly declared with
*}
-setup %gray {* Sign.add_consts_i [(Binding.name "BAR", @{typ "nat"}, NoSyn)] *}
+setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}
text {*
Now
@@ -1266,7 +1268,7 @@
(*
setup {*
Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)]
- #> PureThy.add_defs false [((Binding.name "foo_def",
+ #> PureThy.add_defs false [((@{binding "foo_def"},
Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])]
#> snd
*}