tuned ML-antiquotations; added intro portions.
+ −
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]+ −
"@{thm my_conjIa}+ −
|> Thm.proof_body_of+ −
|> get_names"+ −
"[\"Introspection.my_conjIa\"]"}+ −
\<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]+ −
"@{thm my_conjIa}+ −
|> Thm.proof_body_of+ −
|> get_pbodies+ −
|> map get_names+ −
|> List.concat"+ −
"[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", + −
\"Pure.protectI\"]"}+ −
\<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]+ −
"@{thm my_conjIb}+ −
|> Thm.proof_body_of+ −
|> get_pbodies+ −
|> map get_names+ −
|> List.concat"+ −
"[\"Pure.protectD\", \"Pure.protectI\"]"}+ −
\<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]+ −
"@{thm my_conjIc}+ −
|> Thm.proof_body_of+ −
|> get_pbodies+ −
|> map get_names+ −
|> List.concat"+ −
"[\"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>+ −
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]+ −
"@{thm my_conjIa}+ −
|> Thm.proof_body_of+ −
|> get_pbodies+ −
|> map get_pbodies+ −
|> (map o map) get_names+ −
|> List.concat+ −
|> List.concat+ −
|> duplicates (op =)"+ −
"[\"\", \"Pure.protectD\",+ −
\"Pure.protectI\"]"}+ −
\<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+ −
+ −
+ −