Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" -> "prefix lemma")

8 files changed, 107 insertions, 107 deletions

diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy
index 287b4006..4b39876a 100644
--- a/Test/dafny3/Filter.dfy
+++ b/Test/dafny3/Filter.dfy
@@ -13,20 +13,20 @@ copredicate IsSubStream(s: Stream, u: Stream)
   In(s.head, u) && IsSubStream(s.tail, u)

 }

 

-ghost method Lemma_InTail<T>(x: T, s: Stream<T>)

+lemma Lemma_InTail<T>(x: T, s: Stream<T>)

   requires In(x, s.tail);

   ensures In(x, s);

 {

   var n :| 0 <= n && Tail(s.tail, n).head == x;

   assert Tail(s, n+1).head == x;

 }

-comethod Lemma_TailSubStream(s: Stream, u: Stream)

+colemma Lemma_TailSubStream(s: Stream, u: Stream)

   requires IsSubStream(s, u.tail);

   ensures IsSubStream(s, u);

 {

   Lemma_InTail(s.head, u);

 }

-ghost method Lemma_TailSubStreamK(s: Stream, u: Stream, k: nat)  // this lemma could have been used to prove the previous one

+lemma Lemma_TailSubStreamK(s: Stream, u: Stream, k: nat)  // this lemma could have been used to prove the previous one

   requires IsSubStream#[k](s, u.tail);

   ensures IsSubStream#[k](s, u);

 {

@@ -35,7 +35,7 @@ ghost method Lemma_TailSubStreamK(s: Stream, u: Stream, k: nat)  // this lemma c
     Lemma_TailSubStreamK(s.tail, u, k-1);

   }

 }

-ghost method Lemma_InSubStream<T>(x: T, s: Stream<T>, u: Stream<T>)

+lemma Lemma_InSubStream<T>(x: T, s: Stream<T>, u: Stream<T>)

   requires In(x, s) && IsSubStream(s, u);

   ensures In(x, u);

 {

@@ -57,7 +57,7 @@ copredicate AllP(s: Stream, h: PredicateHandle)
 {

   P(s.head, h) && AllP(s.tail, h)

 }

-ghost method Lemma_InAllP<T>(x: T, s: Stream<T>, h: PredicateHandle)

+lemma Lemma_InAllP<T>(x: T, s: Stream<T>, h: PredicateHandle)

   requires In(x, s) && AllP(s, h);

   ensures P(x, h);

 {

@@ -80,7 +80,7 @@ copredicate AlwaysAnother(s: Stream, h: PredicateHandle)
 {

   IsAnother(s, h) && AlwaysAnother(s.tail, h)

 }

-comethod Lemma_AllImpliesAlwaysAnother(s: Stream, h: PredicateHandle)

+colemma Lemma_AllImpliesAlwaysAnother(s: Stream, h: PredicateHandle)

   requires AllP(s, h);

   ensures AlwaysAnother(s, h);

 {

@@ -118,7 +118,7 @@ function Filter(s: Stream, h: PredicateHandle): Stream
     Filter(s.tail, h)

 }

 // properties about Filter

-comethod Filter_AlwaysAnother(s: Stream, h: PredicateHandle)

+colemma Filter_AlwaysAnother(s: Stream, h: PredicateHandle)

   requires AlwaysAnother(s, h);

   ensures AllP(Filter(s, h), h);

   decreases Next(s, h);

@@ -129,7 +129,7 @@ comethod Filter_AlwaysAnother(s: Stream, h: PredicateHandle)
     Filter_AlwaysAnother#[_k](s.tail, h);

   }

 }

-comethod Filter_IsSubStream(s: Stream, h: PredicateHandle)

+colemma Filter_IsSubStream(s: Stream, h: PredicateHandle)

   requires AlwaysAnother(s, h);

   ensures IsSubStream(Filter(s, h), s);

   decreases Next(s, h);

@@ -160,7 +160,7 @@ comethod Filter_IsSubStream(s: Stream, h: PredicateHandle)
 }

 

 // The following says nothing about the order of the elements in the stream

-ghost method Theorem_Filter<T>(s: Stream<T>, h: PredicateHandle)

+lemma Theorem_Filter<T>(s: Stream<T>, h: PredicateHandle)

   requires AlwaysAnother(s, h);

   ensures forall x :: In(x, Filter(s, h)) <==> In(x, s) && P(x, h);

 {

@@ -177,7 +177,7 @@ ghost method Theorem_Filter<T>(s: Stream<T>, h: PredicateHandle)
   }

 }

 

-ghost method FS_Ping<T>(s: Stream<T>, h: PredicateHandle, x: T)

+lemma FS_Ping<T>(s: Stream<T>, h: PredicateHandle, x: T)

   requires AlwaysAnother(s, h) && In(x, Filter(s, h));

   ensures In(x, s) && P(x, h);

 {

@@ -189,7 +189,7 @@ ghost method FS_Ping<T>(s: Stream<T>, h: PredicateHandle, x: T)
   Lemma_InAllP(x, Filter(s, h), h);

 }

 

-ghost method FS_Pong<T>(s: Stream<T>, h: PredicateHandle, x: T, k: nat)

+lemma FS_Pong<T>(s: Stream<T>, h: PredicateHandle, x: T, k: nat)

   requires AlwaysAnother(s, h) && In(x, s) && P(x, h);

   requires Tail(s, k).head == x;

   ensures In(x, Filter(s, h));

@@ -226,19 +226,19 @@ copredicate IncrFrom(s: Stream, low: int, ord: PredicateHandle)
   low <= Ord(s.head, ord) && IncrFrom(s.tail, Ord(s.head, ord) + 1, ord)

 }

 

-comethod Lemma_Incr0(s: Stream, low: int, ord: PredicateHandle)

+colemma Lemma_Incr0(s: Stream, low: int, ord: PredicateHandle)

   requires IncrFrom(s, low, ord);

   ensures Increasing(s, ord);

 {

 }

-comethod Lemma_Incr1(s: Stream, ord: PredicateHandle)

+colemma Lemma_Incr1(s: Stream, ord: PredicateHandle)

   requires Increasing(s, ord);

   ensures IncrFrom(s, Ord(s.head, ord), ord);

 {

   Lemma_Incr1(s.tail, ord);

 }

 

-ghost method Theorem_FilterPreservesOrdering(s: Stream, h: PredicateHandle, ord: PredicateHandle)

+lemma Theorem_FilterPreservesOrdering(s: Stream, h: PredicateHandle, ord: PredicateHandle)

   requires Increasing(s, ord) && AlwaysAnother(s, h);

   ensures Increasing(Filter(s, h), ord);

 {

@@ -246,7 +246,7 @@ ghost method Theorem_FilterPreservesOrdering(s: Stream, h: PredicateHandle, ord:
   Lemma_FilterPreservesIncrFrom(s, h, Ord(s.head, ord), ord);

   Lemma_Incr0(Filter(s, h), Ord(s.head, ord), ord);

 }

-comethod Lemma_FilterPreservesIncrFrom(s: Stream, h: PredicateHandle, low: int, ord: PredicateHandle)

+colemma Lemma_FilterPreservesIncrFrom(s: Stream, h: PredicateHandle, low: int, ord: PredicateHandle)

   requires IncrFrom(s, low, ord) && AlwaysAnother(s, h) && low <= Ord(s.head, ord);

   ensures IncrFrom(Filter(s, h), low, ord);

   decreases Next(s, h);

diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy
index 8709a6d8..5c5c0412 100644
--- a/Test/dafny3/InductionVsCoinduction.dfy
+++ b/Test/dafny3/InductionVsCoinduction.dfy
@@ -62,7 +62,7 @@ function SAppend(xs: Stream, ys: Stream): Stream
   we also get ==#[k].

 */

 

-ghost method {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream, c:Stream)

+lemma {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream, c:Stream)

   ensures SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c));

   decreases k;

 {

@@ -72,7 +72,7 @@ ghost method {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream,
   }

 }

 

-ghost method SAppendIsAssociative(a:Stream, b:Stream, c:Stream)

+lemma SAppendIsAssociative(a:Stream, b:Stream, c:Stream)

   ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c));

 {

   forall k:nat { SAppendIsAssociativeK(k, a, b, c); }

@@ -80,8 +80,8 @@ ghost method SAppendIsAssociative(a:Stream, b:Stream, c:Stream)
   assert (forall k:nat :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c)));

 }

 

-// Equivalent proof using the comethod syntax.

-comethod {:induction false} SAppendIsAssociativeC(a:Stream, b:Stream, c:Stream)

+// Equivalent proof using the colemma syntax.

+colemma {:induction false} SAppendIsAssociativeC(a:Stream, b:Stream, c:Stream)

   ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c));

 {

   match (a) {

@@ -91,26 +91,26 @@ comethod {:induction false} SAppendIsAssociativeC(a:Stream, b:Stream, c:Stream)
 }

 

 // In fact the proof can be fully automatic.

-comethod SAppendIsAssociative_Auto(a:Stream, b:Stream, c:Stream)

+colemma SAppendIsAssociative_Auto(a:Stream, b:Stream, c:Stream)

   ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c));

 {

 }

 

-comethod {:induction false} UpPos(n:int)

+colemma {:induction false} UpPos(n:int)

   requires n > 0;

   ensures Pos(Up(n));

 {

   UpPos(n+1);

 }

 

-comethod UpPos_Auto(n:int)

+colemma UpPos_Auto(n:int)

   requires n > 0;

   ensures Pos(Up(n));

 {

 }

 

 // This does induction and coinduction in the same proof.

-comethod {:induction false} FivesUpPos(n:int)

+colemma {:induction false} FivesUpPos(n:int)

   requires n > 0;

   ensures Pos(FivesUp(n));

   decreases 4 - (n-1) % 5;

@@ -124,7 +124,7 @@ comethod {:induction false} FivesUpPos(n:int)
 

 // Again, Dafny can just employ induction tactic and do it automatically.

 // The only hint required is the decrease clause.

-comethod FivesUpPos_Auto(n:int)

+colemma FivesUpPos_Auto(n:int)

   requires n > 0;

   ensures Pos(FivesUp(n));

   decreases 4 - (n-1) % 5;

diff --git a/Test/dafny3/InfiniteTrees.dfy b/Test/dafny3/InfiniteTrees.dfy
index e189dc4a..32a868bb 100644
--- a/Test/dafny3/InfiniteTrees.dfy
+++ b/Test/dafny3/InfiniteTrees.dfy
@@ -10,12 +10,12 @@ function Tail(s: Stream, n: nat): Stream
     if t == Nil then t else t.tail

 }

 

-ghost method Tail_Lemma0(s: Stream, n: nat)

+lemma Tail_Lemma0(s: Stream, n: nat)

   requires s.Cons? && Tail(s, n).Cons?;

   ensures Tail(s, n).tail == Tail(s.tail, n);

 {

 }

-ghost method Tail_Lemma1(s: Stream, k: nat, n: nat)

+lemma Tail_Lemma1(s: Stream, k: nat, n: nat)

   requires k <= n;

   ensures Tail(s, n).Cons? ==> Tail(s, k).Cons?;

   // Note, the contrapositive of this lemma says:  Tail(s, k) == Nil ==> Tail(s, n) == Nil

@@ -24,7 +24,7 @@ ghost method Tail_Lemma1(s: Stream, k: nat, n: nat)
     assert Tail(s, n) == Tail(s, n-1).tail;

   }

 }

-ghost method Tail_Lemma2(s: Stream, n: nat)

+lemma Tail_Lemma2(s: Stream, n: nat)

   requires s.Cons? && Tail(s.tail, n).Cons?;

   ensures Tail(s, n).Cons?;

 {

@@ -48,7 +48,7 @@ function AnInfiniteStream(): Stream<int>
 {

   Cons(0, AnInfiniteStream())

 }

-comethod Proposition0()

+colemma Proposition0()

   ensures IsNeverEndingStream(AnInfiniteStream());

 {

 }

@@ -76,7 +76,7 @@ copredicate LowerThan(s: Stream<Tree>, n: nat)
 // Co-predicate LowerThan(s, n) recurses on LowerThan(s.tail, n).  Thus, a property of LowerThan is that

 // LowerThan(s, h) implies LowerThan(s', h) for any suffix s' of s.

 

-ghost method LowerThan_Lemma(s: Stream<Tree>, n: nat, h: nat)

+lemma LowerThan_Lemma(s: Stream<Tree>, n: nat, h: nat)

   ensures LowerThan(s, h) ==> LowerThan(Tail(s, n), h);

 {

   Tail_Lemma1(s, 0, n);

@@ -113,7 +113,7 @@ function SkinnyTree(): Tree
 {

   Node(Cons(SkinnyTree(), Nil))

 }

-ghost method Proposition1()

+lemma Proposition1()

   ensures IsFiniteSomewhere(SkinnyTree()) && !HasBoundedHeight(SkinnyTree());

 {

   assert forall n :: 0 <= n ==> !LowerThan(SkinnyTree().children, n);

@@ -121,7 +121,7 @@ ghost method Proposition1()
 

 // Any tree where all paths have bounded height are finite somewhere.

 

-ghost method Theorem0(t: Tree)

+lemma Theorem0(t: Tree)

   requires HasBoundedHeight(t);

   ensures IsFiniteSomewhere(t);

 {

@@ -133,7 +133,7 @@ ghost method Theorem0(t: Tree)
   */

   var k := FindNil(t.children, n);

 }

-ghost method FindNil(s: Stream<Tree>, n: nat) returns (k: nat)

+lemma FindNil(s: Stream<Tree>, n: nat) returns (k: nat)

   requires LowerThan(s, n);

   ensures !InfiniteEverywhere#[k](s);

 {

@@ -175,17 +175,17 @@ function ATreeChildren(): Stream<Tree>
 {

   Cons(Node(Nil), ATreeChildren())

 }

-ghost method Proposition2()

+lemma Proposition2()

   ensures !HasFiniteHeightEverywhere_Bad(ATree());

 {

   Proposition2_Lemma0();

   Proposition2_Lemma1(ATreeChildren());

 }

-comethod Proposition2_Lemma0()

+colemma Proposition2_Lemma0()

   ensures IsNeverEndingStream(ATreeChildren());

 {

 }

-comethod Proposition2_Lemma1(s: Stream<Tree>)

+colemma Proposition2_Lemma1(s: Stream<Tree>)

   requires IsNeverEndingStream(s);

   ensures InfiniteHeightSomewhere_Bad(s);

 {

@@ -237,7 +237,7 @@ copredicate ValidPath(t: Tree, p: Stream<int>)
     var ch := Tail(t.children, index);

     ch.Cons? && ValidPath(ch.head, tail)

 }

-ghost method ValidPath_Lemma(p: Stream<int>)

+lemma ValidPath_Lemma(p: Stream<int>)

   ensures ValidPath(Node(Nil), p) ==> p == Nil;

 {

   if ValidPath(Node(Nil), p) {

@@ -258,7 +258,7 @@ predicate HasFiniteHeight(t: Tree)
 

 // From this definition, we can prove that any tree of bounded height is also of finite height.

 

-ghost method Theorem1(t: Tree)

+lemma Theorem1(t: Tree)

   requires HasBoundedHeight(t);

   ensures HasFiniteHeight(t);

 {

@@ -267,7 +267,7 @@ ghost method Theorem1(t: Tree)
     Theorem1_Lemma(t, n, p);

   }

 }

-ghost method Theorem1_Lemma(t: Tree, n: nat, p: Stream<int>)

+lemma Theorem1_Lemma(t: Tree, n: nat, p: Stream<int>)

   requires LowerThan(t.children, n) && ValidPath(t, p);

   ensures !IsNeverEndingStream(p);

   decreases n;

@@ -311,7 +311,7 @@ function EverLongerSkinnyTrees(n: nat): Stream<Tree>
   Cons(SkinnyFiniteTree(n), EverLongerSkinnyTrees(n+1))

 }

 

-ghost method EverLongerSkinnyTrees_Lemma(k: nat, n: nat)

+lemma EverLongerSkinnyTrees_Lemma(k: nat, n: nat)

   ensures Tail(EverLongerSkinnyTrees(k), n).Cons?;

   ensures Tail(EverLongerSkinnyTrees(k), n).head == SkinnyFiniteTree(k+n);

   decreases n;

@@ -330,13 +330,13 @@ ghost method EverLongerSkinnyTrees_Lemma(k: nat, n: nat)
   }

 }

 

-ghost method Proposition3()

+lemma Proposition3()

   ensures !HasBoundedHeight(FiniteUnboundedTree()) && HasFiniteHeight(FiniteUnboundedTree());

 {

   Proposition3a();

   Proposition3b();

 }

-ghost method Proposition3a()

+lemma Proposition3a()

   ensures !HasBoundedHeight(FiniteUnboundedTree());

 {

   var ch := FiniteUnboundedTree().children;

@@ -350,7 +350,7 @@ ghost method Proposition3a()
     LowerThan_Lemma(ch, n+1, n);

   }

 }

-ghost method Proposition3b()

+lemma Proposition3b()

   ensures HasFiniteHeight(FiniteUnboundedTree());

 {

   var t := FiniteUnboundedTree();

@@ -369,7 +369,7 @@ ghost method Proposition3b()
     Proposition3b_Lemma(si, index, p.tail);

   }

 }

-ghost method Proposition3b_Lemma(t: Tree, h: nat, p: Stream<int>)

+lemma Proposition3b_Lemma(t: Tree, h: nat, p: Stream<int>)

   requires LowerThan(t.children, h) && ValidPath(t, p);

   ensures !IsNeverEndingStream(p);

   decreases h;

@@ -495,7 +495,7 @@ function N2S'(n: nat, num: Number): Stream<int>
   case Succ(next) => N2S'(n + 1, next)

 }

 

-ghost method Path_Lemma0(t: Tree, p: Stream<int>)

+lemma Path_Lemma0(t: Tree, p: Stream<int>)

   requires ValidPath(t, p);

   ensures ValidPath_Alt(t, S2N(p));

 {

@@ -503,7 +503,7 @@ ghost method Path_Lemma0(t: Tree, p: Stream<int>)
     Path_Lemma0'(t, p);

   }

 }

-comethod Path_Lemma0'(t: Tree, p: Stream<int>)

+colemma Path_Lemma0'(t: Tree, p: Stream<int>)

   requires ValidPath(t, p);

   ensures ValidPath_Alt(t, S2N(p));

 {

@@ -526,7 +526,7 @@ comethod Path_Lemma0'(t: Tree, p: Stream<int>)
       }

   }

 }

-comethod Path_Lemma0''(tChildren: Stream<Tree>, n: nat, tail: Stream<int>)

+colemma Path_Lemma0''(tChildren: Stream<Tree>, n: nat, tail: Stream<int>)

   requires var ch := Tail(tChildren, n); ch.Cons? && ValidPath(ch.head, tail);

   ensures ValidPath_Alt'(tChildren, S2N'(n, tail));

 {

@@ -545,7 +545,7 @@ comethod Path_Lemma0''(tChildren: Stream<Tree>, n: nat, tail: Stream<int>)
       Path_Lemma0'(tChildren.head, tail);

   }

 }

-ghost method Path_Lemma1(t: Tree, r: CoOption<Number>)

+lemma Path_Lemma1(t: Tree, r: CoOption<Number>)

   requires ValidPath_Alt(t, r);

   ensures ValidPath(t, N2S(r));

 {

@@ -553,7 +553,7 @@ ghost method Path_Lemma1(t: Tree, r: CoOption<Number>)
     Path_Lemma1'(t, r);

   }

 }

-comethod Path_Lemma1'(t: Tree, r: CoOption<Number>)

+colemma Path_Lemma1'(t: Tree, r: CoOption<Number>)

   requires ValidPath_Alt(t, r);

   ensures ValidPath(t, N2S(r));

   decreases 1;

@@ -576,7 +576,7 @@ comethod Path_Lemma1'(t: Tree, r: CoOption<Number>)
       }

   }

 }

-comethod Path_Lemma1''(s: Stream<Tree>, n: nat, num: Number)

+colemma Path_Lemma1''(s: Stream<Tree>, n: nat, num: Number)

   requires ValidPath_Alt'(Tail(s, n), num);

   ensures ValidPath(Node(s), N2S'(n, num));

   decreases 0, num;

@@ -596,14 +596,14 @@ comethod Path_Lemma1''(s: Stream<Tree>, n: nat, num: Number)
       }

   }

 }

-ghost method Path_Lemma2(p: Stream<int>)

+lemma Path_Lemma2(p: Stream<int>)

   ensures IsNeverEndingStream(p) ==> InfinitePath(S2N(p));

 {

   if IsNeverEndingStream(p) {

     Path_Lemma2'(p);

   }

 }

-comethod Path_Lemma2'(p: Stream<int>)

+colemma Path_Lemma2'(p: Stream<int>)

   requires IsNeverEndingStream(p);

   ensures InfinitePath(S2N(p));

 {

@@ -622,7 +622,7 @@ comethod Path_Lemma2'(p: Stream<int>)
     }

   }

 }

-comethod Path_Lemma2''(p: Stream<int>, n: nat, tail: Stream<int>)

+colemma Path_Lemma2''(p: Stream<int>, n: nat, tail: Stream<int>)

   requires IsNeverEndingStream(p) && p.tail == tail;

   ensures InfinitePath'(S2N'(n, tail));

 {

@@ -648,7 +648,7 @@ comethod Path_Lemma2''(p: Stream<int>, n: nat, tail: Stream<int>)
     }

   }

 }

-ghost method Path_Lemma3(r: CoOption<Number>)

+lemma Path_Lemma3(r: CoOption<Number>)

   ensures InfinitePath(r) ==> IsNeverEndingStream(N2S(r));

 {

   if InfinitePath(r) {

@@ -657,7 +657,7 @@ ghost method Path_Lemma3(r: CoOption<Number>)
     }

   }

 }

-comethod Path_Lemma3'(n: nat, num: Number)

+colemma Path_Lemma3'(n: nat, num: Number)

   requires InfinitePath'(num);

   ensures IsNeverEndingStream(N2S'(n, num));

   decreases num;

@@ -678,7 +678,7 @@ comethod Path_Lemma3'(n: nat, num: Number)
   }

 }

 

-ghost method Theorem2(t: Tree)

+lemma Theorem2(t: Tree)

   ensures HasFiniteHeight(t) <==> HasFiniteHeight_Alt(t);

 {

   if HasFiniteHeight_Alt(t) {

diff --git a/Test/dafny3/Paulson.dfy b/Test/dafny3/Paulson.dfy
index 431ff543..37586ec7 100644
--- a/Test/dafny3/Paulson.dfy
+++ b/Test/dafny3/Paulson.dfy
@@ -10,7 +10,7 @@ function Apply<T>(f: FunctionHandle<T>, argument: T): T
 

 // Function composition

 function After(f: FunctionHandle, g: FunctionHandle): FunctionHandle

-ghost method Definition_After<T>(f: FunctionHandle<T>, g: FunctionHandle<T>, arg: T)

+lemma Definition_After<T>(f: FunctionHandle<T>, g: FunctionHandle<T>, arg: T)

   ensures Apply(After(f, g), arg) == Apply(f, Apply(g, arg));

 

 function Lmap(f: FunctionHandle, a: LList): LList

@@ -29,7 +29,7 @@ function Lappend(a: LList, b: LList): LList
 

 // ---------- Section 8.3 ----------

 

-comethod Example6(f: FunctionHandle, g: FunctionHandle, M: LList)

+colemma Example6(f: FunctionHandle, g: FunctionHandle, M: LList)

   ensures Lmap(After(f, g), M) == Lmap(f, Lmap(g, M));

 {

   match M {

@@ -61,7 +61,7 @@ function Iterates<A>(f: FunctionHandle<LList<A>>, M: LList<A>): LList<LList<A>>
   Cons(M, Iterates(f, Apply(f, M)))

 }

 

-comethod Eq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)

+colemma Eq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)

   ensures Lmap(f, Iterates(f, M)) == Iterates(f, Apply(f, M));

 {

   calc {

@@ -80,7 +80,7 @@ comethod Eq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)
   }

 }

 

-ghost method CorollaryEq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)

+lemma CorollaryEq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)

   ensures Iterates(f, M) == Cons(M, Lmap(f, Iterates(f, M)));

 {

   Eq24(f, M);

@@ -92,7 +92,7 @@ ghost method CorollaryEq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>)
 // Let h be any function

 function h<A>(f: FunctionHandle<LList<A>>, M: LList<A>): LList<LList<A>>

 // ... that satisfies the property in CorollaryEq24:

-ghost method Definition_h<A>(f: FunctionHandle<LList<A>>, M: LList<A>)

+lemma Definition_h<A>(f: FunctionHandle<LList<A>>, M: LList<A>)

   ensures h(f, M) == Cons(M, Lmap(f, h(f, M)));

 

 // Functions to support the proof:

@@ -107,19 +107,19 @@ function LmapIter(n: nat, f: FunctionHandle, arg: LList): LList
   if n == 0 then arg else Lmap(f, LmapIter(n-1, f, arg))

 }

 

-ghost method Lemma25<A>(n: nat, f: FunctionHandle<A>, b: A, M: LList<A>)

+lemma Lemma25<A>(n: nat, f: FunctionHandle<A>, b: A, M: LList<A>)

   ensures LmapIter(n, f, Cons(b, M)) == Cons(Iter(n, f, b), LmapIter(n, f, M));

 {

   // proof is by (automatic) induction

 }

 

-ghost method Lemma26<A>(n: nat, f: FunctionHandle, x: LList)  // (26) in the paper, but with f := LMap f

+lemma Lemma26<A>(n: nat, f: FunctionHandle, x: LList)  // (26) in the paper, but with f := LMap f

   ensures LmapIter(n, f, Lmap(f, x)) == LmapIter(n+1, f, x);

 {

   // proof is by (automatic) induction

 }

 

-comethod BisimulationLemma<A>(n: nat, f: FunctionHandle<LList<A>>, u: LList<A>)

+colemma BisimulationLemma<A>(n: nat, f: FunctionHandle<LList<A>>, u: LList<A>)

   ensures LmapIter(n, f, h(f, u)) == LmapIter(n, f, Iterates(f, u));

 {

   calc {

@@ -146,7 +146,7 @@ comethod BisimulationLemma<A>(n: nat, f: FunctionHandle<LList<A>>, u: LList<A>)
   }

 }

 

-ghost method Example7<A>(f: FunctionHandle<LList<A>>)

+lemma Example7<A>(f: FunctionHandle<LList<A>>)

   // Given the definition of h, prove h(f, _) == Iterates(f, _):

   ensures forall M :: h(f, M) == Iterates(f, M);

 {

@@ -157,13 +157,13 @@ ghost method Example7<A>(f: FunctionHandle<LList<A>>)
 

 // ---------- Section 8.5 ----------

 

-comethod Example8<A>(f: FunctionHandle<A>, M: LList<A>, N: LList<A>)

+colemma Example8<A>(f: FunctionHandle<A>, M: LList<A>, N: LList<A>)

   ensures Lmap(f, Lappend(M, N)) == Lappend(Lmap(f, M), Lmap(f, N));

 {

   // A proof doesn't get any simpler than this

 }

 

-comethod Associativity(a: LList, b: LList, c: LList)

+colemma Associativity(a: LList, b: LList, c: LList)

   ensures Lappend(Lappend(a, b), c) == Lappend(a, Lappend(b, c));

 {

   // Again, Dafny does this proof completely automatically

diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy
index cc92a6f1..b5b0c8bf 100644
--- a/Test/dafny3/SimpleCoinduction.dfy
+++ b/Test/dafny3/SimpleCoinduction.dfy
@@ -18,7 +18,7 @@ function Inc(s: Stream<int>): Stream<int>
   Cons(s.head + 1, Inc(s.tail))

 }

 

-ghost method {:induction false} UpLemma(k: nat, n: int)

+lemma {:induction false} UpLemma(k: nat, n: int)

   ensures Inc(Up(n)) ==#[k] Up(n+1);

 {

   if (k != 0) {

@@ -26,18 +26,18 @@ ghost method {:induction false} UpLemma(k: nat, n: int)
   }

 }

 

-comethod {:induction false} CoUpLemma(n: int)

+colemma {:induction false} CoUpLemma(n: int)

   ensures Inc(Up(n)) == Up(n+1);

 {

   CoUpLemma(n+1);

 }

 

-ghost method UpLemma_Auto(k: nat, n: int)

+lemma UpLemma_Auto(k: nat, n: int)

   ensures Inc(Up(n)) ==#[k] Up(n+1);

 {

 }

 

-comethod CoUpLemma_Auto(n: int)

+colemma CoUpLemma_Auto(n: int)

   ensures Inc(Up(n)) == Up(n+1);

 {

 }

@@ -49,7 +49,7 @@ function Repeat(n: int): Stream<int>
   Cons(n, Repeat(n))

 }

 

-comethod RepeatLemma(n: int)

+colemma RepeatLemma(n: int)

   ensures Inc(Repeat(n)) == Repeat(n+1);

 {

 }

@@ -61,7 +61,7 @@ copredicate True(s: Stream)
   True(s.tail)

 }

 

-comethod AlwaysTrue(s: Stream)

+colemma AlwaysTrue(s: Stream)

   ensures True(s);

 {

 }

@@ -71,7 +71,7 @@ copredicate AlsoTrue(s: Stream)
   AlsoTrue(s)

 }

 

-comethod AlsoAlwaysTrue(s: Stream)

+colemma AlsoAlwaysTrue(s: Stream)

   ensures AlsoTrue(s);

 {

 }

@@ -81,7 +81,7 @@ copredicate TT(y: int)
   TT(y+1)

 }

 

-comethod AlwaysTT(y: int)

+colemma AlwaysTT(y: int)

   ensures TT(y);

 {

 }

@@ -112,12 +112,12 @@ copredicate AtMost(a: IList<int>, b: IList<int>)
   case ICons(h,t) => b.ICons? && h <= b.head && AtMost(t, b.tail)

 }

 

-comethod ZerosAndOnes_Theorem0()

+colemma ZerosAndOnes_Theorem0()

   ensures AtMost(zeros(), ones());

 {

 }

 

-comethod ZerosAndOnes_Theorem1()

+colemma ZerosAndOnes_Theorem1()

   ensures Append(zeros(), ones()) == zeros();

 {

 }

diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy
index f13c5c0a..1d566545 100644
--- a/Test/dafny3/Streams.dfy
+++ b/Test/dafny3/Streams.dfy
@@ -40,7 +40,7 @@ function map_fg(M: Stream<X>): Stream<X>
 // ----- Theorems

 

 // map (f * g) M = map f (map g M)

-comethod Theorem0(M: Stream<X>)

+colemma Theorem0(M: Stream<X>)

   ensures map_fg(M) == map_f(map_g(M));

 {

   match (M) {

@@ -49,21 +49,21 @@ comethod Theorem0(M: Stream<X>)
       Theorem0(N);

   }

 }

-comethod Theorem0_Alt(M: Stream<X>)

+colemma Theorem0_Alt(M: Stream<X>)

   ensures map_fg(M) == map_f(map_g(M));

 {

   if (M.Cons?) {

     Theorem0_Alt(M.tail);

   }

 }

-ghost method Theorem0_Par(M: Stream<X>)

+lemma Theorem0_Par(M: Stream<X>)

   ensures map_fg(M) == map_f(map_g(M));

 {

   forall k: nat {

     Theorem0_Ind(k, M);

   }

 }

-ghost method Theorem0_Ind(k: nat, M: Stream<X>)

+lemma Theorem0_Ind(k: nat, M: Stream<X>)

   ensures map_fg(M) ==#[k] map_f(map_g(M));

 {

   if (k != 0) {

@@ -74,13 +74,13 @@ ghost method Theorem0_Ind(k: nat, M: Stream<X>)
     }

   }

 }

-ghost method Theorem0_AutoInd(k: nat, M: Stream<X>)

+lemma Theorem0_AutoInd(k: nat, M: Stream<X>)

   ensures map_fg(M) ==#[k] map_f(map_g(M));

 // {  // TODO: this is not working yet, apparently

 // }

 

 // map f (append M N) = append (map f M) (map f N)

-comethod Theorem1(M: Stream<X>, N: Stream<X>)

+colemma Theorem1(M: Stream<X>, N: Stream<X>)

   ensures map_f(append(M, N)) == append(map_f(M), map_f(N));

 {

   match (M) {

@@ -89,21 +89,21 @@ comethod Theorem1(M: Stream<X>, N: Stream<X>)
       Theorem1(M', N);

   }

 }

-comethod Theorem1_Alt(M: Stream<X>, N: Stream<X>)

+colemma Theorem1_Alt(M: Stream<X>, N: Stream<X>)

   ensures map_f(append(M, N)) == append(map_f(M), map_f(N));

 {

   if (M.Cons?) {

     Theorem1_Alt(M.tail, N);

   }

 }

-ghost method Theorem1_Par(M: Stream<X>, N: Stream<X>)

+lemma Theorem1_Par(M: Stream<X>, N: Stream<X>)

   ensures map_f(append(M, N)) == append(map_f(M), map_f(N));

 {

   forall k: nat {

     Theorem1_Ind(k, M, N);

   }

 }

-ghost method Theorem1_Ind(k: nat, M: Stream<X>, N: Stream<X>)

+lemma Theorem1_Ind(k: nat, M: Stream<X>, N: Stream<X>)

   ensures map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));

 {

   // this time, try doing the 'if' inside the 'match' (instead of the other way around)

@@ -115,24 +115,24 @@ ghost method Theorem1_Ind(k: nat, M: Stream<X>, N: Stream<X>)
       }

   }

 }

-ghost method Theorem1_AutoInd(k: nat, M: Stream<X>, N: Stream<X>)

+lemma Theorem1_AutoInd(k: nat, M: Stream<X>, N: Stream<X>)

   ensures map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));

 // {  // TODO: this is not working yet, apparently

 // }

-ghost method Theorem1_AutoForall()

+lemma Theorem1_AutoForall()

 {

 //  assert forall k: nat, M, N :: map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));  // TODO: this is not working yet, apparently

 }

 

 // append NIL M = M

-ghost method Theorem2(M: Stream<X>)

+lemma Theorem2(M: Stream<X>)

   ensures append(Nil, M) == M;

 {

   // trivial

 }

 

 // append M NIL = M

-comethod Theorem3(M: Stream<X>)

+colemma Theorem3(M: Stream<X>)

   ensures append(M, Nil) == M;

 {

   match (M) {

@@ -141,7 +141,7 @@ comethod Theorem3(M: Stream<X>)
       Theorem3(N);

   }

 }

-comethod Theorem3_Alt(M: Stream<X>)

+colemma Theorem3_Alt(M: Stream<X>)

   ensures append(M, Nil) == M;

 {

   if (M.Cons?) {

@@ -150,7 +150,7 @@ comethod Theorem3_Alt(M: Stream<X>)
 }

 

 // append M (append N P) = append (append M N) P

-comethod Theorem4(M: Stream<X>, N: Stream<X>, P: Stream<X>)

+colemma Theorem4(M: Stream<X>, N: Stream<X>, P: Stream<X>)

   ensures append(M, append(N, P)) == append(append(M, N), P);

 {

   match (M) {

@@ -159,7 +159,7 @@ comethod Theorem4(M: Stream<X>, N: Stream<X>, P: Stream<X>)
       Theorem4(M', N, P);

   }

 }

-comethod Theorem4_Alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)

+colemma Theorem4_Alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)

   ensures append(M, append(N, P)) == append(append(M, N), P);

 {

   if (M.Cons?) {

@@ -241,7 +241,7 @@ function Prepend<T>(x: T, M: Stream<Stream>): Stream<Stream>
   case Cons(s, N) => Cons(Cons(x, s), Prepend(x, N))

 }

 

-comethod Prepend_Lemma<T>(x: T, M: Stream<Stream>)

+colemma Prepend_Lemma<T>(x: T, M: Stream<Stream>)

   ensures StreamOfNonEmpties(Prepend(x, M));

 {

   match M {

@@ -250,7 +250,7 @@ comethod Prepend_Lemma<T>(x: T, M: Stream<Stream>)
   }

 }

 

-ghost method Theorem_Flatten<T>(M: Stream<Stream>, startMarker: T)

+lemma Theorem_Flatten<T>(M: Stream<Stream>, startMarker: T)

   ensures

     StreamOfNonEmpties(Prepend(startMarker, M)) ==> // always holds, on account of Prepend_Lemma;

                                           // but until (co-)method can be called from functions,

@@ -261,7 +261,7 @@ ghost method Theorem_Flatten<T>(M: Stream<Stream>, startMarker: T)
   Lemma_Flatten(Nil, M, startMarker);

 }

 

-comethod Lemma_Flatten<T>(prefix: Stream, M: Stream<Stream>, startMarker: T)

+colemma Lemma_Flatten<T>(prefix: Stream, M: Stream<Stream>, startMarker: T)

   ensures

     StreamOfNonEmpties(Prepend(startMarker, M)) ==> // always holds, on account of Prepend_Lemma;

                                           // but until (co-)method can be called from functions,

@@ -325,7 +325,7 @@ comethod Lemma_Flatten<T>(prefix: Stream, M: Stream<Stream>, startMarker: T)
   }

 }

 

-comethod Lemma_FlattenAppend0<T>(s: Stream, M: Stream<Stream>, startMarker: T)

+colemma Lemma_FlattenAppend0<T>(s: Stream, M: Stream<Stream>, startMarker: T)

   ensures PrependThenFlattenStartMarker(s, M, startMarker) == append(s, PrependThenFlattenStartMarker(Nil, M, startMarker));

 {

   match (s) {

@@ -335,7 +335,7 @@ comethod Lemma_FlattenAppend0<T>(s: Stream, M: Stream<Stream>, startMarker: T)
   }

 }

 

-comethod Lemma_FlattenAppend1<T>(s: Stream, M: Stream<Stream>)

+colemma Lemma_FlattenAppend1<T>(s: Stream, M: Stream<Stream>)

   requires StreamOfNonEmpties(M);

   ensures PrependThenFlattenNonEmpties(s, M) == append(s, PrependThenFlattenNonEmpties(Nil, M));

 {

diff --git a/Test/dafny3/WideTrees.dfy b/Test/dafny3/WideTrees.dfy
index e381726e..3fa99256 100644
--- a/Test/dafny3/WideTrees.dfy
+++ b/Test/dafny3/WideTrees.dfy
@@ -36,12 +36,12 @@ function SmallTrees(n: nat): Stream<Tree>
   if n == 0 then SNil else SCons(SmallTree(n-1), SmallTrees(n))

 }

 // prove that the tree returned by SmallTree is finite

-ghost method Theorem(n: nat)

+lemma Theorem(n: nat)

   ensures HasBoundedHeight(SmallTree(n));

 {

   Lemma(n);

 }

-comethod Lemma(n: nat)

+colemma Lemma(n: nat)

   ensures LowerThan(SmallTrees(n), n);

 {

   if 0 < n {

diff --git a/Test/dafny3/Zip.dfy b/Test/dafny3/Zip.dfy
index 80e8cd91..629861f9 100644
--- a/Test/dafny3/Zip.dfy
+++ b/Test/dafny3/Zip.dfy
@@ -23,11 +23,11 @@ function even(xs: Stream): Stream
 function odd(xs: Stream): Stream

   { even(xs.tl) }

 

-comethod EvenOddLemma(xs: Stream)

+colemma EvenOddLemma(xs: Stream)

   ensures zip(even(xs), odd(xs)) == xs;

 { EvenOddLemma(xs.tl.tl); }

 

-comethod EvenZipLemma(xs:Stream, ys:Stream)

+colemma EvenZipLemma(xs:Stream, ys:Stream)

   ensures even(zip(xs, ys)) == xs;

 { /* Automatic. */ }

 

@@ -35,7 +35,7 @@ function bzip(xs: Stream, ys: Stream, f:bool) : Stream
   { if f then Cons(xs.hd, bzip(xs.tl, ys, !f))

     else      Cons(ys.hd, bzip(xs, ys.tl, !f)) }

 

-comethod BzipZipLemma(xs:Stream, ys:Stream)

+colemma BzipZipLemma(xs:Stream, ys:Stream)

   ensures zip(xs, ys) == bzip(xs, ys, true);

 { BzipZipLemma(xs.tl, ys.tl); }

 

@@ -54,7 +54,7 @@ function blink(): Stream<int>
   Cons(0, Cons(1, blink()))

 }

 

-comethod BzipBlinkLemma()

+colemma BzipBlinkLemma()

   ensures zip(const(0), const(1)) == blink();

 {

   BzipBlinkLemma(); 

@@ -66,13 +66,13 @@ function zip2(xs: Stream, ys: Stream): Stream
   Cons(xs.hd, zip2(ys, xs.tl))

 }

 

-comethod Zip201Lemma()

+colemma Zip201Lemma()

   ensures zip2(const(0), const(1)) == blink();

 {

   Zip201Lemma();

 }

 

-comethod ZipZip2Lemma(xs:Stream, ys:Stream)

+colemma ZipZip2Lemma(xs:Stream, ys:Stream)

   ensures zip(xs, ys) == zip2(xs, ys);

 {

   ZipZip2Lemma(xs.tl, ys.tl);

@@ -84,13 +84,13 @@ function bswitch(xs: Stream, f:bool) : Stream
   else      Cons(xs.hd,      bswitch(xs.tl, !f))

 }

 

-comethod BswitchLemma(xs:Stream)

+colemma BswitchLemma(xs:Stream)

   ensures zip(odd(xs), even(xs)) == bswitch(xs, true);

 {

   BswitchLemma(xs.tl.tl);

 }

 

-comethod Bswitch2Lemma(xs:Stream, ys:Stream)

+colemma Bswitch2Lemma(xs:Stream, ys:Stream)

   ensures zip(xs, ys) == bswitch(zip(ys, xs), true);

 {

   Bswitch2Lemma(xs.tl, ys.tl);