tidied
authorpaulson
Wed, 18 Nov 1998 16:24:33 +0100
changeset 5932 737559a43e71
parent 5931 325300576da7
child 5933 7b0f502a25b1
tidied
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom.ML	Wed Nov 18 15:10:46 1998 +0100
+++ b/src/HOL/Auth/Yahalom.ML	Wed Nov 18 16:24:33 1998 +0100
@@ -449,8 +449,7 @@
 \                : set evs";
 by (etac rev_mp 1);
 by (etac yahalom.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Blast_tac);
+by Auto_tac;
 qed "Says_Server_imp_YM2";
 
 
@@ -470,8 +469,7 @@
 (*Prove YM3 by showing that no NB can also be an NA*)
 by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj]
 	                addSEs [MPair_parts]
-		        addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
-    THEN flexflex_tac);
+		        addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4);
 (*YM2: similar freshness reasoning*) 
 by (blast_tac (claset() addSEs partsEs
 		        addDs  [Says_imp_spies RS analz.Inj,
@@ -482,23 +480,22 @@
 (*Fake*)
 by (spy_analz_tac 1);
 (** LEVEL 7: YM4 and Oops remain **)
-by (ALLGOALS Clarify_tac);
+by (ALLGOALS (Clarify_tac THEN' 
+	      full_simp_tac (simpset() addsimps [all_conj_distrib])));
 (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
 by (not_bad_tac "Aa" 1);
 by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
 by (forward_tac [Says_Server_imp_YM2] 3);
-by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
-(*  use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
-by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key,
-			       impOfSubs Fake_analz_insert]) 1);
+by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
+(*  use Says_unique_NB to identify message components: Aa=A, Ba=B*)
+by (blast_tac (claset() addDs [Says_unique_NB, Spy_not_see_encrypted_key]) 1);
 (** LEVEL 13 **)
 (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   covered by the quantified Oops assumption.*)
-by (full_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
 by (expand_case_tac "NB = NBa" 1);
 (*If NB=NBa then all other components of the Oops message agree*)
-by (blast_tac (claset() addDs [Says_unique_NB]) 1 THEN flexflex_tac);
+by (blast_tac (claset() addDs [Says_unique_NB]) 1);
 (*case NB ~= NBa*)
 by (asm_simp_tac (simpset() addsimps [single_Nonce_secrecy]) 1);
 by (Clarify_tac 1);
--- a/src/HOL/Auth/Yahalom2.ML	Wed Nov 18 15:10:46 1998 +0100
+++ b/src/HOL/Auth/Yahalom2.ML	Wed Nov 18 16:24:33 1998 +0100
@@ -196,8 +196,9 @@
 	        addsimps [analz_insert_eq, analz_insert_freshK])));
 (*Oops*)
 by (blast_tac (claset() addDs [unique_session_keys]) 3);
-(*YM3*)
-by (blast_tac (claset() delrules [impCE]) 2);
+(*YM3: delete a useless induction hypothesis*)
+by (thin_tac "?P-->?Q" 2);
+by (Blast_tac 2);
 (*Fake*) 
 by (spy_analz_tac 1);
 val lemma = result() RS mp RS mp RSN(2,rev_notE);
@@ -350,10 +351,11 @@
 (*Fake*)
 by (Blast_tac 1);
 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
-by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); 
+by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); 
 (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
 by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1);
-(*yes: apply unicity of session keys*)
+(*yes: delete a useless induction hypothesis; apply unicity of session keys*)
+by (thin_tac "?P-->?Q" 1);
 by (not_bad_tac "Aa" 1);
 by (blast_tac (claset() addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
 			addDs  [unique_session_keys]) 1);