# HG changeset patch
# User paulson
# Date 867746759 -7200
# Node ID c2334f9532ab9689da2eaa406ccd9c971b30b811
# Parent  fb3c38c88c08a1fe5b6c12cc22f3f1c10825a7ef
New and stronger lemmas; more default simp/cla rules

diff -r fb3c38c88c08 -r c2334f9532ab src/HOL/Auth/Public.ML
--- a/src/HOL/Auth/Public.ML	Tue Jul 01 10:39:28 1997 +0200
+++ b/src/HOL/Auth/Public.ML	Tue Jul 01 10:45:59 1997 +0200
@@ -52,7 +52,18 @@
 (*** Basic properties of pubK & priK ***)
 
 AddIffs [inj_pubK RS inj_eq];
-Addsimps [priK_neq_pubK, priK_neq_pubK RS not_sym];
+AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];
+
+goalw thy [isSymKey_def] "~ isSymKey (pubK A)";
+by (Simp_tac 1);
+qed "not_isSymKey_pubK";
+
+goalw thy [isSymKey_def] "~ isSymKey (priK A)";
+by (Simp_tac 1);
+qed "not_isSymKey_priK";
+
+AddIffs [not_isSymKey_pubK, not_isSymKey_priK];
+
 
 (*Agents see their own private keys!*)
 goal thy "A ~= Spy --> Key (priK A) : sees lost A evs";
@@ -61,10 +72,10 @@
 by (Auto_tac ());
 qed_spec_mp "sees_own_priK";
 
-(*All public keys are visible*)
-goal thy "Key (pubK A) : sees lost A evs";
+(*All public keys are visible to all*)
+goal thy "Key (pubK A) : sees lost B evs";
 by (list.induct_tac "evs" 1);
-by (agent.induct_tac "A" 1);
+by (agent.induct_tac "B" 1);
 by (Auto_tac ());
 qed_spec_mp "sees_pubK";
 
@@ -74,7 +85,7 @@
 by (Auto_tac());
 qed "Spy_sees_lost";
 
-AddIffs [sees_pubK];
+AddIffs [sees_pubK, sees_pubK RS analz.Inj];
 AddSIs  [sees_own_priK, Spy_sees_lost];