--- a/ProgTutorial/General.thy Wed Oct 14 02:32:53 2009 +0200
+++ b/ProgTutorial/General.thy Wed Oct 14 12:33:38 2009 +0200
@@ -779,8 +779,7 @@
final statement of the theorem.
@{ML_response_fake [display, gray]
- "string_of_thm @{context} my_thm
-|> tracing"
+ "tracing (string_of_thm @{context} my_thm)"
"\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
However, internally the code-snippet constructs the following
@@ -801,7 +800,7 @@
While we obtained a theorem as result, this theorem is not
yet stored in Isabelle's theorem database. Consequently, it cannot be
- referenced later on. One way to store it in the theorem database is
+ referenced on the user level. One way to store it in the theorem database is
by using the function @{ML_ind note in LocalTheory}.
*}
@@ -811,14 +810,15 @@
text {*
The first argument @{ML_ind theoremK in Thm} is a kind indicator, which
- classifies the theorem. For a theorem arising from a definition we should
- use @{ML_ind definitionK in Thm}, for an axiom @{ML_ind axiomK in Thm}, for
- ``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK
- in Thm}. The second argument is the name under which we store the theorem
- or theorems. The third can contain a list of (theorem) attributes. We will
- explain them in detail in Section~\ref{sec:attributes}. Below we
- use such an attribute in order add the theorem to the simpset.
- have to declare:
+ 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}, 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. We will explain them 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 {*
@@ -827,11 +827,13 @@
[Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
text {*
- Note that we have to use another name for the theorem, since Isabelle does
- not allow to store another theorem 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 the previous chapter, we can check
- whether the theorem has actually been added.
+ Note that we have to use another name under which the theorem is stored,
+ since Isabelle does not allow us to store another theorem 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
+ the previous chapter, we can check whether the theorem has actually been
+ added.
+
@{ML_response [display,gray]
"let
@@ -853,14 +855,14 @@
or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. As can be seen
the theorem does not have any meta-variables that would be present if we proved
- this theorem on the user-level. We will see later on, we have to construct
- meta-variables in a theorem explicitly.
+ this theorem on the user-level. We will see later on that usually we have to
+ construct meta-variables in theorems explicitly.
*}
text {*
There is a multitude of functions that manage or manipulate theorems. For example
- we can test theorems for (alpha) equality. Suppose you proved the following three
- facts.
+ we can test theorems for alpha equality. Suppose you proved the following three
+ theorems.
*}
lemma
@@ -869,7 +871,7 @@
and thm3: "\<forall>y. Q y" sorry
text {*
- Testing for equality using the function @{ML_ind eq_thm in Thm} produces:
+ Testing them for alpha equality using the function @{ML_ind eq_thm in Thm} produces:
@{ML_response [display,gray]
"(Thm.eq_thm (@{thm thm1}, @{thm thm2}),
@@ -885,10 +887,9 @@
val eq = @{thm True_def}
in
(Thm.lhs_of eq, Thm.rhs_of eq)
- |> pairself (tracing o string_of_cterm @{context})
+ |> pairself (string_of_cterm @{context})
end"
- "True
-(\<lambda>x. x) = (\<lambda>x. x)"}
+ "(True, (\<lambda>x. x) = (\<lambda>x. x))"}
Other function produce terms that can be pattern-matched.
Suppose the following two theorems.
@@ -899,16 +900,14 @@
and foo_test2: "A \<longrightarrow> B \<longrightarrow> C" sorry
text {*
- We can deconstruct them into premises and conclusions as follows.
+ We can destruct them into premises and conclusions as follows.
@{ML_response_fake [display,gray]
"let
val ctxt = @{context}
fun prems_and_concl thm =
- [\"Premises: \" ^
- (string_of_terms ctxt (Thm.prems_of thm))] @
- [\"Conclusion: \" ^
- (string_of_term ctxt (Thm.concl_of thm))]
+ [\"Premises: \" ^ (string_of_terms ctxt (Thm.prems_of thm))] @
+ [\"Conclusion: \" ^ (string_of_term ctxt (Thm.concl_of thm))]
|> cat_lines
|> tracing
in
@@ -1080,59 +1079,6 @@
oops
-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 function 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_ind add_consts_i in Sign}.
- 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 "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 on the Isabelle level using the command \isacommand{term}
-
- \begin{isabelle}
- \isacommand{term}~@{text [quotes] "BAR"}\\
- @{text "> \"BAR\" :: \"'a\""}
- \end{isabelle}
-
- you do not obtain a constant of type @{typ nat}, but a free variable (printed in
- 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 "BAR"}, @{typ "nat"}, NoSyn)] *}
-
-text {*
- Now
-
- \begin{isabelle}
- \isacommand{term}~@{text [quotes] "BAR"}\\
- @{text "> \"BAR\" :: \"nat\""}
- \end{isabelle}
-
- returns a (black) constant with the type @{typ nat}.
-
- A similar command is \isacommand{local\_setup}, which expects a function
- of type @{ML_type "local_theory -> local_theory"}. Later on we will also
- use the commands \isacommand{method\_setup} for installing methods in the
- current theory and \isacommand{simproc\_setup} for adding new simprocs to
- the current simpset.
-*}
-
section {* Theorem Attributes\label{sec:attributes} *}
text {*
@@ -1358,7 +1304,58 @@
\end{readmore}
*}
+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 function 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_ind add_consts_i in Sign}.
+ 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 "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 on the Isabelle level using the command \isacommand{term}
+
+ \begin{isabelle}
+ \isacommand{term}~@{text [quotes] "BAR"}\\
+ @{text "> \"BAR\" :: \"'a\""}
+ \end{isabelle}
+
+ you do not obtain a constant of type @{typ nat}, but a free variable (printed in
+ 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 "BAR"}, @{typ "nat"}, NoSyn)] *}
+
+text {*
+ Now
+
+ \begin{isabelle}
+ \isacommand{term}~@{text [quotes] "BAR"}\\
+ @{text "> \"BAR\" :: \"nat\""}
+ \end{isabelle}
+
+ returns a (black) constant with the type @{typ nat}.
+
+ A similar command is \isacommand{local\_setup}, which expects a function
+ of type @{ML_type "local_theory -> local_theory"}. Later on we will also
+ use the commands \isacommand{method\_setup} for installing methods in the
+ current theory and \isacommand{simproc\_setup} for adding new simprocs to
+ the current simpset.
+*}
section {* Theories (TBD) *}