src/Sequents/Modal0.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 2073 fb0655539d05
child 17481 75166ebb619b
permissions -rw-r--r--
tidying
paulson@2073
     1
(*  Title:      Modal/modal0
paulson@2073
     2
    ID:         $Id$
paulson@2073
     3
    Author:     Martin Coen
paulson@2073
     4
    Copyright   1991  University of Cambridge
paulson@2073
     5
*)
paulson@2073
     6
paulson@2073
     7
structure Modal0_rls = 
paulson@2073
     8
struct
paulson@2073
     9
paulson@2073
    10
val rewrite_rls = [Modal0.strimp_def,Modal0.streqv_def];
paulson@2073
    11
paulson@2073
    12
local
paulson@2073
    13
  val iffR = prove_goal thy 
paulson@2073
    14
      "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
paulson@2073
    15
   (fn prems=>
paulson@2073
    16
    [ (rewtac iff_def),
paulson@2073
    17
      (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
paulson@2073
    18
paulson@2073
    19
  val iffL = prove_goal thy 
paulson@2073
    20
     "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
paulson@2073
    21
   (fn prems=>
paulson@2073
    22
    [ rewtac iff_def,
paulson@2073
    23
      (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ])
paulson@2073
    24
in
paulson@2073
    25
val safe_rls   = [basic,conjL,conjR,disjL,disjR,impL,impR,notL,notR,iffL,iffR];
paulson@2073
    26
val unsafe_rls = [allR,exL];
paulson@2073
    27
val bound_rls  = [allL,exR];
paulson@2073
    28
end
paulson@2073
    29
paulson@2073
    30
end;