443 |
443 |
444 @{subgoals[display,indent=0]} |
444 @{subgoals[display,indent=0]} |
445 *} |
445 *} |
446 |
446 |
447 oops |
447 oops |
|
448 |
|
449 section {* Elimination *} |
|
450 |
|
451 text {* |
|
452 A definition of function @{text f} gives rise to two kinds of elimination rules. Rule @{text f.cases} |
|
453 simply describes case analysis according to the patterns used in the definition: |
|
454 *} |
|
455 |
|
456 fun list_to_option :: "'a list \<Rightarrow> 'a option" |
|
457 where |
|
458 "list_to_option [x] = Some x" |
|
459 | "list_to_option _ = None" |
|
460 |
|
461 thm list_to_option.cases |
|
462 text {* |
|
463 @{thm[display] list_to_option.cases} |
|
464 |
|
465 Note that this rule does not mention the function at all, but only describes the cases used for |
|
466 defining it. In contrast, the rule @{thm[source] list_to_option.elims} also tell us what the function |
|
467 value will be in each case: |
|
468 *} |
|
469 thm list_to_option.elims |
|
470 text {* |
|
471 @{thm[display] list_to_option.elims} |
|
472 |
|
473 \noindent |
|
474 This lets us eliminate an assumption of the form @{prop "list_to_option xs = y"} and replace it |
|
475 with the two cases, e.g.: |
|
476 *} |
|
477 |
|
478 lemma "list_to_option xs = y \<Longrightarrow> P" |
|
479 proof (erule list_to_option.elims) |
|
480 fix x assume "xs = [x]" "y = Some x" thus P sorry |
|
481 next |
|
482 assume "xs = []" "y = None" thus P sorry |
|
483 next |
|
484 fix a b xs' assume "xs = a # b # xs'" "y = None" thus P sorry |
|
485 qed |
|
486 |
|
487 |
|
488 text {* |
|
489 Sometimes it is convenient to derive specialized versions of the @{text elim} rules above and |
|
490 keep them around as facts explicitly. For example, it is natural to show that if |
|
491 @{prop "list_to_option xs = Some y"}, then @{term xs} must be a singleton. The command |
|
492 \cmd{fun\_cases} derives such facts automatically, by instantiating and simplifying the general |
|
493 elimination rules given some pattern: |
|
494 *} |
|
495 |
|
496 fun_cases list_to_option_SomeE[elim]: "list_to_option xs = Some y" |
|
497 |
|
498 thm list_to_option_SomeE |
|
499 text {* |
|
500 @{thm[display] list_to_option_SomeE} |
|
501 *} |
|
502 |
448 |
503 |
449 section {* General pattern matching *} |
504 section {* General pattern matching *} |
450 text{*\label{genpats} *} |
505 text{*\label{genpats} *} |
451 |
506 |
452 subsection {* Avoiding automatic pattern splitting *} |
507 subsection {* Avoiding automatic pattern splitting *} |