--- a/src/Doc/Functions/Functions.thy Tue Oct 01 22:50:42 2013 +0200
+++ b/src/Doc/Functions/Functions.thy Tue Oct 01 23:46:46 2013 +0200
@@ -446,6 +446,61 @@
oops
+section {* Elimination *}
+
+text {*
+ A definition of function @{text f} gives rise to two kinds of elimination rules. Rule @{text f.cases}
+ simply describes case analysis according to the patterns used in the definition:
+*}
+
+fun list_to_option :: "'a list \<Rightarrow> 'a option"
+where
+ "list_to_option [x] = Some x"
+| "list_to_option _ = None"
+
+thm list_to_option.cases
+text {*
+ @{thm[display] list_to_option.cases}
+
+ Note that this rule does not mention the function at all, but only describes the cases used for
+ defining it. In contrast, the rule @{thm[source] list_to_option.elims} also tell us what the function
+ value will be in each case:
+*}
+thm list_to_option.elims
+text {*
+ @{thm[display] list_to_option.elims}
+
+ \noindent
+ This lets us eliminate an assumption of the form @{prop "list_to_option xs = y"} and replace it
+ with the two cases, e.g.:
+*}
+
+lemma "list_to_option xs = y \<Longrightarrow> P"
+proof (erule list_to_option.elims)
+ fix x assume "xs = [x]" "y = Some x" thus P sorry
+next
+ assume "xs = []" "y = None" thus P sorry
+next
+ fix a b xs' assume "xs = a # b # xs'" "y = None" thus P sorry
+qed
+
+
+text {*
+ Sometimes it is convenient to derive specialized versions of the @{text elim} rules above and
+ keep them around as facts explicitly. For example, it is natural to show that if
+ @{prop "list_to_option xs = Some y"}, then @{term xs} must be a singleton. The command
+ \cmd{fun\_cases} derives such facts automatically, by instantiating and simplifying the general
+ elimination rules given some pattern:
+*}
+
+fun_cases list_to_option_SomeE[elim]: "list_to_option xs = Some y"
+
+thm list_to_option_SomeE
+text {*
+ @{thm[display] list_to_option_SomeE}
+*}
+
+
section {* General pattern matching *}
text{*\label{genpats} *}
--- a/src/Doc/IsarRef/HOL_Specific.thy Tue Oct 01 22:50:42 2013 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy Tue Oct 01 23:46:46 2013 +0200
@@ -261,6 +261,7 @@
@{command_def (HOL) "fun"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def (HOL) "function"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
@{command_def (HOL) "termination"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
+ @{command_def (HOL) "fun_cases"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
\end{matharray}
@{rail "
@@ -275,6 +276,8 @@
functionopts: '(' (('sequential' | 'domintros') + ',') ')'
;
@@{command (HOL) termination} @{syntax term}?
+ ;
+ @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and')
"}
\begin{description}
@@ -329,6 +332,10 @@
definition. After the proof is closed, the recursive equations and
the induction principle is established.
+ \item @{command (HOL) "fun_cases"} generates specialized elimination
+ rules for function equations. It expects one or more function equations
+ and produces rules that eliminate the given equalities, following the cases
+ given in the function definition.
\end{description}
Recursive definitions introduced by the @{command (HOL) "function"}
--- a/src/Doc/ROOT Tue Oct 01 22:50:42 2013 +0200
+++ b/src/Doc/ROOT Tue Oct 01 23:46:46 2013 +0200
@@ -53,7 +53,7 @@
"document/style.sty"
session Functions (doc) in "Functions" = HOL +
- options [document_variants = "functions", skip_proofs = false]
+ options [document_variants = "functions", skip_proofs = false, quick_and_dirty]
theories Functions
files
"../prepare_document"