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