equal
deleted
inserted
replaced
105 (*Nobody can have used non-existent keys!*) |
105 (*Nobody can have used non-existent keys!*) |
106 goal thy "!!evs. evs : otway ==> \ |
106 goal thy "!!evs. evs : otway ==> \ |
107 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
107 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
108 by (parts_induct_tac 1); |
108 by (parts_induct_tac 1); |
109 (*Fake*) |
109 (*Fake*) |
110 by (best_tac |
110 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); |
111 (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
|
112 addIs [impOfSubs analz_subset_parts] |
|
113 addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] |
|
114 addss (simpset())) 1); |
|
115 (*OR1-3*) |
111 (*OR1-3*) |
116 by (ALLGOALS Blast_tac); |
112 by (ALLGOALS Blast_tac); |
117 qed_spec_mp "new_keys_not_used"; |
113 qed_spec_mp "new_keys_not_used"; |
118 |
114 |
119 bind_thm ("new_keys_not_analzd", |
115 bind_thm ("new_keys_not_analzd", |