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