# HG changeset patch # User berghofe # Date 1210150759 -7200 # Node ID da662ff93503f099207e4e06ae2d470331266086 # Parent d334a6d695982c16996e5bb2bc7c33cd8c93bc01 - Instantiated parts_insert_substD to avoid problems with HO unification - Replaced auto by fastsimp in proof of parts_invKey, since auto looped because of the new encoding of sets diff -r d334a6d69598 -r da662ff93503 src/HOL/Auth/Guard/Extensions.thy --- a/src/HOL/Auth/Guard/Extensions.thy Wed May 07 10:59:18 2008 +0200 +++ b/src/HOL/Auth/Guard/Extensions.thy Wed May 07 10:59:19 2008 +0200 @@ -206,7 +206,7 @@ lemma parts_invKey [rule_format,dest]:"X:parts {Y} ==> X:analz (insert (Crypt K Y) H) --> X ~:analz H --> Key (invKey K):analz H" -by (erule parts.induct, auto dest: parts.Fst parts.Snd parts.Body) +by (erule parts.induct, (fastsimp dest: parts.Fst parts.Snd parts.Body)+) lemma in_analz: "Y:analz H ==> EX X. X:H & Y:parts {X}" by (erule analz.induct, auto intro: parts.Fst parts.Snd parts.Body) @@ -215,7 +215,7 @@ lemma Crypt_synth_insert: "[| Crypt K X:parts (insert Y H); Y:synth (analz H); Key K ~:analz H |] ==> Crypt K X:parts H" -apply (drule parts_insert_substD, clarify) +apply (drule parts_insert_substD [where P="%S. Crypt K X : S"], clarify) apply (frule in_sub) apply (frule parts_mono) by auto