leon - Inox で抽象関数を宣言する方法

Question

楕円曲線の特定のプロパティを証明しています。そのために、フィールド操作を処理するいくつかの関数に依存しています。しかし、私は Inox がこれらの関数の実装について推論するのではなく、関数の特定のプロパティを仮定するだけにしたいと考えています。

たとえば、点の加算p1 = (x1,y1) and p2 = (x2,y2)が交換可能であることを証明しているとします。ポイントの追加を実装するには、そのコンポーネント (つまり、フィールドの要素) の追加を実装する関数が必要です。

追加は次の形になります。

val addFunction = mkFunDef(addID)() { case Seq() => 
    val args: Seq[ValDef] = Seq("f1" :: F, "f2" :: F)  
    val retType: Type = F
    val body: Seq[Variable] => Expr = { case Seq(f1,f2) =>
      //do the addition for this field
    } 
    (args, retType, body)
}

この関数では、次のようなプロパティを指定できます。

val addAssociative: Expr = forall("x" :: F, "y" :: F, "z" :: F){ case (x, y, z) => 
    (x ^+ (y ^+ z)) === ((x ^+ y) ^+ z)
}

whereは、この他の質問^+で示されている add に対応する中置演算子です。

展開中に Inox が何も想定しないようにボディに挿入する適切な式は何ですか?