1(* Title: Sequents/S43.thy 2 Author: Martin Coen 3 Copyright 1991 University of Cambridge 4 5This implements Rajeev Gore's sequent calculus for S43. 6*) 7 8theory S43 9imports Modal0 10begin 11 12consts 13 S43pi :: "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', 14 seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop" 15syntax 16 "_S43pi" :: "[seq, seq, seq, seq, seq, seq] \<Rightarrow> prop" 17 ("S43pi((_);(_);(_);(_);(_);(_))" [] 5) 18 19parse_translation \<open> 20 let 21 val tr = seq_tr; 22 fun s43pi_tr [s1, s2, s3, s4, s5, s6] = 23 Const (\<^const_syntax>\<open>S43pi\<close>, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6; 24 in [(\<^syntax_const>\<open>_S43pi\<close>, K s43pi_tr)] end 25\<close> 26 27print_translation \<open> 28let 29 val tr' = seq_tr'; 30 fun s43pi_tr' [s1, s2, s3, s4, s5, s6] = 31 Const(\<^syntax_const>\<open>_S43pi\<close>, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6; 32in [(\<^const_syntax>\<open>S43pi\<close>, K s43pi_tr')] end 33\<close> 34 35axiomatization 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 79ML \<open> 80structure 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 92method_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 100lemma "\<turnstile> []P \<longrightarrow> P" by S43_solve 101lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by S43_solve (* normality*) 102lemma "\<turnstile> (P--<Q) \<longrightarrow> []P \<longrightarrow> []Q" by S43_solve 103lemma "\<turnstile> P \<longrightarrow> <>P" by S43_solve 104 105lemma "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve 106lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve 107lemma "\<turnstile> [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P>-<Q)" by S43_solve 108lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S43_solve 109lemma "\<turnstile> []P \<longleftrightarrow> \<not> <>(\<not> P)" by S43_solve 110lemma "\<turnstile> [](\<not>P) \<longleftrightarrow> \<not> <>P" by S43_solve 111lemma "\<turnstile> \<not> []P \<longleftrightarrow> <>(\<not> P)" by S43_solve 112lemma "\<turnstile> [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by S43_solve 113lemma "\<turnstile> \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>Q" by S43_solve 114 115lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve 116lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve 117lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve 118lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve 119lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve 120lemma "\<turnstile> <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by S43_solve 121lemma "\<turnstile> (P --< Q) \<and> (Q --<R ) \<longrightarrow> (P --< R)" by S43_solve 122lemma "\<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 127lemma "\<turnstile> []A \<longrightarrow> A" by S43_solve (* refexivity *) 128lemma "\<turnstile> []A \<longrightarrow> [][]A" by S43_solve (* transitivity *) 129lemma "\<turnstile> []A \<longrightarrow> <>A" by S43_solve (* seriality *) 130lemma "\<turnstile> <>[](<>A \<longrightarrow> []<>A)" by S43_solve 131lemma "\<turnstile> <>[](<>[]A \<longrightarrow> []A)" by S43_solve 132lemma "\<turnstile> []P \<longleftrightarrow> [][]P" by S43_solve 133lemma "\<turnstile> <>P \<longleftrightarrow> <><>P" by S43_solve 134lemma "\<turnstile> <>[]<>P \<longrightarrow> <>P" by S43_solve 135lemma "\<turnstile> []<>P \<longleftrightarrow> []<>[]<>P" by S43_solve 136lemma "\<turnstile> <>[]P \<longleftrightarrow> <>[]<>[]P" by S43_solve 137 138(* Theorems for system S4 from Hughes and Cresswell, p.60 *) 139 140lemma "\<turnstile> []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S43_solve 141lemma "\<turnstile> ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S43_solve 142 143(* These are from Hailpern, LNCS 129 *) 144 145lemma "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve 146lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve 147lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S43_solve 148 149lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> (<>P \<longrightarrow> <>Q)" by S43_solve 150lemma "\<turnstile> []P \<longrightarrow> []<>P" by S43_solve 151lemma "\<turnstile> <>[]P \<longrightarrow> <>P" by S43_solve 152 153lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve 154lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve 155lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve 156lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve 157lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve 158 159 160(* Theorems of system S43 *) 161 162lemma "\<turnstile> <>[]P \<longrightarrow> []<>P" by S43_solve 163lemma "\<turnstile> <>[]P \<longrightarrow> [][]<>P" by S43_solve 164lemma "\<turnstile> [](<>P \<or> <>Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve 165lemma "\<turnstile> <>[]P \<and> <>[]Q \<longrightarrow> <>([]P \<and> []Q)" by S43_solve 166lemma "\<turnstile> []([]P \<longrightarrow> []Q) \<or> []([]Q \<longrightarrow> []P)" by S43_solve 167lemma "\<turnstile> [](<>P \<longrightarrow> <>Q) \<or> [](<>Q \<longrightarrow> <>P)" by S43_solve 168lemma "\<turnstile> []([]P \<longrightarrow> Q) \<or> []([]Q \<longrightarrow> P)" by S43_solve 169lemma "\<turnstile> [](P \<longrightarrow> <>Q) \<or> [](Q \<longrightarrow> <>P)" by S43_solve 170lemma "\<turnstile> [](P \<longrightarrow> []Q \<longrightarrow> R) \<or> [](P \<or> ([]R \<longrightarrow> Q))" by S43_solve 171lemma "\<turnstile> [](P \<or> (Q \<longrightarrow> <>C)) \<or> [](P \<longrightarrow> C \<longrightarrow> <>Q)" by S43_solve 172lemma "\<turnstile> []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve 173lemma "\<turnstile> <>P \<and> <>Q \<longrightarrow> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve 174lemma "\<turnstile> [](P \<or> Q) \<and> []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve 175lemma "\<turnstile> <>P \<and> <>Q \<longrightarrow> <>(P \<and> Q) \<or> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve 176lemma "\<turnstile> <>[]<>P \<longleftrightarrow> []<>P" by S43_solve 177lemma "\<turnstile> []<>[]P \<longleftrightarrow> <>[]P" by S43_solve 178 179(* These are from Hailpern, LNCS 129 *) 180 181lemma "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve 182lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve 183lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> []P \<longrightarrow> <>Q" by S43_solve 184 185lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> <>P \<longrightarrow> <>Q" by S43_solve 186lemma "\<turnstile> []P \<longrightarrow> []<>P" by S43_solve 187lemma "\<turnstile> <>[]P \<longrightarrow> <>P" by S43_solve 188lemma "\<turnstile> []<>[]P \<longrightarrow> []<>P" by S43_solve 189lemma "\<turnstile> <>[]P \<longrightarrow> <>[]<>P" by S43_solve 190lemma "\<turnstile> <>[]P \<longrightarrow> []<>P" by S43_solve 191lemma "\<turnstile> []<>[]P \<longleftrightarrow> <>[]P" by S43_solve 192lemma "\<turnstile> <>[]<>P \<longleftrightarrow> []<>P" by S43_solve 193 194lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve 195lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve 196lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve 197lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve 198lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve 199lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve 200lemma "\<turnstile> <>[]P \<and> <>[]Q \<longrightarrow> <>(P \<and> Q)" by S43_solve 201lemma "\<turnstile> <>[](P \<and> Q) \<longleftrightarrow> <>[]P \<and> <>[]Q" by S43_solve 202lemma "\<turnstile> []<>(P \<or> Q) \<longleftrightarrow> []<>P \<or> []<>Q" by S43_solve 203 204end 205