# HG changeset patch
# User paulson
# Date 1251384585 -3600
# Node ID 569e8d6729a119e8cf6e0ab11003de8beee0c110
# Parent  e87d9c78910c10a4bc3b63fa53e2aa047c2aca8e
More streamlining using metis.

diff -r e87d9c78910c -r 569e8d6729a1 src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Thu Aug 27 09:28:52 2009 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Thu Aug 27 15:49:45 2009 +0100
@@ -318,9 +318,7 @@
     @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *} 
 apply (force dest!: Crypt_imp_keysFor)
 txt{*NS4*}
-apply (blast dest: B_trusts_NS3
-	           Says_imp_knows_Spy [THEN analz.Inj]
-                   Crypt_Spy_analz_bad unique_session_keys)
+apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
 done
 
 text{*This version no longer assumes that K is secure*}
@@ -349,9 +347,7 @@
 txt{*NS2*}
 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
 txt{*NS4*}
-apply (blast dest: B_trusts_NS3
-	     dest: Says_imp_knows_Spy [THEN analz.Inj]
-                   unique_session_keys Crypt_Spy_analz_bad)
+apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
 done
 
 
@@ -475,18 +471,15 @@
 apply (erule rev_mp)
 apply (erule rev_mp)
 apply (erule ns_shared.induct, analz_mono_contra)
-apply (frule_tac [5] Says_S_message_form)
 apply (simp_all)
 txt{*Fake*}
 apply blast
 txt{*NS2*}
 apply (force dest!: Crypt_imp_keysFor)
-txt{*NS3, much quicker having installed @{term Says_S_message_form} before simplication*}
-apply fastsimp
+txt{*NS3*}
+apply (metis NS3_msg_in_parts_spies parts_cut_eq)
 txt{*NS5, the most important case, can be solved by unicity*}
-apply (case_tac "Aa \<in> bad")
-apply (force dest!: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst])
-apply (blast dest: A_trusts_NS2 unique_session_keys)
+apply (metis A_trusts_NS2 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst analz.Snd unique_session_keys)
 done
 
 lemma A_Issues_B: