From d47400c8a1ba72497cc145173aa6ad9f6b1b5a85 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Sun, 23 Feb 2014 17:27:26 -0800
Subject: Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix
 method" -> "prefix lemma")

---
 Test/dafny3/Filter.dfy                 | 30 ++++++++--------
 Test/dafny3/InductionVsCoinduction.dfy | 18 +++++-----
 Test/dafny3/InfiniteTrees.dfy          | 62 +++++++++++++++++-----------------
 Test/dafny3/Paulson.dfy                | 22 ++++++------
 Test/dafny3/SimpleCoinduction.dfy      | 20 +++++------
 Test/dafny3/Streams.dfy                | 42 +++++++++++------------
 Test/dafny3/WideTrees.dfy              |  4 +--
 Test/dafny3/Zip.dfy                    | 16 ++++-----
 8 files changed, 107 insertions(+), 107 deletions(-)

(limited to 'Test/dafny3')

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);
-- 
cgit v1.2.3