# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1340114542 -3600
# Node ID 92a3600e50e4422c885bc2e13d0c7edb09c4c4d8
# Parent  25f544b077f9e911ffbfad97be9a44809eb3b54c
added a new recipe for introspecting theorems (suggested by Lukas and Rafal)

diff -r 25f544b077f9 -r 92a3600e50e4 ProgTutorial/Intro.thy
--- 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.
diff -r 25f544b077f9 -r 92a3600e50e4 ProgTutorial/ROOT.ML
--- 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";
diff -r 25f544b077f9 -r 92a3600e50e4 ProgTutorial/Recipes/Introspection.thy
--- /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
+  
+
diff -r 25f544b077f9 -r 92a3600e50e4 ProgTutorial/document/root.tex
--- 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\\
diff -r 25f544b077f9 -r 92a3600e50e4 progtutorial.pdf
Binary file progtutorial.pdf has changed