--- a/ProgTutorial/Essential.thy	Tue Jun 19 17:58:12 2012 +0100
+++ b/ProgTutorial/Essential.thy	Wed Jun 20 08:29:12 2012 +0100
@@ -1513,8 +1513,8 @@
   val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"}
 
   val Pt_implies_Qt = 
-        Thm.assume assm1
-        |> Thm.forall_elim @{cterm "t::nat"}
+    Thm.assume assm1
+    |> Thm.forall_elim @{cterm "t::nat"}
   
   val Qt = Thm.implies_elim Pt_implies_Qt (Thm.assume assm2)
 in
@@ -1568,8 +1568,8 @@
   The first argument of @{ML note in Local_Theory} is the name under
   which we store the theorem or theorems. The second argument can contain a
   list of theorem attributes, which we will explain in detail in
-  Section~\ref{sec:attributes}. Below we just use one such attribute for
-  adding the theorem to the simpset:
+  Section~\ref{sec:attributes}. Below we just use one such attribute,
+  @{ML_ind simp_add in Simplifier}, for adding the theorem to the simpset:
 *}
 
 local_setup %gray {*
@@ -1928,7 +1928,7 @@
 *}
 
 lemma
-  shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
+shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
 proof (cases rule: foo_data')
 
 (*<*)oops(*>*)
@@ -1950,7 +1950,7 @@
 *}
 
 lemma
-  shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
+shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
 proof (cases rule: foo_data)
 
 (*<*)oops(*>*)
@@ -1964,8 +1964,125 @@
 @{text ">     let \"?case\" = \"?P\""}
 \end{tabular}*}
 
+ 
+text {*
+  One often wants to know the theorems that are used in the proof 
+  of a theorem. They can be obtained by introspecting the theorem.
+  To introspect a theorem, let us define the following three functions that 
+  analyse the @{ML_type_ind proof_body} data-structure from the structure 
+  @{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 three 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
+
+lemma my_conjIc:
+shows "A \<and> B \<Longrightarrow> A \<and> B"
+apply(auto)
+done
 
 text {*
+  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}
+  |> Thm.proof_body_of
+  |> get_names"
+  "[\"Essential.my_conjIa\"]"}
+
+  whereby @{text "Essential"} 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 first proof above 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}
+  |> Thm.proof_body_of
+  |> get_pbodies
+  |> map get_names
+  |> List.concat"
+  "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", 
+  \"Pure.protectI\"]"}
+
+  The theorems @{thm [source] protectD} and @{thm [source]
+  protectI} that are internal theorems 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\"]"}
+
+  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 by the theorems that
+  are returned for @{thm [source] my_conjIc}.
+
+  @{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} say, which
+  means we obtain the theorems that are used in order to prove
+  @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] 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 the file @{ML_file "Pure/proofterm.ML"}. The implementation 
+  of theorems and related functions are in @{ML_file "Pure/thm.ML"}.  
+  \end{readmore}
+
   One great feature of Isabelle is its document preparation system, where
   proved theorems can be quoted in documents referencing directly their
   formalisation. This helps tremendously to minimise cut-and-paste errors. However,
@@ -2002,7 +2119,7 @@
 *}
 
 theorem style_test:
-  shows "\<forall>x y z. (x, x) = (y, z)" sorry
+shows "\<forall>x y z. (x, x) = (y, z)" sorry
 
 text {*
   Now printing out in a document the theorem @{thm [source] style_test} normally

--- a/ProgTutorial/Intro.thy	Tue Jun 19 17:58:12 2012 +0100
+++ b/ProgTutorial/Intro.thy	Wed Jun 20 08:29:12 2012 +0100
@@ -288,15 +288,18 @@
   are by him.
 
   \item {\bf Lukas Bulwahn} made me aware of a problem with recursive
-  parsers and contributed exercise \ref{ex:contextfree} and contributed to
-  recipe \ref{rec:introspection}.
+  parsers and contributed exercise \ref{ex:contextfree} and contributed 
+  ``introspection'' of theorems 
+  \ref{sec:theorems}.
+
 
   \item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing}
   about parsing.
 
   \item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
 
-  \item {\bf Rafal Kolanski} contributed to recipe \ref{rec:introspection}.
+  \item {\bf Rafal Kolanski} contributed the ``introspection'' of theorems 
+  \ref{sec:theorems}.
 
   \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps'' 
   chapter and also contributed the material on @{ML_funct Named_Thms}.

--- a/ProgTutorial/Parsing.thy	Tue Jun 19 17:58:12 2012 +0100
+++ b/ProgTutorial/Parsing.thy	Wed Jun 20 08:29:12 2012 +0100
@@ -1109,9 +1109,9 @@
 *}
 
 ML %grayML{*
-structure Result = 
-  Proof_Data (type T = unit -> term
-              fun init thy () = error "Result")
+structure Result = Proof_Data 
+  (type T = unit -> term
+   fun init thy () = error "Result")
 
 val result_cookie = (Result.get, Result.put, "Result.put") *}
 

--- a/ProgTutorial/ROOT.ML	Tue Jun 19 17:58:12 2012 +0100
+++ b/ProgTutorial/ROOT.ML	Wed Jun 20 08:29:12 2012 +0100
@@ -29,7 +29,6 @@
 use_thy "Recipes/ExternalSolver";
 use_thy "Recipes/Oracle";
 use_thy "Recipes/Sat";
-use_thy "Recipes/Introspection";
 use_thy "Recipes/USTypes";
 
 use_thy "Solutions";

--- a/ProgTutorial/Recipes/Introspection.thy	Tue Jun 19 17:58:12 2012 +0100
+++ b/ProgTutorial/Recipes/Introspection.thy	Wed Jun 20 08:29:12 2012 +0100
@@ -61,7 +61,7 @@
   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
+  theorem.  Notice that the first proof above 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.
@@ -75,8 +75,8 @@
   "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", 
   \"Pure.protectI\"]"}
 
-  Note the theorems @{thm [source] protectD} and @{thm [source]
-  protectI} that are internal theorems which are always part of a
+  The theorems @{thm [source] protectD} and @{thm [source]
+  protectI} that are internal theorems 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.
 
@@ -90,7 +90,8 @@
 
   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.
+  and @{thm [source] my_conjIb}, as can be seen by the theorems that
+  are returned for @{thm [source] my_conjIc}.
 
   @{ML_response [display,gray]
   "@{thm my_conjIc}
@@ -103,7 +104,7 @@
   \"Pure.protectI\"]"}
 
   Of course we can also descend into the second level of the tree 
-  ``behind'' @{thm [source] my_conjIa}, which
+  ``behind'' @{thm [source] my_conjIa} say, which
   means we obtain the theorems that are used in order to prove
   @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
 

Binary file progtutorial.pdf has changed