73 * Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded', |
73 * Isar: methods 'unfold' / 'fold', attributes 'unfolded' / 'folded', |
74 and command 'unfolding' now all support object-level equalities |
74 and command 'unfolding' now all support object-level equalities |
75 (potentially conditional). The underlying notion of rewrite rule is |
75 (potentially conditional). The underlying notion of rewrite rule is |
76 analogous to the 'rule_format' attribute, but *not* that of the |
76 analogous to the 'rule_format' attribute, but *not* that of the |
77 Simplifier (which is usually more generous). |
77 Simplifier (which is usually more generous). |
|
78 |
|
79 * Isar: the conclusion of a long theorem statement is now either |
|
80 'shows' (a simultaneous conjunction, as before), or 'obtains' |
|
81 (essentially a disjunction of cases with local parameters and |
|
82 assumptions). The latter allows to express general elimination rules |
|
83 adequately. In this notation common elimination rules look like this: |
|
84 |
|
85 lemma exE: -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis" |
|
86 assumes "EX x. P x" |
|
87 obtains x where "P x" |
|
88 |
|
89 lemma conjE: -- "A & B ==> (A ==> B ==> thesis) ==> thesis" |
|
90 assumes "A & B" |
|
91 obtains A and B |
|
92 |
|
93 lemma disjE: -- "A | B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis" |
|
94 assumes "A | B" |
|
95 obtains |
|
96 A |
|
97 | B |
|
98 |
|
99 The subsequent classical rules refer to the formal "thesis" |
|
100 explicitly: |
|
101 |
|
102 lemma classical: -- "(~ thesis ==> thesis) ==> thesis" |
|
103 obtains "~ thesis" |
|
104 |
|
105 lemma Peirce's_Law: -- "((thesis ==> A) ==> thesis) ==> thesis" |
|
106 obtains "thesis ==> A" |
|
107 |
|
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 |
|
110 case names may be specified in parentheses; these will be also used to |
|
111 annotate the resulting rule for later use with the 'cases' method |
|
112 (cf. attribute case_names). |
|
113 |
|
114 * Isar: 'obtain' takes an optional case name for the local context |
|
115 introduction rule (default "that"). |
78 |
116 |
79 * Provers/induct: improved internal context management to support |
117 * Provers/induct: improved internal context management to support |
80 local fixes and defines on-the-fly. Thus explicit meta-level |
118 local fixes and defines on-the-fly. Thus explicit meta-level |
81 connectives !! and ==> are rarely required anymore in inductive goals |
119 connectives !! and ==> are rarely required anymore in inductive goals |
82 (using object-logic connectives for this purpose has been long |
120 (using object-logic connectives for this purpose has been long |
116 ... |
154 ... |
117 |
155 |
118 See also HOL/Isar_examples/Puzzle.thy for an application of the this |
156 See also HOL/Isar_examples/Puzzle.thy for an application of the this |
119 particular technique. |
157 particular technique. |
120 |
158 |
121 (3) This is how to perform existential reasoning ('obtain') by |
159 (3) This is how to perform existential reasoning ('obtains' or |
122 induction, while avoiding explicit object-logic encodings: |
160 'obtain') by induction, while avoiding explicit object-logic |
123 |
161 encodings: |
124 fix n :: nat |
162 |
125 obtain x :: 'a where "P n x" and "Q n x" |
163 lemma |
|
164 fixes n :: nat |
|
165 obtains x :: 'a where "P n x" and "Q n x" |
126 proof (induct n fixing: thesis) |
166 proof (induct n fixing: thesis) |
127 case 0 |
167 case 0 |
128 obtain x where "P 0 x" and "Q 0 x" sorry |
168 obtain x where "P 0 x" and "Q 0 x" sorry |
129 then show thesis by (rule 0) |
169 then show thesis by (rule 0) |
130 next |
170 next |