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

author | wenzelm |

Wed, 23 Nov 2005 18:52:00 +0100 | |

changeset 18233 | 5a124c76e92f |

parent 18232 | bc367912603f |

child 18234 | 0183318232f2 |

tuned;

NEWS | file | annotate | diff | comparison | revisions | |

doc-src/IsarRef/pure.tex | file | annotate | diff | comparison | revisions |

--- a/NEWS Wed Nov 23 18:51:59 2005 +0100 +++ b/NEWS Wed Nov 23 18:52:00 2005 +0100 @@ -61,6 +61,48 @@ have "!!x. P x ==> Q x" by fact == note `!!x. P x ==> Q x` have "P a ==> Q a" by fact == note `P a ==> Q a` +* 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 +(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 +parameters: + + lemma + fixes n :: nat and x :: 'a + assumes a: "A n x" + shows "P n x" + using a -- {* make induct insert fact a *} + proof (induct n fixing: x) -- {* generalize goal to "!!x. A n x ==> P n x" *} + case (0 x) + show ?case sorry + next + case (Suc n x) + note `!!x. A n x ==> P n x` -- {* induction hypotheses, according to induction rule *} + note `A (Suc n) x` -- {* induction premises, stemming from fact a *} + show ?case sorry + qed + +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 +sufficiently flexible induction hypotheses). + + lemma + fixes a :: "'a => nat" + assumes a: "A (a x)" + shows "P (a x)" + using a + proof (induct n == "a x" fixing: x) + ... + +See also HOL/Isar_examples/Puzzle.thy for an application of the latter +technique. + * Input syntax now supports dummy variable binding "%_. b", where the body does not mention the bound variable. Note that dummy patterns implicitly depend on their context of bounds, which makes "{_. _}"

--- a/doc-src/IsarRef/pure.tex Wed Nov 23 18:51:59 2005 +0100 +++ b/doc-src/IsarRef/pure.tex Wed Nov 23 18:52:00 2005 +0100 @@ -838,7 +838,7 @@ corresponding number of sub-goals prior to an initial method application, via $\PROOFNAME$ (\S\ref{sec:proof-steps}) or $\APPLYNAME$ (\S\ref{sec:tactic-commands}). The $induct$ method covered in -\S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously. +\S\ref{sec:cases-induct} acts on multiple claims simultaneously. Claims at the theory level may be either in short or long form. A short goal merely consists of several simultaneous propositions (often just one). A long