# HG changeset patch
# User paulson
# Date 985855477 -7200
# Node ID 756c5034f08bbf33a41aa730ea3bda505c00c6c4
# Parent  f417841385b79b2f7845c89d8205a12028984c13
misc tidying; changing the predicate isSymKey to the set symKeys

diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/Message.thy	Thu Mar 29 10:44:37 2001 +0200
@@ -10,10 +10,6 @@
 theory Message = Main
 files ("Message_lemmas.ML"):
 
-(*Eliminates a commonly-occurring expression*)
-lemma [simp] : "~ (\<forall> x. x\<noteq>y)"
-by blast
-
 (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
 lemma [simp] : "A Un (B Un A) = B Un A"
 by blast
@@ -31,8 +27,8 @@
     that of a public key is the private key and vice versa*)
 
 constdefs
-  isSymKey :: "key=>bool"
-  "isSymKey K == (invKey K = K)"
+  symKeys :: "key set"
+  "symKeys == {K. invKey K = K}"
 
 datatype  (*We allow any number of friendly agents*)
   agent = Server | Friend nat | Spy
diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/Message_lemmas.ML
--- a/src/HOL/Auth/Message_lemmas.ML	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/Message_lemmas.ML	Thu Mar 29 10:44:37 2001 +0200
@@ -14,7 +14,7 @@
 val analz_mono = thm "analz_mono";
 val synth_mono = thm "synth_mono";
 val HPair_def = thm "HPair_def";
-val isSymKey_def = thm "isSymKey_def";
+val symKeys_def = thm "symKeys_def";
 
 structure parts =
   struct
diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/NS_Public.thy
--- a/src/HOL/Auth/NS_Public.thy	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/NS_Public.thy	Thu Mar 29 10:44:37 2001 +0200
@@ -40,8 +40,6 @@
               \<in> set evs3\<rbrakk>
           \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public"
 
-  (*No Oops message.  Should there be one?*)
-
 declare knows_Spy_partsEs [elim]
 declare analz_subset_parts [THEN subsetD, dest]
 declare Fake_parts_insert [THEN subsetD, dest]
diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/NS_Public_Bad.thy
--- a/src/HOL/Auth/NS_Public_Bad.thy	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Mar 29 10:44:37 2001 +0200
@@ -43,8 +43,6 @@
            Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk>
           \<Longrightarrow> Says A B (Crypt (pubK B) (Nonce NB)) # evs3 \<in> ns_public"
 
-  (*No Oops message.  Should there be one?*)
-
 declare knows_Spy_partsEs [elim]
 declare analz_subset_parts [THEN subsetD, dest]
 declare Fake_parts_insert [THEN subsetD, dest]
diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/OtwayRees.ML	Thu Mar 29 10:44:37 2001 +0200
@@ -18,7 +18,7 @@
 
 (*A "possibility property": there are traces that reach the end*)
 Goal "B \\<noteq> Server   \
-\     ==> \\<exists>NA K. \\<exists>evs \\<in> otway.          \
+\     ==> \\<exists>K. \\<exists>evs \\<in> otway.          \
 \            Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
 \              \\<in> set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/OtwayRees.thy
--- a/src/HOL/Auth/OtwayRees.thy	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/OtwayRees.thy	Thu Mar 29 10:44:37 2001 +0200
@@ -60,8 +60,8 @@
 
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.
-           Need B ~= Server because we allow messages to self.*)
-    OR4  "[| evs4 \\<in> otway;  B ~= Server;
+           Need B \\<noteq> Server because we allow messages to self.*)
+    OR4  "[| evs4 \\<in> otway;  B \\<noteq> Server;
              Says B Server {|Nonce NA, Agent A, Agent B, X', 
                              Crypt (shrK B)
                                    {|Nonce NA, Nonce NB, Agent A, Agent B|}|}
diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/OtwayRees_AN.ML
--- a/src/HOL/Auth/OtwayRees_AN.ML	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Mar 29 10:44:37 2001 +0200
@@ -18,7 +18,7 @@
 
 (*A "possibility property": there are traces that reach the end*)
 Goal "B \\<noteq> Server   \
-\     ==> \\<exists>K. \\<exists>NA. \\<exists>evs \\<in> otway.                                      \
+\     ==> \\<exists>K. \\<exists>evs \\<in> otway.                                      \
 \          Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
 \            \\<in> set evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/OtwayRees_AN.thy
--- a/src/HOL/Auth/OtwayRees_AN.thy	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy	Thu Mar 29 10:44:37 2001 +0200
@@ -58,8 +58,8 @@
 
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.
-           Need B ~= Server because we allow messages to self.*)
-    OR4  "[| evs4 \\<in> otway;  B ~= Server; 
+           Need B \\<noteq> Server because we allow messages to self.*)
+    OR4  "[| evs4 \\<in> otway;  B \\<noteq> Server; 
              Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} \\<in>set evs4;
              Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
                \\<in>set evs4 |]
diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/Public_lemmas.ML
--- a/src/HOL/Auth/Public_lemmas.ML	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/Public_lemmas.ML	Thu Mar 29 10:44:37 2001 +0200
@@ -24,20 +24,24 @@
 AddIffs [priK_inj_eq];
 AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];
 
-Goalw [isSymKey_def] "~ isSymKey (pubK A)";
+Goalw [symKeys_def] "pubK A \\<notin> symKeys";
 by (Simp_tac 1);
-qed "not_isSymKey_pubK";
+qed "not_symKeys_pubK";
 
-Goalw [isSymKey_def] "~ isSymKey (priK A)";
+Goalw [symKeys_def] "priK A \\<notin> symKeys";
 by (Simp_tac 1);
-qed "not_isSymKey_priK";
+qed "not_symKeys_priK";
 
-AddIffs [not_isSymKey_pubK, not_isSymKey_priK];
+AddIffs [not_symKeys_pubK, not_symKeys_priK];
 
-Goal "[| Crypt K X \\<in> analz H;  isSymKey K;  Key K  \\<in> analz H |] \
+Goal "(K \\<in> symKeys) \\<noteq> (K' \\<in> symKeys) ==> K \\<noteq> K'";
+by (Blast_tac 1); 
+qed "symKeys_neq_imp_neq";
+
+Goal "[| Crypt K X \\<in> analz H;  K \\<in> symKeys;  Key K \\<in> analz H |] \
 \     ==> X \\<in> analz H";
-by (auto_tac(claset(), simpset() addsimps [isSymKey_def]));
-qed "analz_isSymKey_Decrypt";
+by (auto_tac(claset(), simpset() addsimps [symKeys_def]));
+qed "analz_symKeys_Decrypt";
 
 
 (** "Image" equations that hold for injective functions **)
diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/Shared.thy	Thu Mar 29 10:44:37 2001 +0200
@@ -15,7 +15,7 @@
   shrK    :: "agent => key"  (*symmetric keys*)
 
 axioms
-  isSym_keys: "isSymKey K"	(*All keys are symmetric*)
+  isSym_keys: "K \\<in> symKeys"	(*All keys are symmetric*)
   inj_shrK:   "inj shrK"	(*No two agents have the same long-term key*)
 
 primrec
diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/Shared_lemmas.ML
--- a/src/HOL/Auth/Shared_lemmas.ML	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/Shared_lemmas.ML	Thu Mar 29 10:44:37 2001 +0200
@@ -17,8 +17,11 @@
 (*Injectiveness: Agents' long-term keys are distinct.*)
 AddIffs [inj_shrK RS inj_eq];
 
-(* invKey(shrK A) = shrK A *)
-Addsimps [rewrite_rule [isSymKey_def] isSym_keys];
+Goal "invKey K = K";
+by (cut_facts_tac [rewrite_rule [symKeys_def] isSym_keys] 1);
+by Auto_tac;
+qed "invKey_K";
+Addsimps [invKey_K];
 
 
 Goal "[| Crypt K X \\<in> analz H;  Key K  \\<in> analz H |] ==> X \\<in> analz H";
@@ -87,11 +90,11 @@
 
 (*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
   from long-term shared keys*)
-Goal "Key K ~: used evs ==> K ~: range shrK";
+Goal "Key K \\<notin> used evs ==> K \\<notin> range shrK";
 by (Blast_tac 1);
 qed "Key_not_used";
 
-Goal "Key K ~: used evs ==> shrK B ~= K";
+Goal "Key K \\<notin> used evs ==> shrK B \\<noteq> K";
 by (Blast_tac 1);
 qed "shrK_neq";
 
@@ -100,13 +103,13 @@
 
 (*** Fresh nonces ***)
 
-Goal "Nonce N ~: parts (initState B)";
+Goal "Nonce N \\<notin> parts (initState B)";
 by (induct_tac "B" 1);
 by Auto_tac;
 qed "Nonce_notin_initState";
 AddIffs [Nonce_notin_initState];
 
-Goal "Nonce N ~: used []";
+Goal "Nonce N \\<notin> used []";
 by (simp_tac (simpset() addsimps [used_Nil]) 1);
 qed "Nonce_notin_used_empty";
 Addsimps [Nonce_notin_used_empty];
@@ -115,7 +118,7 @@
 (*** Supply fresh nonces for possibility theorems. ***)
 
 (*In any trace, there is an upper bound N on the greatest nonce in use.*)
-Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
+Goal "EX N. ALL n. N<=n --> Nonce n \\<notin> used evs";
 by (induct_tac "evs" 1);
 by (res_inst_tac [("x","0")] exI 1);
 by (ALLGOALS (asm_simp_tac
@@ -126,12 +129,12 @@
 by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
 val lemma = result();
 
-Goal "EX N. Nonce N ~: used evs";
+Goal "EX N. Nonce N \\<notin> used evs";
 by (rtac (lemma RS exE) 1);
 by (Blast_tac 1);
 qed "Nonce_supply1";
 
-Goal "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
+Goal "EX N N'. Nonce N \\<notin> used evs & Nonce N' \\<notin> used evs' & N \\<noteq> N'";
 by (cut_inst_tac [("evs","evs")] lemma 1);
 by (cut_inst_tac [("evs","evs'")] lemma 1);
 by (Clarify_tac 1);
@@ -141,8 +144,8 @@
 				      less_Suc_eq_le]) 1);
 qed "Nonce_supply2";
 
-Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
-\                   Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
+Goal "EX N N' N''. Nonce N \\<notin> used evs & Nonce N' \\<notin> used evs' & \
+\                   Nonce N'' \\<notin> used evs'' & N \\<noteq> N' & N' \\<noteq> N'' & N \\<noteq> N''";
 by (cut_inst_tac [("evs","evs")] lemma 1);
 by (cut_inst_tac [("evs","evs'")] lemma 1);
 by (cut_inst_tac [("evs","evs''")] lemma 1);
@@ -154,7 +157,7 @@
 				      less_Suc_eq_le]) 1);
 qed "Nonce_supply3";
 
-Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
+Goal "Nonce (@ N. Nonce N \\<notin> used evs) \\<notin> used evs";
 by (rtac (lemma RS exE) 1);
 by (rtac someI 1);
 by (Blast_tac 1);
@@ -162,12 +165,12 @@
 
 (*** Supply fresh keys for possibility theorems. ***)
 
-Goal "EX K. Key K ~: used evs";
+Goal "EX K. Key K \\<notin> used evs";
 by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
 by (Blast_tac 1);
 qed "Key_supply1";
 
-Goal "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
+Goal "EX K K'. Key K \\<notin> used evs & Key K' \\<notin> used evs' & K \\<noteq> K'";
 by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
 by (etac exE 1);
 by (cut_inst_tac [("evs","evs'")] 
@@ -175,8 +178,8 @@
 by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *)
 qed "Key_supply2";
 
-Goal "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
-\                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
+Goal "EX K K' K''. Key K \\<notin> used evs & Key K' \\<notin> used evs' & \
+\                      Key K'' \\<notin> used evs'' & K \\<noteq> K' & K' \\<noteq> K'' & K \\<noteq> K''";
 by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
 by (etac exE 1);
 (*Blast_tac requires instantiation of the keys for some reason*)
@@ -188,7 +191,7 @@
 by (Blast_tac 1);
 qed "Key_supply3";
 
-Goal "Key (@ K. Key K ~: used evs) ~: used evs";
+Goal "Key (@ K. Key K \\<notin> used evs) \\<notin> used evs";
 by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
 by (rtac someI 1);
 by (Blast_tac 1);
@@ -197,7 +200,7 @@
 (*** Tactics for possibility theorems ***)
 
 (*Omitting used_Says makes the tactic much faster: it leaves expressions
-    such as  Nonce ?N ~: used evs that match Nonce_supply*)
+    such as  Nonce ?N \\<notin> used evs that match Nonce_supply*)
 fun possibility_tac st = st |>
    (REPEAT 
     (ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets] 
@@ -217,7 +220,7 @@
 
 (*** Specialized rewriting for analz_insert_freshK ***)
 
-Goal "A <= - (range shrK) ==> shrK x ~: A";
+Goal "A <= - (range shrK) ==> shrK x \\<notin> A";
 by (Blast_tac 1);
 qed "subset_Compl_range";
 
diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/TLS.ML
--- a/src/HOL/Auth/TLS.ML	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/TLS.ML	Thu Mar 29 10:44:37 2001 +0200
@@ -27,21 +27,17 @@
 AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
 
 (* invKey(sessionK x) = sessionK x*)
-Addsimps [isSym_sessionK, rewrite_rule [isSymKey_def] isSym_sessionK];
+Addsimps [isSym_sessionK, rewrite_rule [symKeys_def] isSym_sessionK];
 
 
 (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
 
 Goal "pubK A \\<noteq> sessionK arg";
-by (rtac notI 1);
-by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
-by (Full_simp_tac 1);
+by (simp_tac (simpset() addsimps [symKeys_neq_imp_neq]) 1);
 qed "pubK_neq_sessionK";
 
 Goal "priK A \\<noteq> sessionK arg";
-by (rtac notI 1);
-by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
-by (Full_simp_tac 1);
+by (simp_tac (simpset() addsimps [symKeys_neq_imp_neq]) 1);
 qed "priK_neq_sessionK";
 
 val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK];
diff -r f417841385b7 -r 756c5034f08b src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Wed Mar 28 13:40:06 2001 +0200
+++ b/src/HOL/Auth/TLS.thy	Thu Mar 29 10:44:37 2001 +0200
@@ -72,7 +72,7 @@
   inj_sessionK  "inj sessionK"	
 
   (*sessionK makes symmetric keys*)
-  isSym_sessionK "isSymKey (sessionK nonces)"
+  isSym_sessionK "sessionK nonces \\<in> symKeys"
 
 
 consts    tls :: event list set