src/Modal/modal0.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 0 a5a9c433f639
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	91/Modal/modal0
     2     ID:         $Id$
     3     Author: 	Martin Coen
     4     Copyright   1991  University of Cambridge
     5 *)
     6 
     7 Modal0 = LK +
     8 
     9 consts
    10   box		:: "o=>o"	("[]_" [50] 50)
    11   dia		:: "o=>o"	("<>_" [50] 50)
    12   "--<",">-<"	:: "[o,o]=>o"	(infixr 25)
    13   "@Lstar"	:: "[sequence,sequence]=>prop"	("(_)|L>(_)" [6,6] 5)
    14   "@Rstar"	:: "[sequence,sequence]=>prop"	("(_)|R>(_)" [6,6] 5)
    15   Lstar,Rstar	:: "[sobj=>sobj,sobj=>sobj]=>prop"
    16 
    17 rules
    18   (* Definitions *)
    19 
    20   strimp_def	"P --< Q == [](P --> Q)"
    21   streqv_def	"P >-< Q == (P --< Q) & (Q --< P)"
    22 end
    23 
    24 ML
    25 
    26 local
    27 
    28   val Lstar = "Lstar";
    29   val Rstar = "Rstar";
    30   val SLstar = "@Lstar";
    31   val SRstar = "@Rstar";
    32 
    33   fun star_tr c [s1,s2] = Const(c,dummyT)$LK.seq_tr1 s1$LK.seq_tr1 s2;
    34   fun star_tr' c [Abs(_,_,s1),Abs(_,_,s2)] = 
    35          Const(c,dummyT) $ LK.seq_tr1' s1 $ LK.seq_tr1' s2;
    36 in
    37 val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
    38 val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
    39 end;