src/Sequents/S43.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (22 months ago)
changeset 66924 b4d4027f743b
parent 61386 0a29a984a91b
child 69593 3dda49e08b9d
permissions -rw-r--r--
more permissive;
     1 (*  Title:      Sequents/S43.thy
     2     Author:     Martin Coen
     3     Copyright   1991  University of Cambridge
     4 
     5 This implements Rajeev Gore's sequent calculus for S43.
     6 *)
     7 
     8 theory S43
     9 imports Modal0
    10 begin
    11 
    12 consts
    13   S43pi :: "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq',
    14              seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
    15 syntax
    16   "_S43pi" :: "[seq, seq, seq, seq, seq, seq] \<Rightarrow> prop"
    17                          ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
    18 
    19 parse_translation \<open>
    20   let
    21     val tr  = seq_tr;
    22     fun s43pi_tr [s1, s2, s3, s4, s5, s6] =
    23       Const (@{const_syntax S43pi}, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
    24   in [(@{syntax_const "_S43pi"}, K s43pi_tr)] end
    25 \<close>
    26 
    27 print_translation \<open>
    28 let
    29   val tr' = seq_tr';
    30   fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =
    31     Const(@{syntax_const "_S43pi"}, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
    32 in [(@{const_syntax S43pi}, K s43pi_tr')] end
    33 \<close>
    34 
    35 axiomatization where
    36 (* Definition of the star operation using a set of Horn clauses  *)
    37 (* For system S43: gamma * == {[]P | []P : gamma}                *)
    38 (*                 delta * == {<>P | <>P : delta}                *)
    39 
    40   lstar0:         "|L>" and
    41   lstar1:         "$G |L> $H \<Longrightarrow> []P, $G |L> []P, $H" and
    42   lstar2:         "$G |L> $H \<Longrightarrow>   P, $G |L>      $H" and
    43   rstar0:         "|R>" and
    44   rstar1:         "$G |R> $H \<Longrightarrow> <>P, $G |R> <>P, $H" and
    45   rstar2:         "$G |R> $H \<Longrightarrow>   P, $G |R>      $H" and
    46 
    47 (* Set of Horn clauses to generate the antecedents for the S43 pi rule       *)
    48 (* ie                                                                        *)
    49 (*           S1...Sk,Sk+1...Sk+m                                             *)
    50 (*     ----------------------------------                                    *)
    51 (*     <>P1...<>Pk, $G \<turnstile> $H, []Q1...[]Qm                                    *)
    52 (*                                                                           *)
    53 (*  where Si == <>P1...<>Pi-1,<>Pi+1,..<>Pk,Pi, $G * \<turnstile> $H *, []Q1...[]Qm    *)
    54 (*    and Sj == <>P1...<>Pk, $G * \<turnstile> $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj    *)
    55 (*    and 1<=i<=k and k<j<=k+m                                               *)
    56 
    57   S43pi0:         "S43pi $L;; $R;; $Lbox; $Rdia" and
    58   S43pi1:
    59    "\<lbrakk>(S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox \<turnstile> $R,$Rdia\<rbrakk> \<Longrightarrow>
    60        S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia" and
    61   S43pi2:
    62    "\<lbrakk>(S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox \<turnstile> $R',P,$R,$Rdia\<rbrakk> \<Longrightarrow>
    63        S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia" and
    64 
    65 (* Rules for [] and <> for S43 *)
    66 
    67   boxL:           "$E, P, $F, []P \<turnstile> $G \<Longrightarrow> $E, []P, $F \<turnstile> $G" and
    68   diaR:           "$E \<turnstile> $F, P, $G, <>P \<Longrightarrow> $E \<turnstile> $F, <>P, $G" and
    69   pi1:
    70    "\<lbrakk>$L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;
    71       S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia\<rbrakk> \<Longrightarrow>
    72    $L1, <>P, $L2 \<turnstile> $R" and
    73   pi2:
    74    "\<lbrakk>$L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;
    75       S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia\<rbrakk> \<Longrightarrow>
    76    $L \<turnstile> $R1, []P, $R2"
    77 
    78 
    79 ML \<open>
    80 structure S43_Prover = Modal_ProverFun
    81 (
    82   val rewrite_rls = @{thms rewrite_rls}
    83   val safe_rls = @{thms safe_rls}
    84   val unsafe_rls = @{thms unsafe_rls} @ [@{thm pi1}, @{thm pi2}]
    85   val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}]
    86   val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
    87     @{thm rstar1}, @{thm rstar2}, @{thm S43pi0}, @{thm S43pi1}, @{thm S43pi2}]
    88 )
    89 \<close>
    90 
    91 
    92 method_setup S43_solve = \<open>
    93   Scan.succeed (fn ctxt => SIMPLE_METHOD
    94     (S43_Prover.solve_tac ctxt 2 ORELSE S43_Prover.solve_tac ctxt 3))
    95 \<close>
    96 
    97 
    98 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    99 
   100 lemma "\<turnstile> []P \<longrightarrow> P" by S43_solve
   101 lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by S43_solve   (* normality*)
   102 lemma "\<turnstile> (P--<Q) \<longrightarrow> []P \<longrightarrow> []Q" by S43_solve
   103 lemma "\<turnstile> P \<longrightarrow> <>P" by S43_solve
   104 
   105 lemma "\<turnstile>  [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
   106 lemma "\<turnstile>  <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
   107 lemma "\<turnstile>  [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P>-<Q)" by S43_solve
   108 lemma "\<turnstile>  <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S43_solve
   109 lemma "\<turnstile>        []P \<longleftrightarrow> \<not> <>(\<not> P)" by S43_solve
   110 lemma "\<turnstile>     [](\<not>P) \<longleftrightarrow> \<not> <>P" by S43_solve
   111 lemma "\<turnstile>       \<not> []P \<longleftrightarrow> <>(\<not> P)" by S43_solve
   112 lemma "\<turnstile>      [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by S43_solve
   113 lemma "\<turnstile> \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>Q" by S43_solve
   114 
   115 lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
   116 lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
   117 lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
   118 lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
   119 lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
   120 lemma "\<turnstile> <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by S43_solve
   121 lemma "\<turnstile> (P --< Q) \<and> (Q --<R ) \<longrightarrow> (P --< R)" by S43_solve
   122 lemma "\<turnstile> []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
   123 
   124 
   125 (* Theorems of system S4 from Hughes and Cresswell, p.46 *)
   126 
   127 lemma "\<turnstile> []A \<longrightarrow> A" by S43_solve             (* refexivity *)
   128 lemma "\<turnstile> []A \<longrightarrow> [][]A" by S43_solve         (* transitivity *)
   129 lemma "\<turnstile> []A \<longrightarrow> <>A" by S43_solve           (* seriality *)
   130 lemma "\<turnstile> <>[](<>A \<longrightarrow> []<>A)" by S43_solve
   131 lemma "\<turnstile> <>[](<>[]A \<longrightarrow> []A)" by S43_solve
   132 lemma "\<turnstile> []P \<longleftrightarrow> [][]P" by S43_solve
   133 lemma "\<turnstile> <>P \<longleftrightarrow> <><>P" by S43_solve
   134 lemma "\<turnstile> <>[]<>P \<longrightarrow> <>P" by S43_solve
   135 lemma "\<turnstile> []<>P \<longleftrightarrow> []<>[]<>P" by S43_solve
   136 lemma "\<turnstile> <>[]P \<longleftrightarrow> <>[]<>[]P" by S43_solve
   137 
   138 (* Theorems for system S4 from Hughes and Cresswell, p.60 *)
   139 
   140 lemma "\<turnstile> []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S43_solve
   141 lemma "\<turnstile> ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S43_solve
   142 
   143 (* These are from Hailpern, LNCS 129 *)
   144 
   145 lemma "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
   146 lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
   147 lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S43_solve
   148 
   149 lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> (<>P \<longrightarrow> <>Q)" by S43_solve
   150 lemma "\<turnstile> []P \<longrightarrow> []<>P" by S43_solve
   151 lemma "\<turnstile> <>[]P \<longrightarrow> <>P" by S43_solve
   152 
   153 lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
   154 lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
   155 lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
   156 lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
   157 lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
   158 
   159 
   160 (* Theorems of system S43 *)
   161 
   162 lemma "\<turnstile> <>[]P \<longrightarrow> []<>P" by S43_solve
   163 lemma "\<turnstile> <>[]P \<longrightarrow> [][]<>P" by S43_solve
   164 lemma "\<turnstile> [](<>P \<or> <>Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve
   165 lemma "\<turnstile> <>[]P \<and> <>[]Q \<longrightarrow> <>([]P \<and> []Q)" by S43_solve
   166 lemma "\<turnstile> []([]P \<longrightarrow> []Q) \<or> []([]Q \<longrightarrow> []P)" by S43_solve
   167 lemma "\<turnstile> [](<>P \<longrightarrow> <>Q) \<or> [](<>Q \<longrightarrow> <>P)" by S43_solve
   168 lemma "\<turnstile> []([]P \<longrightarrow> Q) \<or> []([]Q \<longrightarrow> P)" by S43_solve
   169 lemma "\<turnstile> [](P \<longrightarrow> <>Q) \<or> [](Q \<longrightarrow> <>P)" by S43_solve
   170 lemma "\<turnstile> [](P \<longrightarrow> []Q \<longrightarrow> R) \<or> [](P \<or> ([]R \<longrightarrow> Q))" by S43_solve
   171 lemma "\<turnstile> [](P \<or> (Q \<longrightarrow> <>C)) \<or> [](P \<longrightarrow> C \<longrightarrow> <>Q)" by S43_solve
   172 lemma "\<turnstile> []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve
   173 lemma "\<turnstile> <>P \<and> <>Q \<longrightarrow> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve
   174 lemma "\<turnstile> [](P \<or> Q) \<and> []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve
   175 lemma "\<turnstile> <>P \<and> <>Q \<longrightarrow> <>(P \<and> Q) \<or> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve
   176 lemma "\<turnstile> <>[]<>P \<longleftrightarrow> []<>P" by S43_solve
   177 lemma "\<turnstile> []<>[]P \<longleftrightarrow> <>[]P" by S43_solve
   178 
   179 (* These are from Hailpern, LNCS 129 *)
   180 
   181 lemma "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
   182 lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
   183 lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> []P \<longrightarrow> <>Q" by S43_solve
   184 
   185 lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> <>P \<longrightarrow> <>Q" by S43_solve
   186 lemma "\<turnstile> []P \<longrightarrow> []<>P" by S43_solve
   187 lemma "\<turnstile> <>[]P \<longrightarrow> <>P" by S43_solve
   188 lemma "\<turnstile> []<>[]P \<longrightarrow> []<>P" by S43_solve
   189 lemma "\<turnstile> <>[]P \<longrightarrow> <>[]<>P" by S43_solve
   190 lemma "\<turnstile> <>[]P \<longrightarrow> []<>P" by S43_solve
   191 lemma "\<turnstile> []<>[]P \<longleftrightarrow> <>[]P" by S43_solve
   192 lemma "\<turnstile> <>[]<>P \<longleftrightarrow> []<>P" by S43_solve
   193 
   194 lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
   195 lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
   196 lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
   197 lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
   198 lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
   199 lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve
   200 lemma "\<turnstile> <>[]P \<and> <>[]Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
   201 lemma "\<turnstile> <>[](P \<and> Q) \<longleftrightarrow> <>[]P \<and> <>[]Q" by S43_solve
   202 lemma "\<turnstile> []<>(P \<or> Q) \<longleftrightarrow> []<>P \<or> []<>Q" by S43_solve
   203 
   204 end