1.1 --- a/src/Doc/Functions/Functions.thy	Tue Oct 01 23:50:35 2013 +0200
     1.2 +++ b/src/Doc/Functions/Functions.thy	Tue Oct 01 23:51:15 2013 +0200
     1.3 @@ -446,6 +446,61 @@
     1.4  
     1.5  oops
     1.6  
     1.7 +section {* Elimination *}
     1.8 +
     1.9 +text {* 
    1.10 +  A definition of function @{text f} gives rise to two kinds of elimination rules. Rule @{text f.cases}
    1.11 +  simply describes case analysis according to the patterns used in the definition:
    1.12 +*}
    1.13 +
    1.14 +fun list_to_option :: "'a list \<Rightarrow> 'a option"
    1.15 +where
    1.16 +  "list_to_option [x] = Some x"
    1.17 +| "list_to_option _ = None"
    1.18 +
    1.19 +thm list_to_option.cases
    1.20 +text {*
    1.21 +  @{thm[display] list_to_option.cases}
    1.22 +
    1.23 +  Note that this rule does not mention the function at all, but only describes the cases used for
    1.24 +  defining it. In contrast, the rule @{thm[source] list_to_option.elims} also tell us what the function
    1.25 +  value will be in each case:
    1.26 +*}
    1.27 +thm list_to_option.elims
    1.28 +text {*
    1.29 +  @{thm[display] list_to_option.elims}
    1.30 +
    1.31 +  \noindent
    1.32 +  This lets us eliminate an assumption of the form @{prop "list_to_option xs = y"} and replace it
    1.33 +  with the two cases, e.g.:
    1.34 +*}
    1.35 +
    1.36 +lemma "list_to_option xs = y \<Longrightarrow> P"
    1.37 +proof (erule list_to_option.elims)
    1.38 +  fix x assume "xs = [x]" "y = Some x" thus P sorry
    1.39 +next
    1.40 +  assume "xs = []" "y = None" thus P sorry
    1.41 +next
    1.42 +  fix a b xs' assume "xs = a # b # xs'" "y = None" thus P sorry
    1.43 +qed
    1.44 +
    1.45 +
    1.46 +text {*
    1.47 +  Sometimes it is convenient to derive specialized versions of the @{text elim} rules above and
    1.48 +  keep them around as facts explicitly. For example, it is natural to show that if 
    1.49 +  @{prop "list_to_option xs = Some y"}, then @{term xs} must be a singleton. The command 
    1.50 +  \cmd{fun\_cases} derives such facts automatically, by instantiating and simplifying the general 
    1.51 +  elimination rules given some pattern:
    1.52 +*}
    1.53 +
    1.54 +fun_cases list_to_option_SomeE[elim]: "list_to_option xs = Some y"
    1.55 +
    1.56 +thm list_to_option_SomeE
    1.57 +text {*
    1.58 +  @{thm[display] list_to_option_SomeE}
    1.59 +*}
    1.60 +
    1.61 +
    1.62  section {* General pattern matching *}
    1.63  text{*\label{genpats} *}
    1.64  

     2.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Tue Oct 01 23:50:35 2013 +0200
     2.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Tue Oct 01 23:51:15 2013 +0200
     2.3 @@ -261,6 +261,7 @@
     2.4      @{command_def (HOL) "fun"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.5      @{command_def (HOL) "function"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
     2.6      @{command_def (HOL) "termination"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
     2.7 +    @{command_def (HOL) "fun_cases"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     2.8    \end{matharray}
     2.9  
    2.10    @{rail "
    2.11 @@ -275,6 +276,8 @@
    2.12      functionopts: '(' (('sequential' | 'domintros') + ',') ')'
    2.13      ;
    2.14      @@{command (HOL) termination} @{syntax term}?
    2.15 +    ;
    2.16 +    @@{command (HOL) fun_cases} (@{syntax thmdecl}? @{syntax prop} + @'and')
    2.17    "}
    2.18  
    2.19    \begin{description}
    2.20 @@ -329,6 +332,10 @@
    2.21    definition.  After the proof is closed, the recursive equations and
    2.22    the induction principle is established.
    2.23  
    2.24 +  \item @{command (HOL) "fun_cases"} generates specialized elimination
    2.25 +  rules for function equations. It expects one or more function equations
    2.26 +  and produces rules that eliminate the given equalities, following the cases
    2.27 +  given in the function definition.
    2.28    \end{description}
    2.29  
    2.30    Recursive definitions introduced by the @{command (HOL) "function"}

     3.1 --- a/src/Doc/ROOT	Tue Oct 01 23:50:35 2013 +0200
     3.2 +++ b/src/Doc/ROOT	Tue Oct 01 23:51:15 2013 +0200
     3.3 @@ -53,7 +53,7 @@
     3.4      "document/style.sty"
     3.5  
     3.6  session Functions (doc) in "Functions" = HOL +
     3.7 -  options [document_variants = "functions", skip_proofs = false]
     3.8 +  options [document_variants = "functions", skip_proofs = false, quick_and_dirty]
     3.9    theories Functions
    3.10    files
    3.11      "../prepare_document"