29 diaR: "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G" and |
29 diaR: "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G" and |
30 diaL: |
30 diaL: |
31 "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; |
31 "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; |
32 $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G" |
32 $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G" |
33 |
33 |
34 ML {* |
34 ML \<open> |
35 structure S4_Prover = Modal_ProverFun |
35 structure S4_Prover = Modal_ProverFun |
36 ( |
36 ( |
37 val rewrite_rls = @{thms rewrite_rls} |
37 val rewrite_rls = @{thms rewrite_rls} |
38 val safe_rls = @{thms safe_rls} |
38 val safe_rls = @{thms safe_rls} |
39 val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}] |
39 val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}] |
40 val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}] |
40 val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}] |
41 val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0}, |
41 val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0}, |
42 @{thm rstar1}, @{thm rstar2}] |
42 @{thm rstar1}, @{thm rstar2}] |
43 ) |
43 ) |
44 *} |
44 \<close> |
45 |
45 |
46 method_setup S4_solve = |
46 method_setup S4_solve = |
47 {* Scan.succeed (fn ctxt => SIMPLE_METHOD (S4_Prover.solve_tac ctxt 2)) *} |
47 \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (S4_Prover.solve_tac ctxt 2))\<close> |
48 |
48 |
49 |
49 |
50 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) |
50 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *) |
51 |
51 |
52 lemma "|- []P --> P" by S4_solve |
52 lemma "|- []P --> P" by S4_solve |