haskhol-core-1.1.0: src/HaskHOL/Core/Kernel.hs
{-# LANGUAGE PatternSynonyms #-}
{-|
Module: HaskHOL.Core.Kernel
Copyright: (c) The University of Kansas 2013
LICENSE: BSD3
Maintainer: ecaustin@ittc.ku.edu
Stability: unstable
Portability: unknown
This module exports the logical kernel of HaskHOL. It consists of:
* A safe view of HOL theorems for HaskHOL.
* The primitive inference rules of the system.
* The primitive, stateless theory extension functions.
For clarity, all of these items have been seperated based on their influential
system: HOL Light, Stateless HOL, and HOL2P.
Note that, per the stateless approach, any stateful, but still primitive,
functions related to theorems or theory extension have been relocated to the
"HaskHOL.Core.State" module.
-}
module HaskHOL.Core.Kernel
( -- * A View of HOL Types, Terms, and Theorems
-- ** A Quick Note on Pattern Synonyms
-- $ViewPatterns
-- ** Destructors and Accessors for Theorems
HOLThm
, pattern Thm
, destThm
, hyp
, concl
-- * HOL Light Primitive Inference Rules
, primREFL
, primTRANS
, primMK_COMB
, primABS
, primBETA
, primASSUME
, primEQ_MP
, primDEDUCT_ANTISYM
, primINST_TYPE
, primINST_TYPE_FULL
, primINST
-- * HOL2P Primitive Inference Rules
, primTYABS
, primTYAPP2
, primTYAPP
, primTYBETA
-- * Stateless HOL Primitive Theory Extensions
, axiomThm
, newDefinedConst
, newDefinedTypeOp
-- * Primitive Re-Exports
, module HaskHOL.Core.Kernel.Types
, module HaskHOL.Core.Kernel.Terms
) where
import HaskHOL.Core.Lib
import HaskHOL.Core.Kernel.Prims
import HaskHOL.Core.Kernel.Types
import HaskHOL.Core.Kernel.Terms
import Data.Hashable
{-
Used to quickly make an equality between two terms we know to be of the same
type. Not exposed to the user.
-}
safeMkEq :: HOLTerm -> HOLTerm -> HOLTerm
safeMkEq l r =
let eq = tmEq $ typeOf l in
CombIn (CombIn eq l) r
{-
Unions two lists of terms, ordering the result modulo alpha-equivalence. Not
exposed to the user.
-}
termUnion :: [HOLTerm] -> [HOLTerm] -> [HOLTerm]
termUnion [] l2 = l2
termUnion l1 [] = l1
termUnion l1@(h1:t1) l2@(h2:t2) =
case alphaOrder h1 h2 of
EQ -> h1 : termUnion t1 t2
LT -> h1 : termUnion t1 l2
_ -> h2 : termUnion l1 t2
{-
Removes a term from a term list, ordering the result modulo alpha-equivalence.
Not exposed to the user.
-}
termRemove :: HOLTerm -> [HOLTerm] -> [HOLTerm]
termRemove _ [] = []
termRemove t l@(s:ss) =
case alphaOrder t s of
GT -> s : termRemove t ss
EQ -> ss
_ -> l
{-
Maps a function over a list of terms, termUnion-ing the result at each step.
Roughly equivalent to a composition of nub and map that orders the result
modulo alpha-equivalence. Not exposed to the user
-}
termImage :: (HOLTerm -> HOLTerm) -> [HOLTerm] -> [HOLTerm]
termImage _ [] = []
termImage f (h:t) = termUnion [f h] $ termImage f t
termImageM :: Monad m => (HOLTerm -> m HOLTerm) -> [HOLTerm] -> m [HOLTerm]
termImageM _ [] = return []
termImageM f (h:t) =
do h' <- f h
liftM (termUnion [h']) $ termImageM f t
{-
HOL Light Theorem Primitives
-}
{-|
Destructs a theorem, returning its list of assumption terms and conclusion
term.
-}
destThm :: HOLThm -> ([HOLTerm], HOLTerm)
destThm (ThmIn as c) = (as, c)
-- | Accessor for the hypotheses, or assumption terms, of a theorem.
hyp :: HOLThm -> [HOLTerm]
hyp (ThmIn as _) = as
-- | Accessor for the conclusion term of a theorem.
concl :: HOLThm -> HOLTerm
concl (ThmIn _ c) = c
{-
HOL Light Primitive Inference Rules
-}
-- Basic Equality Rules
{-|@
t
-----------
|- t = t
@
Never fails.
-}
primREFL :: HOLTerm -> HOLThm
primREFL tm = ThmIn [] $ safeMkEq tm tm
{-|@
A1 |- t1 = t2 A2 |- t2 = t3
-------------------------------
A1 U A2 |- t1 = t3
@
Fails with 'Left' in the following cases:
* The middle terms are not alpha-equivalent.
* One, or both, of the theorem conclusions is not an equation.
-}
primTRANS :: HOLThm -> HOLThm -> Either String HOLThm
primTRANS (ThmIn as1 (CombIn eql@(CombIn (TmEq _) _) m1)) (ThmIn as2 (m2 := r))
| m1 `aConv` m2 =
let as' = termUnion as1 as2 in
Right . ThmIn as' $ CombIn eql r
| otherwise = Left "primTRANS: middle terms don't agree"
primTRANS _ _ = Left "primTRANS: not both equations"
-- Basic Congruence Rules
{-|@
A1 |- f = g A2 |- x = y
---------------------------
A1 U A2 |- f x = g y
@
Fails with 'Left' in the following cases:
* One, or both, of the theorem conclusions is not an equation.
* The first theorem conclusion is not an equation of function terms.
* The types of the function terms and argument terms do not agree.
-}
primMK_COMB :: HOLThm -> HOLThm -> Either String HOLThm
primMK_COMB (ThmIn as1 (l1 := r1)) (ThmIn as2 (l2 := r2)) =
case typeOf l1 of
TyAppIn TyOpFun (ty:_:_)
| typeOf l2 `tyAConv` ty ->
let as' = termUnion as1 as2 in
Right . ThmIn as' $ safeMkEq (CombIn l1 l2) (CombIn r1 r2)
| otherwise -> Left "primMK_COMB: types do not agree"
_ -> Left "primMK_COMB: not a function type"
primMK_COMB _ _ = Left "primMK_COMB: not both equations"
{-|@
A |- t1 = t2
-------------------------------
A |- (\\ x . t1) = (\\ x . t2)
@
Fails with 'Left' in the following cases:
* The term to bind is free in the assumption list of the theorem.
* The conclusion of the theorem is not an equation.
-}
primABS :: HOLTerm -> HOLThm -> Either String HOLThm
primABS v@VarIn{} (ThmIn as (l := r))
| any (varFreeIn v) as =
Left "primABS: variable is free in assumptions"
| otherwise =
Right . ThmIn as $ safeMkEq (AbsIn v l) (AbsIn v r)
primABS _ _ = Left "primABS: not an equation"
-- Beta Reduction
{-|@
(\\ x . t) x
----------------------------
|- (\\ x . t) x = t
@
Fails with 'Left' in the following cases:
* The term is not a valid application.
* The reduction is not a trivial one, i.e. the argument term is not equivalent
to the bound variable.
-}
primBETA :: HOLTerm -> Either String HOLThm
primBETA t@(CombIn (AbsIn bv bod) arg)
| arg == bv =
Right . ThmIn [] $ safeMkEq t bod
| otherwise = Left "primBETA_PRIM: not a trivial beta reduction"
primBETA _ = Left "primBETA_PRIM: not a valid application"
-- Deduction Rules
{-|@
t
-----------
t |- t
@
Fails with 'Left' if the term is not a proposition.
-}
primASSUME :: HOLTerm -> Either String HOLThm
primASSUME tm
| typeOf tm == tyBool = Right $ ThmIn [tm] tm
| otherwise = Left "primASSUME"
{-|@
A1 |- t1 = t2 A2 |- t1
----------------------------
A1 U A2 |- t2
@
Fails with 'Left' in the following cases:
* The conclusion of the first theorem is not an equation.
* The conclusion term of the second theorem and the left hand side of the
equation are not alpha-equivalent.
-}
primEQ_MP :: HOLThm -> HOLThm -> Either String HOLThm
primEQ_MP (ThmIn as1 (l := r)) (ThmIn as2 c)
| l `aConv` c =
let as' = termUnion as1 as2 in
Right $ ThmIn as' r
| otherwise = Left "primEQ_MP: terms do not agree"
primEQ_MP _ _ = Left "primEQ_MP: term is not an equation"
{-|@
A |- p B |- q
--------------------------------
(A - q) U (B - p) |- p \<=\> q
@
Never fails.
-}
primDEDUCT_ANTISYM :: HOLThm -> HOLThm -> HOLThm
primDEDUCT_ANTISYM (ThmIn as p) (ThmIn bs q) =
let as' = termRemove q as `termUnion` termRemove p bs in
ThmIn as' $ safeMkEq p q
-- Instantiation Rules
{-|@
[(ty1, tv1), ..., (tyn, tvn)] A |- t
----------------------------------------
A[ty1, ..., tyn/tv1, ..., tvn]
|- t[ty1, ..., tyn/tv1, ..., tvn]
@
Never fails.
-}
primINST_TYPE :: Inst a b => [(a, b)] -> HOLThm -> HOLThm
primINST_TYPE tyenv (ThmIn as t) =
let instFun = inst tyenv in
ThmIn (termImage instFun as) $ instFun t
-- | A version of 'primINST_TYPE' that instantiates a theorem via 'instFull'.
primINST_TYPE_FULL :: SubstTrip -> HOLThm -> HOLThm
primINST_TYPE_FULL tyenv (ThmIn as t) =
let instFun = instFull tyenv in
ThmIn (termImage instFun as) $ instFun t
{-|@
[(t1, x1), ..., (tn, xn)] A |- t
------------------------------------
A[t1, ..., tn/x1, ..., xn]
|- t[t1, ..., tn/x1, ..., xn]
@
Fails with 'Nothing' in the case where a bad substitution list is provided.
-}
primINST :: HOLTermEnv -> HOLThm -> Maybe HOLThm
primINST env (ThmIn as t) =
let instFun = varSubst env in
do as' <- termImageM instFun as
liftM (ThmIn as') $ instFun t
{-
HOL2P Primitive Inference Rules
-}
-- Type Congruence rules
{-|@
A |- t1 = t2
-------------------------------
A |- (\\\\ x . t1) = (\\\\ x . t2)
@
Fails with 'Left' in the following cases:
* The type to bind is not a small type variable.
* The conclusion of the theorem is not an equation.
* The type to bind is free in the assumption list of the theorem.
* The type variable to bind is free in the conclusion of the theorem.
-}
primTYABS :: HOLType -> HOLThm -> Either String HOLThm
primTYABS tv@(TyVarIn True _) (ThmIn as (l := r))
| tv `notElem` typeVarsInTerms as =
let fvs = frees l `union` frees r in
if any (\ x -> tv `elem` tyVars (typeOf x)) fvs
then Left "primTYABS: type variable is free in conclusion"
else Right . ThmIn as $ safeMkEq (TyAbsIn tv l) (TyAbsIn tv r)
| otherwise =
Left "primTYABS: type variable is free in assumptions"
primTYABS (TyVarIn True _) _ =
Left "primTYABS: conclusion not an equation"
primTYABS _ _ =
Left "primTYABS: first argument not a small type variable"
{-|@
A |- t1 = t2
-------------------------------
A |- t1 [: ty1] = t2 [: ty2]
@
Fails with 'Left' in the following cases:
* The conclusion of the theorem is not an equation of terms of universal type.
* The type arguments are not alpha-equivalent.
* One, or both, of the type arguments is not small.
-}
primTYAPP2 :: HOLType -> HOLType -> HOLThm -> Either String HOLThm
primTYAPP2 ty1 ty2 (ThmIn as (l := r))
| ty1 `tyAConv` ty2 =
case typeOf l of
UTypeIn{}
| not $ isSmall ty1 ->
Left "primTYAPP2: ty1 not small"
| not $ isSmall ty2 ->
Left "primTYAPP2: ty2 not small"
| otherwise ->
Right . ThmIn as $ safeMkEq (TyCombIn l ty1) (TyCombIn r ty2)
_ -> Left "primTYAPP2: terms not of universal type"
| otherwise =
Left "primTYAPP2: type arguments not alpha-convertible"
primTYAPP2 _ _ _ = Left "primTYAPP2: conclusion not an equation"
{-|@
A |- t1 = t2
----------------------------
A |- t1 [: ty] = t2 [: ty]
@
Fails with 'Nothing' if the conclusion of the theorem is not an equation.
Note that 'primTYAPP' is equivalent to 'primTYAPP2' when the same type is
applied to both sides, i.e.
@ primTYAPP ty === primTYAPP2 ty ty @
-}
primTYAPP :: HOLType -> HOLThm -> Either String HOLThm
primTYAPP ty thm@(ThmIn _ (_ := _)) =
primTYAPP2 ty ty thm
primTYAPP _ _ = Left "primTYAPP"
-- Type Beta Reduction
{-|@
(\\\\ ty . t[ty]) [: ty]
---------------------------------
|- (\\\\ ty . t[ty]) [: ty] = t
@
Fails with 'Left' in the following cases:
* The term is not a valid type application.
* The reduction is not a trivial one, i.e. the argument type is not equivalent
to the bound type variable.
-}
primTYBETA :: HOLTerm -> Either String HOLThm
primTYBETA tm@(TyCombIn (TyAbsIn tv bod) argt)
| argt == tv =
Right . ThmIn [] $ safeMkEq tm bod
| otherwise = Left "primTYBETA: not a trivial type beta reduction"
primTYBETA _ = Left "primTYBETA: not a valid type application"
{-
Stateless HOL Theory Extension Primitives
Note that the following primitives are in HaskHOL.Core.State as per
Stateless HOL:
axioms, newAxiom, newBasicDefinition, newBasicTypeDefinition
-}
{-|
Creates a new axiom theorem.
Note that, as discussed in the documentation for 'HOLThm', the introduction of
axioms is not tracked until the stateful layer of the system is introduced so
be careful using this function.
-}
axiomThm :: HOLTerm -> HOLThm
axiomThm = ThmIn []
{-|@
c = t
-----------
|- c = t
@
Creates a new defined constant given a term that equates a variable of the
desired constant name and type to its desired definition. The return value
is a pair of the new constant and its definitional theorem.
Note that internally the constant is tagged with its definitional term via the
@Defined@ 'ConstTag'.
Fails with 'Left' in the following cases:
* The provided term is not an equation.
* The provided term is not closed.
* There are free type variables present in the definition that are not also in
the desired type of the constant.
-}
newDefinedConst :: HOLTerm -> Either String (HOLTerm, HOLThm)
newDefinedConst ((VarIn cname ty) := r)
| not $ freesIn [] r =
Left "newDefinedConst: not closed"
| not $ typeVarsInTerm r `subset` tyVars ty =
Left "newDefinedConst: type vars not refelcted in const"
| otherwise =
let c = ConstIn cname ty (DefinedIn $ hash r)
dth = ThmIn [] $ safeMkEq c r in
Right (c, dth)
newDefinedConst _ = Left "newDefinedConst: not an equation"
{-|@
|- p x:rep
-----------------------------------------------------------------
(|- mk:rep->ty (dest:ty->rep a) = a, |- P r \<=\> dest(mk r) = r)
@
Creates a new defined type constant that is defined as an inhabited subset
of an existing type constant. The return value is a pentuple that
collectively provides a bijection between the new type and the old type.
The following four items are taken as input:
* The name of the new type constant - @ty@ in the above sequent.
* The name of the new term constant that will be used to make an instance of
the new type - @mk@ in the above sequent.
* The name of the new term constant that will be used to destruct an instance
of the new type - @dest@ in the above sequent.
* A theorem proving that the desired subset is non-empty. The conclusion of
this theorem must take the form @p x@ where @p@ is the predicate that
defines the subset and @x@ is a witness to inhabitation.
The following items are returned as part of the resultant pentuple:
* The new defined type operator. These type operators carry their name,
arity, and definitional theorem. The arity, in this case, is inferred from
the number of free type variables found in the predicate of the definitional
theorem.
* The new term constants, @mk@ and @dest@, as described above. Note that
constants constructed in this manner are tagged with special instances of
'ConstTag', @MkAbstract@ and @DestAbstract@ accordingly, that carry the
name, arity, and definitional theorem of their related type constant.
* The two theorems proving the bijection, as shown in the sequent above.
-}
newDefinedTypeOp :: Text -> Text -> Text -> HOLThm ->
Either String (TypeOp, HOLTerm, HOLTerm, HOLThm, HOLThm)
newDefinedTypeOp tyname absname repname (ThmIn [] c@(CombIn p x))
| containsUType $ typeOf x =
Left "newDefinedTypeOp: must not contain universal types"
| not $ freesIn [] p =
Left "newDefinedTypeOp: predicate is not closed"
| otherwise =
let tys = sort (<=) $ typeVarsInTerm p
arity = length tys
hsh = hash c
atyop = TyDefinedIn tyname arity hsh
rty = typeOf x
aty = TyAppIn atyop tys
atm = VarIn "a" aty
rtm = VarIn "r" rty
absCon = ConstIn absname (TyAppIn tyOpFun [rty, aty]) $
MkAbstractIn tyname arity hsh
repCon = ConstIn repname (TyAppIn tyOpFun [aty, rty]) $
DestAbstractIn tyname arity hsh
c1 = CombIn absCon $ CombIn repCon atm
c2 = CombIn p rtm
c3 = CombIn repCon $ CombIn absCon rtm in
Right (atyop, absCon, repCon,
ThmIn [] $ safeMkEq c1 atm,
ThmIn [] . safeMkEq c2 $ safeMkEq c3 rtm)
newDefinedTypeOp _ _ _ _ = Left "newDefinedTypeOp: poorly formed predicate"
-- Documentation copied from HaskHOL.Core.Prims
{-$ViewPatterns
The primitive data types of HaskHOL are implemented using pattern synonyms in
order to simulate private data types:
* Internal constructors are hidden to prevent manual construction of terms.
* Unideriectional pattern synonyms ('Thm', etc.) are exposed to enable
pattern matching.
-}