|
1 |
|
2 theory Introspection |
|
3 imports "../Appendix" |
|
4 begin |
|
5 |
|
6 section {* Introspection of Theorems and Proofs \label{rec:introspection} *} |
|
7 |
|
8 text{* |
|
9 {\bf Problem:} |
|
10 How to obtain all theorems that are used in the proof of a theorem?\smallskip |
|
11 |
|
12 {\bf Solution:} They can be obtained by introspecting the theorem.\smallskip |
|
13 |
|
14 To introspect a theorem, let us define the following three functions that |
|
15 analyse the @{ML_type proof_body} data-structure from @{ML_struct Proofterm}. |
|
16 *} |
|
17 |
|
18 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms |
|
19 val get_names = map #1 o pthms_of |
|
20 val get_pbodies = map (Future.join o #3) o pthms_of *} |
|
21 |
|
22 text {* |
|
23 To see what their purpose is, consider the following two short proofs. |
|
24 *} |
|
25 |
|
26 lemma my_conjIa: |
|
27 shows "A \<and> B \<Longrightarrow> A \<and> B" |
|
28 apply(rule conjI) |
|
29 apply(drule conjunct1) |
|
30 apply(assumption) |
|
31 apply(drule conjunct2) |
|
32 apply(assumption) |
|
33 done |
|
34 |
|
35 lemma my_conjIb: |
|
36 shows "A \<and> B \<Longrightarrow> A \<and> B" |
|
37 apply(assumption) |
|
38 done |
|
39 |
|
40 text {* |
|
41 While the theorems used in these proofs is obvious, in general it |
|
42 is not obvious, because of automated provers that can be part of a |
|
43 proof. Fortunately, ``behind'' every completed proof is a tree of |
|
44 theorems that records all theorems that are employed for establishing |
|
45 theorems like @{thm [source] my_conjIa}. We can traverse this tree |
|
46 once a theorem is established. Let us first extract the name of the |
|
47 established theorem from this tree. This can be done with |
|
48 |
|
49 @{ML_response [display,gray] |
|
50 "@{thm my_conjIa} |
|
51 |> Thm.proof_body_of |
|
52 |> get_names" |
|
53 "[\"Introspection.my_conjIa\"]"} |
|
54 |
|
55 whereby @{text "Introspection"} refers to the theory name in which we established |
|
56 @{thm [source] my_conjIa}. Notice that the apply-proof of this theorem references |
|
57 three other theorems. We can obtain them by descending into the first level of the |
|
58 proof-tree, as follows. |
|
59 |
|
60 @{ML_response [display,gray] |
|
61 "@{thm my_conjIa} |
|
62 |> Thm.proof_body_of |
|
63 |> get_pbodies |
|
64 |> map get_names |
|
65 |> List.concat" |
|
66 "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", |
|
67 \"Pure.protectI\"]"} |
|
68 |
|
69 Note that the theorems @{thm [source] "protectD"} and @{thm [source] |
|
70 protectI} are internal theorems that are always part of a |
|
71 proof in Isabelle. Note also that applications of @{text assumption} do not |
|
72 count as a separate theorem, as you can see in the following code. |
|
73 |
|
74 @{ML_response [display,gray] |
|
75 "@{thm my_conjIb} |
|
76 |> Thm.proof_body_of |
|
77 |> get_pbodies |
|
78 |> map get_names |
|
79 |> List.concat" |
|
80 "[\"Pure.protectD\", \"Pure.protectI\"]"} |
|
81 |
|
82 Of course we can also descend to the second level of the tree |
|
83 ``behind'' @{thm [source] my_conjIa}, which |
|
84 means we obtain the theorems that are used in order to prove |
|
85 @{thm [source] conjunct1}, @{thm conjunct2} and @{thm conjI}. |
|
86 |
|
87 @{ML_response [display, gray] |
|
88 "@{thm my_conjIa} |
|
89 |> Thm.proof_body_of |
|
90 |> get_pbodies |
|
91 |> map get_pbodies |
|
92 |> (map o map) get_names |
|
93 |> List.concat |
|
94 |> List.concat |
|
95 |> duplicates (op=)" |
|
96 "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\", |
|
97 \"Pure.protectI\"]"} |
|
98 |
|
99 \begin{readmore} |
|
100 The data-structure @{ML_type proof_body} is implemented |
|
101 in @{ML_file "Pure/proofterm.ML"}. The functions concerning the |
|
102 structure of theorems are in @{ML_file "Pure/thm.ML"}. |
|
103 \end{readmore} |
|
104 |
|
105 *} |
|
106 |
|
107 |
|
108 |
|
109 end |
|
110 |
|
111 |