Made /rewriteFocalPredicates:1 the default

4 files changed, 13 insertions, 13 deletions

diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index 0dce8af9..c8bb45c7 100644
--- a/Test/dafny0/CoinductiveProofs.dfy
+++ b/Test/dafny0/CoinductiveProofs.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /rewriteFocalPredicates:1 "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 codatatype Stream<T> = Cons(head: T, tail: Stream)

diff --git a/Test/dafny0/InductivePredicates.dfy b/Test/dafny0/InductivePredicates.dfy
index 8d05af11..e9aa7604 100644
--- a/Test/dafny0/InductivePredicates.dfy
+++ b/Test/dafny0/InductivePredicates.dfy
@@ -58,7 +58,7 @@ inductive lemma {:induction false} IL_EvenBetter(x: natinf)
   if {

     case x.N? && x.n == 0 =>

       // trivial

-    case x.N? && 2 <= x.n && Even(N(x.n - 2)) =>

+    case x.N? && 2 <= x.n && Even(N(x.n - 2)) =>  // syntactic rewrite makes this like in IL

       IL_EvenBetter(N(x.n - 2));

   }

 }

@@ -142,7 +142,7 @@ module Alt {
     }

   }

 

-  inductive lemma {:induction false} MyLemma_NiceButNotFast(x: natinf)

+  inductive lemma {:induction false} MyLemma_Nicer(x: natinf)  // same as MyLemma_NotSoNice but relying on syntactic rewrites

     requires Even(x)

     ensures x.N? && x.n % 2 == 0

   {

@@ -151,7 +151,7 @@ module Alt {
         // trivial

       case exists y :: x == S(S(y)) && Even(y) =>

         var y :| x == S(S(y)) && Even(y);

-        MyLemma_NiceButNotFast(y);

+        MyLemma_Nicer(y);

         assert x.n == y.n + 2;

     }

   }

diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy
index 6f541396..4f8b35ec 100644
--- a/Test/dafny3/Filter.dfy
+++ b/Test/dafny3/Filter.dfy
@@ -157,11 +157,11 @@ colemma Filter_IsSubStream(s: Stream, P: Predicate)
     calc {

       true;

     ==  { Filter_IsSubStream(s.tail, P); }  // induction hypothesis

-      IsSubStream#[_k-1](Filter(s.tail, P), s.tail);

+      IsSubStream(Filter(s.tail, P), s.tail);

     == // { assert Filter(s.tail, h) == Filter(s, h).tail; }

-      IsSubStream#[_k-1](Filter(s, P).tail, s.tail);

+      IsSubStream(Filter(s, P).tail, s.tail);

     ==> { Lemma_TailSubStreamK(Filter(s, P).tail, s, _k-1); }

-      IsSubStream#[_k-1](Filter(s, P).tail, s);

+      IsSubStream(Filter(s, P).tail, s);

     }

     calc {

       In(Filter(s, P).head, s);

diff --git a/Test/dafny4/NipkowKlein-chapter7.dfy b/Test/dafny4/NipkowKlein-chapter7.dfy
index aae94550..0c089895 100644
--- a/Test/dafny4/NipkowKlein-chapter7.dfy
+++ b/Test/dafny4/NipkowKlein-chapter7.dfy
@@ -162,8 +162,8 @@ inductive lemma SmallStep_is_deterministic(cs: (com, state), cs': (com, state),
   case Seq(c0, c1) =>

     if c0 == SKIP {

     } else {

-      var c0' :| cs'.0 == Seq(c0', c1) && small_step#[_k-1](c0, cs.1, c0', cs'.1);

-      var c0'' :| cs''.0 == Seq(c0'', c1) && small_step#[_k-1](c0, cs.1, c0'', cs''.1);

+      var c0' :| cs'.0 == Seq(c0', c1) && small_step(c0, cs.1, c0', cs'.1);

+      var c0'' :| cs''.0 == Seq(c0'', c1) && small_step(c0, cs.1, c0'', cs''.1);

       SmallStep_is_deterministic((c0, cs.1), (c0', cs'.1), (c0'', cs''.1));

     }

   case If(b, thn, els) =>

@@ -200,7 +200,7 @@ inductive lemma BigStep_implies_SmallStepStar(c: com, s: state, t: state)
   case Assign(x, a) =>

     assert small_step_star(SKIP, t, SKIP, t);

   case Seq(c0, c1) =>

-    var s' :| big_step#[_k-1](c0, s, s') && big_step#[_k-1](c1, s', t);

+    var s' :| big_step(c0, s, s') && big_step(c1, s', t);

     calc <== {

       small_step_star(c, s, SKIP, t);

       { star_transitive(Seq(c0, c1), s, Seq(SKIP, c1), s', SKIP, t); }

@@ -226,7 +226,7 @@ inductive lemma BigStep_implies_SmallStepStar(c: com, s: state, t: state)
         true;

       }

     } else {

-      var s' :| big_step#[_k-1](body, s, s') && big_step#[_k-1](While(b, body), s', t);

+      var s' :| big_step(body, s, s') && big_step(While(b, body), s', t);

       calc <== {

         small_step_star(c, s, SKIP, t);

         { assert small_step(c, s, If(b, Seq(body, While(b, body)), SKIP), s); }

@@ -253,7 +253,7 @@ inductive lemma lemma_7_13(c0: com, s0: state, c: com, t: state, c1: com)
 {

   if c0 == c && s0 == t {

   } else {

-    var c', s' :| small_step(c0, s0, c', s') && small_step_star#[_k-1](c', s', c, t);

+    var c', s' :| small_step(c0, s0, c', s') && small_step_star(c', s', c, t);

     lemma_7_13(c', s', c, t, c1);

   }

 }

@@ -264,7 +264,7 @@ inductive lemma SmallStepStar_implies_BigStep(c: com, s: state, t: state)
 {

   if c == SKIP && s == t {

   } else {

-    var c', s' :| small_step(c, s, c', s') && small_step_star#[_k-1](c', s', SKIP, t);

+    var c', s' :| small_step(c, s, c', s') && small_step_star(c', s', SKIP, t);

     SmallStep_plus_BigStep(c, s, c', s', t);

   }

 }