# HG changeset patch
# User paulson
# Date 985253220 -3600
# Node ID 54a86efcb0ba6ee86805ee68d6cf6d953a60f729
# Parent  279004936bb0c31301f4a54ad5c1e2623198bf0f
some X-symbols

diff -r 279004936bb0 -r 54a86efcb0ba src/HOL/Auth/Message_lemmas.ML
--- a/src/HOL/Auth/Message_lemmas.ML	Mon Mar 19 17:25:42 2001 +0100
+++ b/src/HOL/Auth/Message_lemmas.ML	Thu Mar 22 10:27:00 2001 +0100
@@ -46,15 +46,15 @@
 
 
 (*Equations hold because constructors are injective; cannot prove for all f*)
-Goal "(Friend x : Friend`A) = (x:A)";
+Goal "(Friend x \\<in> Friend`A) = (x:A)";
 by Auto_tac;
 qed "Friend_image_eq";
 
-Goal "(Key x : Key`A) = (x:A)";
+Goal "(Key x \\<in> Key`A) = (x:A)";
 by Auto_tac;
 qed "Key_image_eq";
 
-Goal "(Nonce x ~: Key`A)";
+Goal "(Nonce x \\<notin> Key`A)";
 by Auto_tac;
 qed "Nonce_Key_image_eq";
 Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
@@ -132,7 +132,7 @@
 qed "keysFor_image_Key";
 Addsimps [keysFor_image_Key];
 
-Goalw [keysFor_def] "Crypt K X : H ==> invKey K : keysFor H";
+Goalw [keysFor_def] "Crypt K X \\<in> H ==> invKey K \\<in> keysFor H";
 by (Blast_tac 1);
 qed "Crypt_imp_invKey_keysFor";
 
@@ -140,8 +140,8 @@
 (**** Inductive relation "parts" ****)
 
 val major::prems = 
-Goal "[| {|X,Y|} : parts H;       \
-\         [| X : parts H; Y : parts H |] ==> P  \
+Goal "[| {|X,Y|} \\<in> parts H;       \
+\         [| X \\<in> parts H; Y \\<in> parts H |] ==> P  \
 \     |] ==> P";
 by (cut_facts_tac [major] 1);
 by (resolve_tac prems 1);
@@ -326,7 +326,7 @@
 
 
 (*In any message, there is an upper bound N on its greatest nonce.*)
-Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
+Goal "EX N. ALL n. N<=n --> Nonce n \\<notin> parts {msg}";
 by (induct_tac "msg" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
 (*MPair case: blast_tac works out the necessary sum itself!*)
@@ -340,8 +340,8 @@
 (**** Inductive relation "analz" ****)
 
 val major::prems = 
-Goal "[| {|X,Y|} : analz H;       \
-\            [| X : analz H; Y : analz H |] ==> P  \
+Goal "[| {|X,Y|} \\<in> analz H;       \
+\            [| X \\<in> analz H; Y \\<in> analz H |] ==> P  \
 \         |] ==> P";
 by (cut_facts_tac [major] 1);
 by (resolve_tac prems 1);
@@ -424,7 +424,7 @@
 
 (*Can only pull out Keys if they are not needed to decrypt the rest*)
 Goalw [keysFor_def]
-    "K ~: keysFor (analz H) ==>  \
+    "K \\<notin> keysFor (analz H) ==>  \
 \         analz (insert (Key K) H) = insert (Key K) (analz H)";
 by (analz_tac 1);
 qed "analz_insert_Key";
@@ -440,13 +440,13 @@
 qed "analz_insert_MPair";
 
 (*Can pull out enCrypted message if the Key is not known*)
-Goal "Key (invKey K) ~: analz H ==>  \
+Goal "Key (invKey K) \\<notin> analz H ==>  \
 \              analz (insert (Crypt K X) H) = \
 \              insert (Crypt K X) (analz H)";
 by (analz_tac 1);
 qed "analz_insert_Crypt";
 
-Goal "Key (invKey K) : analz H ==>  \
+Goal "Key (invKey K) \\<in> analz H ==>  \
 \              analz (insert (Crypt K X) H) <= \
 \              insert (Crypt K X) (analz (insert X H))";
 by (rtac subsetI 1);
@@ -454,7 +454,7 @@
 by Auto_tac;
 val lemma1 = result();
 
-Goal "Key (invKey K) : analz H ==>  \
+Goal "Key (invKey K) \\<in> analz H ==>  \
 \              insert (Crypt K X) (analz (insert X H)) <= \
 \              analz (insert (Crypt K X) H)";
 by Auto_tac;
@@ -463,7 +463,7 @@
 by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
 val lemma2 = result();
 
-Goal "Key (invKey K) : analz H ==>  \
+Goal "Key (invKey K) \\<in> analz H ==>  \
 \              analz (insert (Crypt K X) H) = \
 \              insert (Crypt K X) (analz (insert X H))";
 by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
@@ -474,10 +474,10 @@
   Use with split_if;  apparently split_tac does not cope with patterns
   such as "analz (insert (Crypt K X) H)" *)
 Goal "analz (insert (Crypt K X) H) =                \
-\         (if (Key (invKey K) : analz H)                \
+\         (if (Key (invKey K) \\<in> analz H)                \
 \          then insert (Crypt K X) (analz (insert X H)) \
 \          else insert (Crypt K X) (analz H))";
-by (case_tac "Key (invKey K)  : analz H " 1);
+by (case_tac "Key (invKey K)  \\<in> analz H " 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [analz_insert_Crypt, 
 						analz_insert_Decrypt])));
 qed "analz_Crypt_if";
@@ -562,7 +562,7 @@
 qed "analz_insert_cong";
 
 (*If there are no pairs or encryptions then analz does nothing*)
-Goal "[| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt K X ~: H |] ==> \
+Goal "[| ALL X Y. {|X,Y|} \\<notin> H;  ALL X K. Crypt K X \\<notin> H |] ==> \
 \         analz H = H";
 by Safe_tac;
 by (etac analz.induct 1);
@@ -622,23 +622,23 @@
 by (Blast_tac 1);
 qed "synth_cut";
 
-Goal "Agent A : synth H";
+Goal "Agent A \\<in> synth H";
 by (Blast_tac 1);
 qed "Agent_synth";
 
-Goal "Number n : synth H";
+Goal "Number n \\<in> synth H";
 by (Blast_tac 1);
 qed "Number_synth";
 
-Goal "(Nonce N : synth H) = (Nonce N : H)";
+Goal "(Nonce N \\<in> synth H) = (Nonce N \\<in> H)";
 by (Blast_tac 1);
 qed "Nonce_synth_eq";
 
-Goal "(Key K : synth H) = (Key K : H)";
+Goal "(Key K \\<in> synth H) = (Key K \\<in> H)";
 by (Blast_tac 1);
 qed "Key_synth_eq";
 
-Goal "Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
+Goal "Key K \\<notin> H ==> (Crypt K X \\<in> synth H) = (Crypt K X \\<in> H)";
 by (Blast_tac 1);
 qed "Crypt_synth_eq";
 
@@ -647,7 +647,7 @@
 
 
 Goalw [keysFor_def]
-    "keysFor (synth H) = keysFor H Un invKey`{K. Key K : H}";
+    "keysFor (synth H) = keysFor H Un invKey`{K. Key K \\<in> H}";
 by (Blast_tac 1);
 qed "keysFor_synth";
 Addsimps [keysFor_synth];
@@ -706,7 +706,7 @@
 Goal "X: synth (analz G) ==> \
 \     analz (insert X H) <= synth (analz G) Un analz (G Un H)";
 by (rtac subsetI 1);
-by (subgoal_tac "x : analz (synth (analz G) Un H)" 1);
+by (subgoal_tac "x \\<in> analz (synth (analz G) Un H)" 1);
 by (blast_tac (claset() addIs [impOfSubs analz_mono,
 			       impOfSubs (analz_mono RS synth_mono)]) 2);
 by (Full_simp_tac 1);
@@ -725,21 +725,21 @@
 
 (*Without this equation, other rules for synth and analz would yield
   redundant cases*)
-Goal "({|X,Y|} : synth (analz H)) = \
-\     (X : synth (analz H) & Y : synth (analz H))";
+Goal "({|X,Y|} \\<in> synth (analz H)) = \
+\     (X \\<in> synth (analz H) & Y \\<in> synth (analz H))";
 by (Blast_tac 1);
 qed "MPair_synth_analz";
 
 AddIffs [MPair_synth_analz];
 
-Goal "[| Key K : analz H;  Key (invKey K) : analz H |] \
-\      ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
+Goal "[| Key K \\<in> analz H;  Key (invKey K) \\<in> analz H |] \
+\      ==> (Crypt K X \\<in> synth (analz H)) = (X \\<in> synth (analz H))";
 by (Blast_tac 1);
 qed "Crypt_synth_analz";
 
 
-Goal "X ~: synth (analz H) \
-\     ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
+Goal "X \\<notin> synth (analz H) \
+\     ==> (Hash{|X,Y|} \\<in> synth (analz H)) = (Hash{|X,Y|} \\<in> analz H)";
 by (Blast_tac 1);
 qed "Hash_synth_analz";
 Addsimps [Hash_synth_analz];
@@ -812,9 +812,9 @@
 by (Simp_tac 1);
 qed "analz_insert_HPair";
 
-Goalw [HPair_def] "X ~: synth (analz H) \
-\   ==> (Hash[X] Y : synth (analz H)) = \
-\       (Hash {|X, Y|} : analz H & Y : synth (analz H))";
+Goalw [HPair_def] "X \\<notin> synth (analz H) \
+\   ==> (Hash[X] Y \\<in> synth (analz H)) = \
+\       (Hash {|X, Y|} \\<in> analz H & Y \\<in> synth (analz H))";
 by (Simp_tac 1);
 by (Blast_tac 1);
 qed "HPair_synth_analz";
@@ -847,7 +847,7 @@
 (*** Tactics useful for many protocol proofs ***)
 
 (*Prove base case (subgoal i) and simplify others.  A typical base case
-  concerns  Crypt K X ~: Key`shrK`bad  and cannot be proved by rewriting
+  concerns  Crypt K X \\<notin> Key`shrK`bad  and cannot be proved by rewriting
   alone.*)
 fun prove_simple_subgoals_tac i = 
     force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN
@@ -859,7 +859,7 @@
 			       impOfSubs Fake_parts_insert]) i;
 
 (*Apply rules to break down assumptions of the form
-  Y : parts(insert X H)  and  Y : analz(insert X H)
+  Y \\<in> parts(insert X H)  and  Y \\<in> analz(insert X H)
 *)
 val Fake_insert_tac = 
     dresolve_tac [impOfSubs Fake_analz_insert,