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