231 by (erule analz.induct, auto dest: kparts_analz_sub) |
231 by (erule analz.induct, auto dest: kparts_analz_sub) |
232 |
232 |
233 lemma analz_kparts_analz: "X:analz (kparts H) ==> X:analz H" |
233 lemma analz_kparts_analz: "X:analz (kparts H) ==> X:analz H" |
234 by (erule analz.induct, auto dest: kparts_analz) |
234 by (erule analz.induct, auto dest: kparts_analz) |
235 |
235 |
236 lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==> |
236 lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==> X:analz (kparts {Z} Un kparts H)" |
237 X:analz (kparts {Z} Un kparts H)" |
|
238 by (rule analz_sub, auto) |
237 by (rule analz_sub, auto) |
239 |
238 |
240 lemma Nonce_kparts_synth [rule_format]: "Y:synth (analz G) |
239 lemma Nonce_kparts_synth [rule_format]: "Y:synth (analz G) |
241 ==> Nonce n:kparts {Y} --> Nonce n:analz G" |
240 ==> Nonce n:kparts {Y} --> Nonce n:analz G" |
242 by (erule synth.induct, auto) |
241 by (erule synth.induct, auto) |
245 Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Y:parts G" |
244 Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Y:parts G" |
246 apply (drule parts_insert_substD [where P="%S. Y : S"], clarify) |
245 apply (drule parts_insert_substD [where P="%S. Y : S"], clarify) |
247 apply (drule in_sub, drule_tac X=Y in parts_sub, simp) |
246 apply (drule in_sub, drule_tac X=Y in parts_sub, simp) |
248 by (auto dest: Nonce_kparts_synth) |
247 by (auto dest: Nonce_kparts_synth) |
249 |
248 |
250 lemma Crypt_insert_synth: "[| Crypt K Y:parts (insert X G); X:synth (analz G); |
249 lemma Crypt_insert_synth: |
251 Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Crypt K Y:parts G" |
250 "[| Crypt K Y:parts (insert X G); X:synth (analz G); Nonce n:kparts {Y}; Nonce n ~:analz G |] |
252 apply (drule parts_insert_substD [where P="%S. Crypt K Y : S"], clarify) |
251 ==> Crypt K Y:parts G" |
253 apply (drule in_sub, drule_tac X="Crypt K Y" in parts_sub, simp, clarsimp) |
252 by (metis Fake_parts_insert_in_Un Nonce_kparts_synth UnE analz_conj_parts synth_simps(5)) |
254 apply (ind_cases "Crypt K Y:synth (analz G)") |
253 |
255 by (auto dest: Nonce_kparts_synth) |
|
256 |
254 |
257 subsection{*analz is pparts + analz of kparts*} |
255 subsection{*analz is pparts + analz of kparts*} |
258 |
256 |
259 lemma analz_pparts_kparts: "X:analz H ==> X:pparts H | X:analz (kparts H)" |
257 lemma analz_pparts_kparts: "X:analz H ==> X:pparts H | X:analz (kparts H)" |
260 apply (erule analz.induct) |
258 by (erule analz.induct, auto) |
261 apply (rule_tac X=X in is_MPairE, blast, blast) |
|
262 apply (erule disjE, rule_tac X=X in is_MPairE, blast, blast, blast) |
|
263 by (erule disjE, rule_tac X=Y in is_MPairE, blast+) |
|
264 |
259 |
265 lemma analz_pparts_kparts_eq: "analz H = pparts H Un analz (kparts H)" |
260 lemma analz_pparts_kparts_eq: "analz H = pparts H Un analz (kparts H)" |
266 by (rule eq, auto dest: analz_pparts_kparts pparts_analz analz_kparts_analz) |
261 by (rule eq, auto dest: analz_pparts_kparts pparts_analz analz_kparts_analz) |
267 |
262 |
268 lemmas analz_pparts_kparts_substI = analz_pparts_kparts_eq [THEN ssubst] |
263 lemmas analz_pparts_kparts_substI = analz_pparts_kparts_eq [THEN ssubst] |
269 lemmas analz_pparts_kparts_substD |
264 lemmas analz_pparts_kparts_substD = analz_pparts_kparts_eq [THEN sym, THEN ssubst] |
270 = analz_pparts_kparts_eq [THEN sym, THEN ssubst] |
|
271 |
265 |
272 end |
266 end |