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

author | wenzelm |

Sun, 30 Jul 2000 13:06:20 +0200 | |

changeset 9477 | 9506127f6fbb |

parent 9476 | 2210dffb9764 |

child 9478 | d7e354c16dc6 |

obtain;

--- a/src/HOL/Isar_examples/BasicLogic.thy Sun Jul 30 13:04:58 2000 +0200 +++ b/src/HOL/Isar_examples/BasicLogic.thy Sun Jul 30 13:06:20 2000 +0200 @@ -401,6 +401,31 @@ qed; qed; +text {* + Explicit $\exists$-elimination as seen above can become quite + cumbersome in practice. The derived Isar language element + ``\isakeyword{obtain}'' provides a more handsome way to do + generalized existence reasoning. +*}; + +lemma "(EX x. P (f x)) --> (EX x. P x)"; +proof; + assume "EX x. P (f x)"; + then; obtain a where "P (f a)"; by blast; + thus "EX x. P x"; ..; +qed; + +text {* + Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and + \isakeyword{assume} together with a soundness proof of the + elimination involved. Thus it behaves similar to any other forward + proof element. Also note that due to the nature of general existence + reasoning involved here, any result exported from the context of an + \isakeyword{obtain} statement may \emph{not} refer to the parameters + introduced there. +*}; + + subsubsection {* Deriving rules in Isabelle *};