author paulson Thu, 22 Mar 2001 10:27:00 +0100 changeset 11217 54a86efcb0ba parent 11216 279004936bb0 child 11218 4b71d38fa6e6
some X-symbols
```--- 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";
@@ -132,7 +132,7 @@
qed "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";
@@ -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";

-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";
@@ -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,```