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