src/Sequents/Modal0.thy
author wenzelm
Thu Dec 07 00:42:04 2006 +0100 (2006-12-07)
changeset 21687 f689f729afab
parent 21426 87ac12bed1ab
child 35113 1a0c129bb2e0
permissions -rw-r--r--
reorganized structure Goal vs. Tactic;
     1 (*  Title:      Sequents/Modal0.thy
     2     ID:         $Id$
     3     Author:     Martin Coen
     4     Copyright   1991  University of Cambridge
     5 *)
     6 
     7 theory Modal0
     8 imports LK0
     9 uses "modal.ML"
    10 begin
    11 
    12 consts
    13   box           :: "o=>o"       ("[]_" [50] 50)
    14   dia           :: "o=>o"       ("<>_" [50] 50)
    15   strimp        :: "[o,o]=>o"   (infixr "--<" 25)
    16   streqv        :: "[o,o]=>o"   (infixr ">-<" 25)
    17   Lstar         :: "two_seqi"
    18   Rstar         :: "two_seqi"
    19 
    20 syntax
    21   "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
    22   "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
    23 
    24 ML {*
    25   val Lstar = "Lstar";
    26   val Rstar = "Rstar";
    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 *}
    33 
    34 parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
    35 print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
    36 
    37 defs
    38   strimp_def:    "P --< Q == [](P --> Q)"
    39   streqv_def:    "P >-< Q == (P --< Q) & (Q --< P)"
    40 
    41 
    42 lemmas rewrite_rls = strimp_def streqv_def
    43 
    44 lemma iffR:
    45     "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
    46   apply (unfold iff_def)
    47   apply (assumption | rule conjR impR)+
    48   done
    49 
    50 lemma iffL:
    51     "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
    52   apply (unfold iff_def)
    53   apply (assumption | rule conjL impL basic)+
    54   done
    55 
    56 lemmas safe_rls = basic conjL conjR disjL disjR impL impR notL notR iffL iffR
    57   and unsafe_rls = allR exL
    58   and bound_rls = allL exR
    59 
    60 end