{- |
module: $Header$
description: Higher order logic derived rules of inference
license: MIT

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

module HOL.Rule
where

import Control.Monad (foldM,guard)
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set

import HOL.Data
import HOL.Name
import HOL.Sequent (Sequent)
import qualified HOL.Sequent as Sequent
import qualified HOL.Subst as Subst
import qualified HOL.Term as Term
import qualified HOL.TermAlpha as TermAlpha
import HOL.Thm (Thm)
import qualified HOL.Thm as Thm
import HOL.Util (mkUnsafe2)
import qualified HOL.Var as Var

-------------------------------------------------------------------------------
-- Applying equalities at subterms
-------------------------------------------------------------------------------

rator :: Thm -> Term -> Maybe Thm
rator :: Thm -> Term -> Maybe Thm
rator Thm
th Term
tm = Thm -> Thm -> Maybe Thm
Thm.mkApp Thm
th (Term -> Thm
Thm.refl Term
tm)

ratorUnsafe :: Thm -> Term -> Thm
ratorUnsafe :: Thm -> Term -> Thm
ratorUnsafe = String -> (Thm -> Term -> Maybe Thm) -> Thm -> Term -> Thm
forall a b c. String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 String
"HOL.Rule.rator" Thm -> Term -> Maybe Thm
rator

rand :: Term -> Thm -> Maybe Thm
rand :: Term -> Thm -> Maybe Thm
rand Term
tm Thm
th = Thm -> Thm -> Maybe Thm
Thm.mkApp (Term -> Thm
Thm.refl Term
tm) Thm
th

randUnsafe :: Term -> Thm -> Thm
randUnsafe :: Term -> Thm -> Thm
randUnsafe = String -> (Term -> Thm -> Maybe Thm) -> Term -> Thm -> Thm
forall a b c. String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 String
"HOL.Rule.rand" Term -> Thm -> Maybe Thm
rand

-------------------------------------------------------------------------------
-- Symmetry of equality
-------------------------------------------------------------------------------

sym :: Thm -> Maybe Thm
sym :: Thm -> Maybe Thm
sym Thm
th = do
    Term
el <- Term -> Maybe Term
Term.rator (Term -> Maybe Term) -> Term -> Maybe 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
Thm.concl Thm
th
    (Term
e,Term
l) <- Term -> Maybe (Term, Term)
Term.destApp Term
el
    let th0 :: Thm
th0 = Term -> Thm
Thm.refl Term
l
    Thm
th1 <- Term -> Thm -> Maybe Thm
rand Term
e Thm
th
    Thm
th2 <- Thm -> Thm -> Maybe Thm
Thm.mkApp Thm
th1 Thm
th0
    Thm -> Thm -> Maybe Thm
Thm.eqMp Thm
th2 Thm
th0

-------------------------------------------------------------------------------
-- Transitivity of equality
-------------------------------------------------------------------------------

trans :: Thm -> Thm -> Maybe Thm
trans :: Thm -> Thm -> Maybe Thm
trans Thm
th1 Thm
th2 = do
    Term
tm <- Term -> Maybe Term
Term.rator (Term -> Maybe Term) -> Term -> Maybe 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
Thm.concl Thm
th1
    Thm
th3 <- Term -> Thm -> Maybe Thm
rand Term
tm Thm
th2
    Thm -> Thm -> Maybe Thm
Thm.eqMp Thm
th3 Thm
th1

transUnsafe :: Thm -> Thm -> Thm
transUnsafe :: Thm -> Thm -> Thm
transUnsafe = String -> (Thm -> Thm -> Maybe Thm) -> Thm -> Thm -> Thm
forall a b c. String -> (a -> b -> Maybe c) -> a -> b -> c
mkUnsafe2 String
"HOL.Rule.trans" Thm -> Thm -> Maybe Thm
trans

-------------------------------------------------------------------------------
-- Proving hypotheses
-------------------------------------------------------------------------------

proveHyp :: Thm -> Thm -> Maybe Thm
proveHyp :: Thm -> Thm -> Maybe Thm
proveHyp Thm
th1 Thm
th2 = do
    let th3 :: Thm
th3 = Thm -> Thm -> Thm
Thm.deductAntisym Thm
th1 Thm
th2
    Thm -> Thm -> Maybe Thm
Thm.eqMp Thm
th3 Thm
th1

-------------------------------------------------------------------------------
-- Alpha conversion
-------------------------------------------------------------------------------

alpha :: Term -> Thm -> Maybe Thm
alpha :: Term -> Thm -> Maybe Thm
alpha Term
c Thm
th =
    if TermAlpha -> Term
TermAlpha.dest (Thm -> TermAlpha
Thm.concl Thm
th) Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
c then Thm -> Maybe Thm
forall a. a -> Maybe a
Just Thm
th
    else Thm -> Thm -> Maybe Thm
Thm.eqMp (Term -> Thm
Thm.refl Term
c) Thm
th

alphaHyp :: Term -> Thm -> Maybe Thm
alphaHyp :: Term -> Thm -> Maybe Thm
alphaHyp Term
h Thm
th =
    case TermAlpha -> Set TermAlpha -> Maybe TermAlpha
forall a. Ord a => a -> Set a -> Maybe a
Set.lookupLE TermAlpha
ha (Thm -> Set TermAlpha
Thm.hyp Thm
th) of
      Maybe TermAlpha
Nothing -> Maybe Thm
forall a. Maybe a
Nothing
      Just TermAlpha
ha' ->
        if TermAlpha
ha' TermAlpha -> TermAlpha -> Bool
forall a. Eq a => a -> a -> Bool
/= TermAlpha
ha then Maybe Thm
forall a. Maybe a
Nothing
        else if TermAlpha -> Term
TermAlpha.dest TermAlpha
ha' Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
h then Thm -> Maybe Thm
forall a. a -> Maybe a
Just Thm
th
        else do
          Thm
th0 <- Term -> Maybe Thm
Thm.assume Term
h
          Thm -> Thm -> Maybe Thm
proveHyp Thm
th0 Thm
th
  where
    ha :: TermAlpha
ha = Term -> TermAlpha
TermAlpha.mk Term
h

alphaSequent :: Sequent -> Thm -> Maybe Thm
alphaSequent :: Sequent -> Thm -> Maybe Thm
alphaSequent Sequent
sq Thm
th = do
    Thm
th0 <- Term -> Thm -> Maybe Thm
alpha (TermAlpha -> Term
TermAlpha.dest TermAlpha
c) Thm
th
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Thm -> Set TermAlpha
Thm.hyp Thm
th Set TermAlpha -> Set TermAlpha -> Bool
forall a. Eq a => a -> a -> Bool
== Set TermAlpha
h)
    (Thm -> Term -> Maybe Thm) -> Thm -> [Term] -> Maybe Thm
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((Term -> Thm -> Maybe Thm) -> Thm -> Term -> Maybe Thm
forall a b c. (a -> b -> c) -> b -> a -> c
flip Term -> Thm -> Maybe Thm
alphaHyp) Thm
th0 [Term]
hl
  where
    (Set TermAlpha
h,TermAlpha
c) = Sequent -> (Set TermAlpha, TermAlpha)
Sequent.dest Sequent
sq
    hl :: [Term]
hl = (TermAlpha -> Term) -> [TermAlpha] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map TermAlpha -> Term
TermAlpha.dest ([TermAlpha] -> [Term]) -> [TermAlpha] -> [Term]
forall a b. (a -> b) -> a -> b
$ Set TermAlpha -> [TermAlpha]
forall a. Set a -> [a]
Set.toList Set TermAlpha
h

-------------------------------------------------------------------------------
-- The new principle of constant definition
-------------------------------------------------------------------------------

defineConstList :: [(Name,Var)] -> Thm -> Maybe ([Const],Thm)
defineConstList :: [(Name, Var)] -> Thm -> Maybe ([Const], Thm)
defineConstList [(Name, Var)]
nvs Thm
th = do
    Map Var Term
vm <- (Map Var Term -> TermAlpha -> Maybe (Map Var Term))
-> Map Var Term -> [TermAlpha] -> Maybe (Map Var Term)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map Var Term -> TermAlpha -> Maybe (Map Var Term)
addVar Map Var Term
forall k a. Map k a
Map.empty ([TermAlpha] -> Maybe (Map Var Term))
-> [TermAlpha] -> Maybe (Map Var Term)
forall a b. (a -> b) -> a -> b
$ Set TermAlpha -> [TermAlpha]
forall a. Set a -> [a]
Set.toList (Set TermAlpha -> [TermAlpha]) -> Set TermAlpha -> [TermAlpha]
forall a b. (a -> b) -> a -> b
$ Thm -> Set TermAlpha
Thm.hyp Thm
th
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Set Var -> Set Var -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (TermAlpha -> Set Var
forall a. HasFree a => a -> Set Var
Var.free (Thm -> TermAlpha
Thm.concl Thm
th)) (Map Var Term -> Set Var
forall k a. Map k a -> Set k
Map.keysSet Map Var Term
vm))
    ([Const]
cs,[(Var, Term)]
vcs,[Thm]
defs,Map Var Term
vm0) <- (([Const], [(Var, Term)], [Thm], Map Var Term)
 -> (Name, Var)
 -> Maybe ([Const], [(Var, Term)], [Thm], Map Var Term))
-> ([Const], [(Var, Term)], [Thm], Map Var Term)
-> [(Name, Var)]
-> Maybe ([Const], [(Var, Term)], [Thm], Map Var Term)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ([Const], [(Var, Term)], [Thm], Map Var Term)
-> (Name, Var)
-> Maybe ([Const], [(Var, Term)], [Thm], Map Var Term)
delVar ([],[],[],Map Var Term
vm) [(Name, Var)]
nvs
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Map Var Term -> Bool
forall k a. Map k a -> Bool
Map.null Map Var Term
vm0)
    let sub :: Subst
sub = [(TypeVar, Type)] -> [(Var, Term)] -> Subst
Subst.fromListUnsafe [] [(Var, Term)]
vcs
    Thm
def <- (Thm -> Thm -> Maybe Thm) -> Thm -> [Thm] -> Maybe Thm
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((Thm -> Thm -> Maybe Thm) -> Thm -> Thm -> Maybe Thm
forall a b c. (a -> b -> c) -> b -> a -> c
flip Thm -> Thm -> Maybe Thm
proveHyp) (Subst -> Thm -> Thm
Thm.subst Subst
sub Thm
th) [Thm]
defs
    ([Const], Thm) -> Maybe ([Const], Thm)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Const]
cs,Thm
def)
  where
    addVar :: Map Var Term -> TermAlpha -> Maybe (Map Var Term)
addVar Map Var Term
vm TermAlpha
h = do
      (Term
vt,Term
tm) <- 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
h
      Var
v <- Term -> Maybe Var
Term.destVar Term
vt
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Var -> Map Var Term -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.notMember Var
v Map Var Term
vm)
      Map Var Term -> Maybe (Map Var Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Var Term -> Maybe (Map Var Term))
-> Map Var Term -> Maybe (Map Var Term)
forall a b. (a -> b) -> a -> b
$ Var -> Term -> Map Var Term -> Map Var Term
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v Term
tm Map Var Term
vm

    delVar :: ([Const], [(Var, Term)], [Thm], Map Var Term)
-> (Name, Var)
-> Maybe ([Const], [(Var, Term)], [Thm], Map Var Term)
delVar ([Const]
cs,[(Var, Term)]
vcs,[Thm]
defs,Map Var Term
vm) (Name
n,Var
v) = do
      Term
tm <- Var -> Map Var Term -> Maybe Term
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Var
v Map Var Term
vm
      (Const
c,Thm
def) <- Name -> Term -> Maybe (Const, Thm)
Thm.defineConst Name
n Term
tm
      let vc :: (Var, Term)
vc = (Var
v, Const -> Type -> Term
Term.mkConst Const
c (Var -> Type
Var.typeOf Var
v))
      ([Const], [(Var, Term)], [Thm], Map Var Term)
-> Maybe ([Const], [(Var, Term)], [Thm], Map Var Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Const
c Const -> [Const] -> [Const]
forall a. a -> [a] -> [a]
: [Const]
cs, (Var, Term)
vc (Var, Term) -> [(Var, Term)] -> [(Var, Term)]
forall a. a -> [a] -> [a]
: [(Var, Term)]
vcs, Thm
def Thm -> [Thm] -> [Thm]
forall a. a -> [a] -> [a]
: [Thm]
defs, Var -> Map Var Term -> Map Var Term
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Var
v Map Var Term
vm)

-------------------------------------------------------------------------------
-- The legacy (a.k.a. HOL Light) version of defineTypeOp
-------------------------------------------------------------------------------

defineTypeOpLegacy :: Name -> Name -> Name -> [TypeVar] -> Thm ->
                      Maybe (TypeOp,Const,Const,Thm,Thm)
defineTypeOpLegacy :: Name
-> Name
-> Name
-> [TypeVar]
-> Thm
-> Maybe (TypeOp, Const, Const, Thm, Thm)
defineTypeOpLegacy Name
opName Name
absName Name
repName [TypeVar]
tyVarl Thm
existenceTh = do
    (TypeOp
opT,Const
absC,Const
repC,Thm
absRepTh,Thm
repAbsTh) <-
      Name
-> Name
-> Name
-> [TypeVar]
-> Thm
-> Maybe (TypeOp, Const, Const, Thm, Thm)
Thm.defineTypeOp Name
opName Name
absName Name
repName [TypeVar]
tyVarl Thm
existenceTh
    let absRepTh' :: Thm
absRepTh' = (Thm -> Maybe Thm) -> Thm -> Thm
forall t p. (t -> Maybe p) -> t -> p
unsafe Thm -> Maybe Thm
convertAbsRep Thm
absRepTh
    let repAbsTh' :: Thm
repAbsTh' = (Thm -> Maybe Thm) -> Thm -> Thm
forall t p. (t -> Maybe p) -> t -> p
unsafe Thm -> Maybe Thm
convertRepAbs Thm
repAbsTh
    (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
    unsafe :: (t -> Maybe p) -> t -> p
unsafe t -> Maybe p
convert t
th =
        case t -> Maybe p
convert t
th of
          Just p
th' -> p
th'
          Maybe p
Nothing -> String -> p
forall a. HasCallStack => String -> a
error String
"HOL.Rule.defineTypeOpLegacy failed"

    convertAbsRep :: Thm -> Maybe Thm
convertAbsRep Thm
th0 = do  -- ⊢ (\a. abs (rep a)) = (\a. a)
        Term
aId <- Term -> Maybe Term
Term.rhs (Term -> Maybe Term) -> Term -> Maybe 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
Thm.concl Thm
th0  -- \a. a
        (Var
_,Term
aTm) <- Term -> Maybe (Var, Term)
Term.destAbs Term
aId  -- a
        Thm
th1 <- Thm -> Term -> Maybe Thm
rator Thm
th0 Term
aTm  -- ⊢ (\a. abs (rep a)) a = (\a. a) a
        (Term
tm0,Term
rhsTm) <- 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
Thm.concl Thm
th1
        (Term
eqTm,Term
lhsTm) <- Term -> Maybe (Term, Term)
Term.destApp Term
tm0
        Thm
th2 <- Term -> Maybe Thm
Thm.betaConv Term
lhsTm  -- ⊢ (\a. abs (rep a)) a = abs (rep a)
        Thm
th3 <- Term -> Thm -> Maybe Thm
rand Term
eqTm Thm
th2
        Thm
th4 <- Term -> Maybe Thm
Thm.betaConv Term
rhsTm  -- ⊢ (\a. a) a = a
        Thm
th5 <- Thm -> Thm -> Maybe Thm
Thm.mkApp Thm
th3 Thm
th4
        Thm -> Thm -> Maybe Thm
Thm.eqMp Thm
th5 Thm
th1  -- ⊢ abs (rep a) = a

    convertRepAbs :: Thm -> Maybe Thm
convertRepAbs Thm
th0 = do  -- (\r. rep (abs r) = r) = (\r. p r)
        Term
tm0 <- Term -> Maybe Term
Term.lhs (Term -> Maybe Term) -> Term -> Maybe 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
Thm.concl Thm
th0
        (Var
_,Term
tm1) <- Term -> Maybe (Var, Term)
Term.destAbs Term
tm0  -- rep (abs r) = r
        Term
rTm <- Term -> Maybe Term
Term.rhs Term
tm1  -- r
        Thm
th1 <- Thm -> Term -> Maybe Thm
rator Thm
th0 Term
rTm  -- ⊢ (\r. rep (abs r) = r) r <=> (\r. p r) r
        (Term
tm2,Term
rhsTm) <- 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
Thm.concl Thm
th1
        (Term
iffTm,Term
lhsTm) <- Term -> Maybe (Term, Term)
Term.destApp Term
tm2
        Thm
th2 <- Term -> Maybe Thm
Thm.betaConv Term
lhsTm
        Thm
th3 <- Term -> Thm -> Maybe Thm
rand Term
iffTm Thm
th2
        Thm
th4 <- Term -> Maybe Thm
Thm.betaConv Term
rhsTm
        Thm
th5 <- Thm -> Thm -> Maybe Thm
Thm.mkApp Thm
th3 Thm
th4
        Thm
th6 <- Thm -> Thm -> Maybe Thm
Thm.eqMp Thm
th5 Thm
th1  -- ⊢ rep (abs r) = r <=> p r
        Thm -> Maybe Thm
sym Thm
th6  -- ⊢ p r <=> rep (abs r) = r