src/HOLCF/IOA/meta_theory/TL.ML
author mueller
Wed Jan 14 16:38:04 1998 +0100 (1998-01-14)
changeset 4577 674b0b354feb
parent 4559 8e604d885b54
child 4681 a331c1f5a23e
permissions -rw-r--r--
added thms wrt weakening and strengthening in Abstraction;
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
mueller@4559
    10
goal thy "[] <> (.~ P) = (.~ <> [] P)";
mueller@4559
    11
br ext 1;
mueller@4559
    12
by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1);
mueller@4559
    13
auto();
mueller@4559
    14
qed"simple_try";
mueller@4559
    15
mueller@4559
    16
goal thy "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
mueller@4559
    21
goal thy "~(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
mueller@4559
    27
goal thy "(<> 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
mueller@4559
    39
goal thy "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);
mueller@4559
    42
auto();
mueller@4559
    43
qed"suffix_refl";
mueller@4559
    44
mueller@4559
    45
goal thy "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
mueller@4559
    53
goal thy "!!x. [| suffix y x ; suffix z y |]  ==> suffix z x";
mueller@4559
    54
by (asm_full_simp_tac (simpset() addsimps [suffix_def])1);
mueller@4559
    55
auto();
mueller@4559
    56
by (res_inst_tac [("x","s1 @@ s1a")] exI 1);
mueller@4559
    57
auto();
mueller@4559
    58
by (simp_tac (simpset() addsimps [Conc_assoc]) 1); 
mueller@4559
    59
qed"suffix_trans";
mueller@4559
    60
mueller@4559
    61
goal thy "s |= [] F .--> [] [] F";
mueller@4559
    62
by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def,tsuffix_def])1);
mueller@4559
    63
auto();
mueller@4559
    64
bd suffix_trans 1;
mueller@4559
    65
ba 1;
mueller@4559
    66
by (eres_inst_tac [("x","s2a")] allE 1);
mueller@4559
    67
auto();
mueller@4559
    68
qed"transT";
mueller@4559
    69
mueller@4559
    70
mueller@4559
    71
goal thy "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
(*
mueller@4559
    77
goal thy "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);
mueller@4559
    79
br impI 1;
mueller@4559
    80
be conjE 1;
mueller@4559
    81
be exE 1;
mueller@4559
    82
be exE 1;
mueller@4559
    83
mueller@4559
    84
mueller@4559
    85
br disjI1 1;
mueller@4559
    86
mueller@4559
    87
goal thy "!!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
mueller@4559
   103
goal thy "!! 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
mueller@4559
   107
goal thy "!! 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
mueller@4559
   111
goal thy "!! P. valid P ==> validT ([] (Init P))";
mueller@4559
   112
br STL1a 1;
mueller@4559
   113
be 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 !!! *)
mueller@4559
   119
goal thy "!! 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
mueller@4559
   131
goalw thy [tsuffix_def,suffix_def]
mueller@4559
   132
"s~=UU & s~=nil --> tsuffix s2 (TL`s) --> tsuffix s2 s";
mueller@4559
   133
auto();
mueller@4559
   134
by (Seq_case_simp_tac "s" 1);
mueller@4559
   135
by (res_inst_tac [("x","a>>s1")] exI 1);
mueller@4559
   136
auto();
mueller@4559
   137
qed_spec_mp"tsuffix_TL";
mueller@4559
   138
mueller@4559
   139
val tsuffix_TL2 = conjI RS tsuffix_TL;
mueller@4559
   140
mueller@4559
   141
mueller@4559
   142
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def] 
mueller@4559
   143
   "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
mueller@4559
   144
auto();
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 *)
mueller@4559
   149
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
mueller@4559
   150
auto();
mueller@4559
   151
bd tsuffix_TL2 1;
mueller@4559
   152
by (REPEAT (atac 1));
mueller@4559
   153
auto();
mueller@4559
   154
qed"LTL1";
mueller@4559
   155
mueller@4559
   156
mueller@4559
   157
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
mueller@4559
   158
    "s |= .~ (Next F) .--> (Next (.~ F))";
mueller@4559
   159
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
mueller@4559
   160
qed"LTL2a";
mueller@4559
   161
mueller@4559
   162
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
mueller@4559
   163
    "s |= (Next (.~ F)) .--> (.~ (Next F))";
mueller@4559
   164
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
mueller@4559
   165
qed"LTL2b";
mueller@4559
   166
mueller@4559
   167
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
mueller@4559
   168
"ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)";
mueller@4559
   169
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
mueller@4559
   170
qed"LTL3";
mueller@4559
   171
mueller@4559
   172
goalw thy [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def] 
mueller@4559
   173
 "s |= [] (F .--> Next F) .--> F .--> []F";
mueller@4559
   174
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
mueller@4559
   175
auto();
mueller@4559
   176
mueller@4559
   177
mueller@4559
   178
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
mueller@4559
   179
auto();
mueller@4559
   180
mueller@4559
   181
mueller@4577
   182
mueller@4577
   183
mueller@4577
   184
goal thy "!! P. [| validT (P .--> Q); validT P |] ==> validT Q";
mueller@4577
   185
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1);
mueller@4577
   186
qed"ModusPonens";
mueller@4577
   187
mueller@4577
   188
(* works only if validT is defined without restriction to s~=UU, s~=nil *)
mueller@4577
   189
goal thy "!! P. validT P ==> validT (Next P)";
mueller@4577
   190
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1);
mueller@4577
   191
(* qed"NextTauto"; *)