author | paulson |
Fri, 29 Jan 1999 16:23:56 +0100 | |
changeset 6161 | bc2a76ce1ea3 |
parent 5976 | 44290b71a85f |
child 10835 | f4745d77e620 |
permissions | -rw-r--r-- |
4559 | 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 |
||
5068 | 10 |
Goal "[] <> (.~ P) = (.~ <> [] P)"; |
5132 | 11 |
by (rtac ext 1); |
4559 | 12 |
by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1); |
5132 | 13 |
by Auto_tac; |
5976 | 14 |
qed"simple"; |
4559 | 15 |
|
5068 | 16 |
Goal "nil |= [] P"; |
4559 | 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 |
||
5068 | 21 |
Goal "~(nil |= <> P)"; |
4559 | 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 |
||
5068 | 27 |
Goal "(<> F) s = (? s2. tsuffix s2 s & F s2)"; |
4559 | 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 |
||
5068 | 39 |
Goal "suffix s s"; |
4559 | 40 |
by (simp_tac (simpset() addsimps [suffix_def])1); |
41 |
by (res_inst_tac [("x","nil")] exI 1); |
|
5132 | 42 |
by Auto_tac; |
4559 | 43 |
qed"suffix_refl"; |
44 |
||
5068 | 45 |
Goal "s~=UU & s~=nil --> (s |= [] F .--> F)"; |
4559 | 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 |
||
6161 | 53 |
Goal "[| suffix y x ; suffix z y |] ==> suffix z x"; |
4559 | 54 |
by (asm_full_simp_tac (simpset() addsimps [suffix_def])1); |
5132 | 55 |
by Auto_tac; |
4559 | 56 |
by (res_inst_tac [("x","s1 @@ s1a")] exI 1); |
5132 | 57 |
by Auto_tac; |
4559 | 58 |
by (simp_tac (simpset() addsimps [Conc_assoc]) 1); |
59 |
qed"suffix_trans"; |
|
60 |
||
5068 | 61 |
Goal "s |= [] F .--> [] [] F"; |
4559 | 62 |
by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def,tsuffix_def])1); |
5132 | 63 |
by Auto_tac; |
64 |
by (dtac suffix_trans 1); |
|
65 |
by (assume_tac 1); |
|
4559 | 66 |
by (eres_inst_tac [("x","s2a")] allE 1); |
5132 | 67 |
by Auto_tac; |
4559 | 68 |
qed"transT"; |
69 |
||
70 |
||
5068 | 71 |
Goal "s |= [] (F .--> G) .--> [] F .--> [] G"; |
4559 | 72 |
by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def])1); |
73 |
qed"normalT"; |
|
74 |
||
75 |
||
76 |
section "TLA Rules by Lamport"; |
|
77 |
||
78 |
(* ---------------------------------------------------------------- *) |
|
79 |
(* TLA Rules by Lamport *) |
|
80 |
(* ---------------------------------------------------------------- *) |
|
81 |
||
6161 | 82 |
Goal "validT P ==> validT ([] P)"; |
4559 | 83 |
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Box_def,tsuffix_def])1); |
84 |
qed"STL1a"; |
|
85 |
||
6161 | 86 |
Goal "valid P ==> validT (Init P)"; |
4559 | 87 |
by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,Init_def])1); |
88 |
qed"STL1b"; |
|
89 |
||
6161 | 90 |
Goal "valid P ==> validT ([] (Init P))"; |
5132 | 91 |
by (rtac STL1a 1); |
92 |
by (etac STL1b 1); |
|
4559 | 93 |
qed"STL1"; |
94 |
||
95 |
(* Note that unlift and HD is not at all used !!! *) |
|
6161 | 96 |
Goal "valid (P .--> Q) ==> validT ([] (Init P) .--> [] (Init Q))"; |
4559 | 97 |
by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1); |
98 |
qed"STL4"; |
|
99 |
||
100 |
||
101 |
section "LTL Axioms by Manna/Pnueli"; |
|
102 |
||
103 |
(* ---------------------------------------------------------------- *) |
|
104 |
(* LTL Axioms by Manna/Pnueli *) |
|
105 |
(* ---------------------------------------------------------------- *) |
|
106 |
||
107 |
||
5068 | 108 |
Goalw [tsuffix_def,suffix_def] |
4559 | 109 |
"s~=UU & s~=nil --> tsuffix s2 (TL`s) --> tsuffix s2 s"; |
5132 | 110 |
by Auto_tac; |
4559 | 111 |
by (Seq_case_simp_tac "s" 1); |
112 |
by (res_inst_tac [("x","a>>s1")] exI 1); |
|
5132 | 113 |
by Auto_tac; |
4559 | 114 |
qed_spec_mp"tsuffix_TL"; |
115 |
||
116 |
val tsuffix_TL2 = conjI RS tsuffix_TL; |
|
117 |
||
4833 | 118 |
Delsplits[split_if]; |
5068 | 119 |
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def] |
4559 | 120 |
"s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))"; |
5132 | 121 |
by Auto_tac; |
4559 | 122 |
(* []F .--> F *) |
123 |
by (eres_inst_tac [("x","s")] allE 1); |
|
124 |
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1); |
|
125 |
(* []F .--> Next [] F *) |
|
4833 | 126 |
by (asm_full_simp_tac (simpset() addsplits [split_if]) 1); |
5132 | 127 |
by Auto_tac; |
128 |
by (dtac tsuffix_TL2 1); |
|
4559 | 129 |
by (REPEAT (atac 1)); |
5132 | 130 |
by Auto_tac; |
4559 | 131 |
qed"LTL1"; |
4833 | 132 |
Addsplits[split_if]; |
4559 | 133 |
|
134 |
||
5068 | 135 |
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def] |
4559 | 136 |
"s |= .~ (Next F) .--> (Next (.~ F))"; |
4833 | 137 |
by (Asm_full_simp_tac 1); |
4559 | 138 |
qed"LTL2a"; |
139 |
||
5068 | 140 |
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def] |
4559 | 141 |
"s |= (Next (.~ F)) .--> (.~ (Next F))"; |
4833 | 142 |
by (Asm_full_simp_tac 1); |
4559 | 143 |
qed"LTL2b"; |
144 |
||
5068 | 145 |
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def] |
4559 | 146 |
"ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)"; |
4833 | 147 |
by (Asm_full_simp_tac 1); |
4559 | 148 |
qed"LTL3"; |
149 |
||
5068 | 150 |
Goalw [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def] |
4559 | 151 |
"s |= [] (F .--> Next F) .--> F .--> []F"; |
4833 | 152 |
by (Asm_full_simp_tac 1); |
5132 | 153 |
by Auto_tac; |
4559 | 154 |
|
155 |
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1); |
|
5132 | 156 |
by Auto_tac; |
4559 | 157 |
|
158 |
||
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
159 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
160 |
|
6161 | 161 |
Goal "[| validT (P .--> Q); validT P |] ==> validT Q"; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
162 |
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
163 |
qed"ModusPonens"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
164 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
165 |
(* works only if validT is defined without restriction to s~=UU, s~=nil *) |
6161 | 166 |
Goal "validT P ==> validT (Next P)"; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
167 |
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1); |
4681 | 168 |
(* qed"NextTauto"; *) |