src/Sequents/S4.thy
 changeset 17481 75166ebb619b parent 2073 fb0655539d05 child 21426 87ac12bed1ab
equal inserted replaced
17480:fd19f77dcf60 17481:75166ebb619b
`     1 (*  Title:      Modal/S4`
`     1 (*  Title:      Modal/S4.thy`
`     2     ID:         \$Id\$`
`     2     ID:         \$Id\$`
`     3     Author:     Martin Coen`
`     3     Author:     Martin Coen`
`     4     Copyright   1991  University of Cambridge`
`     4     Copyright   1991  University of Cambridge`
`     5 *)`
`     5 *)`
`     6 `
`     6 `
`     7 S4 = Modal0 +`
`     7 theory S4`
`     8 rules`
`     8 imports Modal0`
`       `
`     9 begin`
`       `
`    10 `
`       `
`    11 axioms`
`     9 (* Definition of the star operation using a set of Horn clauses *)`
`    12 (* Definition of the star operation using a set of Horn clauses *)`
`    10 (* For system S4:  gamma * == {[]P | []P : gamma}               *)`
`    13 (* For system S4:  gamma * == {[]P | []P : gamma}               *)`
`    11 (*                 delta * == {<>P | <>P : delta}               *)`
`    14 (*                 delta * == {<>P | <>P : delta}               *)`
`    12 `
`    15 `
`    13   lstar0         "|L>"`
`    16   lstar0:         "|L>"`
`    14   lstar1         "\$G |L> \$H ==> []P, \$G |L> []P, \$H"`
`    17   lstar1:         "\$G |L> \$H ==> []P, \$G |L> []P, \$H"`
`    15   lstar2         "\$G |L> \$H ==>   P, \$G |L>      \$H"`
`    18   lstar2:         "\$G |L> \$H ==>   P, \$G |L>      \$H"`
`    16   rstar0         "|R>"`
`    19   rstar0:         "|R>"`
`    17   rstar1         "\$G |R> \$H ==> <>P, \$G |R> <>P, \$H"`
`    20   rstar1:         "\$G |R> \$H ==> <>P, \$G |R> <>P, \$H"`
`    18   rstar2         "\$G |R> \$H ==>   P, \$G |R>      \$H"`
`    21   rstar2:         "\$G |R> \$H ==>   P, \$G |R>      \$H"`
`    19 `
`    22 `
`    20 (* Rules for [] and <> *)`
`    23 (* Rules for [] and <> *)`
`    21 `
`    24 `
`    22   boxR`
`    25   boxR:`
`    23    "[| \$E |L> \$E';  \$F |R> \$F';  \$G |R> \$G';  `
`    26    "[| \$E |L> \$E';  \$F |R> \$F';  \$G |R> \$G';`
`    24            \$E'         |- \$F', P, \$G'|] ==> \$E          |- \$F, []P, \$G"`
`    27            \$E'         |- \$F', P, \$G'|] ==> \$E          |- \$F, []P, \$G"`
`    25   boxL     "\$E,P,\$F,[]P |-         \$G    ==> \$E, []P, \$F |-          \$G"`
`    28   boxL:     "\$E,P,\$F,[]P |-         \$G    ==> \$E, []P, \$F |-          \$G"`
`    26 `
`    29 `
`    27   diaR     "\$E          |- \$F,P,\$G,<>P   ==> \$E          |- \$F, <>P, \$G"`
`    30   diaR:     "\$E          |- \$F,P,\$G,<>P   ==> \$E          |- \$F, <>P, \$G"`
`    28   diaL`
`    31   diaL:`
`    29    "[| \$E |L> \$E';  \$F |L> \$F';  \$G |R> \$G';  `
`    32    "[| \$E |L> \$E';  \$F |L> \$F';  \$G |R> \$G';`
`    30            \$E', P, \$F' |-         \$G'|] ==> \$E, <>P, \$F |- \$G"`
`    33            \$E', P, \$F' |-         \$G'|] ==> \$E, <>P, \$F |- \$G"`
`       `
`    34 `
`       `
`    35 ML {* use_legacy_bindings (the_context ()) *}`
`       `
`    36 `
`    31 end`
`    37 end`