From bbd4170bdae224472d70945fafafbfb7fa1827c9 Mon Sep 17 00:00:00 2001
From: Lars Hupel <lars.hupel@mytum.de>
Date: Thu, 24 Sep 2015 16:10:55 +0200
Subject: [PATCH] quantifier support for Isabelle
---
.../leon/solvers/isabelle/Translator.scala | 9 ++++---
.../isabelle/valid/Quantifiers.scala | 26 +++++++++++++++++++
2 files changed, 32 insertions(+), 3 deletions(-)
create mode 100644 src/test/resources/regression/verification/isabelle/valid/Quantifiers.scala
diff --git a/src/main/scala/leon/solvers/isabelle/Translator.scala b/src/main/scala/leon/solvers/isabelle/Translator.scala
index 47d62bb5c..c0c9446f1 100644
--- a/src/main/scala/leon/solvers/isabelle/Translator.scala
+++ b/src/main/scala/leon/solvers/isabelle/Translator.scala
@@ -44,15 +44,15 @@ final class Translator(context: LeonContext, program: Program, types: Types, sys
}
def term(expr: Expr, bounds: List[Identifier], consts: (FunDef, Typ) => Term): Future[Term] = {
- def mkAbs(params: List[Identifier], body: Expr, bounds: List[Identifier]): Future[Term] = params match {
+ def mkAbs(params: List[Identifier], body: Expr, bounds: List[Identifier], wrap: Term => Term = identity): Future[Term] = params match {
case Nil => term(body, bounds, consts)
case p :: ps =>
for {
- rec <- mkAbs(ps, body, p :: bounds)
+ rec <- mkAbs(ps, body, p :: bounds, wrap)
typ <- types.typ(p.getType)
}
yield
- Abs(p.mangledName /* name hint, no logical content */, typ, rec)
+ wrap(Abs(p.mangledName /* name hint, no logical content */, typ, rec))
}
def nary(const: Term, xs: Expr*) =
@@ -180,6 +180,9 @@ final class Translator(context: LeonContext, program: Program, types: Types, sys
case Lambda(args, expr) =>
mkAbs(args.map(_.id).toList, expr, bounds)
+ case Forall(args, expr) =>
+ mkAbs(args.map(_.id).toList, expr, bounds, wrap = mkApp(Const("HOL.All", Typ.dummyT), _))
+
case CaseClass(typ, exprs) =>
lookupConstructor(typ).map(_.term).flatMap { nary(_, exprs: _*) }
diff --git a/src/test/resources/regression/verification/isabelle/valid/Quantifiers.scala b/src/test/resources/regression/verification/isabelle/valid/Quantifiers.scala
new file mode 100644
index 000000000..b0e815c57
--- /dev/null
+++ b/src/test/resources/regression/verification/isabelle/valid/Quantifiers.scala
@@ -0,0 +1,26 @@
+import leon.lang._
+
+object Quantifiers {
+
+ def swapping[A, B](p: (A, B) => Boolean) = {
+ require(forall((x: A, y: B) => p(x, y)))
+ forall((y: B, x: A) => p(x, y))
+ }.holds
+
+ def swapping_curry[A, B](p: A => B => Boolean) = {
+ require(forall((x: A) => forall((y: B) => p(x)(y))))
+ forall((y: B) => forall((x: A) => p(x)(y)))
+ }.holds
+
+ def inst[A](p: A => Boolean, a: A) = {
+ require(forall((x: A) => p(a)))
+ p(a)
+ }.holds
+
+ def exists[A](p: A => Boolean) =
+ !forall((x: A) => !p(x))
+
+ def drinkersPrinciple[A](d: A => Boolean) =
+ exists((x: A) => d(x) ==> forall((y: A) => d(y))).holds
+
+}
--
GitLab