equal
deleted
inserted
replaced
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_structure Proofterm}. |
17 \<close> |
17 \<close> |
18 |
18 |
19 ML %grayML\<open>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\<close> |
21 val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of\<close> |
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_matchresult [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 \<close> |
60 \<close> |
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 |
68 first level of the proof-tree, as follows. |
68 first level of the proof-tree, as follows. |
69 |
69 |
70 @{ML_response_fake [display,gray] |
70 @{ML_matchresult_fake [display,gray] |
71 "@{thm my_conjIa} |
71 "@{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" |
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_response_fake [display,gray] |
85 @{ML_matchresult_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" |
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_response_fake [display,gray] |
99 @{ML_matchresult_fake [display,gray] |
100 "@{thm my_conjIc} |
100 "@{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" |
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_response_fake [display, gray] |
115 @{ML_matchresult_fake [display, gray] |
116 "@{thm my_conjIa} |
116 "@{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 |
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 \<close> |
126 \<close> |
|
127 |
|
128 |
|
129 |
127 text \<open> |
130 text \<open> |
128 \begin{readmore} |
131 \begin{readmore} |
129 The data-structure @{ML_type proof_body} is implemented |
132 The data-structure @{ML_type proof_body} is implemented |
130 in the file @{ML_file "Pure/proofterm.ML"}. The implementation |
133 in the file @{ML_file "Pure/proofterm.ML"}. The implementation |
131 of theorems and related functions are in @{ML_file "Pure/thm.ML"}. |
134 of theorems and related functions are in @{ML_file "Pure/thm.ML"}. |