summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Sequents/S43.thy

changeset 61385 | 538100cc4399 |

parent 60770 | 240563fbf41d |

child 61386 | 0a29a984a91b |

--- a/src/Sequents/S43.thy Sat Oct 10 19:22:05 2015 +0200 +++ b/src/Sequents/S43.thy Sat Oct 10 20:51:39 2015 +0200 @@ -10,10 +10,10 @@ begin consts - S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq', - seq'=>seq', seq'=>seq', seq'=>seq'] => prop" + S43pi :: "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', + seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop" syntax - "_S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop" + "_S43pi" :: "[seq, seq, seq, seq, seq, seq] \<Rightarrow> prop" ("S43pi((_);(_);(_);(_);(_);(_))" [] 5) parse_translation \<open> @@ -38,11 +38,11 @@ (* delta * == {<>P | <>P : delta} *) lstar0: "|L>" and - lstar1: "$G |L> $H ==> []P, $G |L> []P, $H" and - lstar2: "$G |L> $H ==> P, $G |L> $H" and + lstar1: "$G |L> $H \<Longrightarrow> []P, $G |L> []P, $H" and + lstar2: "$G |L> $H \<Longrightarrow> P, $G |L> $H" and rstar0: "|R>" and - rstar1: "$G |R> $H ==> <>P, $G |R> <>P, $H" and - rstar2: "$G |R> $H ==> P, $G |R> $H" and + rstar1: "$G |R> $H \<Longrightarrow> <>P, $G |R> <>P, $H" and + rstar2: "$G |R> $H \<Longrightarrow> P, $G |R> $H" and (* Set of Horn clauses to generate the antecedents for the S43 pi rule *) (* ie *) @@ -56,23 +56,23 @@ S43pi0: "S43pi $L;; $R;; $Lbox; $Rdia" and S43pi1: - "[| (S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox |- $R,$Rdia |] ==> + "\<lbrakk>(S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox |- $R,$Rdia\<rbrakk> \<Longrightarrow> S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia" and S43pi2: - "[| (S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox |- $R',P,$R,$Rdia |] ==> + "\<lbrakk>(S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox |- $R',P,$R,$Rdia\<rbrakk> \<Longrightarrow> S43pi $L';; $R'; []P,$R; $Lbox;$Rdia" and (* Rules for [] and <> for S43 *) - boxL: "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G" and - diaR: "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G" and + boxL: "$E, P, $F, []P |- $G \<Longrightarrow> $E, []P, $F |- $G" and + diaR: "$E |- $F, P, $G, <>P \<Longrightarrow> $E |- $F, <>P, $G" and pi1: - "[| $L1,<>P,$L2 |L> $Lbox; $L1,<>P,$L2 |R> $Ldia; $R |L> $Rbox; $R |R> $Rdia; - S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> + "\<lbrakk>$L1,<>P,$L2 |L> $Lbox; $L1,<>P,$L2 |R> $Ldia; $R |L> $Rbox; $R |R> $Rdia; + S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia\<rbrakk> \<Longrightarrow> $L1, <>P, $L2 |- $R" and pi2: - "[| $L |L> $Lbox; $L |R> $Ldia; $R1,[]P,$R2 |L> $Rbox; $R1,[]P,$R2 |R> $Rdia; - S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==> + "\<lbrakk>$L |L> $Lbox; $L |R> $Ldia; $R1,[]P,$R2 |L> $Rbox; $R1,[]P,$R2 |R> $Rdia; + S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia\<rbrakk> \<Longrightarrow> $L |- $R1, []P, $R2" @@ -97,108 +97,108 @@ (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) -lemma "|- []P --> P" by S43_solve -lemma "|- [](P-->Q) --> ([]P-->[]Q)" by S43_solve (* normality*) -lemma "|- (P--<Q) --> []P --> []Q" by S43_solve -lemma "|- P --> <>P" by S43_solve +lemma "|- []P \<longrightarrow> P" by S43_solve +lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by S43_solve (* normality*) +lemma "|- (P--<Q) \<longrightarrow> []P \<longrightarrow> []Q" by S43_solve +lemma "|- P \<longrightarrow> <>P" by S43_solve -lemma "|- [](P & Q) <-> []P & []Q" by S43_solve -lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve -lemma "|- [](P<->Q) <-> (P>-<Q)" by S43_solve -lemma "|- <>(P-->Q) <-> ([]P--><>Q)" by S43_solve -lemma "|- []P <-> ~<>(~P)" by S43_solve -lemma "|- [](~P) <-> ~<>P" by S43_solve -lemma "|- ~[]P <-> <>(~P)" by S43_solve -lemma "|- [][]P <-> ~<><>(~P)" by S43_solve -lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by S43_solve +lemma "|- [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve +lemma "|- <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve +lemma "|- [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P>-<Q)" by S43_solve +lemma "|- <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S43_solve +lemma "|- []P \<longleftrightarrow> \<not> <>(\<not> P)" by S43_solve +lemma "|- [](\<not>P) \<longleftrightarrow> \<not> <>P" by S43_solve +lemma "|- \<not> []P \<longleftrightarrow> <>(\<not> P)" by S43_solve +lemma "|- [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by S43_solve +lemma "|- \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>Q" by S43_solve -lemma "|- []P | []Q --> [](P | Q)" by S43_solve -lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve -lemma "|- [](P | Q) --> []P | <>Q" by S43_solve -lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve -lemma "|- [](P | Q) --> <>P | []Q" by S43_solve -lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by S43_solve -lemma "|- (P--<Q) & (Q--<R) --> (P--<R)" by S43_solve -lemma "|- []P --> <>Q --> <>(P & Q)" by S43_solve +lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve +lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve +lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve +lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve +lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve +lemma "|- <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by S43_solve +lemma "|- (P --< Q) \<and> (Q --<R ) \<longrightarrow> (P --< R)" by S43_solve +lemma "|- []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by S43_solve (* Theorems of system S4 from Hughes and Cresswell, p.46 *) -lemma "|- []A --> A" by S43_solve (* refexivity *) -lemma "|- []A --> [][]A" by S43_solve (* transitivity *) -lemma "|- []A --> <>A" by S43_solve (* seriality *) -lemma "|- <>[](<>A --> []<>A)" by S43_solve -lemma "|- <>[](<>[]A --> []A)" by S43_solve -lemma "|- []P <-> [][]P" by S43_solve -lemma "|- <>P <-> <><>P" by S43_solve -lemma "|- <>[]<>P --> <>P" by S43_solve -lemma "|- []<>P <-> []<>[]<>P" by S43_solve -lemma "|- <>[]P <-> <>[]<>[]P" by S43_solve +lemma "|- []A \<longrightarrow> A" by S43_solve (* refexivity *) +lemma "|- []A \<longrightarrow> [][]A" by S43_solve (* transitivity *) +lemma "|- []A \<longrightarrow> <>A" by S43_solve (* seriality *) +lemma "|- <>[](<>A \<longrightarrow> []<>A)" by S43_solve +lemma "|- <>[](<>[]A \<longrightarrow> []A)" by S43_solve +lemma "|- []P \<longleftrightarrow> [][]P" by S43_solve +lemma "|- <>P \<longleftrightarrow> <><>P" by S43_solve +lemma "|- <>[]<>P \<longrightarrow> <>P" by S43_solve +lemma "|- []<>P \<longleftrightarrow> []<>[]<>P" by S43_solve +lemma "|- <>[]P \<longleftrightarrow> <>[]<>[]P" by S43_solve (* Theorems for system S4 from Hughes and Cresswell, p.60 *) -lemma "|- []P | []Q <-> []([]P | []Q)" by S43_solve -lemma "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)" by S43_solve +lemma "|- []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S43_solve +lemma "|- ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S43_solve (* These are from Hailpern, LNCS 129 *) -lemma "|- [](P & Q) <-> []P & []Q" by S43_solve -lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve -lemma "|- <>(P --> Q) <-> ([]P --> <>Q)" by S43_solve +lemma "|- [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve +lemma "|- <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve +lemma "|- <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S43_solve -lemma "|- [](P --> Q) --> (<>P --> <>Q)" by S43_solve -lemma "|- []P --> []<>P" by S43_solve -lemma "|- <>[]P --> <>P" by S43_solve +lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> (<>P \<longrightarrow> <>Q)" by S43_solve +lemma "|- []P \<longrightarrow> []<>P" by S43_solve +lemma "|- <>[]P \<longrightarrow> <>P" by S43_solve -lemma "|- []P | []Q --> [](P | Q)" by S43_solve -lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve -lemma "|- [](P | Q) --> []P | <>Q" by S43_solve -lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve -lemma "|- [](P | Q) --> <>P | []Q" by S43_solve +lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve +lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve +lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve +lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve +lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve (* Theorems of system S43 *) -lemma "|- <>[]P --> []<>P" by S43_solve -lemma "|- <>[]P --> [][]<>P" by S43_solve -lemma "|- [](<>P | <>Q) --> []<>P | []<>Q" by S43_solve -lemma "|- <>[]P & <>[]Q --> <>([]P & []Q)" by S43_solve -lemma "|- []([]P --> []Q) | []([]Q --> []P)" by S43_solve -lemma "|- [](<>P --> <>Q) | [](<>Q --> <>P)" by S43_solve -lemma "|- []([]P --> Q) | []([]Q --> P)" by S43_solve -lemma "|- [](P --> <>Q) | [](Q --> <>P)" by S43_solve -lemma "|- [](P --> []Q-->R) | [](P | ([]R --> Q))" by S43_solve -lemma "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)" by S43_solve -lemma "|- []([]P | Q) & [](P | []Q) --> []P | []Q" by S43_solve -lemma "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)" by S43_solve -lemma "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q" by S43_solve -lemma "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)" by S43_solve -lemma "|- <>[]<>P <-> []<>P" by S43_solve -lemma "|- []<>[]P <-> <>[]P" by S43_solve +lemma "|- <>[]P \<longrightarrow> []<>P" by S43_solve +lemma "|- <>[]P \<longrightarrow> [][]<>P" by S43_solve +lemma "|- [](<>P \<or> <>Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve +lemma "|- <>[]P \<and> <>[]Q \<longrightarrow> <>([]P \<and> []Q)" by S43_solve +lemma "|- []([]P \<longrightarrow> []Q) \<or> []([]Q \<longrightarrow> []P)" by S43_solve +lemma "|- [](<>P \<longrightarrow> <>Q) \<or> [](<>Q \<longrightarrow> <>P)" by S43_solve +lemma "|- []([]P \<longrightarrow> Q) \<or> []([]Q \<longrightarrow> P)" by S43_solve +lemma "|- [](P \<longrightarrow> <>Q) \<or> [](Q \<longrightarrow> <>P)" by S43_solve +lemma "|- [](P \<longrightarrow> []Q \<longrightarrow> R) \<or> [](P \<or> ([]R \<longrightarrow> Q))" by S43_solve +lemma "|- [](P \<or> (Q \<longrightarrow> <>C)) \<or> [](P \<longrightarrow> C \<longrightarrow> <>Q)" by S43_solve +lemma "|- []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve +lemma "|- <>P \<and> <>Q \<longrightarrow> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve +lemma "|- [](P \<or> Q) \<and> []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve +lemma "|- <>P \<and> <>Q \<longrightarrow> <>(P \<and> Q) \<or> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve +lemma "|- <>[]<>P \<longleftrightarrow> []<>P" by S43_solve +lemma "|- []<>[]P \<longleftrightarrow> <>[]P" by S43_solve (* These are from Hailpern, LNCS 129 *) -lemma "|- [](P & Q) <-> []P & []Q" by S43_solve -lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve -lemma "|- <>(P --> Q) <-> []P --> <>Q" by S43_solve +lemma "|- [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve +lemma "|- <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve +lemma "|- <>(P \<longrightarrow> Q) \<longleftrightarrow> []P \<longrightarrow> <>Q" by S43_solve -lemma "|- [](P --> Q) --> <>P --> <>Q" by S43_solve -lemma "|- []P --> []<>P" by S43_solve -lemma "|- <>[]P --> <>P" by S43_solve -lemma "|- []<>[]P --> []<>P" by S43_solve -lemma "|- <>[]P --> <>[]<>P" by S43_solve -lemma "|- <>[]P --> []<>P" by S43_solve -lemma "|- []<>[]P <-> <>[]P" by S43_solve -lemma "|- <>[]<>P <-> []<>P" by S43_solve +lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> <>P \<longrightarrow> <>Q" by S43_solve +lemma "|- []P \<longrightarrow> []<>P" by S43_solve +lemma "|- <>[]P \<longrightarrow> <>P" by S43_solve +lemma "|- []<>[]P \<longrightarrow> []<>P" by S43_solve +lemma "|- <>[]P \<longrightarrow> <>[]<>P" by S43_solve +lemma "|- <>[]P \<longrightarrow> []<>P" by S43_solve +lemma "|- []<>[]P \<longleftrightarrow> <>[]P" by S43_solve +lemma "|- <>[]<>P \<longleftrightarrow> []<>P" by S43_solve -lemma "|- []P | []Q --> [](P | Q)" by S43_solve -lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve -lemma "|- [](P | Q) --> []P | <>Q" by S43_solve -lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve -lemma "|- [](P | Q) --> <>P | []Q" by S43_solve -lemma "|- [](P | Q) --> []<>P | []<>Q" by S43_solve -lemma "|- <>[]P & <>[]Q --> <>(P & Q)" by S43_solve -lemma "|- <>[](P & Q) <-> <>[]P & <>[]Q" by S43_solve -lemma "|- []<>(P | Q) <-> []<>P | []<>Q" by S43_solve +lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve +lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve +lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve +lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve +lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve +lemma "|- [](P \<or> Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve +lemma "|- <>[]P \<and> <>[]Q \<longrightarrow> <>(P \<and> Q)" by S43_solve +lemma "|- <>[](P \<and> Q) \<longleftrightarrow> <>[]P \<and> <>[]Q" by S43_solve +lemma "|- []<>(P \<or> Q) \<longleftrightarrow> []<>P \<or> []<>Q" by S43_solve end