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