205 |
205 |
206 subsection{*Lemmas about lists, for reasoning about Issues*} |
206 subsection{*Lemmas about lists, for reasoning about Issues*} |
207 |
207 |
208 lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)" |
208 lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)" |
209 apply (induct_tac "evs") |
209 apply (induct_tac "evs") |
|
210 apply (rename_tac [2] a b) |
210 apply (induct_tac [2] "a", auto) |
211 apply (induct_tac [2] "a", auto) |
211 done |
212 done |
212 |
213 |
213 lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs" |
214 lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs" |
214 apply (induct_tac "evs") |
215 apply (induct_tac "evs") |
|
216 apply (rename_tac [2] a b) |
215 apply (induct_tac [2] "a", auto) |
217 apply (induct_tac [2] "a", auto) |
216 done |
218 done |
217 |
219 |
218 lemma spies_Notes_rev: "spies (evs @ [Notes A X]) = |
220 lemma spies_Notes_rev: "spies (evs @ [Notes A X]) = |
219 (if A:bad then insert X (spies evs) else spies evs)" |
221 (if A:bad then insert X (spies evs) else spies evs)" |
220 apply (induct_tac "evs") |
222 apply (induct_tac "evs") |
|
223 apply (rename_tac [2] a b) |
221 apply (induct_tac [2] "a", auto) |
224 apply (induct_tac [2] "a", auto) |
222 done |
225 done |
223 |
226 |
224 lemma spies_evs_rev: "spies evs = spies (rev evs)" |
227 lemma spies_evs_rev: "spies evs = spies (rev evs)" |
225 apply (induct_tac "evs") |
228 apply (induct_tac "evs") |
|
229 apply (rename_tac [2] a b) |
226 apply (induct_tac [2] "a") |
230 apply (induct_tac [2] "a") |
227 apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev) |
231 apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev) |
228 done |
232 done |
229 |
233 |
230 lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono] |
234 lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono] |
231 |
235 |
232 lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs" |
236 lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs" |
233 apply (induct_tac "evs") |
237 apply (induct_tac "evs") |
|
238 apply (rename_tac [2] a b) |
234 apply (induct_tac [2] "a", auto) |
239 apply (induct_tac [2] "a", auto) |
235 txt{* Resembles @{text"used_subset_append"} in theory Event.*} |
240 txt{* Resembles @{text"used_subset_append"} in theory Event.*} |
236 done |
241 done |
237 |
242 |
238 lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono] |
243 lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono] |