src/Sequents/T.thy
 changeset 17481 75166ebb619b parent 2073 fb0655539d05 child 21426 87ac12bed1ab
equal inserted replaced
17480:fd19f77dcf60 17481:75166ebb619b
`     1 (*  Title:      Modal/T`
`     1 (*  Title:      Modal/T.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 T = Modal0 +`
`     7 theory T`
`     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 T:  gamma * == {P | []P : gamma}                  *)`
`    13 (* For system T:  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  |-         \$G    ==> \$E, []P, \$F |-          \$G"`
`    28   boxL:     "\$E, P, \$F  |-         \$G    ==> \$E, []P, \$F |-          \$G"`
`    26   diaR     "\$E         |- \$F, P,  \$G    ==> \$E          |- \$F, <>P, \$G"`
`    29   diaR:     "\$E         |- \$F, P,  \$G    ==> \$E          |- \$F, <>P, \$G"`
`    27   diaL`
`    30   diaL:`
`    28    "[| \$E |L> \$E';  \$F |L> \$F';  \$G |R> \$G';  `
`    31    "[| \$E |L> \$E';  \$F |L> \$F';  \$G |R> \$G';`
`    29                \$E', P, \$F'|-         \$G'|] ==> \$E, <>P, \$F |-          \$G"`
`    32                \$E', P, \$F'|-         \$G'|] ==> \$E, <>P, \$F |-          \$G"`
`       `
`    33 `
`       `
`    34 ML {* use_legacy_bindings (the_context ()) *}`
`       `
`    35 `
`    30 end`
`    36 end`