44 goal thy "spies evs <= spies (Says A B X # evs)"; |
44 goal thy "spies evs <= spies (Says A B X # evs)"; |
45 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
45 by (simp_tac (simpset() addsimps [subset_insertI]) 1); |
46 qed "spies_subset_spies_Says"; |
46 qed "spies_subset_spies_Says"; |
47 |
47 |
48 goal thy "spies evs <= spies (Notes A X # evs)"; |
48 goal thy "spies evs <= spies (Notes A X # evs)"; |
49 by (simp_tac (simpset() addsplits [expand_if]) 1); |
49 by (Simp_tac 1); |
50 by (Fast_tac 1); |
50 by (Fast_tac 1); |
51 qed "spies_subset_spies_Notes"; |
51 qed "spies_subset_spies_Notes"; |
52 |
52 |
53 (*Spy sees all traffic*) |
53 (*Spy sees all traffic*) |
54 goal thy "Says A B X : set evs --> X : spies evs"; |
54 goal thy "Says A B X : set evs --> X : spies evs"; |
55 by (induct_tac "evs" 1); |
55 by (induct_tac "evs" 1); |
56 by (ALLGOALS (asm_simp_tac |
56 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); |
57 (simpset() addsplits [expand_event_case, expand_if]))); |
|
58 qed_spec_mp "Says_imp_spies"; |
57 qed_spec_mp "Says_imp_spies"; |
59 |
58 |
60 (*Spy sees Notes of bad agents*) |
59 (*Spy sees Notes of bad agents*) |
61 goal thy "Notes A X : set evs --> A: bad --> X : spies evs"; |
60 goal thy "Notes A X : set evs --> A: bad --> X : spies evs"; |
62 by (induct_tac "evs" 1); |
61 by (induct_tac "evs" 1); |
63 by (ALLGOALS (asm_simp_tac |
62 by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case]))); |
64 (simpset() addsplits [expand_event_case, expand_if]))); |
|
65 qed_spec_mp "Notes_imp_spies"; |
63 qed_spec_mp "Notes_imp_spies"; |
66 |
64 |
67 (*Use with addSEs to derive contradictions from old Says events containing |
65 (*Use with addSEs to derive contradictions from old Says events containing |
68 items known to be fresh*) |
66 items known to be fresh*) |
69 val spies_partsEs = make_elim (Says_imp_spies RS parts.Inj) :: partsEs; |
67 val spies_partsEs = make_elim (Says_imp_spies RS parts.Inj) :: partsEs; |
78 |
76 |
79 goal thy "parts (spies evs) <= used evs"; |
77 goal thy "parts (spies evs) <= used evs"; |
80 by (induct_tac "evs" 1); |
78 by (induct_tac "evs" 1); |
81 by (ALLGOALS (asm_simp_tac |
79 by (ALLGOALS (asm_simp_tac |
82 (simpset() addsimps [parts_insert_spies] |
80 (simpset() addsimps [parts_insert_spies] |
83 addsplits [expand_event_case, expand_if]))); |
81 addsplits [expand_event_case]))); |
84 by (ALLGOALS Blast_tac); |
82 by (ALLGOALS Blast_tac); |
85 qed "parts_spies_subset_used"; |
83 qed "parts_spies_subset_used"; |
86 |
84 |
87 bind_thm ("usedI", impOfSubs parts_spies_subset_used); |
85 bind_thm ("usedI", impOfSubs parts_spies_subset_used); |
88 AddIs [usedI]; |
86 AddIs [usedI]; |
89 |
87 |
90 goal thy "parts (initState B) <= used evs"; |
88 goal thy "parts (initState B) <= used evs"; |
91 by (induct_tac "evs" 1); |
89 by (induct_tac "evs" 1); |
92 by (ALLGOALS (asm_simp_tac |
90 by (ALLGOALS (asm_simp_tac |
93 (simpset() addsimps [parts_insert_spies] |
91 (simpset() addsimps [parts_insert_spies] |
94 addsplits [expand_event_case, expand_if]))); |
92 addsplits [expand_event_case]))); |
95 by (ALLGOALS Blast_tac); |
93 by (ALLGOALS Blast_tac); |
96 bind_thm ("initState_into_used", impOfSubs (result())); |
94 bind_thm ("initState_into_used", impOfSubs (result())); |
97 |
95 |
98 goal thy "used (Says A B X # evs) = parts{X} Un used evs"; |
96 goal thy "used (Says A B X # evs) = parts{X} Un used evs"; |
99 by (Simp_tac 1); |
97 by (Simp_tac 1); |