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_matchresult [display,gray] |
55 @{ML_matchresult [display,gray] |
56 "@{thm my_conjIa} |
56 \<open>@{thm my_conjIa} |
57 |> Thm.proof_body_of |
57 |> Thm.proof_body_of |
58 |> get_names" |
58 |> get_names\<close> |
59 "[\"Introspection.my_conjIa\"]"} |
59 \<open>["Introspection.my_conjIa"]\<close>} |
60 \<close> |
60 \<close> |
61 text \<open> |
61 text \<open> |
62 whereby \<open>Introspection\<close> 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 |
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 |
68 first level of the proof-tree, as follows. |
68 first level of the proof-tree, as follows. |
69 |
69 |
70 @{ML_matchresult_fake [display,gray] |
70 @{ML_matchresult_fake [display,gray] |
71 "@{thm my_conjIa} |
71 \<open>@{thm my_conjIa} |
72 |> Thm.proof_body_of |
72 |> Thm.proof_body_of |
73 |> get_pbodies |
73 |> get_pbodies |
74 |> map get_names |
74 |> map get_names |
75 |> List.concat" |
75 |> List.concat\<close> |
76 "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", |
76 \<open>["HOL.conjunct2", "HOL.conjunct1", "HOL.conjI", "Pure.protectD", |
77 \"Pure.protectI\"]"} |
77 "Pure.protectI"]\<close>} |
78 \<close> |
78 \<close> |
79 text \<open> |
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 \<open>assumption\<close> 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_matchresult_fake [display,gray] |
85 @{ML_matchresult_fake [display,gray] |
86 "@{thm my_conjIb} |
86 \<open>@{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\<close> |
91 "[\"Pure.protectD\", \"Pure.protectI\"]"} |
91 \<open>["Pure.protectD", "Pure.protectI"]\<close>} |
92 \<close> |
92 \<close> |
93 text \<open> |
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 |
99 @{ML_matchresult_fake [display,gray] |
99 @{ML_matchresult_fake [display,gray] |
100 "@{thm my_conjIc} |
100 \<open>@{thm my_conjIc} |
101 |> Thm.proof_body_of |
101 |> Thm.proof_body_of |
102 |> get_pbodies |
102 |> get_pbodies |
103 |> map get_names |
103 |> map get_names |
104 |> List.concat" |
104 |> List.concat\<close> |
105 "[\"HOL.implies_True_equals\", \"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", |
105 \<open>["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"]\<close>} |
108 \<close> |
108 \<close> |
109 text \<open> |
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 |
115 @{ML_matchresult_fake [display, gray] |
115 @{ML_matchresult_fake [display, gray] |
116 "@{thm my_conjIa} |
116 \<open>@{thm my_conjIa} |
117 |> Thm.proof_body_of |
117 |> Thm.proof_body_of |
118 |> get_pbodies |
118 |> get_pbodies |
119 |> map get_pbodies |
119 |> map get_pbodies |
120 |> (map o map) get_names |
120 |> (map o map) get_names |
121 |> List.concat |
121 |> List.concat |
122 |> List.concat |
122 |> List.concat |
123 |> duplicates (op =)" |
123 |> duplicates (op =)\<close> |
124 "[\"\", \"Pure.protectD\", |
124 \<open>["", "Pure.protectD", |
125 \"Pure.protectI\"]"} |
125 "Pure.protectI"]\<close>} |
126 \<close> |
126 \<close> |
127 |
127 |
128 |
128 |
129 |
129 |
130 text \<open> |
130 text \<open> |