src/Sequents/Modal0.thy
author paulson <lp15@cam.ac.uk>
Mon Jun 11 14:34:17 2018 +0100 (14 months ago)
changeset 68424 02e5a44ffe7d
parent 62144 bdab93ccfaf8
child 69593 3dda49e08b9d
permissions -rw-r--r--
the last of the infinite product proofs
     1 (*  Title:      Sequents/Modal0.thy
     2     Author:     Martin Coen
     3     Copyright   1991  University of Cambridge
     4 *)
     5 
     6 theory Modal0
     7 imports LK0
     8 begin
     9 
    10 ML_file "modal.ML"
    11 
    12 consts
    13   box           :: "o\<Rightarrow>o"       ("[]_" [50] 50)
    14   dia           :: "o\<Rightarrow>o"       ("<>_" [50] 50)
    15   Lstar         :: "two_seqi"
    16   Rstar         :: "two_seqi"
    17 
    18 syntax
    19   "_Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
    20   "_Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
    21 
    22 ML \<open>
    23   fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2;
    24   fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
    25 \<close>
    26 
    27 parse_translation \<open>
    28  [(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})),
    29   (@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))]
    30 \<close>
    31 
    32 print_translation \<open>
    33  [(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})),
    34   (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
    35 \<close>
    36 
    37 definition strimp :: "[o,o]\<Rightarrow>o"   (infixr "--<" 25)
    38   where "P --< Q == [](P \<longrightarrow> Q)"
    39 
    40 definition streqv :: "[o,o]\<Rightarrow>o"   (infixr ">-<" 25)
    41   where "P >-< Q == (P --< Q) \<and> (Q --< P)"
    42 
    43 
    44 lemmas rewrite_rls = strimp_def streqv_def
    45 
    46 lemma iffR: "\<lbrakk>$H,P \<turnstile> $E,Q,$F;  $H,Q \<turnstile> $E,P,$F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P \<longleftrightarrow> Q, $F"
    47   apply (unfold iff_def)
    48   apply (assumption | rule conjR impR)+
    49   done
    50 
    51 lemma iffL: "\<lbrakk>$H,$G \<turnstile> $E,P,Q;  $H,Q,P,$G \<turnstile> $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G \<turnstile> $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