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 proof_body} data-structure from @{ML_struct Proofterm}. |
15 analyse the @{ML_type proof_body} data-structure from the structure |
|
16 @{ML_struct Proofterm}. |
16 *} |
17 *} |
17 |
18 |
18 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms |
19 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms |
19 val get_names = map #1 o pthms_of |
20 val get_names = map #1 o pthms_of |
20 val get_pbodies = map (Future.join o #3) o pthms_of *} |
21 val get_pbodies = map (Future.join o #3) o pthms_of *} |
21 |
22 |
22 text {* |
23 text {* |
23 To see what their purpose is, consider the following two short proofs. |
24 To see what their purpose is, consider the following three short proofs. |
24 *} |
25 *} |
25 |
26 |
26 lemma my_conjIa: |
27 lemma my_conjIa: |
27 shows "A \<and> B \<Longrightarrow> A \<and> B" |
28 shows "A \<and> B \<Longrightarrow> A \<and> B" |
28 apply(rule conjI) |
29 apply(rule conjI) |
35 lemma my_conjIb: |
36 lemma my_conjIb: |
36 shows "A \<and> B \<Longrightarrow> A \<and> B" |
37 shows "A \<and> B \<Longrightarrow> A \<and> B" |
37 apply(assumption) |
38 apply(assumption) |
38 done |
39 done |
39 |
40 |
|
41 lemma my_conjIc: |
|
42 shows "A \<and> B \<Longrightarrow> A \<and> B" |
|
43 apply(auto) |
|
44 done |
|
45 |
40 text {* |
46 text {* |
41 While the theorems used in these proofs is obvious, in general it |
47 While the information about which theorems are used is obvious in |
42 is not obvious, because of automated provers that can be part of a |
48 the first two proofs, it is not obvious in the third, because of the |
43 proof. Fortunately, ``behind'' every completed proof is a tree of |
49 @{text auto}-step. Fortunately, ``behind'' every proved theorem is |
44 theorems that records all theorems that are employed for establishing |
50 a proof-tree that records all theorems that are employed for |
45 theorems like @{thm [source] my_conjIa}. We can traverse this tree |
51 establishing this theorem. We can traverse this proof-tree |
46 once a theorem is established. Let us first extract the name of the |
52 extracting this information. Let us first extract the name of the |
47 established theorem from this tree. This can be done with |
53 established theorem. This can be done with |
48 |
54 |
49 @{ML_response [display,gray] |
55 @{ML_response [display,gray] |
50 "@{thm my_conjIa} |
56 "@{thm my_conjIa} |
51 |> Thm.proof_body_of |
57 |> Thm.proof_body_of |
52 |> get_names" |
58 |> get_names" |
53 "[\"Introspection.my_conjIa\"]"} |
59 "[\"Introspection.my_conjIa\"]"} |
54 |
60 |
55 whereby @{text "Introspection"} refers to the theory name in which we established |
61 whereby @{text "Introspection"} refers to the theory name in which |
56 @{thm [source] my_conjIa}. Notice that the apply-proof of this theorem references |
62 we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind |
57 three other theorems. We can obtain them by descending into the first level of the |
63 proof_body_of in Thm} returns a part of the data that is stored in a |
58 proof-tree, as follows. |
64 theorem. Notice that the apply-proof of this theorem references |
|
65 three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} |
|
66 and @{thm [source] conjunct2}. We can obtain them by descending into the |
|
67 first level of the proof-tree, as follows. |
59 |
68 |
60 @{ML_response [display,gray] |
69 @{ML_response [display,gray] |
61 "@{thm my_conjIa} |
70 "@{thm my_conjIa} |
62 |> Thm.proof_body_of |
71 |> Thm.proof_body_of |
63 |> get_pbodies |
72 |> get_pbodies |
64 |> map get_names |
73 |> map get_names |
65 |> List.concat" |
74 |> List.concat" |
66 "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", |
75 "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", |
67 \"Pure.protectI\"]"} |
76 \"Pure.protectI\"]"} |
68 |
77 |
69 Note that the theorems @{thm [source] "protectD"} and @{thm [source] |
78 Note the theorems @{thm [source] protectD} and @{thm [source] |
70 protectI} are internal theorems that are always part of a |
79 protectI} that are internal theorems which are always part of a |
71 proof in Isabelle. Note also that applications of @{text assumption} do not |
80 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. |
81 count as a separate theorem, as you can see in the following code. |
73 |
82 |
74 @{ML_response [display,gray] |
83 @{ML_response [display,gray] |
75 "@{thm my_conjIb} |
84 "@{thm my_conjIb} |
77 |> get_pbodies |
86 |> get_pbodies |
78 |> map get_names |
87 |> map get_names |
79 |> List.concat" |
88 |> List.concat" |
80 "[\"Pure.protectD\", \"Pure.protectI\"]"} |
89 "[\"Pure.protectD\", \"Pure.protectI\"]"} |
81 |
90 |
82 Of course we can also descend to the second level of the tree |
91 Interestingly, but not surprisingly, the proof of @{thm [source] |
|
92 my_conjIc} procceeds quite differently from @{thm [source] my_conjIa} |
|
93 and @{thm [source] my_conjIb}, as can be seen next. |
|
94 |
|
95 @{ML_response [display,gray] |
|
96 "@{thm my_conjIc} |
|
97 |> Thm.proof_body_of |
|
98 |> get_pbodies |
|
99 |> map get_names |
|
100 |> List.concat" |
|
101 "[\"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", |
|
102 \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\", |
|
103 \"Pure.protectI\"]"} |
|
104 |
|
105 Of course we can also descend into the second level of the tree |
83 ``behind'' @{thm [source] my_conjIa}, which |
106 ``behind'' @{thm [source] my_conjIa}, which |
84 means we obtain the theorems that are used in order to prove |
107 means we obtain the theorems that are used in order to prove |
85 @{thm [source] conjunct1}, @{thm conjunct2} and @{thm conjI}. |
108 @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}. |
86 |
109 |
87 @{ML_response [display, gray] |
110 @{ML_response [display, gray] |
88 "@{thm my_conjIa} |
111 "@{thm my_conjIa} |
89 |> Thm.proof_body_of |
112 |> Thm.proof_body_of |
90 |> get_pbodies |
113 |> get_pbodies |
96 "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\", |
119 "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\", |
97 \"Pure.protectI\"]"} |
120 \"Pure.protectI\"]"} |
98 |
121 |
99 \begin{readmore} |
122 \begin{readmore} |
100 The data-structure @{ML_type proof_body} is implemented |
123 The data-structure @{ML_type proof_body} is implemented |
101 in @{ML_file "Pure/proofterm.ML"}. The functions concerning the |
124 in the file @{ML_file "Pure/proofterm.ML"}. The implementation |
102 structure of theorems are in @{ML_file "Pure/thm.ML"}. |
125 of theorems and related functions are in @{ML_file "Pure/thm.ML"}. |
103 \end{readmore} |
126 \end{readmore} |
104 |
|
105 *} |
127 *} |
106 |
128 |
107 |
129 |
108 |
130 |
109 end |
131 end |