src/Sequents/S43.thy
 changeset 35113 1a0c129bb2e0 parent 30549 d2d7874648bd child 39159 0dec18004e75
equal inserted replaced
35112:ff6f60e6ab85 35113:1a0c129bb2e0
`     1 (*  Title:      Modal/S43.thy`
`     1 (*  Title:      Modal/S43.thy`
`     3     Author:     Martin Coen`
`     2     Author:     Martin Coen`
`     4     Copyright   1991  University of Cambridge`
`     3     Copyright   1991  University of Cambridge`
`     5 `
`     4 `
`     6 This implements Rajeev Gore's sequent calculus for S43.`
`     5 This implements Rajeev Gore's sequent calculus for S43.`
`     7 *)`
`     6 *)`
`    12 `
`    11 `
`    13 consts`
`    12 consts`
`    14   S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',`
`    13   S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',`
`    15              seq'=>seq', seq'=>seq', seq'=>seq'] => prop"`
`    14              seq'=>seq', seq'=>seq', seq'=>seq'] => prop"`
`    16 syntax`
`    15 syntax`
`    17   "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"`
`    16   "_S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"`
`    18                          ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)`
`    17                          ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)`
`    19 `
`    18 `
`    20 ML {*`
`    19 parse_translation {*`
`    21   val S43pi  = "S43pi";`
`    20   let`
`    22   val SS43pi = "@S43pi";`
`    21     val tr  = seq_tr;`
`    23 `
`    22     fun s43pi_tr [s1, s2, s3, s4, s5, s6] =`
`    24   val tr  = seq_tr;`
`    23       Const (@{const_syntax S43pi}, dummyT) \$ tr s1 \$ tr s2 \$ tr s3 \$ tr s4 \$ tr s5 \$ tr s6;`
`       `
`    24   in [(@{syntax_const "_S43pi"}, s43pi_tr)] end`
`       `
`    25 *}`
`       `
`    26 `
`       `
`    27 print_translation {*`
`       `
`    28 let`
`    25   val tr' = seq_tr';`
`    29   val tr' = seq_tr';`
`    26 `
`    30   fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =`
`    27   fun s43pi_tr[s1,s2,s3,s4,s5,s6]=`
`    31     Const(@{syntax_const "_S43pi"}, dummyT) \$ tr' s1 \$ tr' s2 \$ tr' s3 \$ tr' s4 \$ tr' s5 \$ tr' s6;`
`    28         Const(S43pi,dummyT)\$tr s1\$tr s2\$tr s3\$tr s4\$tr s5\$tr s6;`
`    32 in [(@{const_syntax S43pi}, s43pi_tr')] end`
`    29   fun s43pi_tr'[s1,s2,s3,s4,s5,s6] =`
`       `
`    30         Const(SS43pi,dummyT)\$tr' s1\$tr' s2\$tr' s3\$tr' s4\$tr' s5\$tr' s6;`
`       `
`    31 `
`       `
`    32 *}`
`    33 *}`
`    36 `
`    34 `
`    37 axioms`
`    35 axioms`
`    38 (* Definition of the star operation using a set of Horn clauses  *)`
`    36 (* Definition of the star operation using a set of Horn clauses  *)`
`    39 (* For system S43: gamma * == {[]P | []P : gamma}                *)`
`    37 (* For system S43: gamma * == {[]P | []P : gamma}                *)`
`    40 (*                 delta * == {<>P | <>P : delta}                *)`
`    38 (*                 delta * == {<>P | <>P : delta}                *)`