src/Sequents/Modal0.thy
changeset 35113 1a0c129bb2e0
parent 21426 87ac12bed1ab
child 48891 c0eafbd55de3
equal deleted inserted replaced
35112:ff6f60e6ab85 35113:1a0c129bb2e0
     1 (*  Title:      Sequents/Modal0.thy
     1 (*  Title:      Sequents/Modal0.thy
     2     ID:         $Id$
       
     3     Author:     Martin Coen
     2     Author:     Martin Coen
     4     Copyright   1991  University of Cambridge
     3     Copyright   1991  University of Cambridge
     5 *)
     4 *)
     6 
     5 
     7 theory Modal0
     6 theory Modal0
    16   streqv        :: "[o,o]=>o"   (infixr ">-<" 25)
    15   streqv        :: "[o,o]=>o"   (infixr ">-<" 25)
    17   Lstar         :: "two_seqi"
    16   Lstar         :: "two_seqi"
    18   Rstar         :: "two_seqi"
    17   Rstar         :: "two_seqi"
    19 
    18 
    20 syntax
    19 syntax
    21   "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
    20   "_Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
    22   "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
    21   "_Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
    23 
    22 
    24 ML {*
    23 ML {*
    25   val Lstar = "Lstar";
    24   fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2;
    26   val Rstar = "Rstar";
    25   fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
    27   val SLstar = "@Lstar";
       
    28   val SRstar = "@Rstar";
       
    29 
       
    30   fun star_tr c [s1,s2] = Const(c,dummyT)$ seq_tr s1$ seq_tr s2;
       
    31   fun star_tr' c [s1,s2] = Const(c,dummyT) $ seq_tr' s1 $ seq_tr' s2;
       
    32 *}
    26 *}
    33 
    27 
    34 parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
    28 parse_translation {*
    35 print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
    29  [(@{syntax_const "_Lstar"}, star_tr @{const_syntax Lstar}),
       
    30   (@{syntax_const "_Rstar"}, star_tr @{const_syntax Rstar})]
       
    31 *}
       
    32 
       
    33 print_translation {*
       
    34  [(@{const_syntax Lstar}, star_tr' @{syntax_const "_Lstar"}),
       
    35   (@{const_syntax Rstar}, star_tr' @{syntax_const "_Rstar"})]
       
    36 *}
    36 
    37 
    37 defs
    38 defs
    38   strimp_def:    "P --< Q == [](P --> Q)"
    39   strimp_def:    "P --< Q == [](P --> Q)"
    39   streqv_def:    "P >-< Q == (P --< Q) & (Q --< P)"
    40   streqv_def:    "P >-< Q == (P --< Q) & (Q --< P)"
    40 
    41