--- a/ProgTutorial/Recipes/Introspection.thy Tue Jun 19 15:04:00 2012 +0100
+++ b/ProgTutorial/Recipes/Introspection.thy Tue Jun 19 17:27:10 2012 +0100
@@ -12,7 +12,8 @@
{\bf Solution:} They can be obtained by introspecting the theorem.\smallskip
To introspect a theorem, let us define the following three functions that
- analyse the @{ML_type proof_body} data-structure from @{ML_struct Proofterm}.
+ analyse the @{ML_type proof_body} data-structure from the structure
+ @{ML_struct Proofterm}.
*}
ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms
@@ -20,7 +21,7 @@
val get_pbodies = map (Future.join o #3) o pthms_of *}
text {*
- To see what their purpose is, consider the following two short proofs.
+ To see what their purpose is, consider the following three short proofs.
*}
lemma my_conjIa:
@@ -37,14 +38,19 @@
apply(assumption)
done
+lemma my_conjIc:
+ shows "A \<and> B \<Longrightarrow> A \<and> B"
+apply(auto)
+done
+
text {*
- While the theorems used in these proofs is obvious, in general it
- is not obvious, because of automated provers that can be part of a
- proof. Fortunately, ``behind'' every completed proof is a tree of
- theorems that records all theorems that are employed for establishing
- theorems like @{thm [source] my_conjIa}. We can traverse this tree
- once a theorem is established. Let us first extract the name of the
- established theorem from this tree. This can be done with
+ While the information about which theorems are used is obvious in
+ the first two proofs, it is not obvious in the third, because of the
+ @{text auto}-step. Fortunately, ``behind'' every proved theorem is
+ a proof-tree that records all theorems that are employed for
+ establishing this theorem. We can traverse this proof-tree
+ extracting this information. Let us first extract the name of the
+ established theorem. This can be done with
@{ML_response [display,gray]
"@{thm my_conjIa}
@@ -52,10 +58,13 @@
|> get_names"
"[\"Introspection.my_conjIa\"]"}
- whereby @{text "Introspection"} refers to the theory name in which we established
- @{thm [source] my_conjIa}. Notice that the apply-proof of this theorem references
- three other theorems. We can obtain them by descending into the first level of the
- proof-tree, as follows.
+ whereby @{text "Introspection"} refers to the theory name in which
+ we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
+ proof_body_of in Thm} returns a part of the data that is stored in a
+ theorem. Notice that the apply-proof of this theorem references
+ three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1}
+ and @{thm [source] conjunct2}. We can obtain them by descending into the
+ first level of the proof-tree, as follows.
@{ML_response [display,gray]
"@{thm my_conjIa}
@@ -66,8 +75,8 @@
"[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\",
\"Pure.protectI\"]"}
- Note that the theorems @{thm [source] "protectD"} and @{thm [source]
- protectI} are internal theorems that are always part of a
+ Note the theorems @{thm [source] protectD} and @{thm [source]
+ protectI} that are internal theorems which are always part of a
proof in Isabelle. Note also that applications of @{text assumption} do not
count as a separate theorem, as you can see in the following code.
@@ -79,10 +88,24 @@
|> List.concat"
"[\"Pure.protectD\", \"Pure.protectI\"]"}
- Of course we can also descend to the second level of the tree
+ Interestingly, but not surprisingly, the proof of @{thm [source]
+ my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
+ and @{thm [source] my_conjIb}, as can be seen next.
+
+ @{ML_response [display,gray]
+ "@{thm my_conjIc}
+ |> Thm.proof_body_of
+ |> get_pbodies
+ |> map get_names
+ |> List.concat"
+ "[\"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\",
+ \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
+ \"Pure.protectI\"]"}
+
+ Of course we can also descend into the second level of the tree
``behind'' @{thm [source] my_conjIa}, which
means we obtain the theorems that are used in order to prove
- @{thm [source] conjunct1}, @{thm conjunct2} and @{thm conjI}.
+ @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
@{ML_response [display, gray]
"@{thm my_conjIa}
@@ -98,10 +121,9 @@
\begin{readmore}
The data-structure @{ML_type proof_body} is implemented
- in @{ML_file "Pure/proofterm.ML"}. The functions concerning the
- structure of theorems are in @{ML_file "Pure/thm.ML"}.
+ in the file @{ML_file "Pure/proofterm.ML"}. The implementation
+ of theorems and related functions are in @{ML_file "Pure/thm.ML"}.
\end{readmore}
-
*}