> module InfLib where
> import Theorem
> import List

Derived inference rules to support the tactics.


Undischarge: the reverse of discharge.  From
  A |- a ==> b
deduce
  A,a |- b

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

Add an assumption.  Given b, from
  A |- t
deduce
  A,b |- t
In fact it is like
  (A-{b}),b |- t
with the assumption list in that order.

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

Add many assumptions at once.  Given the list B of assumptions to
add, from
  A |- t
deduce
  A u B |- t
In fact, it is
  (A-B) u B |- t
with the assumption list in that order.

> add_assum_list as thm = foldl (flip add_assum) thm as