# HG changeset patch
# User paulson
# Date 905441424 -7200
# Node ID 0c4e3d024ec9678cba5988ff59472f8c46cd04e8
# Parent  1dbaf888f4e75a6625525f8005a002b9b656b19e
deleted not_Says_to_self

diff -r 1dbaf888f4e7 -r 0c4e3d024ec9 src/HOL/UNITY/NSP_Bad.ML
--- a/src/HOL/UNITY/NSP_Bad.ML	Thu Sep 10 17:29:56 1998 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML	Thu Sep 10 17:30:24 1998 +0200
@@ -40,20 +40,6 @@
 
 (**** Inductive proofs about ns_public ****)
 
-(*Nobody sends themselves messages*)
-Goal "Invariant Nprg {s. ALL X. Says A A X ~: set s}";
-by (rtac InvariantI 1);
-by (Force_tac 1);
-by (constrains_tac 1);
-by Auto_tac;
-qed "not_Says_to_self";
-
-(** HOW TO USE??  They don't seem to be needed!
-Addsimps [not_Says_to_self];
-AddSEs   [not_Says_to_self RSN (2, rev_notE)];
-**)
-
-
 (*can be used to simulate analz_mono_contra_tac
 val analz_impI = read_instantiate_sg (sign_of thy)
                 [("P", "?Y ~: analz (spies ?evs)")] impI;
diff -r 1dbaf888f4e7 -r 0c4e3d024ec9 src/HOL/UNITY/NSP_Bad.thy
--- a/src/HOL/UNITY/NSP_Bad.thy	Thu Sep 10 17:29:56 1998 +0200
+++ b/src/HOL/UNITY/NSP_Bad.thy	Thu Sep 10 17:30:24 1998 +0200
@@ -22,7 +22,7 @@
   Fake :: "(state*state) set"
     "Fake == {(s,s').
 	      EX B X. s' = Says Spy B X # s
-		    & B ~= Spy & X: synth (analz (spies s))}"
+		    & X: synth (analz (spies s))}"
   
   (*The numeric suffixes on A identify the rule*)
 
@@ -31,7 +31,7 @@
     "NS1 == {(s1,s').
 	     EX A1 B NA.
 	         s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
-	       & A1 ~= B & Nonce NA ~: used s1}"
+	       & Nonce NA ~: used s1}"
   
   (*Bob responds to Alice's message with a further nonce*)
   NS2 :: "(state*state) set"
@@ -39,7 +39,7 @@
 	     EX A' A2 B NA NB.
 	         s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2
                & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) : set s2
-	       & A2 ~= B & Nonce NB ~: used s2}"
+	       & Nonce NB ~: used s2}"
  
   (*Alice proves her existence by sending NB back to Bob.*)
   NS3 :: "(state*state) set"