src/HOLCF/IOA/meta_theory/TL.ML
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 6161 bc2a76ce1ea3
child 12218 6597093b77e7
permissions -rw-r--r--
` -> $
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@5976
    14
qed"simple";
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
paulson@6161
    53
Goal "[| 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
section "TLA Rules by Lamport";
mueller@4559
    77
mueller@4559
    78
(* ---------------------------------------------------------------- *)
mueller@4559
    79
(*                      TLA Rules by Lamport                        *)
mueller@4559
    80
(* ---------------------------------------------------------------- *)
mueller@4559
    81
paulson@6161
    82
Goal "validT P ==> validT ([] P)";
mueller@4559
    83
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Box_def,tsuffix_def])1);
mueller@4559
    84
qed"STL1a";
mueller@4559
    85
paulson@6161
    86
Goal "valid P ==> validT (Init P)";
mueller@4559
    87
by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,Init_def])1);
mueller@4559
    88
qed"STL1b";
mueller@4559
    89
paulson@6161
    90
Goal "valid P ==> validT ([] (Init P))";
wenzelm@5132
    91
by (rtac STL1a 1);
wenzelm@5132
    92
by (etac STL1b 1);
mueller@4559
    93
qed"STL1";
mueller@4559
    94
mueller@4559
    95
(* Note that unlift and HD is not at all used !!! *)
paulson@6161
    96
Goal "valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))";
mueller@4559
    97
by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1);
mueller@4559
    98
qed"STL4";
mueller@4559
    99
mueller@4559
   100
mueller@4559
   101
section "LTL Axioms by Manna/Pnueli";
mueller@4559
   102
mueller@4559
   103
(* ---------------------------------------------------------------- *)
mueller@4559
   104
(*                LTL Axioms by Manna/Pnueli                        *)
mueller@4559
   105
(* ---------------------------------------------------------------- *)
mueller@4559
   106
mueller@4559
   107
wenzelm@5068
   108
Goalw [tsuffix_def,suffix_def]
nipkow@10835
   109
"s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s";
wenzelm@5132
   110
by Auto_tac;
mueller@4559
   111
by (Seq_case_simp_tac "s" 1);
mueller@4559
   112
by (res_inst_tac [("x","a>>s1")] exI 1);
wenzelm@5132
   113
by Auto_tac;
mueller@4559
   114
qed_spec_mp"tsuffix_TL";
mueller@4559
   115
mueller@4559
   116
val tsuffix_TL2 = conjI RS tsuffix_TL;
mueller@4559
   117
nipkow@4833
   118
Delsplits[split_if];
wenzelm@5068
   119
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def] 
mueller@4559
   120
   "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
wenzelm@5132
   121
by Auto_tac;
mueller@4559
   122
(* []F .--> F *)
mueller@4559
   123
by (eres_inst_tac [("x","s")] allE 1);
mueller@4559
   124
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
mueller@4559
   125
(* []F .--> Next [] F *)
nipkow@4833
   126
by (asm_full_simp_tac (simpset() addsplits [split_if]) 1);
wenzelm@5132
   127
by Auto_tac;
wenzelm@5132
   128
by (dtac tsuffix_TL2 1);
mueller@4559
   129
by (REPEAT (atac 1));
wenzelm@5132
   130
by Auto_tac;
mueller@4559
   131
qed"LTL1";
nipkow@4833
   132
Addsplits[split_if];
mueller@4559
   133
mueller@4559
   134
wenzelm@5068
   135
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
mueller@4559
   136
    "s |= .~ (Next F) .--> (Next (.~ F))";
nipkow@4833
   137
by (Asm_full_simp_tac 1);
mueller@4559
   138
qed"LTL2a";
mueller@4559
   139
wenzelm@5068
   140
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
mueller@4559
   141
    "s |= (Next (.~ F)) .--> (.~ (Next F))";
nipkow@4833
   142
by (Asm_full_simp_tac 1);
mueller@4559
   143
qed"LTL2b";
mueller@4559
   144
wenzelm@5068
   145
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def] 
mueller@4559
   146
"ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)";
nipkow@4833
   147
by (Asm_full_simp_tac 1);
mueller@4559
   148
qed"LTL3";
mueller@4559
   149
wenzelm@5068
   150
Goalw [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def] 
mueller@4559
   151
 "s |= [] (F .--> Next F) .--> F .--> []F";
nipkow@4833
   152
by (Asm_full_simp_tac 1);
wenzelm@5132
   153
by Auto_tac;
mueller@4559
   154
mueller@4559
   155
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
wenzelm@5132
   156
by Auto_tac;
mueller@4559
   157
mueller@4559
   158
mueller@4577
   159
mueller@4577
   160
paulson@6161
   161
Goal "[| validT (P .--> Q); validT P |] ==> validT Q";
mueller@4577
   162
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1);
mueller@4577
   163
qed"ModusPonens";
mueller@4577
   164
mueller@4577
   165
(* works only if validT is defined without restriction to s~=UU, s~=nil *)
paulson@6161
   166
Goal "validT P ==> validT (Next P)";
mueller@4577
   167
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1);
nipkow@4681
   168
(* qed"NextTauto"; *)