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