--- a/ProgTutorial/General.thy Mon Oct 19 02:02:21 2009 +0200
+++ b/ProgTutorial/General.thy Mon Oct 19 14:10:42 2009 +0200
@@ -598,7 +598,7 @@
Make sure you use the functions defined in @{ML_file "HOL/Tools/hologic.ML"}
for constructing the terms for the logical connectives.\footnote{Thanks to Roy
- Dyckhoff for this exercise.}
+ Dyckhoff for suggesting this exercise and working out the details.}
\end{exercise}
*}
@@ -825,7 +825,7 @@
yet stored in Isabelle's theorem database. Consequently, it cannot be
referenced on the user level. One way to store it in the theorem database is
by using the function @{ML_ind note in LocalTheory}.\footnote{\bf FIXME: make sure a pointer
- to the section about local-setup is given eralier.}
+ to the section about local-setup is given earlier.}
*}
local_setup %gray {*
@@ -833,16 +833,17 @@
((@{binding "my_thm"}, []), [my_thm]) #> snd *}
text {*
- The first argument @{ML_ind theoremK in Thm} is a kind indicator, which
- classifies the theorem. There are several such kind indicators: for a
- theorem arising from a definition we should use @{ML_ind definitionK in
- Thm}, for an axiom @{ML_ind axiomK in Thm}, and for ``normal'' theorems the
- kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK in Thm}. The second
- argument of @{ML note in LocalTheory} is the name under which we store the
- theorem or theorems. The third argument can contain a list of theorem
- attributes, which we will explain in detail in Section~\ref{sec:attributes}.
- Below we just use one such attribute in order add
- the theorem to the simpset:
+ The fourth argument of @{ML note in LocalTheory} is the list of theorems we
+ want to store under a name. The first argument @{ML_ind theoremK in Thm} is
+ a kind indicator, which classifies the theorem. There are several such kind
+ indicators: for a theorem arising from a definition you should use @{ML_ind
+ definitionK in Thm}, for an axiom @{ML_ind axiomK in Thm}, and for
+ ``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK
+ in Thm}. The second argument of @{ML note in LocalTheory} is the name under
+ which we store the theorem or theorems. The third argument can contain a
+ list of theorem attributes, which we will explain in detail in
+ Section~\ref{sec:attributes}. Below we just use one such attribute in order
+ add the theorem to the simpset:
*}
local_setup %gray {*
@@ -852,9 +853,10 @@
text {*
Note that we have to use another name under which the theorem is stored,
- since Isabelle does not allow us to store two theorems under the same
- name. The attribute needs to be wrapped inside the function @{ML_ind
- internal in Attrib}. If we use the function @{ML get_thm_names_from_ss} from
+ since Isabelle does not allow us to call @{ML_ind note in LocalTheory} twice
+ with the same name. The attribute needs to be wrapped inside the function @{ML_ind
+ internal in Attrib} from the structure @{ML_struct Attrib}. If we use the function
+ @{ML get_thm_names_from_ss} from
the previous chapter, we can check whether the theorem has actually been
added.
@@ -954,7 +956,7 @@
@{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}.
\end{readmore}
- The simplifier can be used to unfold definition in theorms. To show
+ The simplifier can be used to unfold definition in theorems. To show
this we build the theorem @{term "True \<equiv> True"} (Line 1) and then
unfold the constant @{term "True"} according to its definition (Line 2).
@@ -966,12 +968,14 @@
"(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}
Often it is necessary to transform theorems to and from the object
- logic, that is eplacing all @{text "\<longrightarrow>"} and @{text "\<forall>"} with @{text "\<Longrightarrow>"}
- and @{text "\<And>"}, respectively. A reason for such transformations is
- that definitions can only be stated using object logic connectives, while
- theorems using the connectives from the meta logic are more convenient for
- reasoning. The function @{ML_ind rulify in ObjectLogic} replaces all
- object connectives by equivalents in the meta logic. For example
+ logic, that is replacing all @{text "\<longrightarrow>"} and @{text "\<forall>"} by @{text "\<Longrightarrow>"}
+ and @{text "\<And>"}, or the other way around. A reason for such a transformation
+ might be stating a definition. The reason is that definitions can only be
+ stated using object logic connectives, while theorems using the connectives
+ from the meta logic are more convenient for reasoning. Therefore there are
+ some build in functions which help with these transformations. The function
+ @{ML_ind rulify in ObjectLogic}
+ replaces all object connectives by equivalents in the meta logic. For example
@{ML_response_fake [display, gray]
"ObjectLogic.rulify @{thm foo_test2}"
@@ -993,12 +997,13 @@
a meta-equation between the given theorem and the theorem transformed
into the object logic. The result is the theorem with object logic
connectives. However, in order to completely transform a theorem
- such as @{thm [source] list.induct}, which is of the form
+ involving meta variables, such as @{thm [source] list.induct}, which
+ is of the form
@{thm [display] list.induct}
we have to first abstract over the meta variables @{text "?P"} and
- @{text "?list"} in the theorem. For this we can use the function
+ @{text "?list"}. For this we can use the function
@{ML_ind forall_intr_vars in Drule}. This allows us to implement the
following function for atomizing a theorem.
*}
@@ -1019,9 +1024,9 @@
"\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
Theorems can also be produced from terms by giving an explicit proof.
- One way to achive this is by using the function @{ML_ind prove in Goal}
- in the structure @{ML_struct Goal}. For example below we prove the term
- @{term "P \<Longrightarrow> P"}.
+ One way to achieve this is by using the function @{ML_ind prove in Goal}
+ in the structure @{ML_struct Goal}. For example below we use this function
+ to prove the term @{term "P \<Longrightarrow> P"}.
@{ML_response_fake [display,gray]
"let
@@ -1035,28 +1040,32 @@
This function takes first a context and second a list of strings. This list
specifies which variables should be turned into meta-variables once the term
is proved. The fourth argument is the term to be proved. The fifth is a
- corresponding proof given in form of a tactic. We explain tactics in
- Chapter~\ref{chp:tactical}. In the code above, the tactic proves the theorem
- by assumption.
+ corresponding proof given in form of a tactic (we explain tactics in
+ Chapter~\ref{chp:tactical}). In the code above, the tactic proves the theorem
+ by assumption. As before this code will produce a theorem, but the theorem
+ is not yet stored in the theorem database.
Theorems also contain auxiliary data, such as the name of the theorem, its
kind, the names for cases and so on. This data is stored in a string-string
list and can be retrieved with the function @{ML_ind get_tags in
- Thm}. Assume the following lemma.
+ Thm}. Assume you prove the following lemma.
*}
-lemma foo_data: "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
+lemma foo_data:
+ shows "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
text {*
- So far the the auxiliary data of this lemma is:
+ The auxiliary data of this lemma can be retrieved using the function
+ @{ML_ind get_tags in Thm}. So far the the auxiliary data of this lemma is
@{ML_response_fake [display,gray]
"Thm.get_tags @{thm foo_data}"
"[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}
- When we store lemmas in the theorem database, we may want to explicitly extend
- this data by attaching case names to the two premises of the lemma. This can
- be achieved with the function @{ML_ind name in RuleCases}.
+ consisting of a name and a kind. When we store lemmas in the theorem database,
+ we might want to explicitly extend this data by attaching case names to the
+ two premises of the lemma. This can be done with the function @{ML_ind name in RuleCases}
+ from the structure @{ML_struct RuleCases}.
*}
local_setup %gray {*
@@ -1073,8 +1082,8 @@
"[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"),
(\"case_names\", \"foo_case_one;foo_case_two\")]"}
- You can notice the case names on the user level when using the proof
- methods @{ML_text cases} and @{ML_text induct}. In the proof below
+ You can observe the case names of this lemma on the user level when using
+ the proof methods @{ML_text cases} and @{ML_text induct}. In the proof below
*}
lemma
@@ -1093,8 +1102,8 @@
\end{tabular}*}
text {*
- we can proceed by analysing the cases @{text "foo_case1"} and
- @{text "foo_case2"}. While if the theorem has no names, then
+ we can proceed by analysing the cases @{text "foo_case_one"} and
+ @{text "foo_case_two"}. While if the theorem has no names, then
the cases have standard names @{text 1}, @{text 2} and so
on. This can be seen in the proof below.
*}
@@ -1117,56 +1126,102 @@
text {*
One great feature of Isabelle is its document preparation system, where
- proved theorems can be quoted in the text directly from the formalisation.
- This helps minimises cut-and-paste errors. However, sometimes the verbatim
- quoting is not what is wanted. For such situations Isabelle allows the
- installation of \emph{styles}. These are, roughly speaking, functions from
- terms to terms. The input term stands for the theorem to be presented.
- Let us assume we want to display theorems without leading quantifiers.
- For this we can implement the following function that strips off
- meta-quantifiers.
+ proved theorems can be quoted in documents referencing directly their
+ formalisation. This helps tremendously to minimise cut-and-paste errors. However,
+ sometimes the verbatim quoting is not what is wanted or what can be shown to
+ readers. For such situations Isabelle allows the installation of \emph{theorem
+ styles}. These are, roughly speaking, functions from terms to terms. The input
+ term stands for the theorem to be presented; the output can be constructed to
+ ones wishes. Let us, for example, assume we want to quote theorems without
+ leading @{text \<forall>}-quantifiers. For this we can implement the following function
+ that strips off meta-quantifiers.
*}
-ML {*fun strip_all (Const (@{const_name "All"}, _) $ Abs body) =
- Term.dest_abs body |> snd |> strip_all
- | strip_all (Const (@{const_name "Trueprop"}, _) $ t) = strip_all t
- | strip_all t = t*}
-
-ML {* strip_all @{term "\<forall>x y z. P x y z"}*}
+ML %linenosgray {*fun strip_all_qnt (Const (@{const_name "All"}, _) $ Abs body) =
+ Term.dest_abs body |> snd |> strip_all_qnt
+ | strip_all_qnt (Const (@{const_name "Trueprop"}, _) $ t) =
+ strip_all_qnt t
+ | strip_all_qnt t = t*}
text {*
- Now we can install this function as the theorem style named
- @{text "strip_all"}.
+ We use in Line 2 the function @{ML_ind dest_abs in Term} for deconstructing abstractions,
+ since this function deals correctly with potential name clashes. This function produces
+ a pair consisting of the variable and the body of the abstraction. We are only interested
+ in the body, which we feed into the recursive call. In Line 3 and 4, we also
+ have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can
+ install this function as the theorem style named @{text "my_strip_all_qnt"}.
*}
setup %gray {*
- Term_Style.setup "strip_all" (Scan.succeed (K strip_all))
+ Term_Style.setup "my_strip_all_qnt" (Scan.succeed (K strip_all_qnt))
*}
text {*
- We can test the theorem style with the following theorem
+ We can test this theorem style with the following theorem
*}
theorem style_test:
shows "\<forall>x y z. (x, x) = (y, z)" sorry
text {*
- Now printing out the theorem @{thm [source] style_test} normally
- in a document produces
+ Now printing out in a document the theorem @{thm [source] style_test} normally
+ using @{text "@{thm \<dots>}"} produces
- @{thm [display] style_test}
+ \begin{isabelle}
+ @{text "@{thm style_test}"}\\
+ @{text ">"}~@{thm style_test}
+ \end{isabelle}
- as expected. But with the theorem style @{text "@{thm (strip_all) \<dots>}"}
+ as expected. But with the theorem style @{text "@{thm (my_strip_all_qnt) \<dots>}"}
we obtain
- @{thm [display] (strip_all) style_test}
+ \begin{isabelle}
+ @{text "@{thm (my_strip_all_qnt) style_test}"}\\
+ @{text ">"}~@{thm (my_strip_all_qnt) style_test}\\
+ \end{isabelle}
- without the leading quantifiers. Such theorem styles allow one to
- print out theorems in documents formatted in any way wanted. Next we
- explain theorem attributes, which is another mechanism for treating
- theorems.
+ without the leading quantifiers. We can improve this theorem style by explicitly
+ giving a list of strings that should be used for the replacement of the
+ variables. For this we implement the function which takes a list of strings
+ and uses them as name in the outermost abstractions.
+*}
+
+ML {*fun rename_all [] t = t
+ | rename_all (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) =
+ Const (@{const_name "All"}, U) $ Abs (x, T, rename_all xs t)
+ | rename_all xs (Const (@{const_name "Trueprop"}, U) $ t) =
+ rename_all xs t
+ | rename_all _ t = t*}
+
+text {*
+ We can now install a the modified theorem style as follows
*}
+setup %gray {*
+let
+ val parser = Scan.repeat Args.name
+ fun action xs = K (rename_all xs #> strip_all_qnt)
+in
+ Term_Style.setup "my_strip_all_qnt2" (parser >> action)
+end *}
+
+text {*
+ We can now suggest, for example, two variables for stripping
+ off the @{text \<forall>}-quantifiers, namely:
+
+ \begin{isabelle}
+ @{text "@{thm (my_strip_all_qnt2 x' x'') style_test}"}\\
+ @{text ">"}~@{thm (my_strip_all_qnt2 x' x'') style_test}
+ \end{isabelle}
+
+ Such theorem styles allow one to print out theorems in documents formatted to
+ ones heart content. Next we explain theorem attributes, which is another
+ mechanism for dealing with theorems.
+
+ \begin{readmore}
+ Theorem styles are implemented in @{ML_file "Pure/Thy/term_style.ML"}.
+ \end{readmore}
+*}
section {* Theorem Attributes\label{sec:attributes} *}