Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
isabelle