isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:043ef82000b4
+:371e4375c994
 text {*
 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
+function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking
-@{term P}, @{term Q} and the type @{term "\<tau>"} as arguments can only be
+@{term P} and @{term Q} as arguments can only be written as:
-written as:
+*}
-*}
+ML{*fun make_imp P Q =
-ML{*fun make_imp P Q tau =
 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
+The reason is that you cannot pass the arguments @{term P} and @{term Q}
-@{term "tau"} into an antiquotation. For example the following does \emph{not} work.
+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>))"}
 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
+text {*
-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
 and types easier.\end{readmore}
 strips off all qualifiers.
 \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)
 *}
 section {* Type-Checking *}
 in
 cterm_of @{theory}
 (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:
 @{ML_response_fake [display,gray]
 "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
 section {* Setups (TBD) *}
 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}
+is that \isacommand{setup} expects a functions of type
-to @{ML_type theory}: the input theory is the current theory and the
+@{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
+constant on the ML-level is @{ML Sign.add_consts_i}.
-needs to be \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.
+If you write\footnote{Recall that ML-code  needs to be
-If you write
+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"}\\
 @{text "> \"BAR\" :: \"'a\""}
 \end{isabelle}
 blue) of polymorphic type. The problem is that the ML-expression above did
 not register the declaration with the current theory. This is what the command
 \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
 \begin{isabelle}
 oops
 (*
 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
 *}
 *)
 (*

changeset 186	371e4375c994
parent 185	043ef82000b4
child 188	8939b8fd8603