summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 02 Feb 2006 16:31:28 +0100 | |

changeset 18901 | 701e53c81c25 |

parent 18900 | e7d4e51bd4b1 |

child 18902 | b1e2151574c1 |

* Isar: 'obtains' element;

--- a/NEWS Thu Feb 02 12:54:24 2006 +0100 +++ b/NEWS Thu Feb 02 16:31:28 2006 +0100 @@ -76,6 +76,44 @@ analogous to the 'rule_format' attribute, but *not* that of the Simplifier (which is usually more generous). +* Isar: the conclusion of a long theorem statement is now either +'shows' (a simultaneous conjunction, as before), or 'obtains' +(essentially a disjunction of cases with local parameters and +assumptions). The latter allows to express general elimination rules +adequately. In this notation common elimination rules look like this: + + lemma exE: -- "EX x. P x ==> (!!x. P x ==> thesis) ==> thesis" + assumes "EX x. P x" + obtains x where "P x" + + lemma conjE: -- "A & B ==> (A ==> B ==> thesis) ==> thesis" + assumes "A & B" + obtains A and B + + lemma disjE: -- "A | B ==> (A ==> thesis) ==> (B ==> thesis) ==> thesis" + assumes "A | B" + obtains + A + | B + +The subsequent classical rules refer to the formal "thesis" +explicitly: + + lemma classical: -- "(~ thesis ==> thesis) ==> thesis" + obtains "~ thesis" + + lemma Peirce's_Law: -- "((thesis ==> A) ==> thesis) ==> thesis" + obtains "thesis ==> A" + +The actual proof of an 'obtains' statement is analogous to that of the +Isar 'obtain' element, only that there may be several cases. Optional +case names may be specified in parentheses; these will be also used to +annotate the resulting rule for later use with the 'cases' method +(cf. attribute case_names). + +* Isar: 'obtain' takes an optional case name for the local context +introduction rule (default "that"). + * Provers/induct: improved internal context management to support local fixes and defines on-the-fly. Thus explicit meta-level connectives !! and ==> are rarely required anymore in inductive goals @@ -118,11 +156,13 @@ See also HOL/Isar_examples/Puzzle.thy for an application of the this particular technique. -(3) This is how to perform existential reasoning ('obtain') by -induction, while avoiding explicit object-logic encodings: - - fix n :: nat - obtain x :: 'a where "P n x" and "Q n x" +(3) This is how to perform existential reasoning ('obtains' or +'obtain') by induction, while avoiding explicit object-logic +encodings: + + lemma + fixes n :: nat + obtains x :: 'a where "P n x" and "Q n x" proof (induct n fixing: thesis) case 0 obtain x where "P 0 x" and "Q 0 x" sorry