78 |
78 |
79 * Isar: the conclusion of a long theorem statement is now either |
79 * Isar: the conclusion of a long theorem statement is now either |
80 'shows' (a simultaneous conjunction, as before), or 'obtains' |
80 'shows' (a simultaneous conjunction, as before), or 'obtains' |
81 (essentially a disjunction of cases with local parameters and |
81 (essentially a disjunction of cases with local parameters and |
82 assumptions). The latter allows to express general elimination rules |
82 assumptions). The latter allows to express general elimination rules |
83 adequately. In this notation common elimination rules look like this: |
83 adequately; in this notation common elimination rules look like this: |
84 |
84 |
85 lemma exE: -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis" |
85 lemma exE: -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis" |
86 assumes "EX x. P x" |
86 assumes "EX x. P x" |
87 obtains x where "P x" |
87 obtains x where "P x" |
88 |
88 |
94 assumes "A | B" |
94 assumes "A | B" |
95 obtains |
95 obtains |
96 A |
96 A |
97 | B |
97 | B |
98 |
98 |
99 The subsequent classical rules refer to the formal "thesis" |
99 The subsequent classical rules even refer to the formal "thesis" |
100 explicitly: |
100 explicitly: |
101 |
101 |
102 lemma classical: -- "(~ thesis ==> thesis) ==> thesis" |
102 lemma classical: -- "(~ thesis ==> thesis) ==> thesis" |
103 obtains "~ thesis" |
103 obtains "~ thesis" |
104 |
104 |
105 lemma Peirce's_Law: -- "((thesis ==> A) ==> thesis) ==> thesis" |
105 lemma Peirce's_Law: -- "((thesis ==> something) ==> thesis) ==> thesis" |
106 obtains "thesis ==> A" |
106 obtains "thesis ==> something" |
107 |
107 |
108 The actual proof of an 'obtains' statement is analogous to that of the |
108 The actual proof of an 'obtains' statement is analogous to that of the |
109 Isar 'obtain' element, only that there may be several cases. Optional |
109 Isar proof element 'obtain', only that there may be several cases. |
110 case names may be specified in parentheses; these will be also used to |
110 Optional case names may be specified in parentheses; these will be |
111 annotate the resulting rule for later use with the 'cases' method |
111 available both in the present proof and as annotations in the |
112 (cf. attribute case_names). |
112 resulting rule, for later use with the 'cases' method (cf. attribute |
|
113 case_names). |
113 |
114 |
114 * Isar: 'obtain' takes an optional case name for the local context |
115 * Isar: 'obtain' takes an optional case name for the local context |
115 introduction rule (default "that"). |
116 introduction rule (default "that"). |
116 |
117 |
117 * Provers/induct: improved internal context management to support |
118 * Provers/induct: improved internal context management to support |