137 |
137 |
138 subsection{*Lemmas for reasoning about predicate "Issues"*} |
138 subsection{*Lemmas for reasoning about predicate "Issues"*} |
139 |
139 |
140 lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)" |
140 lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)" |
141 apply (induct_tac "evs") |
141 apply (induct_tac "evs") |
|
142 apply (rename_tac [2] a b) |
142 apply (induct_tac [2] "a", auto) |
143 apply (induct_tac [2] "a", auto) |
143 done |
144 done |
144 |
145 |
145 lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs" |
146 lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs" |
146 apply (induct_tac "evs") |
147 apply (induct_tac "evs") |
|
148 apply (rename_tac [2] a b) |
147 apply (induct_tac [2] "a", auto) |
149 apply (induct_tac [2] "a", auto) |
148 done |
150 done |
149 |
151 |
150 lemma spies_Notes_rev: "spies (evs @ [Notes A X]) = |
152 lemma spies_Notes_rev: "spies (evs @ [Notes A X]) = |
151 (if A:bad then insert X (spies evs) else spies evs)" |
153 (if A:bad then insert X (spies evs) else spies evs)" |
152 apply (induct_tac "evs") |
154 apply (induct_tac "evs") |
|
155 apply (rename_tac [2] a b) |
153 apply (induct_tac [2] "a", auto) |
156 apply (induct_tac [2] "a", auto) |
154 done |
157 done |
155 |
158 |
156 lemma spies_evs_rev: "spies evs = spies (rev evs)" |
159 lemma spies_evs_rev: "spies evs = spies (rev evs)" |
157 apply (induct_tac "evs") |
160 apply (induct_tac "evs") |
|
161 apply (rename_tac [2] a b) |
158 apply (induct_tac [2] "a") |
162 apply (induct_tac [2] "a") |
159 apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev) |
163 apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev) |
160 done |
164 done |
161 |
165 |
162 lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono] |
166 lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono] |
163 |
167 |
164 lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs" |
168 lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs" |
165 apply (induct_tac "evs") |
169 apply (induct_tac "evs") |
|
170 apply (rename_tac [2] a b) |
166 apply (induct_tac [2] "a", auto) |
171 apply (induct_tac [2] "a", auto) |
167 txt{* Resembles @{text"used_subset_append"} in theory Event.*} |
172 txt{* Resembles @{text"used_subset_append"} in theory Event.*} |
168 done |
173 done |
169 |
174 |
170 lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono] |
175 lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono] |
172 |
177 |
173 text{*Lemmas for reasoning about predicate "before"*} |
178 text{*Lemmas for reasoning about predicate "before"*} |
174 lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)" |
179 lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)" |
175 apply (induct_tac "evs") |
180 apply (induct_tac "evs") |
176 apply simp |
181 apply simp |
|
182 apply (rename_tac a b) |
177 apply (induct_tac "a") |
183 apply (induct_tac "a") |
178 apply auto |
184 apply auto |
179 done |
185 done |
180 |
186 |
181 lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)" |
187 lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)" |
182 apply (induct_tac "evs") |
188 apply (induct_tac "evs") |
183 apply simp |
189 apply simp |
|
190 apply (rename_tac a b) |
184 apply (induct_tac "a") |
191 apply (induct_tac "a") |
185 apply auto |
192 apply auto |
186 done |
193 done |
187 |
194 |
188 lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs" |
195 lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs" |
189 apply (induct_tac "evs") |
196 apply (induct_tac "evs") |
190 apply simp |
197 apply simp |
|
198 apply (rename_tac a b) |
191 apply (induct_tac "a") |
199 apply (induct_tac "a") |
192 apply auto |
200 apply auto |
193 done |
201 done |
194 |
202 |
195 lemma used_evs_rev: "used evs = used (rev evs)" |
203 lemma used_evs_rev: "used evs = used (rev evs)" |
196 apply (induct_tac "evs") |
204 apply (induct_tac "evs") |
197 apply simp |
205 apply simp |
|
206 apply (rename_tac a b) |
198 apply (induct_tac "a") |
207 apply (induct_tac "a") |
199 apply (simp add: used_Says_rev) |
208 apply (simp add: used_Says_rev) |
200 apply (simp add: used_Gets_rev) |
209 apply (simp add: used_Gets_rev) |
201 apply (simp add: used_Notes_rev) |
210 apply (simp add: used_Notes_rev) |
202 done |
211 done |
203 |
212 |
204 lemma used_takeWhile_used [rule_format]: |
213 lemma used_takeWhile_used [rule_format]: |
205 "x : used (takeWhile P X) --> x : used X" |
214 "x : used (takeWhile P X) --> x : used X" |
206 apply (induct_tac "X") |
215 apply (induct_tac "X") |
207 apply simp |
216 apply simp |
|
217 apply (rename_tac a b) |
208 apply (induct_tac "a") |
218 apply (induct_tac "a") |
209 apply (simp_all add: used_Nil) |
219 apply (simp_all add: used_Nil) |
210 apply (blast dest!: initState_into_used)+ |
220 apply (blast dest!: initState_into_used)+ |
211 done |
221 done |
212 |
222 |