HaskHOL.Core.Kernel

This module exports the logical kernel of HaskHOL. It consists of:

• The view pattern required to pattern match on terms outside of the kernel.
• 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.

A View of HOL Types, Terms, and Theorems

A Quick Note on View Patterns

The primitive data types of HaskHOL are implemented using view patterns in order to simulate private data types:

• Internal constructors are hidden to prevent manual construction of terms.
• View constructors (those of HOLTypeView, HOLTermView, and HOLThmView) are exposed to enable pattern matching.
• View patterns, as defined by instances of the view function from the Viewable class, provide a conversion between the two sets of constructors.

view :: Viewable a b => a -> b

The view pattern function for HaskHOL's primitive data types:

• For types - Converts from HOLType to HOLTypeView.
• For terms - Converts from HOLTerm to HOLTermView.
• For theorems - Converts from HOLThm to HOLThmView.

Destructors and Accessors for Theorems

data HOLThm

The HOLThm data type defines HOL Theorems in HaskHOL. A theorem is defined simply as a list of assumption terms and a conclusion term.

Note that this representation, in combination with a stateless approach, means that the introduction of axioms is not tracked in the kernel. Axioms can be tracked once the stateful layer of the prover is introduced, though. For more details see the documentation for newAxiom.

Instances

Eq HOLThm

Ord HOLThm

Typeable HOLThm

NFData HOLThm

Lift HOLThm

Protected HOLThm

ShowHOL HOLThm thry

data HOLThmView

The view pattern data type for HOL theorems.

Constructors

Thm [HOLTerm] HOLTerm

destThm :: HOLThm -> ([HOLTerm], HOLTerm)

Destructs a theorem, returning its list of assumption terms and conclusion term.

hyp :: HOLThm -> [HOLTerm]

Accessor for the hypotheses, or assumption terms, of a theorem.

concl :: HOLThm -> HOLTerm

Accessor for the conclusion term of a theorem.

HOL Light Primitive Inference Rules

primREFL :: HOLTerm -> HOLThm

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

Never fails.

primTRANS :: HOLThm -> HOLThm -> Either String HOLThm

 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.

primMK_COMB :: HOLThm -> HOLThm -> Either String HOLThm

 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.

primABS :: HOLTerm -> HOLThm -> Either String HOLThm

          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.

primBETA :: HOLTerm -> Either String HOLThm

        (\ x . t[x]) x
-------------------------------
     |- (\ x . t) x = t[x]

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.

primASSUME :: HOLTerm -> Maybe HOLThm

     t
-----------
   t |- t

Fails with Nothing if the term is not a proposition.

primEQ_MP :: HOLThm -> HOLThm -> Either String HOLThm

 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.

primDEDUCT_ANTISYM_RULE :: HOLThm -> HOLThm -> HOLThm

       A |- p       B |- q       
----------------------------------
 (A - {q}) U (B - {p}) |- p <=> q

Never fails.

primINST_TYPE :: Inst a b => [(a, b)] -> HOLThm -> HOLThm

 [(ty1, tv1), ..., (tyn, tvn)]   A |- t              
----------------------------------------
   A[ty1, ..., tyn/tv1, ..., tvn]
    |- t[ty1, ..., tyn/tv1, ..., tvn]

Never fails.

primINST_TYPE_FULL :: SubstTrip -> HOLThm -> HOLThm

A version of primINST_TYPE that instantiates a theorem via instFull.

primINST :: HOLTermEnv -> HOLThm -> HOLThm

 [(t1, x1), ..., (tn, xn)]   A |- t          
------------------------------------
   A[t1, ..., tn/x1, ..., xn]
    |- t[t1, ..., tn/x1, ..., xn]   

Never fails.

HOL2P Primitive Inference Rules

primTYABS :: HOLType -> HOLThm -> Either String HOLThm

          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.

primTYAPP2 :: HOLType -> HOLType -> HOLThm -> Either String HOLThm

          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.

primTYAPP :: HOLType -> HOLThm -> Maybe HOLThm

        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

primTYBETA :: HOLTerm -> Either String HOLThm

     (\\ 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.

Stateless HOL Primitive Theory Extensions

axiomThm :: HOLTerm -> HOLThm

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.

newDefinedConst :: HOLTerm -> Either String (HOLTerm, HOLThm)

   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.

newDefinedTypeOp :: String -> String -> String -> HOLThm -> Either String (TypeOp, HOLTerm, HOLTerm, HOLThm, HOLThm)

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

Primitive Re-Exports

module HaskHOL.Core.Kernel.Types

module HaskHOL.Core.Kernel.Terms