Portability | unknown |
---|---|

Stability | unstable |

Maintainer | ecaustin@ittc.ku.edu |

Safe Haskell | None |

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.

- view :: Viewable a b => a -> b
- data HOLThm
- data HOLThmView = Thm [HOLTerm] HOLTerm
- destThm :: HOLThm -> ([HOLTerm], HOLTerm)
- hyp :: HOLThm -> [HOLTerm]
- concl :: HOLThm -> HOLTerm
- primREFL :: HOLTerm -> HOLThm
- primTRANS :: HOLThm -> HOLThm -> Either String HOLThm
- primMK_COMB :: HOLThm -> HOLThm -> Either String HOLThm
- primABS :: HOLTerm -> HOLThm -> Either String HOLThm
- primBETA :: HOLTerm -> Either String HOLThm
- primASSUME :: HOLTerm -> Maybe HOLThm
- primEQ_MP :: HOLThm -> HOLThm -> Either String HOLThm
- primDEDUCT_ANTISYM_RULE :: HOLThm -> HOLThm -> HOLThm
- primINST_TYPE :: Inst a b => [(a, b)] -> HOLThm -> HOLThm
- primINST_TYPE_FULL :: SubstTrip -> HOLThm -> HOLThm
- primINST :: HOLTermEnv -> HOLThm -> HOLThm
- primTYABS :: HOLType -> HOLThm -> Either String HOLThm
- primTYAPP2 :: HOLType -> HOLType -> HOLThm -> Either String HOLThm
- primTYAPP :: HOLType -> HOLThm -> Maybe HOLThm
- primTYBETA :: HOLTerm -> Either String HOLThm
- axiomThm :: HOLTerm -> HOLThm
- newDefinedConst :: HOLTerm -> Either String (HOLTerm, HOLThm)
- newDefinedTypeOp :: String -> String -> String -> HOLThm -> Either String (TypeOp, HOLTerm, HOLTerm, HOLThm, HOLThm)
- module HaskHOL.Core.Kernel.Types
- module HaskHOL.Core.Kernel.Terms

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

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

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`

.

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

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

# HOL Light Primitive Inference Rules

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

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 HOLThmSource

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 HOLThmSource

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 HOLThmSource

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

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

Fails with `Nothing`

if the term is not a proposition.

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

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

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

Never fails.

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

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

Never fails.

primINST_TYPE_FULL :: SubstTrip -> HOLThm -> HOLThmSource

A version of `primINST_TYPE`

that instantiates a theorem via `instFull`

.

primINST :: HOLTermEnv -> HOLThm -> HOLThmSource

[(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 HOLThmSource

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 HOLThmSource

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 HOLThmSource

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 HOLThmSource

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

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

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

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