{- |
module: $Header$
description: Higher order logic theorems
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

module HOL.Thm (
  Thm,
  assume,
  axiomOfChoice,
  axiomOfExtensionality,
  axiomOfInfinity,
  betaConv,
  concl,
  deductAntisym,
  defineConst,
  defineTypeOp,
  dest,
  eqMp,
  hyp,
  mkAbs,
  mkAbsUnsafe,
  mkApp,
  mkAppUnsafe,
  nullHyp,
  refl,
  standardAxioms,
  subst)
where

import Control.Monad (guard)
import Data.Set (Set)
import qualified Data.Set as Set
import qualified HOL.Const as Const
import HOL.Data
import HOL.Name
import HOL.Sequent (Sequent)
import qualified HOL.Sequent as Sequent
import HOL.Subst (Subst)
import qualified HOL.Subst as Subst
import qualified HOL.Term as Term
import HOL.TermAlpha (TermAlpha)
import qualified HOL.TermAlpha as TermAlpha
import qualified HOL.Type as Type
import qualified HOL.TypeOp as TypeOp
import qualified HOL.TypeVar as TypeVar
import HOL.Util (mkUnsafe2)
import qualified HOL.Var as Var

-------------------------------------------------------------------------------
-- Theorems
-------------------------------------------------------------------------------

newtype Thm = Thm Sequent
  deriving (Thm -> Thm -> Bool
(Thm -> Thm -> Bool) -> (Thm -> Thm -> Bool) -> Eq Thm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Thm -> Thm -> Bool
$c/= :: Thm -> Thm -> Bool
== :: Thm -> Thm -> Bool
$c== :: Thm -> Thm -> Bool
Eq,Eq Thm
Eq Thm
-> (Thm -> Thm -> Ordering)
-> (Thm -> Thm -> Bool)
-> (Thm -> Thm -> Bool)
-> (Thm -> Thm -> Bool)
-> (Thm -> Thm -> Bool)
-> (Thm -> Thm -> Thm)
-> (Thm -> Thm -> Thm)
-> Ord Thm
Thm -> Thm -> Bool
Thm -> Thm -> Ordering
Thm -> Thm -> Thm
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Thm -> Thm -> Thm
$cmin :: Thm -> Thm -> Thm
max :: Thm -> Thm -> Thm
$cmax :: Thm -> Thm -> Thm
>= :: Thm -> Thm -> Bool
$c>= :: Thm -> Thm -> Bool
> :: Thm -> Thm -> Bool
$c> :: Thm -> Thm -> Bool
<= :: Thm -> Thm -> Bool
$c<= :: Thm -> Thm -> Bool
< :: Thm -> Thm -> Bool
$c< :: Thm -> Thm -> Bool
compare :: Thm -> Thm -> Ordering
$ccompare :: Thm -> Thm -> Ordering
$cp1Ord :: Eq Thm
Ord,Int -> Thm -> ShowS
[Thm] -> ShowS
Thm -> String
(Int -> Thm -> ShowS)
-> (Thm -> String) -> ([Thm] -> ShowS) -> Show Thm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Thm] -> ShowS
$cshowList :: [Thm] -> ShowS
show :: Thm -> String
$cshow :: Thm -> String
showsPrec :: Int -> Thm -> ShowS
$cshowsPrec :: Int -> Thm -> ShowS
Show)

-------------------------------------------------------------------------------
-- Destructors
-------------------------------------------------------------------------------

dest :: Thm -> Sequent
dest :: Thm -> Sequent
dest (Thm Sequent
sq) = Sequent
sq

hyp :: Thm -> Set TermAlpha
hyp :: Thm -> Set TermAlpha
hyp = Sequent -> Set TermAlpha
Sequent.hyp (Sequent -> Set TermAlpha)
-> (Thm -> Sequent) -> Thm -> Set TermAlpha
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thm -> Sequent
dest

concl :: Thm -> TermAlpha
concl :: Thm -> TermAlpha
concl = Sequent -> TermAlpha
Sequent.concl (Sequent -> TermAlpha) -> (Thm -> Sequent) -> Thm -> TermAlpha
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thm -> Sequent
dest

nullHyp :: Thm -> Bool
nullHyp :: Thm -> Bool
nullHyp = Sequent -> Bool
Sequent.nullHyp (Sequent -> Bool) -> (Thm -> Sequent) -> Thm -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thm -> Sequent
dest

-------------------------------------------------------------------------------
-- Type variables
-------------------------------------------------------------------------------

instance TypeVar.HasVars Thm where
  vars :: Thm -> Set TypeVar
vars = Sequent -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
TypeVar.vars (Sequent -> Set TypeVar) -> (Thm -> Sequent) -> Thm -> Set TypeVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thm -> Sequent
dest

-------------------------------------------------------------------------------
-- Type operators
-------------------------------------------------------------------------------

instance TypeOp.HasOps Thm where
  ops :: Thm -> Set TypeOp
ops = Sequent -> Set TypeOp
forall a. HasOps a => a -> Set TypeOp
TypeOp.ops (Sequent -> Set TypeOp) -> (Thm -> Sequent) -> Thm -> Set TypeOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thm -> Sequent
dest

-------------------------------------------------------------------------------
-- Constants
-------------------------------------------------------------------------------

instance Const.HasConsts Thm where
  consts :: Thm -> Set Const
consts = Sequent -> Set Const
forall a. HasConsts a => a -> Set Const
Const.consts (Sequent -> Set Const) -> (Thm -> Sequent) -> Thm -> Set Const
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thm -> Sequent
dest

-------------------------------------------------------------------------------
-- Free variables
-------------------------------------------------------------------------------

instance Var.HasFree Thm where
  free :: Thm -> Set Var
free = Sequent -> Set Var
forall a. HasFree a => a -> Set Var
Var.free (Sequent -> Set Var) -> (Thm -> Sequent) -> Thm -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Thm -> Sequent
dest

-------------------------------------------------------------------------------
-- Substitutions
-------------------------------------------------------------------------------

instance Subst.CanSubst Thm where
  basicSubst :: Thm -> Subst -> (Maybe Thm, Subst)
basicSubst Thm
th Subst
sub =
      (Maybe Thm
th',Subst
sub')
    where
      Thm Sequent
sq = Thm
th
      (Maybe Sequent
sq',Subst
sub') = Sequent -> Subst -> (Maybe Sequent, Subst)
forall a. CanSubst a => a -> Subst -> (Maybe a, Subst)
Subst.basicSubst Sequent
sq Subst
sub
      th' :: Maybe Thm
th' = (Sequent -> Thm) -> Maybe Sequent -> Maybe Thm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Sequent -> Thm
Thm Maybe Sequent
sq'

-------------------------------------------------------------------------------
-- Standard axioms
-------------------------------------------------------------------------------

standardAxioms :: Set Thm
standardAxioms :: Set Thm
standardAxioms =
    [Thm] -> Set Thm
forall a. Ord a => [a] -> Set a
Set.fromList
      [Thm
axiomOfExtensionality,
       Thm
axiomOfChoice,
       Thm
axiomOfInfinity]

-------------------------------------------------------------------------------
--
-- ------------------------------ axiomOfExtensionality
--   !t : A -> B. (\x. t x) = t
-------------------------------------------------------------------------------

axiomOfExtensionality :: Thm
axiomOfExtensionality :: Thm
axiomOfExtensionality = Sequent -> Thm
Thm Sequent
Sequent.axiomOfExtensionality

-------------------------------------------------------------------------------
--
-- -------------------------------------- axiomOfChoice
--   !p (x : A). p x ==> p ((select) p)
-------------------------------------------------------------------------------

axiomOfChoice :: Thm
axiomOfChoice :: Thm
axiomOfChoice = Sequent -> Thm
Thm Sequent
Sequent.axiomOfChoice

-------------------------------------------------------------------------------
--
-- ------------------------------------------------- axiomOfInfinity
--   ?f : ind -> ind. injective f /\ ~surjective f
-------------------------------------------------------------------------------

axiomOfInfinity :: Thm
axiomOfInfinity :: Thm
axiomOfInfinity = Sequent -> Thm
Thm Sequent
Sequent.axiomOfInfinity

-------------------------------------------------------------------------------
-- Primitive rules of inference
-------------------------------------------------------------------------------

-------------------------------------------------------------------------------
--
-- ---------- assume t
--   t |- t
--
-- Side condition: The term t must have boolean type.
-------------------------------------------------------------------------------

assume :: Term -> Maybe Thm
assume :: Term -> Maybe Thm
assume Term
tm =
    (Sequent -> Thm) -> Maybe Sequent -> Maybe Thm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Sequent -> Thm
Thm (Maybe Sequent -> Maybe Thm) -> Maybe Sequent -> Maybe Thm
forall a b. (a -> b) -> a -> b
$ Set TermAlpha -> TermAlpha -> Maybe Sequent
Sequent.mk Set TermAlpha
h TermAlpha
c
  where
    c :: TermAlpha
c = Term -> TermAlpha
TermAlpha.mk Term
tm
    h :: Set TermAlpha
h = TermAlpha -> Set TermAlpha
forall a. a -> Set a
Set.singleton TermAlpha
c

-------------------------------------------------------------------------------
--
-- ------------------------- betaConv ((\v. t) u)
--   |- (\v. t) u = t[u/v]
-------------------------------------------------------------------------------

betaConv :: Term -> Maybe Thm
betaConv :: Term -> Maybe Thm
betaConv Term
tm = do
    (Term
vt,Term
u) <- Term -> Maybe (Term, Term)
Term.destApp Term
tm
    (Var
v,Term
t) <- Term -> Maybe (Var, Term)
Term.destAbs Term
vt
    let tm' :: Term
tm' = Subst -> Term -> Term
forall a. CanSubst a => Subst -> a -> a
Subst.trySubst (Var -> Term -> Subst
Subst.singletonUnsafe Var
v Term
u) Term
t
    let sq :: Sequent
sq = TermAlpha -> Sequent
Sequent.mkNullHypUnsafe (TermAlpha -> Sequent) -> TermAlpha -> Sequent
forall a b. (a -> b) -> a -> b
$ Term -> TermAlpha
TermAlpha.mk (Term -> TermAlpha) -> Term -> TermAlpha
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
Term.mkEqUnsafe Term
tm Term
tm'
    Thm -> Maybe Thm
forall (m :: * -> *) a. Monad m => a -> m a
return (Thm -> Maybe Thm) -> Thm -> Maybe Thm
forall a b. (a -> b) -> a -> b
$ Sequent -> Thm
Thm Sequent
sq

-------------------------------------------------------------------------------
--         A |- t        B |- u
-- -------------------------------------- deductAntisym
--   (A - {u}) union (B - {t}) |- t = u
-------------------------------------------------------------------------------

deductAntisym :: Thm -> Thm -> Thm
deductAntisym :: Thm -> Thm -> Thm
deductAntisym (Thm Sequent
sq1) (Thm Sequent
sq2) =
    Sequent -> Thm
Thm (Sequent -> Thm) -> Sequent -> Thm
forall a b. (a -> b) -> a -> b
$ Set TermAlpha -> TermAlpha -> Sequent
Sequent.mkUnsafe Set TermAlpha
h TermAlpha
c
  where
    (Set TermAlpha
h1,TermAlpha
c1) = Sequent -> (Set TermAlpha, TermAlpha)
Sequent.dest Sequent
sq1
    (Set TermAlpha
h2,TermAlpha
c2) = Sequent -> (Set TermAlpha, TermAlpha)
Sequent.dest Sequent
sq2
    h :: Set TermAlpha
h = Set TermAlpha -> Set TermAlpha -> Set TermAlpha
forall a. Ord a => Set a -> Set a -> Set a
Set.union (TermAlpha -> Set TermAlpha -> Set TermAlpha
forall a. Ord a => a -> Set a -> Set a
Set.delete TermAlpha
c2 Set TermAlpha
h1) (TermAlpha -> Set TermAlpha -> Set TermAlpha
forall a. Ord a => a -> Set a -> Set a
Set.delete TermAlpha
c1 Set TermAlpha
h2)
    c :: TermAlpha
c = Term -> TermAlpha
TermAlpha.mk (Term -> TermAlpha) -> Term -> TermAlpha
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
Term.mkEqUnsafe (TermAlpha -> Term
TermAlpha.dest TermAlpha
c1) (TermAlpha -> Term
TermAlpha.dest TermAlpha
c2)

-------------------------------------------------------------------------------
--   A |- t = u    B |- t'
-- ------------------------- eqMp
--       A union B |- u
--
-- Side condition: The terms t and t' must be alpha equivalent.
-------------------------------------------------------------------------------

eqMp :: Thm -> Thm -> Maybe Thm
eqMp :: Thm -> Thm -> Maybe Thm
eqMp (Thm Sequent
sq1) (Thm Sequent
sq2) = do
    (Term
t,Term
u) <- Term -> Maybe (Term, Term)
Term.destEq (Term -> Maybe (Term, Term)) -> Term -> Maybe (Term, Term)
forall a b. (a -> b) -> a -> b
$ TermAlpha -> Term
TermAlpha.dest TermAlpha
c1
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term -> TermAlpha
TermAlpha.mk Term
t TermAlpha -> TermAlpha -> Bool
forall a. Eq a => a -> a -> Bool
== TermAlpha
c2)
    let c :: TermAlpha
c = Term -> TermAlpha
TermAlpha.mk Term
u
    Thm -> Maybe Thm
forall (m :: * -> *) a. Monad m => a -> m a
return (Thm -> Maybe Thm) -> Thm -> Maybe Thm
forall a b. (a -> b) -> a -> b
$ Sequent -> Thm
Thm (Sequent -> Thm) -> Sequent -> Thm
forall a b. (a -> b) -> a -> b
$ Set TermAlpha -> TermAlpha -> Sequent
Sequent.mkUnsafe Set TermAlpha
h TermAlpha
c
  where
    (Set TermAlpha
h1,TermAlpha
c1) = Sequent -> (Set TermAlpha, TermAlpha)
Sequent.dest Sequent
sq1
    (Set TermAlpha
h2,TermAlpha
c2) = Sequent -> (Set TermAlpha, TermAlpha)
Sequent.dest Sequent
sq2
    h :: Set TermAlpha
h = Set TermAlpha -> Set TermAlpha -> Set TermAlpha
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set TermAlpha
h1 Set TermAlpha
h2

-------------------------------------------------------------------------------
--        A |- t = u
-- -------------------------- mkAbs v
--   A |- (\v. t) = (\v. u)
--
-- Side condition: The variable v must not be free in A.
-------------------------------------------------------------------------------

mkAbs :: Var -> Thm -> Maybe Thm
mkAbs :: Var -> Thm -> Maybe Thm
mkAbs Var
v (Thm Sequent
sq) = do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Var -> Set TermAlpha -> Bool
forall a. HasFree a => Var -> a -> Bool
Var.notFreeIn Var
v Set TermAlpha
h)
    (Term
t,Term
u) <- Term -> Maybe (Term, Term)
Term.destEq (Term -> Maybe (Term, Term)) -> Term -> Maybe (Term, Term)
forall a b. (a -> b) -> a -> b
$ TermAlpha -> Term
TermAlpha.dest TermAlpha
tu
    let vt :: Term
vt = Var -> Term -> Term
Term.mkAbs Var
v Term
t
    let vu :: Term
vu = Var -> Term -> Term
Term.mkAbs Var
v Term
u
    let c :: TermAlpha
c = Term -> TermAlpha
TermAlpha.mk (Term -> TermAlpha) -> Term -> TermAlpha
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
Term.mkEqUnsafe Term
vt Term
vu
    Thm -> Maybe Thm
forall (m :: * -> *) a. Monad m => a -> m a
return (Thm -> Maybe Thm) -> Thm -> Maybe Thm
forall a b. (a -> b) -> a -> b
$ Sequent -> Thm
Thm (Sequent -> Thm) -> Sequent -> Thm
forall a b. (a -> b) -> a -> b
$ Set TermAlpha -> TermAlpha -> Sequent
Sequent.mkUnsafe Set TermAlpha
h TermAlpha
c
  where
    (Set TermAlpha
h,TermAlpha
tu) = Sequent -> (Set TermAlpha, TermAlpha)
Sequent.dest Sequent
sq

mkAbsUnsafe :: Var -> Thm -> Thm
mkAbsUnsafe :: Var -> Thm -> Thm
mkAbsUnsafe = String -> (Var -> Thm -> Maybe Thm) -> Var -> Thm -> Thm
forall a b c. String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 String
"HOL.Thm.mkAbs" Var -> Thm -> Maybe Thm
mkAbs

-------------------------------------------------------------------------------
--   A |- f = g    B |- x = y
-- ---------------------------- mkApp
--    A union B |- f x = g y
--
-- Side condition: The types of f and x must be compatible.
-------------------------------------------------------------------------------

mkApp :: Thm -> Thm -> Maybe Thm
mkApp :: Thm -> Thm -> Maybe Thm
mkApp (Thm Sequent
sq1) (Thm Sequent
sq2) = do
    (Term
f,Term
g) <- Term -> Maybe (Term, Term)
Term.destEq (Term -> Maybe (Term, Term)) -> Term -> Maybe (Term, Term)
forall a b. (a -> b) -> a -> b
$ TermAlpha -> Term
TermAlpha.dest TermAlpha
c1
    (Term
x,Term
y) <- Term -> Maybe (Term, Term)
Term.destEq (Term -> Maybe (Term, Term)) -> Term -> Maybe (Term, Term)
forall a b. (a -> b) -> a -> b
$ TermAlpha -> Term
TermAlpha.dest TermAlpha
c2
    Term
fx <- Term -> Term -> Maybe Term
Term.mkApp Term
f Term
x
    Term
gy <- Term -> Term -> Maybe Term
Term.mkApp Term
g Term
y
    let c :: TermAlpha
c = Term -> TermAlpha
TermAlpha.mk (Term -> TermAlpha) -> Term -> TermAlpha
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
Term.mkEqUnsafe Term
fx Term
gy
    Thm -> Maybe Thm
forall (m :: * -> *) a. Monad m => a -> m a
return (Thm -> Maybe Thm) -> Thm -> Maybe Thm
forall a b. (a -> b) -> a -> b
$ Sequent -> Thm
Thm (Sequent -> Thm) -> Sequent -> Thm
forall a b. (a -> b) -> a -> b
$ Set TermAlpha -> TermAlpha -> Sequent
Sequent.mkUnsafe Set TermAlpha
h TermAlpha
c
  where
    (Set TermAlpha
h1,TermAlpha
c1) = Sequent -> (Set TermAlpha, TermAlpha)
Sequent.dest Sequent
sq1
    (Set TermAlpha
h2,TermAlpha
c2) = Sequent -> (Set TermAlpha, TermAlpha)
Sequent.dest Sequent
sq2
    h :: Set TermAlpha
h = Set TermAlpha -> Set TermAlpha -> Set TermAlpha
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set TermAlpha
h1 Set TermAlpha
h2

mkAppUnsafe :: Thm -> Thm -> Thm
mkAppUnsafe :: Thm -> Thm -> Thm
mkAppUnsafe = String -> (Thm -> Thm -> Maybe Thm) -> Thm -> Thm -> Thm
forall a b c. String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 String
"HOL.Thm.mkApp" Thm -> Thm -> Maybe Thm
mkApp

-------------------------------------------------------------------------------
--
-- ------------ refl t
--   |- t = t
-------------------------------------------------------------------------------

refl :: Term -> Thm
refl :: Term -> Thm
refl = Sequent -> Thm
Thm (Sequent -> Thm) -> (Term -> Sequent) -> Term -> Thm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermAlpha -> Sequent
Sequent.mkNullHypUnsafe (TermAlpha -> Sequent) -> (Term -> TermAlpha) -> Term -> Sequent
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Term -> TermAlpha
TermAlpha.mk (Term -> TermAlpha) -> (Term -> Term) -> Term -> TermAlpha
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
Term.mkRefl

-------------------------------------------------------------------------------
--          A |- t
-- ------------------------ subst theta
--   A[theta] |- t[theta]
-------------------------------------------------------------------------------

subst :: Subst -> Thm -> Thm
subst :: Subst -> Thm -> Thm
subst = Subst -> Thm -> Thm
forall a. CanSubst a => Subst -> a -> a
Subst.trySubst

-------------------------------------------------------------------------------
-- Principles of definition
-------------------------------------------------------------------------------

-------------------------------------------------------------------------------
--
-- --------------- defineConst name t
--   |- name = t
--
-- where name is a new constant with the same type as the term t.
--
-- Side condition: The term t has no free variables.
-- Side condition: All type variables in t also appear in the type of t.
-------------------------------------------------------------------------------

defineConst :: Name -> Term -> Maybe (Const,Thm)
defineConst :: Name -> Term -> Maybe (Const, Thm)
defineConst Name
name Term
t = do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term -> Bool
forall a. HasFree a => a -> Bool
Var.closed Term
t)
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Set TypeVar -> Set TypeVar -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (Term -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
TypeVar.vars Term
t) (Type -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
TypeVar.vars Type
ty))
    (Const, Thm) -> Maybe (Const, Thm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Const
nameC, Sequent -> Thm
Thm (Sequent -> Thm) -> Sequent -> Thm
forall a b. (a -> b) -> a -> b
$ TermAlpha -> Sequent
Sequent.mkNullHypUnsafe TermAlpha
c)
  where
    nameC :: Const
nameC = Name -> ConstProv -> Const
Const Name
name (ConstDef -> ConstProv
DefConstProv (Term -> ConstDef
ConstDef Term
t))
    ty :: Type
ty = Term -> Type
Term.typeOf Term
t
    c :: TermAlpha
c = Term -> TermAlpha
TermAlpha.mk (Term -> TermAlpha) -> Term -> TermAlpha
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
Term.mkEqUnsafe (Const -> Type -> Term
Term.mkConst Const
nameC Type
ty) Term
t

-------------------------------------------------------------------------------
--             |- p t
-- ---------------------------------------- defineTypeOp name abs rep tyVars
--   |- (\a. abs (rep a)) = (\a. a)
--   |- (\r. rep (abs r) = r) = (\r. p r)
--
-- where if p has type r -> bool, then abs and rep are new constants with
-- types r -> a and a -> r, respectively, where a is the new type
-- tyVars name.
--
-- Side condition: tyVars lists all the type variables in p precisely once.
-------------------------------------------------------------------------------

defineTypeOp :: Name -> Name -> Name -> [TypeVar] -> Thm ->
                Maybe (TypeOp,Const,Const,Thm,Thm)
defineTypeOp :: Name
-> Name
-> Name
-> [TypeVar]
-> Thm
-> Maybe (TypeOp, Const, Const, Thm, Thm)
defineTypeOp Name
opName Name
absName Name
repName [TypeVar]
tyVarl Thm
existenceTh = do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([TypeVar] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeVar]
tyVarl Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Set TypeVar -> Int
forall a. Set a -> Int
Set.size Set TypeVar
tyVars)
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Thm -> Bool
nullHyp Thm
existenceTh)
    (Term
p,Term
witness) <- Term -> Maybe (Term, Term)
Term.destApp (Term -> Maybe (Term, Term)) -> Term -> Maybe (Term, Term)
forall a b. (a -> b) -> a -> b
$ TermAlpha -> Term
TermAlpha.dest (TermAlpha -> Term) -> TermAlpha -> Term
forall a b. (a -> b) -> a -> b
$ Thm -> TermAlpha
concl Thm
existenceTh
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term -> Bool
forall a. HasFree a => a -> Bool
Var.closed Term
p)
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Term -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
TypeVar.vars Term
p Set TypeVar -> Set TypeVar -> Bool
forall a. Eq a => a -> a -> Bool
== Set TypeVar
tyVars)
    let def :: TypeOpDef
def = Term -> [TypeVar] -> TypeOpDef
TypeOpDef Term
p [TypeVar]
tyVarl
    let opT :: TypeOp
opT = Name -> TypeOpProv -> TypeOp
TypeOp Name
opName (TypeOpProv -> TypeOp) -> TypeOpProv -> TypeOp
forall a b. (a -> b) -> a -> b
$ TypeOpDef -> TypeOpProv
DefTypeOpProv TypeOpDef
def
    let absC :: Const
absC = Name -> ConstProv -> Const
Const Name
absName (ConstProv -> Const) -> ConstProv -> Const
forall a b. (a -> b) -> a -> b
$ TypeOpDef -> ConstProv
AbsConstProv TypeOpDef
def
    let repC :: Const
repC = Name -> ConstProv -> Const
Const Name
repName (ConstProv -> Const) -> ConstProv -> Const
forall a b. (a -> b) -> a -> b
$ TypeOpDef -> ConstProv
RepConstProv TypeOpDef
def
    let aTy :: Type
aTy = TypeOp -> [Type] -> Type
Type.mkOp TypeOp
opT ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (TypeVar -> Type) -> [TypeVar] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map TypeVar -> Type
Type.mkVar [TypeVar]
tyVarl
    let rTy :: Type
rTy = Term -> Type
Term.typeOf Term
witness
    let absTm :: Term
absTm = Const -> Type -> Term
Term.mkConst Const
absC (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
Type.mkFun Type
rTy Type
aTy
    let repTm :: Term
repTm = Const -> Type -> Term
Term.mkConst Const
repC (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
Type.mkFun Type
aTy Type
rTy
    let absRepTh :: Thm
absRepTh =
            Sequent -> Thm
Thm (Sequent -> Thm) -> Sequent -> Thm
forall a b. (a -> b) -> a -> b
$ TermAlpha -> Sequent
Sequent.mkNullHypUnsafe (TermAlpha -> Sequent) -> TermAlpha -> Sequent
forall a b. (a -> b) -> a -> b
$ Term -> TermAlpha
TermAlpha.mk Term
c
          where
            aVar :: Var
aVar = Name -> Type -> Var
Var (String -> Name
mkGlobal String
"a") Type
aTy
            aTm :: Term
aTm = Var -> Term
Term.mkVar Var
aVar
            l :: Term
l = Term -> Term -> Term
Term.mkAppUnsafe Term
absTm (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
Term.mkAppUnsafe Term
repTm Term
aTm
            r :: Term
r = Term
aTm
            c :: Term
c = Term -> Term -> Term
Term.mkEqUnsafe (Var -> Term -> Term
Term.mkAbs Var
aVar Term
l) (Var -> Term -> Term
Term.mkAbs Var
aVar Term
r)
    let repAbsTh :: Thm
repAbsTh =
            Sequent -> Thm
Thm (Sequent -> Thm) -> Sequent -> Thm
forall a b. (a -> b) -> a -> b
$ TermAlpha -> Sequent
Sequent.mkNullHypUnsafe (TermAlpha -> Sequent) -> TermAlpha -> Sequent
forall a b. (a -> b) -> a -> b
$ Term -> TermAlpha
TermAlpha.mk Term
c
          where
            rVar :: Var
rVar = Name -> Type -> Var
Var (String -> Name
mkGlobal String
"r") Type
rTy
            rTm :: Term
rTm = Var -> Term
Term.mkVar Var
rVar
            ll :: Term
ll = Term -> Term -> Term
Term.mkAppUnsafe Term
repTm (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
Term.mkAppUnsafe Term
absTm Term
rTm
            l :: Term
l = Term -> Term -> Term
Term.mkEqUnsafe Term
ll Term
rTm
            r :: Term
r = Term -> Term -> Term
Term.mkAppUnsafe Term
p Term
rTm
            c :: Term
c = Term -> Term -> Term
Term.mkEqUnsafe (Var -> Term -> Term
Term.mkAbs Var
rVar Term
l) (Var -> Term -> Term
Term.mkAbs Var
rVar Term
r)
    (TypeOp, Const, Const, Thm, Thm)
-> Maybe (TypeOp, Const, Const, Thm, Thm)
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeOp
opT,Const
absC,Const
repC,Thm
absRepTh,Thm
repAbsTh)
  where
    tyVars :: Set TypeVar
tyVars = [TypeVar] -> Set TypeVar
forall a. Ord a => [a] -> Set a
Set.fromList [TypeVar]
tyVarl