author | nipkow |
Mon, 27 Apr 1998 16:47:50 +0200 | |
changeset 4833 | 2e53109d4bc8 |
parent 4681 | a331c1f5a23e |
child 5068 | fb28eaa07e01 |
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 |
||
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 |
||
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
116 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
117 |
|
4559 | 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 |
||
4833 | 141 |
Delsplits[split_if]; |
4559 | 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 *) |
|
4833 | 149 |
by (asm_full_simp_tac (simpset() addsplits [split_if]) 1); |
4559 | 150 |
auto(); |
151 |
bd tsuffix_TL2 1; |
|
152 |
by (REPEAT (atac 1)); |
|
153 |
auto(); |
|
154 |
qed"LTL1"; |
|
4833 | 155 |
Addsplits[split_if]; |
4559 | 156 |
|
157 |
||
158 |
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] |
|
159 |
"s |= .~ (Next F) .--> (Next (.~ F))"; |
|
4833 | 160 |
by (Asm_full_simp_tac 1); |
4559 | 161 |
qed"LTL2a"; |
162 |
||
163 |
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] |
|
164 |
"s |= (Next (.~ F)) .--> (.~ (Next F))"; |
|
4833 | 165 |
by (Asm_full_simp_tac 1); |
4559 | 166 |
qed"LTL2b"; |
167 |
||
168 |
goalw thy [Next_def,satisfies_def,NOT_def,IMPLIES_def] |
|
169 |
"ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)"; |
|
4833 | 170 |
by (Asm_full_simp_tac 1); |
4559 | 171 |
qed"LTL3"; |
172 |
||
173 |
goalw thy [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def] |
|
174 |
"s |= [] (F .--> Next F) .--> F .--> []F"; |
|
4833 | 175 |
by (Asm_full_simp_tac 1); |
4559 | 176 |
auto(); |
177 |
||
178 |
||
179 |
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1); |
|
180 |
auto(); |
|
181 |
||
182 |
||
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
183 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
184 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
185 |
goal thy "!! P. [| validT (P .--> Q); validT P |] ==> validT Q"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
186 |
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
|
187 |
qed"ModusPonens"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
188 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
189 |
(* works only if validT is defined without restriction to s~=UU, s~=nil *) |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
190 |
goal thy "!! P. validT P ==> validT (Next P)"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
191 |
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1); |
4681 | 192 |
(* qed"NextTauto"; *) |