src/Sequents/Modal0.thy
changeset 17481 75166ebb619b
parent 14765 bafb24c150c1
child 21426 87ac12bed1ab
equal deleted inserted replaced
17480:fd19f77dcf60 17481:75166ebb619b
     1 (*  Title:      Sequents/Modal0
     1 (*  Title:      Sequents/Modal0.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Martin Coen
     3     Author:     Martin Coen
     4     Copyright   1991  University of Cambridge
     4     Copyright   1991  University of Cambridge
     5 *)
     5 *)
     6 
     6 
     7 Modal0 = LK0 +
     7 theory Modal0
       
     8 imports LK0
       
     9 uses "modal.ML"
       
    10 begin
     8 
    11 
     9 consts
    12 consts
    10   box           :: "o=>o"       ("[]_" [50] 50)
    13   box           :: "o=>o"       ("[]_" [50] 50)
    11   dia           :: "o=>o"       ("<>_" [50] 50)
    14   dia           :: "o=>o"       ("<>_" [50] 50)
    12   "--<",">-<"   :: "[o,o]=>o"   (infixr 25)
    15   "--<"         :: "[o,o]=>o"   (infixr 25)
    13   Lstar,Rstar   :: "two_seqi"
    16   ">-<"         :: "[o,o]=>o"   (infixr 25)
       
    17   Lstar         :: "two_seqi"
       
    18   Rstar         :: "two_seqi"
    14 
    19 
    15 syntax
    20 syntax
    16   "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
    21   "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
    17   "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
    22   "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
    18 
    23 
    19 rules
    24 ML {*
    20   (* Definitions *)
       
    21 
       
    22   strimp_def    "P --< Q == [](P --> Q)"
       
    23   streqv_def    "P >-< Q == (P --< Q) & (Q --< P)"
       
    24 end
       
    25 
       
    26 ML
       
    27 
       
    28 local
       
    29 
       
    30   val Lstar = "Lstar";
    25   val Lstar = "Lstar";
    31   val Rstar = "Rstar";
    26   val Rstar = "Rstar";
    32   val SLstar = "@Lstar";
    27   val SLstar = "@Lstar";
    33   val SRstar = "@Rstar";
    28   val SRstar = "@Rstar";
    34 
    29 
    35   fun star_tr c [s1,s2] =
    30   fun star_tr c [s1,s2] = Const(c,dummyT)$ seq_tr s1$ seq_tr s2;
    36       Const(c,dummyT)$Sequents.seq_tr s1$Sequents.seq_tr s2;
    31   fun star_tr' c [s1,s2] = Const(c,dummyT) $ seq_tr' s1 $ seq_tr' s2;
    37   fun star_tr' c [s1,s2] = 
    32 *}
    38       Const(c,dummyT) $ Sequents.seq_tr' s1 $ Sequents.seq_tr' s2;
    33 
    39 in
    34 parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
    40 val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
    35 print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
    41 val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
    36 
    42 end;
    37 defs
       
    38   strimp_def:    "P --< Q == [](P --> Q)"
       
    39   streqv_def:    "P >-< Q == (P --< Q) & (Q --< P)"
       
    40 
       
    41 ML {* use_legacy_bindings (the_context ()) *}
       
    42 
       
    43 end