-----------------------------------------------------------------------------
-- |
-- 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

-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Data.SBV

-- | An uninterpreted function
f :: SWord8 -> SWord8 -> SWord16
f :: SWord8 -> SWord8 -> SWord16
f = 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 forall a. EqSymbolic a => a -> a -> SBool
.== SWord8
yforall a. Num a => a -> a -> a
+SWord8
2 SBool -> SBool -> SBool
.=> SWord8 -> SWord8 -> SWord16
f SWord8
x SWord8
z forall a. EqSymbolic a => a -> a -> SBool
.== SWord8 -> SWord8 -> SWord16
f (SWord8
y forall a. Num a => a -> a -> a
+ SWord8
2) SWord8
z