# HG changeset patch
# User nipkow
# Date 1313161290 -7200
# Node ID 238c5ea1e2ceba8660b2e5e96202ef2ab13d611c
# Parent  a21d3e1e64fd0d6ee0af77da921a329da0527de1
documented extended version of case_names attribute

diff -r a21d3e1e64fd -r 238c5ea1e2ce doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Thu Aug 11 20:32:44 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Fri Aug 12 17:01:30 2011 +0200
@@ -1189,7 +1189,7 @@
     caseref: nameref attributes?
     ;
 
-    @@{attribute case_names} (@{syntax name} +)
+    @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +)
     ;
     @@{attribute case_conclusion} @{syntax name} (@{syntax name} * )
     ;
@@ -1212,7 +1212,10 @@
   
   \item @{attribute case_names}~@{text "c\<^sub>1 \<dots> c\<^sub>k"} declares names for
   the local contexts of premises of a theorem; @{text "c\<^sub>1, \<dots>, c\<^sub>k"}
-  refers to the \emph{suffix} of the list of premises.
+  refers to the \emph{prefix} of the list of premises. Each of the
+  cases @{text "c\<^isub>i"} can be of the form @{text "c[h\<^isub>1 \<dots> h\<^isub>n]"} where
+  the @{text "h\<^isub>1 \<dots> h\<^isub>n"} are the names of the hypotheses in case @{text "c\<^isub>i"}
+  from left to right.
   
   \item @{attribute case_conclusion}~@{text "c d\<^sub>1 \<dots> d\<^sub>k"} declares
   names for the conclusions of a named premise @{text c}; here @{text
diff -r a21d3e1e64fd -r 238c5ea1e2ce doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Thu Aug 11 20:32:44 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Fri Aug 12 17:01:30 2011 +0200
@@ -1594,11 +1594,24 @@
 \rail@nont{\isa{attributes}}[]
 \rail@endbar
 \rail@end
-\rail@begin{2}{}
+\rail@begin{5}{}
 \rail@term{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}}[]
 \rail@plus
 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
-\rail@nextplus{1}
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
+\rail@plus
+\rail@bar
+\rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]
+\rail@nextbar{2}
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@endbar
+\rail@nextplus{3}
+\rail@endplus
+\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
+\rail@endbar
+\rail@nextplus{4}
 \rail@endplus
 \rail@end
 \rail@begin{2}{}
@@ -1642,7 +1655,10 @@
   
   \item \hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} declares names for
   the local contexts of premises of a theorem; \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}}
-  refers to the \emph{suffix} of the list of premises.
+  refers to the \emph{prefix} of the list of premises. Each of the
+  cases \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}} can be of the form \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{5B}{\isacharbrackleft}}h\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ h\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} where
+  the \isa{{\isaliteral{22}{\isachardoublequote}}h\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ h\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} are the names of the hypotheses in case \isa{{\isaliteral{22}{\isachardoublequote}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub i{\isaliteral{22}{\isachardoublequote}}}
+  from left to right.
   
   \item \hyperlink{attribute.case-conclusion}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}conclusion}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} declares
   names for the conclusions of a named premise \isa{c}; here \isa{{\isaliteral{22}{\isachardoublequote}}d\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ d\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{22}{\isachardoublequote}}} refers to the prefix of arguments of a logical formula
diff -r a21d3e1e64fd -r 238c5ea1e2ce src/HOL/Induct/Common_Patterns.thy
--- a/src/HOL/Induct/Common_Patterns.thy	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/HOL/Induct/Common_Patterns.thy	Fri Aug 12 17:01:30 2011 +0200
@@ -378,4 +378,29 @@
   { case 3 show "P3 (Suc n)" sorry }
 qed
 
+
+text {*
+  Cases and hypotheses in each case can be named explicitly.
+*}
+
+inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r
+where
+  refl: "star r x x"
+| step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
+
+text{* Underscores are replaced by the default name hyps: *}
+
+lemmas star_induct = star.induct[case_names base step[r _ IH]]
+
+lemma "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
+proof(induct rule: star_induct)
+print_cases
+  case base thus ?case .
+next
+  case (step a b c)
+  from step.prems have "star r b z" by(rule step.IH)
+  from step.r this show ?case by(rule star.step)
+qed
+
+
 end
\ No newline at end of file