--- a/doc-src/IsarRef/Thy/Proof.thy Fri Aug 12 09:17:24 2011 -0700
+++ b/doc-src/IsarRef/Thy/Proof.thy Fri Aug 12 09:17:30 2011 -0700
@@ -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
--- a/doc-src/IsarRef/Thy/document/Proof.tex Fri Aug 12 09:17:24 2011 -0700
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Fri Aug 12 09:17:30 2011 -0700
@@ -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
--- a/src/HOL/Induct/Common_Patterns.thy Fri Aug 12 09:17:24 2011 -0700
+++ b/src/HOL/Induct/Common_Patterns.thy Fri Aug 12 09:17:30 2011 -0700
@@ -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