author blanchet Tue, 01 Oct 2013 23:51:15 +0200 changeset 54020 0c7b5aa453bb parent 54019 1878bab3e1c9 (current diff) parent 54017 2a3c07f49615 (diff) child 54021 8089e82833b6
merged
--- a/src/Doc/Functions/Functions.thy	Tue Oct 01 23:50:35 2013 +0200
+++ b/src/Doc/Functions/Functions.thy	Tue Oct 01 23:51:15 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 23:50:35 2013 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Tue Oct 01 23:51:15 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 23:50:35 2013 +0200
+++ b/src/Doc/ROOT	Tue Oct 01 23:51:15 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"