48 by (eres_inst_tac [("x","s")] allE 1); |
48 by (eres_inst_tac [("x","s")] allE 1); |
49 by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1); |
49 by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1); |
50 qed"reflT"; |
50 qed"reflT"; |
51 |
51 |
52 |
52 |
53 Goal "!!x. [| suffix y x ; suffix z y |] ==> suffix z x"; |
53 Goal "[| suffix y x ; suffix z y |] ==> suffix z x"; |
54 by (asm_full_simp_tac (simpset() addsimps [suffix_def])1); |
54 by (asm_full_simp_tac (simpset() addsimps [suffix_def])1); |
55 by Auto_tac; |
55 by Auto_tac; |
56 by (res_inst_tac [("x","s1 @@ s1a")] exI 1); |
56 by (res_inst_tac [("x","s1 @@ s1a")] exI 1); |
57 by Auto_tac; |
57 by Auto_tac; |
58 by (simp_tac (simpset() addsimps [Conc_assoc]) 1); |
58 by (simp_tac (simpset() addsimps [Conc_assoc]) 1); |
77 |
77 |
78 (* ---------------------------------------------------------------- *) |
78 (* ---------------------------------------------------------------- *) |
79 (* TLA Rules by Lamport *) |
79 (* TLA Rules by Lamport *) |
80 (* ---------------------------------------------------------------- *) |
80 (* ---------------------------------------------------------------- *) |
81 |
81 |
82 Goal "!! P. validT P ==> validT ([] P)"; |
82 Goal "validT P ==> validT ([] P)"; |
83 by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Box_def,tsuffix_def])1); |
83 by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Box_def,tsuffix_def])1); |
84 qed"STL1a"; |
84 qed"STL1a"; |
85 |
85 |
86 Goal "!! P. valid P ==> validT (Init P)"; |
86 Goal "valid P ==> validT (Init P)"; |
87 by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,Init_def])1); |
87 by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,Init_def])1); |
88 qed"STL1b"; |
88 qed"STL1b"; |
89 |
89 |
90 Goal "!! P. valid P ==> validT ([] (Init P))"; |
90 Goal "valid P ==> validT ([] (Init P))"; |
91 by (rtac STL1a 1); |
91 by (rtac STL1a 1); |
92 by (etac STL1b 1); |
92 by (etac STL1b 1); |
93 qed"STL1"; |
93 qed"STL1"; |
94 |
94 |
95 (* Note that unlift and HD is not at all used !!! *) |
95 (* Note that unlift and HD is not at all used !!! *) |
96 Goal "!! P. valid (P .--> Q) ==> validT ([] (Init P) .--> [] (Init Q))"; |
96 Goal "valid (P .--> Q) ==> validT ([] (Init P) .--> [] (Init Q))"; |
97 by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1); |
97 by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1); |
98 qed"STL4"; |
98 qed"STL4"; |
99 |
99 |
100 |
100 |
101 section "LTL Axioms by Manna/Pnueli"; |
101 section "LTL Axioms by Manna/Pnueli"; |
156 by Auto_tac; |
156 by Auto_tac; |
157 |
157 |
158 |
158 |
159 |
159 |
160 |
160 |
161 Goal "!! P. [| validT (P .--> Q); validT P |] ==> validT Q"; |
161 Goal "[| validT (P .--> Q); validT P |] ==> validT Q"; |
162 by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1); |
162 by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1); |
163 qed"ModusPonens"; |
163 qed"ModusPonens"; |
164 |
164 |
165 (* works only if validT is defined without restriction to s~=UU, s~=nil *) |
165 (* works only if validT is defined without restriction to s~=UU, s~=nil *) |
166 Goal "!! P. validT P ==> validT (Next P)"; |
166 Goal "validT P ==> validT (Next P)"; |
167 by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1); |
167 by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1); |
168 (* qed"NextTauto"; *) |
168 (* qed"NextTauto"; *) |