+
−
theory Introspection+
−
imports "../Appendix"+
−
begin+
−
+
−
section \<open>Introspection of Theorems and Proofs \label{rec:introspection}\<close>+
−
+
−
text\<open>+
−
  {\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_ind proof_body} data-structure from the structure +
−
  @{ML_structure Proofterm}.+
−
\<close>+
−
+
−
ML %grayML\<open>fun pthms_of (PBody {thms, ...}) = map #2 thms +
−
val get_names = (map Proofterm.thm_node_name) o pthms_of +
−
val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of\<close>+
−
+
−
text \<open>+
−
  To see what their purpose is, consider the following three short proofs.+
−
\<close>+
−
+
−
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 \<open>+
−
  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+
−
  \<open>auto\<close>-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_matchresult [display,gray]+
−
  \<open>@{thm my_conjIa}+
−
  |> Thm.proof_body_of+
−
  |> get_names\<close>+
−
  \<open>["Introspection.my_conjIa"]\<close>}+
−
\<close>+
−
text \<open>+
−
  whereby \<open>Introspection\<close> 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_matchresult_fake [display,gray]+
−
  \<open>@{thm my_conjIa}+
−
  |> Thm.proof_body_of+
−
  |> get_pbodies+
−
  |> map get_names+
−
  |> List.concat\<close>+
−
  \<open>["HOL.conjunct2", "HOL.conjunct1", "HOL.conjI", "Pure.protectD", +
−
  "Pure.protectI"]\<close>}+
−
\<close>+
−
text \<open>+
−
  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 \<open>assumption\<close> do not+
−
  count as a separate theorem, as you can see in the following code.+
−
+
−
  @{ML_matchresult_fake [display,gray]+
−
  \<open>@{thm my_conjIb}+
−
  |> Thm.proof_body_of+
−
  |> get_pbodies+
−
  |> map get_names+
−
  |> List.concat\<close>+
−
  \<open>["Pure.protectD", "Pure.protectI"]\<close>}+
−
\<close>+
−
text \<open>+
−
  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_matchresult_fake [display,gray]+
−
  \<open>@{thm my_conjIc}+
−
  |> Thm.proof_body_of+
−
  |> get_pbodies+
−
  |> map get_names+
−
  |> List.concat\<close>+
−
  \<open>["HOL.implies_True_equals", "HOL.Eq_TrueI", "HOL.simp_thms_25", "HOL.eq_reflection", +
−
    "HOL.conjunct2", "HOL.conjunct1", "HOL.TrueI", "Pure.protectD",+
−
    "Pure.protectI"]\<close>}+
−
\<close>+
−
text \<open>+
−
  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_matchresult_fake [display, gray]+
−
  \<open>@{thm my_conjIa}+
−
  |> Thm.proof_body_of+
−
  |> get_pbodies+
−
  |> map get_pbodies+
−
  |> (map o map) get_names+
−
  |> List.concat+
−
  |> List.concat+
−
  |> duplicates (op =)\<close>+
−
  \<open>["", "Pure.protectD",+
−
 "Pure.protectI"]\<close>}+
−
\<close>+
−
+
−
+
−
+
−
text \<open>+
−
  \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}+
−
\<close>+
−
+
−
+
−
+
−
end+
−
  +
−
+
−