src/Sequents/T.thy
 changeset 51309 473303ef6e34 parent 42814 5af15f1e2ef6 child 54742 7a86358a3c0b
equal inserted replaced
51308:51e158e988a5 51309:473303ef6e34
`     5 `
`     5 `
`     6 theory T`
`     6 theory T`
`     7 imports Modal0`
`     7 imports Modal0`
`     8 begin`
`     8 begin`
`     9 `
`     9 `
`    10 axioms`
`    10 axiomatization where`
`    11 (* Definition of the star operation using a set of Horn clauses *)`
`    11 (* Definition of the star operation using a set of Horn clauses *)`
`    12 (* For system T:  gamma * == {P | []P : gamma}                  *)`
`    12 (* For system T:  gamma * == {P | []P : gamma}                  *)`
`    13 (*                delta * == {P | <>P : delta}                  *)`
`    13 (*                delta * == {P | <>P : delta}                  *)`
`    14 `
`    14 `
`    15   lstar0:         "|L>"`
`    15   lstar0:         "|L>" and`
`    16   lstar1:         "\$G |L> \$H ==> []P, \$G |L> P, \$H"`
`    16   lstar1:         "\$G |L> \$H ==> []P, \$G |L> P, \$H" and`
`    17   lstar2:         "\$G |L> \$H ==>   P, \$G |L>    \$H"`
`    17   lstar2:         "\$G |L> \$H ==>   P, \$G |L>    \$H" and`
`    18   rstar0:         "|R>"`
`    18   rstar0:         "|R>" and`
`    19   rstar1:         "\$G |R> \$H ==> <>P, \$G |R> P, \$H"`
`    19   rstar1:         "\$G |R> \$H ==> <>P, \$G |R> P, \$H" and`
`    20   rstar2:         "\$G |R> \$H ==>   P, \$G |R>    \$H"`
`    20   rstar2:         "\$G |R> \$H ==>   P, \$G |R>    \$H" and`
`    21 `
`    21 `
`    22 (* Rules for [] and <> *)`
`    22 (* Rules for [] and <> *)`
`    23 `
`    23 `
`    24   boxR:`
`    24   boxR:`
`    25    "[| \$E |L> \$E';  \$F |R> \$F';  \$G |R> \$G';`
`    25    "[| \$E |L> \$E';  \$F |R> \$F';  \$G |R> \$G';`
`    26                \$E'        |- \$F', P, \$G'|] ==> \$E          |- \$F, []P, \$G"`
`    26                \$E'        |- \$F', P, \$G'|] ==> \$E          |- \$F, []P, \$G" and`
`    27   boxL:     "\$E, P, \$F  |-         \$G    ==> \$E, []P, \$F |-          \$G"`
`    27   boxL:     "\$E, P, \$F  |-         \$G    ==> \$E, []P, \$F |-          \$G" and`
`    28   diaR:     "\$E         |- \$F, P,  \$G    ==> \$E          |- \$F, <>P, \$G"`
`    28   diaR:     "\$E         |- \$F, P,  \$G    ==> \$E          |- \$F, <>P, \$G" and`
`    29   diaL:`
`    29   diaL:`
`    30    "[| \$E |L> \$E';  \$F |L> \$F';  \$G |R> \$G';`
`    30    "[| \$E |L> \$E';  \$F |L> \$F';  \$G |R> \$G';`
`    31                \$E', P, \$F'|-         \$G'|] ==> \$E, <>P, \$F |-          \$G"`
`    31                \$E', P, \$F'|-         \$G'|] ==> \$E, <>P, \$F |-          \$G"`
`    32 `
`    32 `
`    33 ML {*`
`    33 ML {*`