# HG changeset patch
# User krauss
# Date 1380664006 -7200
# Node ID 2a3c07f49615ca3130c44d8f7b5bed32ecd8aeb8
# Parent  769fcbdf2918095296ef84a8ba4dab7692d034d1
basic documentation for function elimination rules and fun_cases

diff -r 769fcbdf2918 -r 2a3c07f49615 src/Doc/Functions/Functions.thy
--- 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} *}
 
diff -r 769fcbdf2918 -r 2a3c07f49615 src/Doc/IsarRef/HOL_Specific.thy
--- 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"}
diff -r 769fcbdf2918 -r 2a3c07f49615 src/Doc/ROOT
--- 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"