This module defines the type of theorems and the primitive inference
rules.

> module Theorem(Theorem, hyp, concl, just, assume, disch, mp,
>                conj_intro, conj_elim,
>                disj_intro, disj_elim,
>                neg_intro, neg_elim,
>                module Term, module Monad) where
> import Term
> import List
> import Monad

> newtype Theorem = T {thm :: ([Term],Term)}
>   deriving Eq

A theorem is an ordered pair of:
- a list of hypotheses/assumptions, used as a set
- the conclusion/consequence

Discussion: We are hiding the internal representation of Theorem.  As
a result, any caller to this module cannot create their own theorems
randomly, but must use our primitive inference rules to obtain new
theorems.  (Of course, they can write their inference rules, but those
have to call ours.)  This is how we prevent faulty logic.  In other
words, we reduce proof verification to type checking --- you aren't
proving anything until you obtain a Theorem.  This idea comes from HOL.


Pretty-printing a theorem (in the Show framework of Haskell.)  The
assumption list and the conclusion are separated by the turnstile
symbol "|-".

> instance Show Theorem where
>   showsPrec _ (T (hs,c)) = showsPrec 0 hs . showString " |- " . showsPrec 0 c

Auxilliary functions to extract the hypotheses and the conclusion of a
theorem.

> hyp = fst . thm
> concl = snd . thm

Now our primitive inference rules.  They are basically from natural
deduction.

Convention: for inferences that may fail, the result type is Maybe t,
where t is the result of success.  We then make use of the monadic
status of Maybe to simplify error handling in sequences of inference
rules.  There are some examples in module Inference of using these
inference rules to build more interested inference rules; they also
illustrate how the Maybe monad helps us handle (and ignore) errors.

We could use the Either type instead of the Maybe type.  Advantage:
it can store the reason of failure when an inference rule fails.

First, a helper function that extracts the successful value of a
Maybe value.  (It aborts if the Maybe value is a failure.)

> just :: Maybe a -> a
> just = maybe (error "inference error") id

Assumption introduction: for any term t, we have
  t |- t

> assume :: Term -> Theorem
> assume t = T ([t],t)

Discharge, aka ==> introduction: from
  A,t |- u
deduce
  A |- t ==> u

> disch :: Term -> Theorem -> Theorem
> disch term thm@(T(hs,c)) = T(delete term hs, Imp term c)

Modus ponens, aka ==> elimination: from
  A1 |- t ==> u
  A2 |- t
deduce
  A1 u A2 |- u

> mp :: Theorem -> Theorem -> Maybe Theorem
> mp (T(h1,c1)) (T(h2,c2))
>   | isImp c1 && sub1 c1 == c2 = Just (T(h1 `union` h2, sub2 c1))
>   | otherwise                 = Nothing

&& introduction: from both
  A1 |- t   A2 |- u
deduce
  A1 u A2 |- t && u

> conj_intro :: (Theorem,Theorem) -> Theorem
> conj_intro (T(h1,c1), T(h2,c2)) = T(h1 `union` h2, Conj c1 c2)

&& elimination: from
  A |- t && u
deduce both
  A |- t  A |- u

> conj_elim :: Theorem -> Maybe (Theorem,Theorem)
> conj_elim (T(h, Conj c1 c2)) = Just (T(h,c1), T(h,c2))
> conj_elim t                  = Nothing

|| introduction: given a term, from
  A |- t
deduce both
  A |- t || term  A |- term || t

> disj_intro :: Term -> Theorem -> (Theorem,Theorem)
> disj_intro term (T(h,c)) = (T(h, Disj c term),T(h, Disj term c))

|| elimination, aka case analysis: from
  A |- x || y
and both
  A1,x |- z  A2,y |- z
deduce
  A u A1 u A2 |- z
the terms x and y are removed from A u A1 u A2.

> disj_elim :: Theorem -> (Theorem,Theorem) -> Maybe Theorem
> disj_elim (T(a, Disj t1 t2)) (T(a1,c1), T(a2,c2))
>   | c1 == c2 &&
>     t1 `elem` a1 &&
>     t2 `elem` a2 = Just (T(a `union` (delete t1 a1) `union` (delete t2 a2),
>                              c1))
>   | otherwise    = Nothing
> disj_elim _ _    = Nothing

~ introduction, aka reductio ad absurdum: given term x, from
  A,x |- y && ~y
deduce
  A |- ~x

> neg_intro :: Term -> Theorem -> Maybe Theorem
> neg_intro x (T(as,Conj y1 (Neg y2)))
>   | y1 == y2 && x `elem` as = Just (T(delete x as, Neg x))
>   | otherwise               = Nothing
> neg_intro _ _               = Nothing

~ elimination, which is reductio ad absurdum dualized:
given term ~x, from
  A,~x |- y && ~y
deduce
  A |- x
We need both versions of reductio ad absurdum because no other
inference rules let us deduce a|-~~a or ~~a|-a.

> neg_elim :: Term -> Theorem -> Maybe Theorem
> neg_elim nx@(Neg x) (T(as,Conj y1 (Neg y2)))
>   | y1 == y2 && nx `elem` as = Just (T(delete nx as, x))
>   | otherwise                = Nothing
> neg_elim _ _                 = Nothing