> 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