
diff -r e2c0138b5cea -r 13d7ea419c5f ProgTutorial/Essential.thy
--- 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




