src/Sequents/S43.thy
changeset 17481 75166ebb619b
parent 14765 bafb24c150c1
child 21426 87ac12bed1ab
     1.1 --- a/src/Sequents/S43.thy	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/S43.thy	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Modal/S43
     1.5 +(*  Title:      Modal/S43.thy
     1.6      ID:         $Id$
     1.7      Author:     Martin Coen
     1.8      Copyright   1991  University of Cambridge
     1.9 @@ -6,7 +6,9 @@
    1.10  This implements Rajeev Gore's sequent calculus for S43.
    1.11  *)
    1.12  
    1.13 -S43 = Modal0 +
    1.14 +theory S43
    1.15 +imports Modal0
    1.16 +begin
    1.17  
    1.18  consts
    1.19    S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
    1.20 @@ -15,17 +17,34 @@
    1.21    "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
    1.22                           ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
    1.23  
    1.24 -rules
    1.25 +ML {*
    1.26 +  val S43pi  = "S43pi";
    1.27 +  val SS43pi = "@S43pi";
    1.28 +
    1.29 +  val tr  = seq_tr;
    1.30 +  val tr' = seq_tr';
    1.31 +
    1.32 +  fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
    1.33 +        Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
    1.34 +  fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
    1.35 +        Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
    1.36 +
    1.37 +*}
    1.38 +
    1.39 +parse_translation {* [(SS43pi,s43pi_tr)] *}
    1.40 +print_translation {* [(S43pi,s43pi_tr')] *}
    1.41 +
    1.42 +axioms
    1.43  (* Definition of the star operation using a set of Horn clauses  *)
    1.44  (* For system S43: gamma * == {[]P | []P : gamma}                *)
    1.45  (*                 delta * == {<>P | <>P : delta}                *)
    1.46  
    1.47 -  lstar0         "|L>"
    1.48 -  lstar1         "$G |L> $H ==> []P, $G |L> []P, $H"
    1.49 -  lstar2         "$G |L> $H ==>   P, $G |L>      $H"
    1.50 -  rstar0         "|R>"
    1.51 -  rstar1         "$G |R> $H ==> <>P, $G |R> <>P, $H"
    1.52 -  rstar2         "$G |R> $H ==>   P, $G |R>      $H"
    1.53 +  lstar0:         "|L>"
    1.54 +  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H"
    1.55 +  lstar2:         "$G |L> $H ==>   P, $G |L>      $H"
    1.56 +  rstar0:         "|R>"
    1.57 +  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H"
    1.58 +  rstar2:         "$G |R> $H ==>   P, $G |R>      $H"
    1.59  
    1.60  (* Set of Horn clauses to generate the antecedents for the S43 pi rule       *)
    1.61  (* ie                                                                        *)
    1.62 @@ -37,43 +56,27 @@
    1.63  (*    and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj    *)
    1.64  (*    and 1<=i<=k and k<j<=k+m                                               *)
    1.65  
    1.66 -  S43pi0         "S43pi $L;; $R;; $Lbox; $Rdia"
    1.67 -  S43pi1
    1.68 -   "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==> 
    1.69 +  S43pi0:         "S43pi $L;; $R;; $Lbox; $Rdia"
    1.70 +  S43pi1:
    1.71 +   "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==>
    1.72         S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia"
    1.73 -  S43pi2
    1.74 -   "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==> 
    1.75 +  S43pi2:
    1.76 +   "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==>
    1.77         S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia"
    1.78  
    1.79  (* Rules for [] and <> for S43 *)
    1.80  
    1.81 -  boxL           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
    1.82 -  diaR           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
    1.83 -  pi1
    1.84 -   "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;  
    1.85 -      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 
    1.86 +  boxL:           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
    1.87 +  diaR:           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
    1.88 +  pi1:
    1.89 +   "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;
    1.90 +      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
    1.91     $L1, <>P, $L2 |- $R"
    1.92 -  pi2
    1.93 -   "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;  
    1.94 -      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> 
    1.95 +  pi2:
    1.96 +   "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;
    1.97 +      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
    1.98     $L |- $R1, []P, $R2"
    1.99 -end
   1.100 -
   1.101 -ML
   1.102  
   1.103 -local
   1.104 -
   1.105 -  val S43pi  = "S43pi";
   1.106 -  val SS43pi = "@S43pi";
   1.107 -
   1.108 -  val tr  = Sequents.seq_tr;
   1.109 -  val tr' = Sequents.seq_tr';
   1.110 +ML {* use_legacy_bindings (the_context ()) *}
   1.111  
   1.112 -  fun s43pi_tr[s1,s2,s3,s4,s5,s6]=
   1.113 -        Const(S43pi,dummyT)$tr s1$tr s2$tr s3$tr s4$tr s5$tr s6;
   1.114 -  fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =
   1.115 -        Const(SS43pi,dummyT)$tr' s1$tr' s2$tr' s3$tr' s4$tr' s5$tr' s6;
   1.116 -in
   1.117 -val parse_translation = [(SS43pi,s43pi_tr)];
   1.118 -val print_translation = [(S43pi,s43pi_tr')]
   1.119  end