theory Introspectionimports "../Appendix"beginsection {* 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_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)donelemma my_conjIb:shows "A \<and> B \<Longrightarrow> A \<and> B"apply(assumption)donelemma my_conjIc:shows "A \<and> B \<Longrightarrow> A \<and> B"apply(auto)donetext {* 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" "[\"Introspection.my_conjIa\"]"} 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} |> Thm.proof_body_of |> get_pbodies |> map get_names |> List.concat" "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", \"Pure.protectI\"]"} 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. @{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 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 [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}*}end