# HG changeset patch # User wenzelm # Date 1454872835 -3600 # Node ID 443256a200336884905bfd9affed5bb88c55690c # Parent e6669fdfe75953ab052f69b7537fd87feabbade5 more on 'consider'; diff -r e6669fdfe759 -r 443256a20033 src/Doc/Isar_Ref/Synopsis.thy --- a/src/Doc/Isar_Ref/Synopsis.thy Sun Feb 07 19:49:50 2016 +0100 +++ b/src/Doc/Isar_Ref/Synopsis.thy Sun Feb 07 20:20:35 2016 +0100 @@ -313,10 +313,10 @@ \ -subsection \Degenerate calculations and bigstep reasoning\ +subsection \Degenerate calculations\ -text \The Idea is to append \this\ to \calculation\, - without rule composition.\ +text \The Idea is to append \this\ to \calculation\, without rule composition. + This is occasionally useful to avoid naming intermediate facts.\ notepad begin @@ -337,19 +337,11 @@ have C \ ultimately have "A \ B \ C" by blast -next - txt \More ambitious bigstep reasoning involving structured results:\ - have "A \ B \ C" \ - moreover - { assume A have R \ } - moreover - { assume B have R \ } - moreover - { assume C have R \ } - ultimately - have R by blast \ \``big-bang integration'' of proof blocks (occasionally fragile)\ end +text \Note that For multi-branch case splitting, it is better to use @{command + consider}.\ + section \Induction\ @@ -1055,6 +1047,36 @@ end +subsection \Elimination statements and case-splitting\ + +text \ + The @{command consider} states rules for generalized elimination and case + splitting. This is like a toplevel statement \<^theory_text>\theorem obtains\ used within + a proof body; or like a multi-branch \<^theory_text>\obtain\ without activation of the + local context elements yet. + + The proof method @{method cases} is able to use such rules with + forward-chaining (e.g.\ via \<^theory_text>\then\). This leads to the subsequent pattern + for case-splitting in a particular situation within a proof. +\ + +notepad +begin + consider (a) A | (b) B | (c) C + \ \ \typically \<^theory_text>\by auto\, \<^theory_text>\by blast\ etc.\ + then have something + proof cases + case a + then show ?thesis \ + next + case b + then show ?thesis \ + next + case c + then show ?thesis \ + qed +end + subsection \Obtaining local contexts\ text \A single ``case'' branch may be inlined into Isar proof text