# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1340123230 -3600
# Node ID efe63c062e48093e8ed65c6781b7832e46387402
# Parent  9e191bc4a82834b72161e097ea09ae8398d883c4
polished introspection section

diff -r 9e191bc4a828 -r efe63c062e48 ProgTutorial/Recipes/Introspection.thy
--- 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}
-  
 *}
 
 
diff -r 9e191bc4a828 -r efe63c062e48 progtutorial.pdf
Binary file progtutorial.pdf has changed