equal
deleted
inserted
replaced
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 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 *} |
18 |
18 |
19 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms |
19 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms |
20 val get_names = map #1 o pthms_of |
20 val get_names = map #1 o pthms_of |
23 text {* |
23 text {* |
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 *} |
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) |
31 apply(assumption) |
31 apply(assumption) |
32 apply(drule conjunct2) |
32 apply(drule conjunct2) |
33 apply(assumption) |
33 apply(assumption) |
34 done |
34 done |
35 |
35 |
36 lemma my_conjIb: |
36 lemma my_conjIb: |
37 shows "A \<and> B \<Longrightarrow> A \<and> B" |
37 shows "A \<and> B \<Longrightarrow> A \<and> B" |
38 apply(assumption) |
38 apply(assumption) |
39 done |
39 done |
40 |
40 |
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 {* |
47 While the information about which theorems are used is obvious in |
47 While the information about which theorems are used is obvious in |