src/Modal/modal0.thy
author wenzelm
Sun, 15 Oct 2000 19:50:35 +0200
changeset 10220 2a726de6e124
parent 0 a5a9c433f639
permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	91/Modal/modal0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Martin Coen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
Modal0 = LK +
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
consts
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
  box		:: "o=>o"	("[]_" [50] 50)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
  dia		:: "o=>o"	("<>_" [50] 50)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
  "--<",">-<"	:: "[o,o]=>o"	(infixr 25)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  "@Lstar"	:: "[sequence,sequence]=>prop"	("(_)|L>(_)" [6,6] 5)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
  "@Rstar"	:: "[sequence,sequence]=>prop"	("(_)|R>(_)" [6,6] 5)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
  Lstar,Rstar	:: "[sobj=>sobj,sobj=>sobj]=>prop"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
rules
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
  (* Definitions *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
  strimp_def	"P --< Q == [](P --> Q)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
  streqv_def	"P >-< Q == (P --< Q) & (Q --< P)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
local
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
  val Lstar = "Lstar";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
  val Rstar = "Rstar";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
  val SLstar = "@Lstar";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
  val SRstar = "@Rstar";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
  fun star_tr c [s1,s2] = Const(c,dummyT)$LK.seq_tr1 s1$LK.seq_tr1 s2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
  fun star_tr' c [Abs(_,_,s1),Abs(_,_,s2)] = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
         Const(c,dummyT) $ LK.seq_tr1' s1 $ LK.seq_tr1' s2;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
val parse_translation = [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
val print_translation = [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
end;