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

author | nipkow |

Wed, 02 Oct 2002 17:25:31 +0200 | |

changeset 13622 | 9768ba6ab5e7 |

parent 13621 | 75ae05e894fa |

child 13623 | c2b235e60f8b |

*** empty log message ***

--- a/doc-src/IsarRef/generic.tex Wed Oct 02 17:03:51 2002 +0200 +++ b/doc-src/IsarRef/generic.tex Wed Oct 02 17:25:31 2002 +0200 @@ -1223,15 +1223,17 @@ applies a certain rule in backward fashion, splitting the result into new goals with the local contexts being augmented in a purely monotonic manner. -In contrast, $induct$ passes the full goal statement through the ``recursive'' -course involved in the induction. Thus the original statement is basically -replaced by separate copies, corresponding to the induction hypotheses and -conclusion; the original goal context is no longer available. This behavior -allows \emph{strengthened induction predicates} to be expressed concisely as -meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to -indicate ``variable'' parameters $\vec x$ and ``recursive'' assumptions -$\vec\phi$. Also note that local definitions may be expressed as $\All{\vec - x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$. +In contrast, $induct$ passes the full goal statement through the +``recursive'' course involved in the induction. Thus the original statement +is basically replaced by separate copies, corresponding to the induction +hypotheses and conclusion; the original goal context is no longer available. +This behavior allows \emph{strengthened induction predicates} to be expressed +concisely as meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp +\psi$ to indicate ``variable'' parameters $\vec x$ and ``recursive'' +assumptions $\vec\phi$. Note that ``$\isarcmd{case}~c$'' already performs +``$\FIX{\vec x}$''. Also note that local definitions may be expressed as +$\All{\vec x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$. + In induction proofs, local assumptions introduced by cases are split into two different kinds: $hyps$ stemming from the rule and $prems$ from the goal