1.1 --- a/src/HOL/Auth/Guard/Analz.thy	Wed Sep 08 13:25:22 2010 +0200
     1.2 +++ b/src/HOL/Auth/Guard/Analz.thy	Wed Sep 08 13:30:41 2010 +0100
     1.3 @@ -233,8 +233,7 @@
     1.4  lemma analz_kparts_analz: "X:analz (kparts H) ==> X:analz H"
     1.5  by (erule analz.induct, auto dest: kparts_analz)
     1.6  
     1.7 -lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==>
     1.8 -X:analz (kparts {Z} Un kparts H)"
     1.9 +lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==> X:analz (kparts {Z} Un kparts H)"
    1.10  by (rule analz_sub, auto)
    1.11  
    1.12  lemma Nonce_kparts_synth [rule_format]: "Y:synth (analz G)
    1.13 @@ -247,26 +246,21 @@
    1.14  apply (drule in_sub, drule_tac X=Y in parts_sub, simp)
    1.15  by (auto dest: Nonce_kparts_synth)
    1.16  
    1.17 -lemma Crypt_insert_synth: "[| Crypt K Y:parts (insert X G); X:synth (analz G);
    1.18 -Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Crypt K Y:parts G"
    1.19 -apply (drule parts_insert_substD [where P="%S. Crypt K Y : S"], clarify)
    1.20 -apply (drule in_sub, drule_tac X="Crypt K Y" in parts_sub, simp, clarsimp)
    1.21 -apply (ind_cases "Crypt K Y:synth (analz G)")
    1.22 -by (auto dest: Nonce_kparts_synth)
    1.23 +lemma Crypt_insert_synth:
    1.24 +  "[| Crypt K Y:parts (insert X G); X:synth (analz G); Nonce n:kparts {Y}; Nonce n ~:analz G |] 
    1.25 +   ==> Crypt K Y:parts G"
    1.26 +by (metis Fake_parts_insert_in_Un Nonce_kparts_synth UnE analz_conj_parts synth_simps(5))
    1.27 +
    1.28  
    1.29  subsection{*analz is pparts + analz of kparts*}
    1.30  
    1.31  lemma analz_pparts_kparts: "X:analz H ==> X:pparts H | X:analz (kparts H)"
    1.32 -apply (erule analz.induct)
    1.33 -apply (rule_tac X=X in is_MPairE, blast, blast)
    1.34 -apply (erule disjE, rule_tac X=X in is_MPairE, blast, blast, blast)
    1.35 -by (erule disjE, rule_tac X=Y in is_MPairE, blast+)
    1.36 +by (erule analz.induct, auto) 
    1.37  
    1.38  lemma analz_pparts_kparts_eq: "analz H = pparts H Un analz (kparts H)"
    1.39  by (rule eq, auto dest: analz_pparts_kparts pparts_analz analz_kparts_analz)
    1.40  
    1.41  lemmas analz_pparts_kparts_substI = analz_pparts_kparts_eq [THEN ssubst]
    1.42 -lemmas analz_pparts_kparts_substD
    1.43 -= analz_pparts_kparts_eq [THEN sym, THEN ssubst]
    1.44 +lemmas analz_pparts_kparts_substD = analz_pparts_kparts_eq [THEN sym, THEN ssubst]
    1.45  
    1.46  end

     2.1 --- a/src/HOL/Auth/Guard/Guard_Yahalom.thy	Wed Sep 08 13:25:22 2010 +0200
     2.2 +++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Wed Sep 08 13:30:41 2010 +0100
     2.3 @@ -11,7 +11,7 @@
     2.4  
     2.5  header{*Yahalom Protocol*}
     2.6  
     2.7 -theory Guard_Yahalom imports Guard_Shared begin
     2.8 +theory Guard_Yahalom imports "../Shared" Guard_Shared begin
     2.9  
    2.10  subsection{*messages used in the protocol*}
    2.11  

     3.1 --- a/src/HOL/Auth/Guard/P1.thy	Wed Sep 08 13:25:22 2010 +0200
     3.2 +++ b/src/HOL/Auth/Guard/P1.thy	Wed Sep 08 13:30:41 2010 +0100
     3.3 @@ -15,7 +15,7 @@
     3.4  
     3.5  header{*Protocol P1*}
     3.6  
     3.7 -theory P1 imports Guard_Public List_Msg begin
     3.8 +theory P1 imports "../Public" Guard_Public List_Msg begin
     3.9  
    3.10  subsection{*Protocol Definition*}
    3.11  

     4.1 --- a/src/HOL/Auth/Message.thy	Wed Sep 08 13:25:22 2010 +0200
     4.2 +++ b/src/HOL/Auth/Message.thy	Wed Sep 08 13:30:41 2010 +0100
     4.3 @@ -582,12 +582,13 @@
     4.4  
     4.5  text{*NO @{text Agent_synth}, as any Agent name can be synthesized.  
     4.6    The same holds for @{term Number}*}
     4.7 -inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
     4.8 -inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
     4.9 -inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
    4.10 -inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
    4.11 -inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
    4.12  
    4.13 +inductive_simps synth_simps [iff]:
    4.14 + "Nonce n \<in> synth H"
    4.15 + "Key K \<in> synth H"
    4.16 + "Hash X \<in> synth H"
    4.17 + "{|X,Y|} \<in> synth H"
    4.18 + "Crypt K X \<in> synth H"
    4.19  
    4.20  lemma synth_increasing: "H \<subseteq> synth(H)"
    4.21  by blast
    4.22 @@ -605,7 +606,7 @@
    4.23  subsubsection{*Idempotence and transitivity *}
    4.24  
    4.25  lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
    4.26 -by (erule synth.induct, blast+)
    4.27 +by (erule synth.induct, auto)
    4.28  
    4.29  lemma synth_idem: "synth (synth H) = synth H"
    4.30  by blast
    4.31 @@ -782,7 +783,7 @@
    4.32       "X \<notin> synth (analz H)  
    4.33      ==> (Hash[X] Y \<in> synth (analz H)) =  
    4.34          (Hash {|X, Y|} \<in> analz H & Y \<in> synth (analz H))"
    4.35 -by (simp add: HPair_def)
    4.36 +by (auto simp add: HPair_def)
    4.37  
    4.38  
    4.39  text{*We do NOT want Crypt... messages broken up in protocols!!*}

     5.1 --- a/src/HOL/Auth/Shared.thy	Wed Sep 08 13:25:22 2010 +0200
     5.2 +++ b/src/HOL/Auth/Shared.thy	Wed Sep 08 13:30:41 2010 +0100
     5.3 @@ -12,7 +12,7 @@
     5.4  begin
     5.5  
     5.6  consts
     5.7 -  shrK    :: "agent => key"  (*symmetric keys*);
     5.8 +  shrK    :: "agent => key"  (*symmetric keys*)
     5.9  
    5.10  specification (shrK)
    5.11    inj_shrK: "inj shrK"
    5.12 @@ -59,7 +59,7 @@
    5.13  (*Specialized to shared-key model: no @{term invKey}*)
    5.14  lemma keysFor_parts_insert:
    5.15       "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |]
    5.16 -      ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
    5.17 +      ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H"
    5.18  by (force dest: Event.keysFor_parts_insert)  
    5.19  
    5.20  lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"