# HG changeset patch
# User paulson
# Date 1283948732 -3600
# Node ID 62332b382dbad0f778ba9ad1c2df84884285459e
# Parent  297cd703f1f0738f63d3a06678f522d584d33675
tidied using inductive_simps

diff -r 297cd703f1f0 -r 62332b382dba src/HOL/Auth/Guard/Analz.thy
--- a/src/HOL/Auth/Guard/Analz.thy	Wed Sep 08 10:45:55 2010 +0200
+++ b/src/HOL/Auth/Guard/Analz.thy	Wed Sep 08 13:25:32 2010 +0100
@@ -233,8 +233,7 @@
 lemma analz_kparts_analz: "X:analz (kparts H) ==> X:analz H"
 by (erule analz.induct, auto dest: kparts_analz)
 
-lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==>
-X:analz (kparts {Z} Un kparts H)"
+lemma analz_kparts_insert: "X:analz (kparts (insert Z H)) ==> X:analz (kparts {Z} Un kparts H)"
 by (rule analz_sub, auto)
 
 lemma Nonce_kparts_synth [rule_format]: "Y:synth (analz G)
@@ -247,26 +246,21 @@
 apply (drule in_sub, drule_tac X=Y in parts_sub, simp)
 by (auto dest: Nonce_kparts_synth)
 
-lemma Crypt_insert_synth: "[| Crypt K Y:parts (insert X G); X:synth (analz G);
-Nonce n:kparts {Y}; Nonce n ~:analz G |] ==> Crypt K Y:parts G"
-apply (drule parts_insert_substD [where P="%S. Crypt K Y : S"], clarify)
-apply (drule in_sub, drule_tac X="Crypt K Y" in parts_sub, simp, clarsimp)
-apply (ind_cases "Crypt K Y:synth (analz G)")
-by (auto dest: Nonce_kparts_synth)
+lemma Crypt_insert_synth:
+  "[| Crypt K Y:parts (insert X G); X:synth (analz G); Nonce n:kparts {Y}; Nonce n ~:analz G |] 
+   ==> Crypt K Y:parts G"
+by (metis Fake_parts_insert_in_Un Nonce_kparts_synth UnE analz_conj_parts synth_simps(5))
+
 
 subsection{*analz is pparts + analz of kparts*}
 
 lemma analz_pparts_kparts: "X:analz H ==> X:pparts H | X:analz (kparts H)"
-apply (erule analz.induct)
-apply (rule_tac X=X in is_MPairE, blast, blast)
-apply (erule disjE, rule_tac X=X in is_MPairE, blast, blast, blast)
-by (erule disjE, rule_tac X=Y in is_MPairE, blast+)
+by (erule analz.induct, auto) 
 
 lemma analz_pparts_kparts_eq: "analz H = pparts H Un analz (kparts H)"
 by (rule eq, auto dest: analz_pparts_kparts pparts_analz analz_kparts_analz)
 
 lemmas analz_pparts_kparts_substI = analz_pparts_kparts_eq [THEN ssubst]
-lemmas analz_pparts_kparts_substD
-= analz_pparts_kparts_eq [THEN sym, THEN ssubst]
+lemmas analz_pparts_kparts_substD = analz_pparts_kparts_eq [THEN sym, THEN ssubst]
 
 end
diff -r 297cd703f1f0 -r 62332b382dba src/HOL/Auth/Guard/Guard_Yahalom.thy
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy	Wed Sep 08 10:45:55 2010 +0200
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Wed Sep 08 13:25:32 2010 +0100
@@ -11,7 +11,7 @@
 
 header{*Yahalom Protocol*}
 
-theory Guard_Yahalom imports Guard_Shared begin
+theory Guard_Yahalom imports "../Shared" Guard_Shared begin
 
 subsection{*messages used in the protocol*}
 
diff -r 297cd703f1f0 -r 62332b382dba src/HOL/Auth/Guard/P1.thy
--- a/src/HOL/Auth/Guard/P1.thy	Wed Sep 08 10:45:55 2010 +0200
+++ b/src/HOL/Auth/Guard/P1.thy	Wed Sep 08 13:25:32 2010 +0100
@@ -15,7 +15,7 @@
 
 header{*Protocol P1*}
 
-theory P1 imports Guard_Public List_Msg begin
+theory P1 imports "../Public" Guard_Public List_Msg begin
 
 subsection{*Protocol Definition*}
 
diff -r 297cd703f1f0 -r 62332b382dba src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Wed Sep 08 10:45:55 2010 +0200
+++ b/src/HOL/Auth/Message.thy	Wed Sep 08 13:25:32 2010 +0100
@@ -582,12 +582,13 @@
 
 text{*NO @{text Agent_synth}, as any Agent name can be synthesized.  
   The same holds for @{term Number}*}
-inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
-inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
-inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"
-inductive_cases MPair_synth [elim!]: "{|X,Y|} \<in> synth H"
-inductive_cases Crypt_synth [elim!]: "Crypt K X \<in> synth H"
 
+inductive_simps synth_simps [iff]:
+ "Nonce n \<in> synth H"
+ "Key K \<in> synth H"
+ "Hash X \<in> synth H"
+ "{|X,Y|} \<in> synth H"
+ "Crypt K X \<in> synth H"
 
 lemma synth_increasing: "H \<subseteq> synth(H)"
 by blast
@@ -605,7 +606,7 @@
 subsubsection{*Idempotence and transitivity *}
 
 lemma synth_synthD [dest!]: "X\<in> synth (synth H) ==> X\<in> synth H"
-by (erule synth.induct, blast+)
+by (erule synth.induct, auto)
 
 lemma synth_idem: "synth (synth H) = synth H"
 by blast
@@ -782,7 +783,7 @@
      "X \<notin> synth (analz H)  
     ==> (Hash[X] Y \<in> synth (analz H)) =  
         (Hash {|X, Y|} \<in> analz H & Y \<in> synth (analz H))"
-by (simp add: HPair_def)
+by (auto simp add: HPair_def)
 
 
 text{*We do NOT want Crypt... messages broken up in protocols!!*}
diff -r 297cd703f1f0 -r 62332b382dba src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Wed Sep 08 10:45:55 2010 +0200
+++ b/src/HOL/Auth/Shared.thy	Wed Sep 08 13:25:32 2010 +0100
@@ -12,7 +12,7 @@
 begin
 
 consts
-  shrK    :: "agent => key"  (*symmetric keys*);
+  shrK    :: "agent => key"  (*symmetric keys*)
 
 specification (shrK)
   inj_shrK: "inj shrK"
@@ -59,7 +59,7 @@
 (*Specialized to shared-key model: no @{term invKey}*)
 lemma keysFor_parts_insert:
      "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |]
-      ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
+      ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H"
 by (force dest: Event.keysFor_parts_insert)  
 
 lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H"