src/Sequents/Modal0.ML
 author paulson Wed, 09 Oct 1996 13:32:33 +0200 changeset 2073 fb0655539d05 child 17481 75166ebb619b permissions -rw-r--r--
New unified treatment of sequent calculi by Sara Kalvala combines the old LK and Modal with the new ILL (Int. Linear Logic)
```
(*  Title:      Modal/modal0
ID:         \$Id\$
Author:     Martin Coen
Copyright   1991  University of Cambridge
*)

structure Modal0_rls =
struct

val rewrite_rls = [Modal0.strimp_def,Modal0.streqv_def];

local
val iffR = prove_goal thy
"[| \$H,P |- \$E,Q,\$F;  \$H,Q |- \$E,P,\$F |] ==> \$H |- \$E, P <-> Q, \$F"
(fn prems=>
[ (rewtac iff_def),
(REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);

val iffL = prove_goal thy
"[| \$H,\$G |- \$E,P,Q;  \$H,Q,P,\$G |- \$E |] ==> \$H, P <-> Q, \$G |- \$E"
(fn prems=>
[ rewtac iff_def,
(REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ])
in
val safe_rls   = [basic,conjL,conjR,disjL,disjR,impL,impR,notL,notR,iffL,iffR];
val unsafe_rls = [allR,exL];
val bound_rls  = [allL,exR];
end

end;
```