author | wenzelm |
Wed, 28 Apr 2010 12:07:52 +0200 | |
changeset 36452 | d37c6eed8117 |
parent 35174 | e15040ae75d7 |
permissions | -rw-r--r-- |
4559 | 1 |
(* Title: HOLCF/IOA/meta_theory/TLS.thy |
12218 | 2 |
Author: Olaf Müller |
17233 | 3 |
*) |
4559 | 4 |
|
17233 | 5 |
header {* A General Temporal Logic *} |
4559 | 6 |
|
17233 | 7 |
theory TL |
8 |
imports Pred Sequence |
|
9 |
begin |
|
10 |
||
36452 | 11 |
default_sort type |
4559 | 12 |
|
13 |
types |
|
17233 | 14 |
'a temporal = "'a Seq predicate" |
4559 | 15 |
|
16 |
||
17233 | 17 |
consts |
4559 | 18 |
suffix :: "'a Seq => 'a Seq => bool" |
19 |
tsuffix :: "'a Seq => 'a Seq => bool" |
|
20 |
||
21 |
validT :: "'a Seq predicate => bool" |
|
22 |
||
23 |
unlift :: "'a lift => 'a" |
|
24 |
||
25 |
Init ::"'a predicate => 'a temporal" ("<_>" [0] 1000) |
|
26 |
||
27 |
Box ::"'a temporal => 'a temporal" ("[] (_)" [80] 80) |
|
28 |
Diamond ::"'a temporal => 'a temporal" ("<> (_)" [80] 80) |
|
17233 | 29 |
Next ::"'a temporal => 'a temporal" |
4559 | 30 |
Leadsto ::"'a temporal => 'a temporal => 'a temporal" (infixr "~>" 22) |
31 |
||
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19741
diff
changeset
|
32 |
notation (xsymbols) |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19741
diff
changeset
|
33 |
Box ("\<box> (_)" [80] 80) and |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19741
diff
changeset
|
34 |
Diamond ("\<diamond> (_)" [80] 80) and |
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
19741
diff
changeset
|
35 |
Leadsto (infixr "\<leadsto>" 22) |
17233 | 36 |
|
4559 | 37 |
defs |
38 |
||
17233 | 39 |
unlift_def: |
28524 | 40 |
"unlift x == (case x of Def y => y)" |
4559 | 41 |
|
42 |
(* this means that for nil and UU the effect is unpredictable *) |
|
17233 | 43 |
Init_def: |
44 |
"Init P s == (P (unlift (HD$s)))" |
|
4559 | 45 |
|
17233 | 46 |
suffix_def: |
47 |
"suffix s2 s == ? s1. (Finite s1 & s = s1 @@ s2)" |
|
4559 | 48 |
|
17233 | 49 |
tsuffix_def: |
4559 | 50 |
"tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s" |
51 |
||
17233 | 52 |
Box_def: |
4559 | 53 |
"([] P) s == ! s2. tsuffix s2 s --> P s2" |
54 |
||
17233 | 55 |
Next_def: |
10835 | 56 |
"(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)" |
4559 | 57 |
|
17233 | 58 |
Diamond_def: |
4559 | 59 |
"<> P == .~ ([] (.~ P))" |
60 |
||
17233 | 61 |
Leadsto_def: |
62 |
"P ~> Q == ([] (P .--> (<> Q)))" |
|
4559 | 63 |
|
17233 | 64 |
validT_def: |
4559 | 65 |
"validT P == ! s. s~=UU & s~=nil --> (s |= P)" |
66 |
||
19741 | 67 |
|
68 |
lemma simple: "[] <> (.~ P) = (.~ <> [] P)" |
|
69 |
apply (rule ext) |
|
70 |
apply (simp add: Diamond_def NOT_def Box_def) |
|
71 |
done |
|
72 |
||
73 |
lemma Boxnil: "nil |= [] P" |
|
74 |
apply (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc) |
|
75 |
done |
|
76 |
||
77 |
lemma Diamondnil: "~(nil |= <> P)" |
|
78 |
apply (simp add: Diamond_def satisfies_def NOT_def) |
|
79 |
apply (cut_tac Boxnil) |
|
80 |
apply (simp add: satisfies_def) |
|
81 |
done |
|
82 |
||
83 |
lemma Diamond_def2: "(<> F) s = (? s2. tsuffix s2 s & F s2)" |
|
84 |
apply (simp add: Diamond_def NOT_def Box_def) |
|
85 |
done |
|
86 |
||
87 |
||
88 |
||
89 |
subsection "TLA Axiomatization by Merz" |
|
90 |
||
91 |
lemma suffix_refl: "suffix s s" |
|
92 |
apply (simp add: suffix_def) |
|
93 |
apply (rule_tac x = "nil" in exI) |
|
94 |
apply auto |
|
95 |
done |
|
96 |
||
97 |
lemma reflT: "s~=UU & s~=nil --> (s |= [] F .--> F)" |
|
98 |
apply (simp add: satisfies_def IMPLIES_def Box_def) |
|
99 |
apply (rule impI)+ |
|
100 |
apply (erule_tac x = "s" in allE) |
|
101 |
apply (simp add: tsuffix_def suffix_refl) |
|
102 |
done |
|
103 |
||
104 |
||
105 |
lemma suffix_trans: "[| suffix y x ; suffix z y |] ==> suffix z x" |
|
106 |
apply (simp add: suffix_def) |
|
107 |
apply auto |
|
108 |
apply (rule_tac x = "s1 @@ s1a" in exI) |
|
109 |
apply auto |
|
110 |
apply (simp (no_asm) add: Conc_assoc) |
|
111 |
done |
|
112 |
||
113 |
lemma transT: "s |= [] F .--> [] [] F" |
|
114 |
apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def tsuffix_def) |
|
115 |
apply auto |
|
116 |
apply (drule suffix_trans) |
|
117 |
apply assumption |
|
118 |
apply (erule_tac x = "s2a" in allE) |
|
119 |
apply auto |
|
120 |
done |
|
121 |
||
122 |
||
123 |
lemma normalT: "s |= [] (F .--> G) .--> [] F .--> [] G" |
|
124 |
apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def) |
|
125 |
done |
|
126 |
||
127 |
||
128 |
subsection "TLA Rules by Lamport" |
|
129 |
||
130 |
lemma STL1a: "validT P ==> validT ([] P)" |
|
131 |
apply (simp add: validT_def satisfies_def Box_def tsuffix_def) |
|
132 |
done |
|
133 |
||
134 |
lemma STL1b: "valid P ==> validT (Init P)" |
|
135 |
apply (simp add: valid_def validT_def satisfies_def Init_def) |
|
136 |
done |
|
137 |
||
138 |
lemma STL1: "valid P ==> validT ([] (Init P))" |
|
139 |
apply (rule STL1a) |
|
140 |
apply (erule STL1b) |
|
141 |
done |
|
142 |
||
143 |
(* Note that unlift and HD is not at all used !!! *) |
|
144 |
lemma STL4: "valid (P .--> Q) ==> validT ([] (Init P) .--> [] (Init Q))" |
|
145 |
apply (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def) |
|
146 |
done |
|
147 |
||
148 |
||
149 |
subsection "LTL Axioms by Manna/Pnueli" |
|
150 |
||
151 |
lemma tsuffix_TL [rule_format (no_asm)]: |
|
152 |
"s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s" |
|
153 |
apply (unfold tsuffix_def suffix_def) |
|
154 |
apply auto |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
25131
diff
changeset
|
155 |
apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *}) |
19741 | 156 |
apply (rule_tac x = "a>>s1" in exI) |
157 |
apply auto |
|
158 |
done |
|
159 |
||
160 |
lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL] |
|
161 |
||
162 |
declare split_if [split del] |
|
163 |
lemma LTL1: |
|
164 |
"s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))" |
|
165 |
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def) |
|
166 |
apply auto |
|
167 |
(* []F .--> F *) |
|
168 |
apply (erule_tac x = "s" in allE) |
|
169 |
apply (simp add: tsuffix_def suffix_refl) |
|
170 |
(* []F .--> Next [] F *) |
|
171 |
apply (simp split add: split_if) |
|
172 |
apply auto |
|
173 |
apply (drule tsuffix_TL2) |
|
174 |
apply assumption+ |
|
175 |
apply auto |
|
176 |
done |
|
177 |
declare split_if [split] |
|
178 |
||
179 |
||
180 |
lemma LTL2a: |
|
181 |
"s |= .~ (Next F) .--> (Next (.~ F))" |
|
182 |
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def) |
|
183 |
apply simp |
|
184 |
done |
|
185 |
||
186 |
lemma LTL2b: |
|
187 |
"s |= (Next (.~ F)) .--> (.~ (Next F))" |
|
188 |
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def) |
|
189 |
apply simp |
|
190 |
done |
|
191 |
||
192 |
lemma LTL3: |
|
193 |
"ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)" |
|
194 |
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def) |
|
195 |
apply simp |
|
196 |
done |
|
197 |
||
198 |
||
199 |
lemma ModusPonens: "[| validT (P .--> Q); validT P |] ==> validT Q" |
|
200 |
apply (simp add: validT_def satisfies_def IMPLIES_def) |
|
201 |
done |
|
17233 | 202 |
|
203 |
end |