> module Inferences where
> import Theorem
> import List

Here are some examples of writing your own inference rules, using only
the primitive inference rules.  Some of them also illustrates how to
use the "do" syntactic sugar and the monadic nature of Maybe to make
error-handling look like exception handling (more like exception
ignoring) in conventional languages.

> disch_all t = if (hyp t == []) then t
>               else disch_all $ disch (head (hyp t)) t

> disch_all2 t = p `mplus` return t
>   where p = if null (hyp t) then mzero :: Maybe Theorem
>             else do let x = disch (head (hyp t)) t
>                     disch_all2 x

> undisch t | isImp c   = mp t (assume (sub1 c))
>           | otherwise = Nothing
>   where c = concl t

> add_assum term thm = just $ mp (disch term thm) (assume term)

> conj_elim_all :: Theorem -> [Theorem]
> conj_elim_all t = just (conj_elimS t [])
>   where conj_elimS :: Theorem -> [Theorem] -> Maybe [Theorem]
>         conj_elimS t ts = p `mplus` return (t:ts)
>           where p = do (x,y) <- conj_elim t
>                        conj_elimS x =<< conj_elimS y ts

> -- sample inference: a ==> b ==> c |- a && b ==> c
> Just thm1 = do let t1 = assume (parse "a ==> b ==> c")
>                    t3 = assume (parse "a && b")
>                (t4,t5) <- conj_elim t3
>                t6 <- mp t1 t4
>                t7 <- mp t6 t5
>                return (disch (parse "a && b") t7)

> -- another example: a && b ==> c |- a ==> b ==> c
> Just thm2 = do let t1 = assume (parse "a && b ==> c")
>                    t2 = conj_intro (assume$parse "a", assume$parse "b")
>                t3 <- mp t1 t2
>                return (disch (parse "a") (disch (parse "b") t3))