--- a/ProgTutorial/Intro.thy Tue Jun 19 05:17:46 2012 +0100
+++ b/ProgTutorial/Intro.thy Tue Jun 19 15:02:22 2012 +0100
@@ -288,7 +288,8 @@
are by him.
\item {\bf Lukas Bulwahn} made me aware of a problem with recursive
- parsers and contributed exercise \ref{ex:contextfree}.
+ parsers and contributed exercise \ref{ex:contextfree} and contributed to
+ recipe \ref{rec:introspection}.
\item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing}
about parsing.
@@ -298,6 +299,8 @@
\item {\bf Alexander Krauss} wrote a very early version of the ``first-steps''
chapter and also contributed the material on @{ML_funct Named_Thms}.
+ \item {\bf Rafal Kolanski} contributed to recipe \ref{rec:introspection}.
+
\item {\bf Tobias Nipkow} contributed recipe \ref{rec:callml}.
\item {\bf Michael Norrish} proofread parts of the text.
--- a/ProgTutorial/ROOT.ML Tue Jun 19 05:17:46 2012 +0100
+++ b/ProgTutorial/ROOT.ML Tue Jun 19 15:02:22 2012 +0100
@@ -29,6 +29,7 @@
use_thy "Recipes/ExternalSolver";
use_thy "Recipes/Oracle";
use_thy "Recipes/Sat";
+use_thy "Recipes/Introspection";
use_thy "Recipes/USTypes";
use_thy "Solutions";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Recipes/Introspection.thy Tue Jun 19 15:02:22 2012 +0100
@@ -0,0 +1,111 @@
+
+theory Introspection
+imports "../Appendix"
+begin
+
+section {* Introspection of Theorems and Proofs \label{rec:introspection} *}
+
+text{*
+ {\bf Problem:}
+ How to obtain all theorems that are used in the proof of a theorem?\smallskip
+
+ {\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}.
+*}
+
+ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms
+val get_names = map #1 o pthms_of
+val get_pbodies = map (Future.join o #3) o pthms_of *}
+
+text {*
+ To see what their purpose is, consider the following two short proofs.
+*}
+
+lemma my_conjIa:
+ shows "A \<and> B \<Longrightarrow> A \<and> B"
+apply(rule conjI)
+apply(drule conjunct1)
+apply(assumption)
+apply(drule conjunct2)
+apply(assumption)
+done
+
+lemma my_conjIb:
+ shows "A \<and> B \<Longrightarrow> A \<and> B"
+apply(assumption)
+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
+
+ @{ML_response [display,gray]
+ "@{thm my_conjIa}
+ |> Thm.proof_body_of
+ |> 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.
+
+ @{ML_response [display,gray]
+ "@{thm my_conjIa}
+ |> Thm.proof_body_of
+ |> get_pbodies
+ |> map get_names
+ |> List.concat"
+ "[\"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
+ 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.
+
+ @{ML_response [display,gray]
+ "@{thm my_conjIb}
+ |> Thm.proof_body_of
+ |> get_pbodies
+ |> map get_names
+ |> List.concat"
+ "[\"Pure.protectD\", \"Pure.protectI\"]"}
+
+ Of course we can also descend to 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}.
+
+ @{ML_response [display, gray]
+ "@{thm my_conjIa}
+ |> Thm.proof_body_of
+ |> get_pbodies
+ |> map get_pbodies
+ |> (map o map) get_names
+ |> List.concat
+ |> List.concat
+ |> duplicates (op=)"
+ "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\",
+ \"Pure.protectI\"]"}
+
+ \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"}.
+ \end{readmore}
+
+*}
+
+
+
+end
+
+
--- a/ProgTutorial/document/root.tex Tue Jun 19 05:17:46 2012 +0100
+++ b/ProgTutorial/document/root.tex Tue Jun 19 15:02:22 2012 +0100
@@ -170,6 +170,7 @@
Sascha & Böhme\\
Lukas & Bulwahn\\
Jeremy & Dawson\\
+ Rafal & Kolanski\\
Alexander & Krauss\\
Tobias & Nipkow\\
Andreas & Schropp\\
Binary file progtutorial.pdf has changed