--- a/ProgTutorial/General.thy Tue Oct 13 22:57:25 2009 +0200
+++ b/ProgTutorial/General.thy Wed Oct 14 02:32:53 2009 +0200
@@ -11,7 +11,7 @@
(*>*)
-chapter {* Isabelle in More Detail \mbox{or, the Good, the Bad and the Ugly} *}
+chapter {* Isabelle in More Detail *}
text {*
Isabelle is build around a few central ideas. One central idea is the
@@ -693,7 +693,7 @@
val zero = @{term \"0::nat\"}
in
cterm_of @{theory}
- (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
+ (Const (@{const_name plus}, [natT, natT] ---> natT) $ zero $ zero)
end" "0 + 0"}
In Isabelle not just terms need to be certified, but also types. For example,
@@ -779,7 +779,8 @@
final statement of the theorem.
@{ML_response_fake [display, gray]
- "string_of_thm @{context} my_thm |> tracing"
+ "string_of_thm @{context} my_thm
+|> tracing"
"\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
However, internally the code-snippet constructs the following
@@ -811,24 +812,26 @@
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
- state @{ML_ind definitionK in Thm}, instead. The second argument is the
- name under which we store the theorem or theorems. The third can contain
- a list of (theorem) attributes. Above it is empty, but if we want to store
- the theorem and at the same time add it to the simpset we have to declare:
+ 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:
*}
local_setup %gray {*
LocalTheory.note Thm.theoremK
- ((@{binding "my_thm_simp"},
- [Attrib.internal (K Simplifier.simp_add)]),
- [my_thm]) #> snd *}
+ ((@{binding "my_thm_simp"},
+ [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 add another theorem under the same name. The attribute can be
- given @{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 been added.
+ 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.
@{ML_response [display,gray]
"let
@@ -838,20 +841,23 @@
end"
"true"}
- Now the theorems @{thm [source] my_thm} and @{thm [source] my_thm_simp} can
- also be referenced with the \isacommand{thm}-command on the user-level of
- Isabelle
+ The main point of storing the theorems @{thm [source] my_thm} and @{thm
+ [source] my_thm_simp} is that they can now also be referenced with the
+ \isacommand{thm}-command on the user-level of Isabelle
+
\begin{isabelle}
\isacommand{thm}~@{text "my_thm"}\isanewline
@{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
\end{isabelle}
- or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Note that the
- theorem does not have any meta-variables that would be present if we proved
- this theorem on the user-level. As we shall see later on, we have to construct
- meta-variables explicitly.
+ 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.
+*}
+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.
@@ -922,6 +928,16 @@
@{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
+ this we build the theorem @{term "True \<equiv> True"} (Line 1) and then
+ unfold the constant according to its definition (Line 2).
+
+ @{ML_response_fake [display,gray,linenos]
+ "Thm.reflexive @{cterm \"True\"}
+ |> Simplifier.rewrite_rule [@{thm True_def}]
+ |> string_of_thm @{context}
+ |> tracing"
+ "(\<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. For example, the function @{ML_ind rulify in ObjectLogic}
@@ -946,10 +962,32 @@
In this code the function @{ML atomize in ObjectLogic} produces
a meta-equation between the given theorem and the theorem transformed
- into the object logic. The function @{ML_ind rewrite_rule in MetaSimplifier}
- unfolds this meta-equation in the given theorem. The result is
- the theorem with object logic connectives.
-x
+ 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}
+
+ @{thm [display] list.induct}
+
+ we have to first abstract over the variables @{text "?P"} and
+ @{text "?list"}. For this we can use the function
+ @{ML_ind forall_intr_vars in Drule}.
+*}
+
+ML{*fun atomize_thm thm =
+let
+ val thm' = forall_intr_vars thm
+ val thm'' = ObjectLogic.atomize (cprop_of thm')
+in
+ MetaSimplifier.rewrite_rule [thm''] thm'
+end*}
+
+text {*
+ For @{thm [source] list.induct} it produces:
+
+ @{ML_response_fake [display, gray]
+ "atomize_thm @{thm list.induct}"
+ "\<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}.
For example