450 definition. After the proof is closed, the recursive equations and |
450 definition. After the proof is closed, the recursive equations and |
451 the induction principle is established. |
451 the induction principle is established. |
452 |
452 |
453 \end{description} |
453 \end{description} |
454 |
454 |
455 %FIXME check |
|
456 |
|
457 Recursive definitions introduced by the @{command (HOL) "function"} |
455 Recursive definitions introduced by the @{command (HOL) "function"} |
458 command accommodate |
456 command accommodate |
459 reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text |
457 reasoning by induction (cf.\ \secref{sec:cases-induct}): rule @{text |
460 "c.induct"} (where @{text c} is the name of the function definition) |
458 "c.induct"} (where @{text c} is the name of the function definition) |
461 refers to a specific induction rule, with parameters named according |
459 refers to a specific induction rule, with parameters named according |
462 to the user-specified equations. |
460 to the user-specified equations. Cases are numbered (starting from 1). |
463 For the @{command (HOL) "primrec"} the induction principle coincides |
461 |
|
462 For @{command (HOL) "primrec"}, the induction principle coincides |
464 with structural recursion on the datatype the recursion is carried |
463 with structural recursion on the datatype the recursion is carried |
465 out. |
464 out. |
466 Case names of @{command (HOL) |
|
467 "primrec"} are that of the datatypes involved, while those of |
|
468 @{command (HOL) "function"} are numbered (starting from 1). |
|
469 |
465 |
470 The equations provided by these packages may be referred later as |
466 The equations provided by these packages may be referred later as |
471 theorem list @{text "f.simps"}, where @{text f} is the (collective) |
467 theorem list @{text "f.simps"}, where @{text f} is the (collective) |
472 name of the functions defined. Individual equations may be named |
468 name of the functions defined. Individual equations may be named |
473 explicitly as well. |
469 explicitly as well. |