equal
deleted
inserted
replaced
481 analz (insert (Crypt K X) H) = |
481 analz (insert (Crypt K X) H) = |
482 insert (Crypt K X) (analz (insert X H))" |
482 insert (Crypt K X) (analz (insert X H))" |
483 by (intro equalityI lemma1 lemma2) |
483 by (intro equalityI lemma1 lemma2) |
484 |
484 |
485 text{*Case analysis: either the message is secure, or it is not! Effective, |
485 text{*Case analysis: either the message is secure, or it is not! Effective, |
486 but can cause subgoals to blow up! Use with @{text "split_if"}; apparently |
486 but can cause subgoals to blow up! Use with @{text "if_split"}; apparently |
487 @{text "split_tac"} does not cope with patterns such as @{term"analz (insert |
487 @{text "split_tac"} does not cope with patterns such as @{term"analz (insert |
488 (Crypt K X) H)"} *} |
488 (Crypt K X) H)"} *} |
489 lemma analz_Crypt_if [simp]: |
489 lemma analz_Crypt_if [simp]: |
490 "analz (insert (Crypt K X) H) = |
490 "analz (insert (Crypt K X) H) = |
491 (if (Key (invKey K) \<in> analz H) |
491 (if (Key (invKey K) \<in> analz H) |