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

author | wenzelm |

Sat, 13 Jun 2015 15:16:59 +0200 | |

changeset 60452 | 3a0d57f1d6ef |

parent 60451 | 1f2b29f78439 |

child 60453 | ba9085f7433f |

tuned comments;

--- a/src/Pure/Isar/obtain.ML Sat Jun 13 14:37:50 2015 +0200 +++ b/src/Pure/Isar/obtain.ML Sat Jun 13 15:16:59 2015 +0200 @@ -1,40 +1,7 @@ (* Title: Pure/Isar/obtain.ML Author: Markus Wenzel, TU Muenchen -The 'obtain' and 'guess' language elements -- generalized existence at -the level of proof texts: 'obtain' involves a proof that certain -fixes/assumes may be introduced into the present context; 'guess' is -similar, but derives these elements from the course of reasoning! - - - <chain_facts> - obtain x where "A x" <proof> == - - have "!!thesis. (!!x. A x ==> thesis) ==> thesis" - proof succeed - fix thesis - assume that [intro?]: "!!x. A x ==> thesis" - <chain_facts> - show thesis - apply (insert that) - <proof> - qed - fix x assm <<obtain_export>> "A x" - - - <chain_facts> - guess x <proof body> <proof end> == - - { - fix thesis - <chain_facts> have "PROP ?guess" - apply magic -- {* turns goal into "thesis ==> #thesis" *} - <proof body> - apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into - "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *} - <proof end> - } - fix x assm <<obtain_export>> "A x" +Generalized existence and cases rules within Isar proof text. *) signature OBTAIN = @@ -59,7 +26,9 @@ structure Obtain: OBTAIN = struct -(** obtain_export **) +(** specification elements **) + +(* obtain_export *) (* [x, A x] @@ -99,9 +68,6 @@ (eliminate ctxt rule xs As, eliminate_term ctxt xs); - -(** specification elements **) - (* result declaration *) fun obtains_attributes (obtains: ('typ, 'term) Element.obtain list) = @@ -207,7 +173,23 @@ -(** obtain **) +(** obtain: augmented context based on generalized existence rule **) + +(* + <chain_facts> + obtain x where "A x" <proof> == + + have "!!thesis. (!!x. A x ==> thesis) ==> thesis" + proof succeed + fix thesis + assume that [intro?]: "!!x. A x ==> thesis" + <chain_facts> + show thesis + apply (insert that) + <proof> + qed + fix x assm <<obtain_export>> "A x" +*) local @@ -315,7 +297,23 @@ -(** guess **) +(** guess: obtain based on tactical result **) + +(* + <chain_facts> + guess x <proof body> <proof end> == + + { + fix thesis + <chain_facts> have "PROP ?guess" + apply magic -- {* turns goal into "thesis ==> #thesis" *} + <proof body> + apply_end magic -- {* turns final "(!!x. P x ==> thesis) ==> #thesis" into + "#((!!x. A x ==> thesis) ==> thesis)" which is a finished goal state *} + <proof end> + } + fix x assm <<obtain_export>> "A x" +*) local