From 886b88e644d1cbb564383c67f3b7935f62e8ef9b Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 18 Dec 2013 11:31:32 -0800
Subject: Added missing file (sorry)

---
 Test/dafny3/OpaqueTrees.dfy | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 Test/dafny3/OpaqueTrees.dfy

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/OpaqueTrees.dfy b/Test/dafny3/OpaqueTrees.dfy
new file mode 100644
index 00000000..a08d0b68
--- /dev/null
+++ b/Test/dafny3/OpaqueTrees.dfy
@@ -0,0 +1,40 @@
+datatype Tree<T> = Leaf(T) | Node(Tree, Tree)
+
+function {:opaque} size(t: Tree): nat
+{
+  match t
+  case Leaf(_) => 1
+  case Node(left, right) => 1 + size(left) + size(right)
+}
+
+function {:opaque} mirror(t: Tree): Tree
+{
+  match t
+  case Leaf(_) => t
+  case Node(left, right) => Node(mirror(right), mirror(left))
+}
+
+lemma {:induction false} MirrorSize(t: Tree)
+  ensures size(mirror(t)) == size(t);
+{
+  match t {
+    case Leaf(x) =>
+      calc {
+        size(mirror(Leaf(x)));
+      ==  { reveal_mirror(); }
+        size(Leaf(x));
+      }
+    case Node(left, right) =>
+      calc {
+        size(mirror(Node(left, right)));
+      ==  { reveal_mirror(); }
+        size(Node(mirror(right), mirror(left)));
+      ==  { reveal_size(); }
+        1 + size(mirror(right)) + size(mirror(left));
+      ==  { MirrorSize(right); MirrorSize(left); }  // induction hypothesis
+        1 + size(right) + size(left);
+      ==  { reveal_size(); }
+        size(Node(left, right));
+      }
+  }
+}
-- 
cgit v1.2.3