# HG changeset patch
# User paulson
# Date 884451572 -3600
# Node ID bb8ff763c93d89bfb9e6feaaa0a7049fd2f667fd
# Parent  41fa62c229c3bafb184346fa4f96d8d37d2792e1
Simplified proofs by omitting PA = {|XA, ...|} from RA2

diff -r 41fa62c229c3 -r bb8ff763c93d src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Sat Jan 10 17:58:42 1998 +0100
+++ b/src/HOL/Auth/Recur.ML	Sat Jan 10 17:59:32 1998 +0100
@@ -133,7 +133,6 @@
 fun parts_induct_tac i = 
     etac recur.induct i				THEN
     forward_tac [RA2_parts_spies] (i+3)	THEN
-    etac subst (i+3) (*RA2: DELETE needless definition of PA!*)  THEN
     forward_tac [respond_imp_responses] (i+4)	THEN
     forward_tac [RA4_parts_spies] (i+5)	THEN
     prove_simple_subgoals_tac i;
@@ -152,9 +151,7 @@
 by (ALLGOALS 
     (asm_simp_tac (simpset() addsimps [parts_insert2, parts_insert_spies])));
 (*RA3*)
-by (blast_tac (claset() addDs [Key_in_parts_respond]) 2);
-(*RA2*)
-by (blast_tac (claset() addSEs partsEs  addDs [parts_cut]) 1);
+by (blast_tac (claset() addDs [Key_in_parts_respond]) 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
@@ -202,7 +199,6 @@
 
 (*For proofs involving analz.*)
 val analz_spies_tac = 
-    etac subst 4 (*RA2: DELETE needless definition of PA!*)  THEN
     dtac RA2_analz_spies 4 THEN 
     forward_tac [respond_imp_responses] 5                THEN
     dtac RA4_analz_spies 6;
@@ -234,7 +230,7 @@
 by (etac recur.induct 1);
 by analz_spies_tac;
 by (REPEAT_FIRST (resolve_tac [allI, impI]));
-by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
+by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
 by (ALLGOALS 
     (asm_simp_tac
      (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
diff -r 41fa62c229c3 -r bb8ff763c93d src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Sat Jan 10 17:58:42 1998 +0100
+++ b/src/HOL/Auth/Recur.thy	Sat Jan 10 17:59:32 1998 +0100
@@ -69,14 +69,10 @@
               # evs1 : recur"
 
          (*Bob's response to Alice's message.  C might be the Server.
-           XA should be the Hash of the remaining components with KA, but
-                Bob cannot check that.
-           P is the previous recur message from Alice's caller.
-           NOTE: existing proofs don't need PA and are complicated by its
-                presence!  See parts_Fake_tac.*)
+           We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because
+           it complicates proofs, so B may respond to any message at all!*)
     RA2  "[| evs2: recur;  B ~= C;  B ~= Server;  Nonce NB ~: used evs2;
-             Says A' B PA : set evs2;  
-             PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
+             Says A' B PA : set evs2 |]
           ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
               # evs2 : recur"