--- /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
+  
+