1 |
1 |
2 theory Introspection |
2 theory Introspection |
3 imports "../Appendix" |
3 imports "../Appendix" |
4 begin |
4 begin |
5 |
5 |
6 section {* Introspection of Theorems and Proofs \label{rec:introspection} *} |
6 section \<open>Introspection of Theorems and Proofs \label{rec:introspection}\<close> |
7 |
7 |
8 text{* |
8 text\<open> |
9 {\bf Problem:} |
9 {\bf Problem:} |
10 How to obtain all theorems that are used in the proof of a theorem?\smallskip |
10 How to obtain all theorems that are used in the proof of a theorem?\smallskip |
11 |
11 |
12 {\bf Solution:} They can be obtained by introspecting the theorem.\smallskip |
12 {\bf Solution:} They can be obtained by introspecting the theorem.\smallskip |
13 |
13 |
14 To introspect a theorem, let us define the following three functions that |
14 To introspect a theorem, let us define the following three functions that |
15 analyse the @{ML_type_ind proof_body} data-structure from the structure |
15 analyse the @{ML_type_ind proof_body} data-structure from the structure |
16 @{ML_struct Proofterm}. |
16 @{ML_struct Proofterm}. |
17 *} |
17 \<close> |
18 |
18 |
19 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms |
19 ML %grayML\<open>fun pthms_of (PBody {thms, ...}) = map #2 thms |
20 val get_names = (map Proofterm.thm_node_name) o pthms_of |
20 val get_names = (map Proofterm.thm_node_name) o pthms_of |
21 val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of *} |
21 val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of\<close> |
22 |
22 |
23 text {* |
23 text \<open> |
24 To see what their purpose is, consider the following three short proofs. |
24 To see what their purpose is, consider the following three short proofs. |
25 *} |
25 \<close> |
26 |
26 |
27 lemma my_conjIa: |
27 lemma my_conjIa: |
28 shows "A \<and> B \<Longrightarrow> A \<and> B" |
28 shows "A \<and> B \<Longrightarrow> A \<and> B" |
29 apply(rule conjI) |
29 apply(rule conjI) |
30 apply(drule conjunct1) |
30 apply(drule conjunct1) |
41 lemma my_conjIc: |
41 lemma my_conjIc: |
42 shows "A \<and> B \<Longrightarrow> A \<and> B" |
42 shows "A \<and> B \<Longrightarrow> A \<and> B" |
43 apply(auto) |
43 apply(auto) |
44 done |
44 done |
45 |
45 |
46 text {* |
46 text \<open> |
47 While the information about which theorems are used is obvious in |
47 While the information about which theorems are used is obvious in |
48 the first two proofs, it is not obvious in the third, because of the |
48 the first two proofs, it is not obvious in the third, because of the |
49 @{text auto}-step. Fortunately, ``behind'' every proved theorem is |
49 \<open>auto\<close>-step. Fortunately, ``behind'' every proved theorem is |
50 a proof-tree that records all theorems that are employed for |
50 a proof-tree that records all theorems that are employed for |
51 establishing this theorem. We can traverse this proof-tree |
51 establishing this theorem. We can traverse this proof-tree |
52 extracting this information. Let us first extract the name of the |
52 extracting this information. Let us first extract the name of the |
53 established theorem. This can be done with |
53 established theorem. This can be done with |
54 |
54 |
55 @{ML_response [display,gray] |
55 @{ML_response [display,gray] |
56 "@{thm my_conjIa} |
56 "@{thm my_conjIa} |
57 |> Thm.proof_body_of |
57 |> Thm.proof_body_of |
58 |> get_names" |
58 |> get_names" |
59 "[\"Introspection.my_conjIa\"]"} |
59 "[\"Introspection.my_conjIa\"]"} |
60 *} |
60 \<close> |
61 text {* |
61 text \<open> |
62 whereby @{text "Introspection"} refers to the theory name in which |
62 whereby \<open>Introspection\<close> refers to the theory name in which |
63 we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind |
63 we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind |
64 proof_body_of in Thm} returns a part of the data that is stored in a |
64 proof_body_of in Thm} returns a part of the data that is stored in a |
65 theorem. Notice that the first proof above references |
65 theorem. Notice that the first proof above references |
66 three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} |
66 three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} |
67 and @{thm [source] conjunct2}. We can obtain them by descending into the |
67 and @{thm [source] conjunct2}. We can obtain them by descending into the |
73 |> get_pbodies |
73 |> get_pbodies |
74 |> map get_names |
74 |> map get_names |
75 |> List.concat" |
75 |> List.concat" |
76 "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", |
76 "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", |
77 \"Pure.protectI\"]"} |
77 \"Pure.protectI\"]"} |
78 *} |
78 \<close> |
79 text {* |
79 text \<open> |
80 The theorems @{thm [source] protectD} and @{thm [source] |
80 The theorems @{thm [source] protectD} and @{thm [source] |
81 protectI} that are internal theorems are always part of a |
81 protectI} that are internal theorems are always part of a |
82 proof in Isabelle. Note also that applications of @{text assumption} do not |
82 proof in Isabelle. Note also that applications of \<open>assumption\<close> do not |
83 count as a separate theorem, as you can see in the following code. |
83 count as a separate theorem, as you can see in the following code. |
84 |
84 |
85 @{ML_response_fake [display,gray] |
85 @{ML_response_fake [display,gray] |
86 "@{thm my_conjIb} |
86 "@{thm my_conjIb} |
87 |> Thm.proof_body_of |
87 |> Thm.proof_body_of |
88 |> get_pbodies |
88 |> get_pbodies |
89 |> map get_names |
89 |> map get_names |
90 |> List.concat" |
90 |> List.concat" |
91 "[\"Pure.protectD\", \"Pure.protectI\"]"} |
91 "[\"Pure.protectD\", \"Pure.protectI\"]"} |
92 *} |
92 \<close> |
93 text {* |
93 text \<open> |
94 Interestingly, but not surprisingly, the proof of @{thm [source] |
94 Interestingly, but not surprisingly, the proof of @{thm [source] |
95 my_conjIc} procceeds quite differently from @{thm [source] my_conjIa} |
95 my_conjIc} procceeds quite differently from @{thm [source] my_conjIa} |
96 and @{thm [source] my_conjIb}, as can be seen by the theorems that |
96 and @{thm [source] my_conjIb}, as can be seen by the theorems that |
97 are returned for @{thm [source] my_conjIc}. |
97 are returned for @{thm [source] my_conjIc}. |
98 |
98 |
103 |> map get_names |
103 |> map get_names |
104 |> List.concat" |
104 |> List.concat" |
105 "[\"HOL.implies_True_equals\", \"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", |
105 "[\"HOL.implies_True_equals\", \"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", |
106 \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\", |
106 \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\", |
107 \"Pure.protectI\"]"} |
107 \"Pure.protectI\"]"} |
108 *} |
108 \<close> |
109 text {* |
109 text \<open> |
110 Of course we can also descend into the second level of the tree |
110 Of course we can also descend into the second level of the tree |
111 ``behind'' @{thm [source] my_conjIa} say, which |
111 ``behind'' @{thm [source] my_conjIa} say, which |
112 means we obtain the theorems that are used in order to prove |
112 means we obtain the theorems that are used in order to prove |
113 @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}. |
113 @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}. |
114 |
114 |
121 |> List.concat |
121 |> List.concat |
122 |> List.concat |
122 |> List.concat |
123 |> duplicates (op =)" |
123 |> duplicates (op =)" |
124 "[\"\", \"Pure.protectD\", |
124 "[\"\", \"Pure.protectD\", |
125 \"Pure.protectI\"]"} |
125 \"Pure.protectI\"]"} |
126 *} |
126 \<close> |
127 text {* |
127 text \<open> |
128 \begin{readmore} |
128 \begin{readmore} |
129 The data-structure @{ML_type proof_body} is implemented |
129 The data-structure @{ML_type proof_body} is implemented |
130 in the file @{ML_file "Pure/proofterm.ML"}. The implementation |
130 in the file @{ML_file "Pure/proofterm.ML"}. The implementation |
131 of theorems and related functions are in @{ML_file "Pure/thm.ML"}. |
131 of theorems and related functions are in @{ML_file "Pure/thm.ML"}. |
132 \end{readmore} |
132 \end{readmore} |
133 *} |
133 \<close> |
134 |
134 |
135 |
135 |
136 |
136 |
137 end |
137 end |
138 |
138 |