1.1 --- a/doc-src/IsarRef/Thy/Proof.thy Fri Aug 12 09:17:24 2011 -0700
1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy Fri Aug 12 09:17:30 2011 -0700
1.3 @@ -1189,7 +1189,7 @@
1.4 caseref: nameref attributes?
1.5 ;
1.6
1.7 - @@{attribute case_names} (@{syntax name} +)
1.8 + @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +)
1.9 ;
1.10 @@{attribute case_conclusion} @{syntax name} (@{syntax name} * )
1.11 ;
1.12 @@ -1212,7 +1212,10 @@
1.13
1.14 \item @{attribute case_names}~@{text "c\<^sub>1 \<dots> c\<^sub>k"} declares names for
1.15 the local contexts of premises of a theorem; @{text "c\<^sub>1, \<dots>, c\<^sub>k"}
1.16 - refers to the \emph{suffix} of the list of premises.
1.17 + refers to the \emph{prefix} of the list of premises. Each of the
1.18 + cases @{text "c\<^isub>i"} can be of the form @{text "c[h\<^isub>1 \<dots> h\<^isub>n]"} where
1.19 + the @{text "h\<^isub>1 \<dots> h\<^isub>n"} are the names of the hypotheses in case @{text "c\<^isub>i"}
1.20 + from left to right.
1.21
1.22 \item @{attribute case_conclusion}~@{text "c d\<^sub>1 \<dots> d\<^sub>k"} declares
1.23 names for the conclusions of a named premise @{text c}; here @{text
2.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex Fri Aug 12 09:17:24 2011 -0700
2.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Fri Aug 12 09:17:30 2011 -0700
2.3 @@ -1594,11 +1594,24 @@
2.4 \rail@nont{\isa{attributes}}[]
2.5 \rail@endbar
2.6 \rail@end
2.7 -\rail@begin{2}{}
2.8 +\rail@begin{5}{}
2.9 \rail@term{\hyperlink{attribute.case-names}{\mbox{\isa{case{\isaliteral{5F}{\isacharunderscore}}names}}}}[]
2.10 \rail@plus
2.11 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
2.12 -\rail@nextplus{1}
2.13 +\rail@bar
2.14 +\rail@nextbar{1}
2.15 +\rail@term{\isa{{\isaliteral{5B}{\isacharbrackleft}}}}[]
2.16 +\rail@plus
2.17 +\rail@bar
2.18 +\rail@term{\isa{{\isaliteral{5F}{\isacharunderscore}}}}[]
2.19 +\rail@nextbar{2}
2.20 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
2.21 +\rail@endbar
2.22 +\rail@nextplus{3}
2.23 +\rail@endplus
2.24 +\rail@term{\isa{{\isaliteral{5D}{\isacharbrackright}}}}[]
2.25 +\rail@endbar
2.26 +\rail@nextplus{4}
2.27 \rail@endplus
2.28 \rail@end
2.29 \rail@begin{2}{}
2.30 @@ -1642,7 +1655,10 @@
2.31
2.32 \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
2.33 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}}}
2.34 - refers to the \emph{suffix} of the list of premises.
2.35 + refers to the \emph{prefix} of the list of premises. Each of the
2.36 + 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
2.37 + 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}}}
2.38 + from left to right.
2.39
2.40 \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
2.41 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
3.1 --- a/src/HOL/Induct/Common_Patterns.thy Fri Aug 12 09:17:24 2011 -0700
3.2 +++ b/src/HOL/Induct/Common_Patterns.thy Fri Aug 12 09:17:30 2011 -0700
3.3 @@ -378,4 +378,29 @@
3.4 { case 3 show "P3 (Suc n)" sorry }
3.5 qed
3.6
3.7 +
3.8 +text {*
3.9 + Cases and hypotheses in each case can be named explicitly.
3.10 +*}
3.11 +
3.12 +inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r
3.13 +where
3.14 + refl: "star r x x"
3.15 +| step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
3.16 +
3.17 +text{* Underscores are replaced by the default name hyps: *}
3.18 +
3.19 +lemmas star_induct = star.induct[case_names base step[r _ IH]]
3.20 +
3.21 +lemma "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
3.22 +proof(induct rule: star_induct)
3.23 +print_cases
3.24 + case base thus ?case .
3.25 +next
3.26 + case (step a b c)
3.27 + from step.prems have "star r b z" by(rule step.IH)
3.28 + from step.r this show ?case by(rule star.step)
3.29 +qed
3.30 +
3.31 +
3.32 end
3.33 \ No newline at end of file