--- a/CookBook/FirstSteps.thy Tue Feb 17 02:12:19 2009 +0000
+++ b/CookBook/FirstSteps.thy Tue Feb 17 13:53:54 2009 +0000
@@ -223,6 +223,7 @@
the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
binds the corresponding variable. However, in Isabelle the names of bound variables are
kept at abstractions for printing purposes, and so should be treated only as comments.
+ Application in Isabelle is realised with the term-constructor @{ML $}.
\begin{readmore}
Terms are described in detail in \isccite{sec:terms}. Their
@@ -429,13 +430,15 @@
(FIXME: @{text "ctyp_of"}, @{ML fastype_of}, @{text dummyT})
+ (FIXME: say something about constants and variables having types as
+ arguments and how they can be constructed with fast-type and dummT)
*}
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
+ pattern matching terms or constructing terms. While it is perfectly ok
to write the function @{text is_true} as follows
*}
@@ -451,12 +454,12 @@
| is_all _ = false*}
text {*
- will not correctly match:
+ will not correctly match the formula @{prop "\<forall>x::nat. P x"}:
@{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
+ fixes the type of the constant @{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
*}
@@ -469,42 +472,46 @@
@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
- matches correctly.
+ matches correctly (the wildcard in the pattern matches any type).
- However there is still a problem: consider the function that attempts to
- pick out a @{text "Nil"}-term:
+ However there is still a problem: consider the similar 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
+ Unfortunately, also this function does \emph{not} work as expected, 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
+ The problem is that on the ML-level the name of a constant is more
+ subtle as you might expect. The function @{ML is_all} worked correctly,
+ because @{term "All"} is such a fundamental constant, which can be referenced
+ by @{ML "Const (\"All\", some_type)" for some_type}. However, 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
+ @{text "Nil"} is defined (@{text "List"}) and also in which datatype
+ (@{text "list"}). Even worse, some constants have a name involving
+ type-classes. Consider for example the constants for @{term "zero"}
+ and @{term "(op *)"}:
@{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
+ While you could use the complete name, for example
+ @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, 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
+ 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.
+ variable parts of the constant's name. Therefore a functions for
+ matching against constants that have a polymorphic type should
+ be written as follows.
*}
ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
@@ -512,9 +519,9 @@
| 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:
+ Note that you also frequently have to calculate what the
+ ``base'' name of a given constant is. For this you can use
+ the function @{ML Sign.base_name}. For example:
(FIXME is there an example for that statement?)
@@ -597,14 +604,6 @@
(FIXME: how to add case-names to goal states)
*}
-section {* Theories and Local Theories *}
-
-section {* Storing Theorems *}
-
-text {* @{ML PureThy.add_thms_dynamic} *}
-
-section {* Theorem Attributes *}
-
section {* Printing Terms and Theorems\label{sec:printing} *}
text {*
@@ -657,6 +656,14 @@
ML{*fun str_of_thms ctxt thms =
commas (map (str_of_thm ctxt) thms)*}
+section {* Theorem Attributes *}
+
+section {* Theories and Local Theories *}
+
+section {* Storing Theorems *}
+
+text {* @{ML PureThy.add_thms_dynamic} *}
+
section {* Combinators\label{sec:combinators} *}