# HG changeset patch
# User paulson
# Date 1309269166 -3600
# Node ID 027dc42505bef8ac1013d751cbf24bbe307eafbc
# Parent  4d375d0fa4b0ae80b8d2333bd8fe035a25d02522
simplified proofs using metis calls

diff -r 4d375d0fa4b0 -r 027dc42505be src/HOL/Auth/CertifiedEmail.thy
--- a/src/HOL/Auth/CertifiedEmail.thy	Tue Jun 28 12:48:00 2011 +0100
+++ b/src/HOL/Auth/CertifiedEmail.thy	Tue Jun 28 14:52:46 2011 +0100
@@ -197,10 +197,7 @@
 txt{*Message 2*}
 apply (blast dest!: Gets_imp_Says elim!: knows_Spy_partsEs)
 txt{*Message 3*}
-apply (frule_tac hr_form, assumption)
-apply (elim disjE exE) 
-apply (simp_all add: parts_insert2)
-apply (blast intro: subsetD [OF parts_mono [OF Set.subset_insertI]])  
+apply (metis parts_insertI)
 done
 
 lemma Spy_dont_know_RPwd [rule_format]:
@@ -226,8 +223,7 @@
 
 lemma Spy_analz_RPwd_iff [simp]:
     "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(spies evs)) = (A\<in>bad)"
-by (auto simp add: Spy_dont_know_RPwd [OF _ analz_subset_parts [THEN subsetD]])
-
+by (metis Spy_know_RPwd_iff Spy_spies_bad_shrK analz.Inj analz_into_parts)
 
 text{*Unused, but a guarantee of sorts*}
 theorem CertAutenticity:
@@ -308,8 +304,7 @@
 apply (clarsimp, blast)
 txt{*Message 2*}
 apply (simp add: parts_insert2, clarify) 
-apply (drule parts_cut, assumption, simp) 
-apply (blast intro: usedI) 
+apply (metis parts_cut Un_empty_left usedI)
 txt{*Message 3*} 
 apply (blast dest: Notes_SSL_imp_used used_parts_subset_parts) 
 done