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

author | wenzelm |

Sun, 27 Nov 2005 20:06:24 +0100 | |

changeset 18267 | 5ee688e36eeb |

parent 18266 | 55c201fe4c95 |

child 18268 | 734f23ad5d8f |

* Provers/induct: obtain pattern;

--- a/NEWS Sun Nov 27 06:01:11 2005 +0100 +++ b/NEWS Sun Nov 27 20:06:24 2005 +0100 @@ -67,9 +67,9 @@ (using object-logic connectives for this purpose has been long obsolete anyway). The subsequent proof patterns illustrate advanced techniques of natural induction; general datatypes and inductive sets -work analogously. - -This is how to ``strengthen'' an inductive goal wrt. certain +work analogously (see also src/HOL/Lambda for realistic examples). + +(1) This is how to ``strengthen'' an inductive goal wrt. certain parameters: lemma @@ -87,10 +87,10 @@ show ?case sorry qed -This is how to perform induction over ``expressions of a certain +(2) This is how to perform induction over ``expressions of a certain form'', using a locally defined inductive parameter n == "a x" together with strengthening (the latter is usually required to get -sufficiently flexible induction hypotheses). +sufficiently flexible induction hypotheses): lemma fixes a :: "'a => nat" @@ -100,8 +100,28 @@ proof (induct n == "a x" fixing: x) ... -See also HOL/Isar_examples/Puzzle.thy for an application of the latter -technique. +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" + proof (induct n fixing: thesis) + case 0 + obtain x where "P 0 x" and "Q 0 x" sorry + then show thesis by (rule "0.prems") + next + case (Suc n) + obtain x where "P n x" and "Q n x" by (rule Suc.hyps) + obtain x where "P (Suc n) x" and "Q (Suc n) x" sorry + then show thesis by (rule Suc.prems) + qed + +Here the 'fixing: thesis' specification essentially modifies the scope +of the formal thesis parameter, in order to the get the whole +existence statement through the induction as expected. * Input syntax now supports dummy variable binding "%_. b", where the body does not mention the bound variable. Note that dummy patterns