1 files changed, 13 insertions, 4 deletions
diff --git a/Test/dafny4/NipkowKlein-chapter3.dfy b/Test/dafny4/NipkowKlein-chapter3.dfy
index 6572359a..3de6a5fc 100644
--- a/Test/dafny4/NipkowKlein-chapter3.dfy
+++ b/Test/dafny4/NipkowKlein-chapter3.dfy
@@ -18,7 +18,7 @@ function append(xs: List, ys: List): List
 // ----- arithmetic expressions -----
 
 type vname = string  // variable names
-datatype aexp = N(n: int) | V(x: vname) | Plus(0: aexp, 1: aexp)  // arithmetic expressions
+datatype aexp = N(n: int) | V(vname) | Plus(aexp, aexp)  // arithmetic expressions
 
 type val = int
 type state = vname -> val
@@ -131,9 +131,15 @@ lemma AsimpCorrect(a: aexp, s: state)
   forall a' | a' < a { AsimpCorrect(a', s); }
 }
 
+// The following lemma is not in the Nipkow and Klein book, but it's a fun one to prove.
+lemma ASimplInvolutive(a: aexp)
+  ensures asimp(asimp(a)) == asimp(a)
+{
+}
+
 // ----- boolean expressions -----
 
-datatype bexp = Bc(v: bool) | Not(op: bexp) | And(0: bexp, 1: bexp) | Less(a0: aexp, a1: aexp)
+datatype bexp = Bc(v: bool) | Not(bexp) | And(bexp, bexp) | Less(aexp, aexp)
 
 function bval(b: bexp, s: state): bool
   reads s.reads
@@ -189,9 +195,12 @@ lemma BsimpCorrect(b: bexp, s: state)
   ensures bval(bsimp(b), s) == bval(b, s)
 {
 /*  Here is one proof, which uses the induction hypothesis any anything smaller than b and also invokes
-    the lemma AsimpCorrect on anything smaller than b.
+    the lemma AsimpCorrect on every arithmetic expression.
   forall b' | b' < b { BsimpCorrect(b', s); } 
-  forall a' | a' < b { AsimpCorrect(a', s); }
+  forall a { AsimpCorrect(a, s); }
+    Yet another possibility is to mark the lemma with {:induction b} and to use the following line in
+    the body:
+  forall a { AsimpCorrect(a, s); }
 */
   // Here is another proof, which makes explicit the uses of the induction hypothesis and the other lemma.
   match b