1221 It is important to note that there is a fundamental difference of the $cases$ |
1221 It is important to note that there is a fundamental difference of the $cases$ |
1222 and $induct$ methods in handling of non-atomic goal statements: $cases$ just |
1222 and $induct$ methods in handling of non-atomic goal statements: $cases$ just |
1223 applies a certain rule in backward fashion, splitting the result into new |
1223 applies a certain rule in backward fashion, splitting the result into new |
1224 goals with the local contexts being augmented in a purely monotonic manner. |
1224 goals with the local contexts being augmented in a purely monotonic manner. |
1225 |
1225 |
1226 In contrast, $induct$ passes the full goal statement through the ``recursive'' |
1226 In contrast, $induct$ passes the full goal statement through the |
1227 course involved in the induction. Thus the original statement is basically |
1227 ``recursive'' course involved in the induction. Thus the original statement |
1228 replaced by separate copies, corresponding to the induction hypotheses and |
1228 is basically replaced by separate copies, corresponding to the induction |
1229 conclusion; the original goal context is no longer available. This behavior |
1229 hypotheses and conclusion; the original goal context is no longer available. |
1230 allows \emph{strengthened induction predicates} to be expressed concisely as |
1230 This behavior allows \emph{strengthened induction predicates} to be expressed |
1231 meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp \psi$ to |
1231 concisely as meta-level rule statements, i.e.\ $\All{\vec x} \vec\phi \Imp |
1232 indicate ``variable'' parameters $\vec x$ and ``recursive'' assumptions |
1232 \psi$ to indicate ``variable'' parameters $\vec x$ and ``recursive'' |
1233 $\vec\phi$. Also note that local definitions may be expressed as $\All{\vec |
1233 assumptions $\vec\phi$. Note that ``$\isarcmd{case}~c$'' already performs |
1234 x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$. |
1234 ``$\FIX{\vec x}$''. Also note that local definitions may be expressed as |
|
1235 $\All{\vec x} n \equiv t[\vec x] \Imp \phi[n]$, with induction over $n$. |
|
1236 |
1235 |
1237 |
1236 In induction proofs, local assumptions introduced by cases are split into two |
1238 In induction proofs, local assumptions introduced by cases are split into two |
1237 different kinds: $hyps$ stemming from the rule and $prems$ from the goal |
1239 different kinds: $hyps$ stemming from the rule and $prems$ from the goal |
1238 statement. This is reflected in the extracted cases accordingly, so invoking |
1240 statement. This is reflected in the extracted cases accordingly, so invoking |
1239 ``$\isarcmd{case}~c$'' will provide separate facts $c\mathord.hyps$ and |
1241 ``$\isarcmd{case}~c$'' will provide separate facts $c\mathord.hyps$ and |