-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Uninterpreted.Function
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates function counter-examples
-----------------------------------------------------------------------------

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Uninterpreted.Function where

import Data.SBV

-- | An uninterpreted function
f :: SWord8 -> SWord8 -> SWord16
f :: SWord8 -> SWord8 -> SWord16
f = String -> SWord8 -> SWord8 -> SWord16
forall a. Uninterpreted a => String -> a
uninterpret String
"f"

-- | Asserts that @f x z == f (y+2) z@ whenever @x == y+2@. Naturally correct:
--
-- >>> prove thmGood
-- Q.E.D.
thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool
thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool
thmGood SWord8
x SWord8
y SWord8
z = SWord8
x SWord8 -> SWord8 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord8
ySWord8 -> SWord8 -> SWord8
forall a. Num a => a -> a -> a
+SWord8
2 SBool -> SBool -> SBool
.=> SWord8 -> SWord8 -> SWord16
f SWord8
x SWord8
z SWord16 -> SWord16 -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SWord8 -> SWord8 -> SWord16
f (SWord8
y SWord8 -> SWord8 -> SWord8
forall a. Num a => a -> a -> a
+ SWord8
2) SWord8
z