equal
deleted
inserted
replaced
59 "[\"Introspection.my_conjIa\"]"} |
59 "[\"Introspection.my_conjIa\"]"} |
60 |
60 |
61 whereby @{text "Introspection"} refers to the theory name in which |
61 whereby @{text "Introspection"} refers to the theory name in which |
62 we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind |
62 we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind |
63 proof_body_of in Thm} returns a part of the data that is stored in a |
63 proof_body_of in Thm} returns a part of the data that is stored in a |
64 theorem. Notice that the apply-proof of this theorem references |
64 theorem. Notice that the first proof above references |
65 three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} |
65 three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} |
66 and @{thm [source] conjunct2}. We can obtain them by descending into the |
66 and @{thm [source] conjunct2}. We can obtain them by descending into the |
67 first level of the proof-tree, as follows. |
67 first level of the proof-tree, as follows. |
68 |
68 |
69 @{ML_response [display,gray] |
69 @{ML_response [display,gray] |
73 |> map get_names |
73 |> map get_names |
74 |> List.concat" |
74 |> List.concat" |
75 "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", |
75 "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", |
76 \"Pure.protectI\"]"} |
76 \"Pure.protectI\"]"} |
77 |
77 |
78 Note the theorems @{thm [source] protectD} and @{thm [source] |
78 The theorems @{thm [source] protectD} and @{thm [source] |
79 protectI} that are internal theorems which are always part of a |
79 protectI} that are internal theorems are always part of a |
80 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 |
81 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. |
82 |
82 |
83 @{ML_response [display,gray] |
83 @{ML_response [display,gray] |
84 "@{thm my_conjIb} |
84 "@{thm my_conjIb} |
88 |> List.concat" |
88 |> List.concat" |
89 "[\"Pure.protectD\", \"Pure.protectI\"]"} |
89 "[\"Pure.protectD\", \"Pure.protectI\"]"} |
90 |
90 |
91 Interestingly, but not surprisingly, the proof of @{thm [source] |
91 Interestingly, but not surprisingly, the proof of @{thm [source] |
92 my_conjIc} procceeds quite differently from @{thm [source] my_conjIa} |
92 my_conjIc} procceeds quite differently from @{thm [source] my_conjIa} |
93 and @{thm [source] my_conjIb}, as can be seen next. |
93 and @{thm [source] my_conjIb}, as can be seen by the theorems that |
|
94 are returned for @{thm [source] my_conjIc}. |
94 |
95 |
95 @{ML_response [display,gray] |
96 @{ML_response [display,gray] |
96 "@{thm my_conjIc} |
97 "@{thm my_conjIc} |
97 |> Thm.proof_body_of |
98 |> Thm.proof_body_of |
98 |> get_pbodies |
99 |> get_pbodies |
101 "[\"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", |
102 "[\"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", |
102 \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\", |
103 \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\", |
103 \"Pure.protectI\"]"} |
104 \"Pure.protectI\"]"} |
104 |
105 |
105 Of course we can also descend into the second level of the tree |
106 Of course we can also descend into the second level of the tree |
106 ``behind'' @{thm [source] my_conjIa}, which |
107 ``behind'' @{thm [source] my_conjIa} say, which |
107 means we obtain the theorems that are used in order to prove |
108 means we obtain the theorems that are used in order to prove |
108 @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}. |
109 @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}. |
109 |
110 |
110 @{ML_response [display, gray] |
111 @{ML_response [display, gray] |
111 "@{thm my_conjIa} |
112 "@{thm my_conjIa} |