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

src/Sequents/S43.thy

changeset 51309 | 473303ef6e34 |

parent 42814 | 5af15f1e2ef6 |

child 52143 | 36ffe23b25f8 |

--- a/src/Sequents/S43.thy Thu Feb 28 14:10:54 2013 +0100 +++ b/src/Sequents/S43.thy Thu Feb 28 14:22:14 2013 +0100 @@ -32,17 +32,17 @@ in [(@{const_syntax S43pi}, s43pi_tr')] end *} -axioms +axiomatization where (* Definition of the star operation using a set of Horn clauses *) (* For system S43: gamma * == {[]P | []P : gamma} *) (* delta * == {<>P | <>P : delta} *) - lstar0: "|L>" - lstar1: "$G |L> $H ==> []P, $G |L> []P, $H" - lstar2: "$G |L> $H ==> P, $G |L> $H" - rstar0: "|R>" - rstar1: "$G |R> $H ==> <>P, $G |R> <>P, $H" - rstar2: "$G |R> $H ==> P, $G |R> $H" + lstar0: "|L>" and + lstar1: "$G |L> $H ==> []P, $G |L> []P, $H" and + lstar2: "$G |L> $H ==> 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 (* Set of Horn clauses to generate the antecedents for the S43 pi rule *) (* ie *) @@ -54,22 +54,22 @@ (* and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj *) (* and 1<=i<=k and k<j<=k+m *) - S43pi0: "S43pi $L;; $R;; $Lbox; $Rdia" + S43pi0: "S43pi $L;; $R;; $Lbox; $Rdia" and S43pi1: "[| (S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox |- $R,$Rdia |] ==> - S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia" + S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia" and S43pi2: "[| (S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox |- $R',P,$R,$Rdia |] ==> - S43pi $L';; $R'; []P,$R; $Lbox;$Rdia" + S43pi $L';; $R'; []P,$R; $Lbox;$Rdia" and (* Rules for [] and <> for S43 *) - boxL: "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G" - diaR: "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G" + boxL: "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G" and + diaR: "$E |- $F, P, $G, <>P ==> $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 |] ==> - $L1, <>P, $L2 |- $R" + $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 |] ==>