--- a/NEWS Sat Jan 07 11:43:42 2006 +0100
+++ b/NEWS Sat Jan 07 12:26:23 2006 +0100
@@ -148,28 +148,59 @@
* Provers/induct: improved handling of simultaneous goals. Instead of
introducing object-level conjunction, the statement is now split into
several conclusions, while the corresponding symbolic cases are
-duplicated accordingly. INCOMPATIBILITY, proofs need to be structured
-explicitly, e.g. like this:
+nested accordingly. INCOMPATIBILITY, proofs need to be structured
+explicitly. For example:
lemma
fixes n :: nat
shows "P n" and "Q n"
proof (induct n)
- case 01
+ case 0 case 1
show "P 0" sorry
next
- case 02
+ case 0 case 2
show "Q 0" sorry
next
- case (Suc1 n)
+ case (Suc n) case 1
note `P n` and `Q n`
show "P (Suc n)" sorry
next
- case (Suc2 n)
+ case (Suc n) case 2
note `P n` and `Q n`
show "Q (Suc n)" sorry
qed
+The split into subcases may be deferred as follows -- this is
+particularly relevant for goal statements with local premises.
+
+ lemma
+ fixes n :: nat
+ shows "A n ==> P n" and "B n ==> Q n"
+ proof (induct n)
+ case 0
+ {
+ case 1
+ note `A 0`
+ show "P 0" sorry
+ next
+ case 2
+ note `B 0`
+ show "Q 0" sorry
+ }
+ next
+ case (Suc n)
+ note `A n ==> P n` and `B n ==> Q n`
+ {
+ case 1
+ note `A (Suc n)`
+ show "P (Suc n)" sorry
+ next
+ case 2
+ note `B (Suc n)`
+ show "Q (Suc n)" sorry
+ }
+ qed
+
If simultaneous goals are to be used with mutual rules, the statement
needs to be structured carefully as a two-level conjunction, using
lists of propositions separated by 'and':