src/Modal/modal0.thy
changeset 0 a5a9c433f639
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Modal/modal0.thy	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,39 @@
     1.4 +(*  Title: 	91/Modal/modal0
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Martin Coen
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +*)
     1.9 +
    1.10 +Modal0 = LK +
    1.11 +
    1.12 +consts
    1.13 +  box		:: "o=>o"	("[]_" [50] 50)
    1.14 +  dia		:: "o=>o"	("<>_" [50] 50)
    1.15 +  "--<",">-<"	:: "[o,o]=>o"	(infixr 25)
    1.16 +  "@Lstar"	:: "[sequence,sequence]=>prop"	("(_)|L>(_)" [6,6] 5)
    1.17 +  "@Rstar"	:: "[sequence,sequence]=>prop"	("(_)|R>(_)" [6,6] 5)
    1.18 +  Lstar,Rstar	:: "[sobj=>sobj,sobj=>sobj]=>prop"
    1.19 +
    1.20 +rules
    1.21 +  (* Definitions *)
    1.22 +
    1.23 +  strimp_def	"P --< Q == [](P --> Q)"
    1.24 +  streqv_def	"P >-< Q == (P --< Q) & (Q --< P)"
    1.25 +end
    1.26 +
    1.27 +ML
    1.28 +
    1.29 +local
    1.30 +
    1.31 +  val Lstar = "Lstar";
    1.32 +  val Rstar = "Rstar";
    1.33 +  val SLstar = "@Lstar";
    1.34 +  val SRstar = "@Rstar";
    1.35 +
    1.36 +  fun star_tr c [s1,s2] = Const(c,dummyT)$LK.seq_tr1 s1$LK.seq_tr1 s2;
    1.37 +  fun star_tr' c [Abs(_,_,s1),Abs(_,_,s2)] = 
    1.38 +         Const(c,dummyT) $ LK.seq_tr1' s1 $ LK.seq_tr1' s2;
    1.39 +in
    1.40 +val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
    1.41 +val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
    1.42 +end;