src/Sequents/Modal0.thy
author wenzelm
Mon Mar 19 21:10:33 2012 +0100 (2012-03-19)
changeset 47022 8eac39af4ec0
parent 35113 1a0c129bb2e0
child 48891 c0eafbd55de3
permissions -rw-r--r--
moved some legacy stuff;
     1 (*  Title:      Sequents/Modal0.thy
     2     Author:     Martin Coen
     3     Copyright   1991  University of Cambridge
     4 *)
     5 
     6 theory Modal0
     7 imports LK0
     8 uses "modal.ML"
     9 begin
    10 
    11 consts
    12   box           :: "o=>o"       ("[]_" [50] 50)
    13   dia           :: "o=>o"       ("<>_" [50] 50)
    14   strimp        :: "[o,o]=>o"   (infixr "--<" 25)
    15   streqv        :: "[o,o]=>o"   (infixr ">-<" 25)
    16   Lstar         :: "two_seqi"
    17   Rstar         :: "two_seqi"
    18 
    19 syntax
    20   "_Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
    21   "_Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
    22 
    23 ML {*
    24   fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2;
    25   fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
    26 *}
    27 
    28 parse_translation {*
    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 *}
    37 
    38 defs
    39   strimp_def:    "P --< Q == [](P --> Q)"
    40   streqv_def:    "P >-< Q == (P --< Q) & (Q --< P)"
    41 
    42 
    43 lemmas rewrite_rls = strimp_def streqv_def
    44 
    45 lemma iffR:
    46     "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
    47   apply (unfold iff_def)
    48   apply (assumption | rule conjR impR)+
    49   done
    50 
    51 lemma iffL:
    52     "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
    53   apply (unfold iff_def)
    54   apply (assumption | rule conjL impL basic)+
    55   done
    56 
    57 lemmas safe_rls = basic conjL conjR disjL disjR impL impR notL notR iffL iffR
    58   and unsafe_rls = allR exL
    59   and bound_rls = allL exR
    60 
    61 end