src/HOLCF/IOA/meta_theory/TL.ML
author wenzelm
Sun Jul 12 11:49:17 1998 +0200 (1998-07-12)
changeset 5132 24f992a25adc
parent 5068 fb28eaa07e01
child 5976 44290b71a85f
permissions -rw-r--r--
isatool expandshort;
mueller@4559
     1
(*  Title:      HOLCF/IOA/meta_theory/TL.ML
mueller@4559
     2
    ID:         $Id$
mueller@4559
     3
    Author:     Olaf M"uller
mueller@4559
     4
    Copyright   1997  TU Muenchen
mueller@4559
     5
mueller@4559
     6
Temporal Logic 
mueller@4559
     7
*)   
mueller@4559
     8
mueller@4559
     9
wenzelm@5068
    10
Goal "[] <> (.~ P) = (.~ <> [] P)";
wenzelm@5132
    11
by (rtac ext 1);
mueller@4559
    12
by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1);
wenzelm@5132
    13
by Auto_tac;
mueller@4559
    14
qed"simple_try";
mueller@4559
    15
wenzelm@5068
    16
Goal "nil |= [] P";
mueller@4559
    17
by (asm_full_simp_tac (simpset() addsimps [satisfies_def,
mueller@4559
    18
     Box_def,tsuffix_def,suffix_def,nil_is_Conc])1);
mueller@4559
    19
qed"Boxnil";
mueller@4559
    20
wenzelm@5068
    21
Goal "~(nil |= <> P)";
mueller@4559
    22
by (simp_tac (simpset() addsimps [Diamond_def,satisfies_def,NOT_def])1);
mueller@4559
    23
by (cut_inst_tac [] Boxnil 1);
mueller@4559
    24
by (asm_full_simp_tac (simpset() addsimps [satisfies_def])1);
mueller@4559
    25
qed"Diamondnil";
mueller@4559
    26
wenzelm@5068
    27
Goal "(<> F) s = (? s2. tsuffix s2 s & F s2)";
mueller@4559
    28
by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1);
mueller@4559
    29
qed"Diamond_def2";
mueller@4559
    30
mueller@4559
    31
mueller@4559
    32
mueller@4559
    33
section "TLA Axiomatization by Merz";
mueller@4559
    34
mueller@4559
    35
(* ---------------------------------------------------------------- *)
mueller@4559
    36
(*                 TLA Axiomatization by Merz                       *)
mueller@4559
    37
(* ---------------------------------------------------------------- *)
mueller@4559
    38
wenzelm@5068
    39
Goal "suffix s s";
mueller@4559
    40
by (simp_tac (simpset() addsimps [suffix_def])1);
mueller@4559
    41
by (res_inst_tac [("x","nil")] exI 1);
wenzelm@5132
    42
by Auto_tac;
mueller@4559
    43
qed"suffix_refl";
mueller@4559
    44
wenzelm@5068
    45
Goal "s~=UU & s~=nil --> (s |= [] F .--> F)";
mueller@4559
    46
by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def])1);
mueller@4559
    47
by (REPEAT (rtac impI 1));
mueller@4559
    48
by (eres_inst_tac [("x","s")] allE 1);
mueller@4559
    49
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
mueller@4559
    50
qed"reflT";
mueller@4559
    51
mueller@4559
    52
wenzelm@5068
    53
Goal "!!x. [| suffix y x ; suffix z y |]  ==> suffix z x";
mueller@4559
    54
by (asm_full_simp_tac (simpset() addsimps [suffix_def])1);
wenzelm@5132
    55
by Auto_tac;
mueller@4559
    56
by (res_inst_tac [("x","s1 @@ s1a")] exI 1);
wenzelm@5132
    57
by Auto_tac;
mueller@4559
    58
by (simp_tac (simpset() addsimps [Conc_assoc]) 1); 
mueller@4559
    59
qed"suffix_trans";
mueller@4559
    60
wenzelm@5068
    61
Goal "s |= [] F .--> [] [] F";
mueller@4559
    62
by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def,tsuffix_def])1);
wenzelm@5132
    63
by Auto_tac;
wenzelm@5132
    64
by (dtac suffix_trans 1);
wenzelm@5132
    65
by (assume_tac 1);
mueller@4559
    66
by (eres_inst_tac [("x","s2a")] allE 1);
wenzelm@5132
    67
by Auto_tac;
mueller@4559
    68
qed"transT";
mueller@4559
    69
mueller@4559
    70
wenzelm@5068
    71
Goal "s |= [] (F .--> G) .--> [] F .--> [] G";
mueller@4559
    72
by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def])1);
mueller@4559
    73
qed"normalT";
mueller@4559
    74
mueller@4559
    75
mueller@4559
    76
(*
wenzelm@5068
    77
Goal "s |= <> F .& <> G .--> (<> (F .& <> G) .| <> (G .& <> F))";
mueller@4559
    78
by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,AND_def,OR_def,Diamond_def2])1);
wenzelm@5132
    79
by (rtac impI 1);
wenzelm@5132
    80
by (etac conjE 1);
wenzelm@5132
    81
by (etac exE 1);
wenzelm@5132
    82
by (etac exE 1);
mueller@4559
    83
mueller@4559
    84
wenzelm@5132
    85
by (rtac disjI1 1);
mueller@4559
    86
wenzelm@5068
    87
Goal "!!s. [| tsuffix s1 s ; tsuffix s2 s|] ==> tsuffix s2 s1 | tsuffix s1 s2";
mueller@4559
    88
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
mueller@4559
    89
by (REPEAT (etac conjE 1));
mueller@4559
    90
by (REPEAT (etac exE 1));
mueller@4559
    91
by (REPEAT (etac conjE 1));
mueller@4559
    92
by (hyp_subst_tac 1);
mueller@4559
    93
mueller@4559
    94
*)
mueller@4559
    95
mueller@4559
    96
mueller@4559
    97
section "TLA Rules by Lamport";
mueller@4559
    98
mueller@4559
    99
(* ---------------------------------------------------------------- *)
mueller@4559
   100
(*                      TLA Rules by Lamport                        *)
mueller@4559
   101
(* ---------------------------------------------------------------- *)
mueller@4559
   102
wenzelm@5068
   103
Goal "!! P. validT P ==> validT ([] P)";
mueller@4559
   104
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Box_def,tsuffix_def])1);
mueller@4559
   105
qed"STL1a";
mueller@4559
   106
wenzelm@5068
   107
Goal "!! P. valid P ==> validT (Init P)";
mueller@4559
   108
by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,Init_def])1);
mueller@4559
   109
qed"STL1b";
mueller@4559
   110
wenzelm@5068
   111
Goal "!! P. valid P ==> validT ([] (Init P))";
wenzelm@5132
   112
by (rtac STL1a 1);
wenzelm@5132
   113
by (etac STL1b 1);
mueller@4559
   114
qed"STL1";
mueller@4559
   115
mueller@4577
   116
mueller@4577
   117
mueller@4559
   118
(* Note that unlift and HD is not at all used !!! *)
wenzelm@5068
   119
Goal "!! P. valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))";
mueller@4559
   120
by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1);
mueller@4559
   121
qed"STL4";
mueller@4559
   122
mueller@4559
   123
mueller@4559
   124
section "LTL Axioms by Manna/Pnueli";
mueller@4559
   125
mueller@4559
   126
(* ---------------------------------------------------------------- *)
mueller@4559
   127
(*                LTL Axioms by Manna/Pnueli                        *)
mueller@4559
   128
(* ---------------------------------------------------------------- *)
mueller@4559
   129
mueller@4559
   130
wenzelm@5068
   131
Goalw [tsuffix_def,suffix_def]
mueller@4559
   132
"s~=UU & s~=nil --> tsuffix s2 (TL`s) --> tsuffix s2 s";
wenzelm@5132
   133
by Auto_tac;
mueller@4559
   134
by (Seq_case_simp_tac "s" 1);
mueller@4559
   135
by (res_inst_tac [("x","a>>s1")] exI 1);
wenzelm@5132
   136
by Auto_tac;
mueller@4559
   137
qed_spec_mp"tsuffix_TL";
mueller@4559
   138
mueller@4559
   139
val tsuffix_TL2 = conjI RS tsuffix_TL;
mueller@4559
   140
nipkow@4833
   141
Delsplits[split_if];
wenzelm@5068
   142
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def] 
mueller@4559
   143
   "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
wenzelm@5132
   144
by Auto_tac;
mueller@4559
   145
(* []F .--> F *)
mueller@4559
   146
by (eres_inst_tac [("x","s")] allE 1);
mueller@4559
   147
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
mueller@4559
   148
(* []F .--> Next [] F *)
nipkow@4833
   149
by (asm_full_simp_tac (simpset() addsplits [split_if]) 1);
wenzelm@5132
   150
by Auto_tac;
wenzelm@5132
   151
by (dtac tsuffix_TL2 1);
mueller@4559
   152
by (REPEAT (atac 1));
wenzelm@5132
   153
by Auto_tac;
mueller@4559
   154
qed"LTL1";
nipkow@4833
   155
Addsplits[split_if];
mueller@4559
   156
mueller@4559
   157
wenzelm@5068
   158
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
mueller@4559
   159
    "s |= .~ (Next F) .--> (Next (.~ F))";
nipkow@4833
   160
by (Asm_full_simp_tac 1);
mueller@4559
   161
qed"LTL2a";
mueller@4559
   162
wenzelm@5068
   163
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
mueller@4559
   164
    "s |= (Next (.~ F)) .--> (.~ (Next F))";
nipkow@4833
   165
by (Asm_full_simp_tac 1);
mueller@4559
   166
qed"LTL2b";
mueller@4559
   167
wenzelm@5068
   168
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
mueller@4559
   169
"ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)";
nipkow@4833
   170
by (Asm_full_simp_tac 1);
mueller@4559
   171
qed"LTL3";
mueller@4559
   172
wenzelm@5068
   173
Goalw [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def] 
mueller@4559
   174
 "s |= [] (F .--> Next F) .--> F .--> []F";
nipkow@4833
   175
by (Asm_full_simp_tac 1);
wenzelm@5132
   176
by Auto_tac;
mueller@4559
   177
mueller@4559
   178
mueller@4559
   179
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
wenzelm@5132
   180
by Auto_tac;
mueller@4559
   181
mueller@4559
   182
mueller@4577
   183
mueller@4577
   184
wenzelm@5068
   185
Goal "!! P. [| validT (P .--> Q); validT P |] ==> validT Q";
mueller@4577
   186
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1);
mueller@4577
   187
qed"ModusPonens";
mueller@4577
   188
mueller@4577
   189
(* works only if validT is defined without restriction to s~=UU, s~=nil *)
wenzelm@5068
   190
Goal "!! P. validT P ==> validT (Next P)";
mueller@4577
   191
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1);
nipkow@4681
   192
(* qed"NextTauto"; *)