merged
authorhuffman
Fri Aug 12 09:17:30 2011 -0700 (2011-08-12)
changeset 4417175ea0e390a92
parent 44170 510ac30f44c0
parent 44164 238c5ea1e2ce
child 44172 21f97048b478
child 44174 d1d79f0e1ea6
merged
     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