summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Sequents/S4.thy

author | bulwahn |

Tue Aug 31 08:00:53 2010 +0200 (2010-08-31) | |

changeset 38950 | 62578950e748 |

parent 35762 | af3ff2ba4c54 |

child 39159 | 0dec18004e75 |

permissions | -rw-r--r-- |

storing options for prolog code generation in the theory

1 (* Title: Sequents/S4.thy

2 Author: Martin Coen

3 Copyright 1991 University of Cambridge

4 *)

6 theory S4

7 imports Modal0

8 begin

10 axioms

11 (* Definition of the star operation using a set of Horn clauses *)

12 (* For system S4: gamma * == {[]P | []P : gamma} *)

13 (* delta * == {<>P | <>P : delta} *)

15 lstar0: "|L>"

16 lstar1: "$G |L> $H ==> []P, $G |L> []P, $H"

17 lstar2: "$G |L> $H ==> P, $G |L> $H"

18 rstar0: "|R>"

19 rstar1: "$G |R> $H ==> <>P, $G |R> <>P, $H"

20 rstar2: "$G |R> $H ==> P, $G |R> $H"

22 (* Rules for [] and <> *)

24 boxR:

25 "[| $E |L> $E'; $F |R> $F'; $G |R> $G';

26 $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G"

27 boxL: "$E,P,$F,[]P |- $G ==> $E, []P, $F |- $G"

29 diaR: "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G"

30 diaL:

31 "[| $E |L> $E'; $F |L> $F'; $G |R> $G';

32 $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G"

34 ML {*

35 structure S4_Prover = Modal_ProverFun

36 (

37 val rewrite_rls = thms "rewrite_rls"

38 val safe_rls = thms "safe_rls"

39 val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"]

40 val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]

41 val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",

42 thm "rstar1", thm "rstar2"]

43 )

44 *}

46 method_setup S4_solve =

47 {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *} "S4 solver"

50 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)

52 lemma "|- []P --> P" by S4_solve

53 lemma "|- [](P-->Q) --> ([]P-->[]Q)" by S4_solve (* normality*)

54 lemma "|- (P--<Q) --> []P --> []Q" by S4_solve

55 lemma "|- P --> <>P" by S4_solve

57 lemma "|- [](P & Q) <-> []P & []Q" by S4_solve

58 lemma "|- <>(P | Q) <-> <>P | <>Q" by S4_solve

59 lemma "|- [](P<->Q) <-> (P>-<Q)" by S4_solve

60 lemma "|- <>(P-->Q) <-> ([]P--><>Q)" by S4_solve

61 lemma "|- []P <-> ~<>(~P)" by S4_solve

62 lemma "|- [](~P) <-> ~<>P" by S4_solve

63 lemma "|- ~[]P <-> <>(~P)" by S4_solve

64 lemma "|- [][]P <-> ~<><>(~P)" by S4_solve

65 lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by S4_solve

67 lemma "|- []P | []Q --> [](P | Q)" by S4_solve

68 lemma "|- <>(P & Q) --> <>P & <>Q" by S4_solve

69 lemma "|- [](P | Q) --> []P | <>Q" by S4_solve

70 lemma "|- <>P & []Q --> <>(P & Q)" by S4_solve

71 lemma "|- [](P | Q) --> <>P | []Q" by S4_solve

72 lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by S4_solve

73 lemma "|- (P--<Q) & (Q--<R) --> (P--<R)" by S4_solve

74 lemma "|- []P --> <>Q --> <>(P & Q)" by S4_solve

77 (* Theorems of system S4 from Hughes and Cresswell, p.46 *)

79 lemma "|- []A --> A" by S4_solve (* refexivity *)

80 lemma "|- []A --> [][]A" by S4_solve (* transitivity *)

81 lemma "|- []A --> <>A" by S4_solve (* seriality *)

82 lemma "|- <>[](<>A --> []<>A)" by S4_solve

83 lemma "|- <>[](<>[]A --> []A)" by S4_solve

84 lemma "|- []P <-> [][]P" by S4_solve

85 lemma "|- <>P <-> <><>P" by S4_solve

86 lemma "|- <>[]<>P --> <>P" by S4_solve

87 lemma "|- []<>P <-> []<>[]<>P" by S4_solve

88 lemma "|- <>[]P <-> <>[]<>[]P" by S4_solve

90 (* Theorems for system S4 from Hughes and Cresswell, p.60 *)

92 lemma "|- []P | []Q <-> []([]P | []Q)" by S4_solve

93 lemma "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)" by S4_solve

95 (* These are from Hailpern, LNCS 129 *)

97 lemma "|- [](P & Q) <-> []P & []Q" by S4_solve

98 lemma "|- <>(P | Q) <-> <>P | <>Q" by S4_solve

99 lemma "|- <>(P --> Q) <-> ([]P --> <>Q)" by S4_solve

101 lemma "|- [](P --> Q) --> (<>P --> <>Q)" by S4_solve

102 lemma "|- []P --> []<>P" by S4_solve

103 lemma "|- <>[]P --> <>P" by S4_solve

105 lemma "|- []P | []Q --> [](P | Q)" by S4_solve

106 lemma "|- <>(P & Q) --> <>P & <>Q" by S4_solve

107 lemma "|- [](P | Q) --> []P | <>Q" by S4_solve

108 lemma "|- <>P & []Q --> <>(P & Q)" by S4_solve

109 lemma "|- [](P | Q) --> <>P | []Q" by S4_solve

111 end