--- a/src/HOL/Auth/Guard/Guard_Public.thy Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Auth/Guard/Guard_Public.thy Thu Feb 15 12:11:00 2018 +0100
@@ -22,7 +22,7 @@
subsubsection\<open>agent associated to a key\<close>
definition agt :: "key => agent" where
-"agt K == @A. K = priK A | K = pubK A"
+"agt K == SOME A. K = priK A | K = pubK A"
lemma agt_priK [simp]: "agt (priK A) = A"
by (simp add: agt_def)
@@ -32,18 +32,18 @@
subsubsection\<open>basic facts about @{term initState}\<close>
-lemma no_Crypt_in_parts_init [simp]: "Crypt K X ~:parts (initState A)"
+lemma no_Crypt_in_parts_init [simp]: "Crypt K X \<notin> parts (initState A)"
by (cases A, auto simp: initState.simps)
-lemma no_Crypt_in_analz_init [simp]: "Crypt K X ~:analz (initState A)"
+lemma no_Crypt_in_analz_init [simp]: "Crypt K X \<notin> analz (initState A)"
by auto
-lemma no_priK_in_analz_init [simp]: "A ~:bad
-==> Key (priK A) ~:analz (initState Spy)"
+lemma no_priK_in_analz_init [simp]: "A \<notin> bad
+\<Longrightarrow> Key (priK A) \<notin> analz (initState Spy)"
by (auto simp: initState.simps)
-lemma priK_notin_initState_Friend [simp]: "A ~= Friend C
-==> Key (priK A) ~: parts (initState (Friend C))"
+lemma priK_notin_initState_Friend [simp]: "A \<noteq> Friend C
+\<Longrightarrow> Key (priK A) \<notin> parts (initState (Friend C))"
by (auto simp: initState.simps)
lemma keyset_init [iff]: "keyset (initState A)"
@@ -52,9 +52,9 @@
subsubsection\<open>sets of private keys\<close>
definition priK_set :: "key set => bool" where
-"priK_set Ks == ALL K. K:Ks --> (EX A. K = priK A)"
+"priK_set Ks \<equiv> \<forall>K. K \<in> Ks \<longrightarrow> (\<exists>A. K = priK A)"
-lemma in_priK_set: "[| priK_set Ks; K:Ks |] ==> EX A. K = priK A"
+lemma in_priK_set: "[| priK_set Ks; K \<in> Ks |] ==> \<exists>A. K = priK A"
by (simp add: priK_set_def)
lemma priK_set1 [iff]: "priK_set {priK A}"
@@ -66,15 +66,15 @@
subsubsection\<open>sets of good keys\<close>
definition good :: "key set => bool" where
-"good Ks == ALL K. K:Ks --> agt K ~:bad"
+"good Ks == \<forall>K. K \<in> Ks \<longrightarrow> agt K \<notin> bad"
-lemma in_good: "[| good Ks; K:Ks |] ==> agt K ~:bad"
+lemma in_good: "[| good Ks; K \<in> Ks |] ==> agt K \<notin> bad"
by (simp add: good_def)
-lemma good1 [simp]: "A ~:bad ==> good {priK A}"
+lemma good1 [simp]: "A \<notin> bad \<Longrightarrow> good {priK A}"
by (simp add: good_def)
-lemma good2 [simp]: "[| A ~:bad; B ~:bad |] ==> good {priK A, priK B}"
+lemma good2 [simp]: "[| A \<notin> bad; B \<notin> bad |] ==> good {priK A, priK B}"
by (simp add: good_def)
subsubsection\<open>greatest nonce used in a trace, 0 if there is no nonce\<close>
@@ -84,7 +84,7 @@
"greatest [] = 0"
| "greatest (ev # evs) = max (greatest_msg (msg ev)) (greatest evs)"
-lemma greatest_is_greatest: "Nonce n:used evs ==> n <= greatest evs"
+lemma greatest_is_greatest: "Nonce n \<in> used evs \<Longrightarrow> n \<le> greatest evs"
apply (induct evs, auto simp: initState.simps)
apply (drule used_sub_parts_used, safe)
apply (drule greatest_msg_is_greatest, arith)
@@ -92,10 +92,10 @@
subsubsection\<open>function giving a new nonce\<close>
-definition new :: "event list => nat" where
-"new evs == Suc (greatest evs)"
+definition new :: "event list \<Rightarrow> nat" where
+"new evs \<equiv> Suc (greatest evs)"
-lemma new_isnt_used [iff]: "Nonce (new evs) ~:used evs"
+lemma new_isnt_used [iff]: "Nonce (new evs) \<notin> used evs"
by (clarify, drule greatest_is_greatest, auto simp: new_def)
subsection\<open>Proofs About Guarded Messages\<close>
@@ -109,13 +109,13 @@
lemmas invKey_invKey_substI = invKey [THEN ssubst]
-lemma "Nonce n:parts {X} ==> Crypt (pubK A) X:guard n {priK A}"
+lemma "Nonce n \<in> parts {X} \<Longrightarrow> Crypt (pubK A) X \<in> guard n {priK A}"
apply (rule pubK_is_invKey_priK_substI, rule invKey_invKey_substI)
by (rule Guard_Nonce, simp+)
subsubsection\<open>guardedness results\<close>
-lemma sign_guard [intro]: "X:guard n Ks ==> sign A X:guard n Ks"
+lemma sign_guard [intro]: "X \<in> guard n Ks \<Longrightarrow> sign A X \<in> guard n Ks"
by (auto simp: sign_def)
lemma Guard_init [iff]: "Guard n Ks (initState B)"
@@ -125,38 +125,38 @@
==> Guard n Ks (knows_max C evs)"
by (simp add: knows_max_def)
-lemma Nonce_not_used_Guard_spies [dest]: "Nonce n ~:used evs
-==> Guard n Ks (spies evs)"
+lemma Nonce_not_used_Guard_spies [dest]: "Nonce n \<notin> used evs
+\<Longrightarrow> Guard n Ks (spies evs)"
by (auto simp: Guard_def dest: not_used_not_known parts_sub)
-lemma Nonce_not_used_Guard [dest]: "[| evs:p; Nonce n ~:used evs;
+lemma Nonce_not_used_Guard [dest]: "[| evs \<in> p; Nonce n \<notin> used evs;
Gets_correct p; one_step p |] ==> Guard n Ks (knows (Friend C) evs)"
by (auto simp: Guard_def dest: known_used parts_trans)
-lemma Nonce_not_used_Guard_max [dest]: "[| evs:p; Nonce n ~:used evs;
+lemma Nonce_not_used_Guard_max [dest]: "[| evs \<in> p; Nonce n \<notin> used evs;
Gets_correct p; one_step p |] ==> Guard n Ks (knows_max (Friend C) evs)"
by (auto simp: Guard_def dest: known_max_used parts_trans)
-lemma Nonce_not_used_Guard_max' [dest]: "[| evs:p; Nonce n ~:used evs;
+lemma Nonce_not_used_Guard_max' [dest]: "[| evs \<in> p; Nonce n \<notin> used evs;
Gets_correct p; one_step p |] ==> Guard n Ks (knows_max' (Friend C) evs)"
apply (rule_tac H="knows_max (Friend C) evs" in Guard_mono)
by (auto simp: knows_max_def)
subsubsection\<open>regular protocols\<close>
-definition regular :: "event list set => bool" where
-"regular p == ALL evs A. evs:p --> (Key (priK A):parts (spies evs)) = (A:bad)"
+definition regular :: "event list set \<Rightarrow> bool" where
+"regular p \<equiv> \<forall>evs A. evs \<in> p \<longrightarrow> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
-lemma priK_parts_iff_bad [simp]: "[| evs:p; regular p |] ==>
-(Key (priK A):parts (spies evs)) = (A:bad)"
+lemma priK_parts_iff_bad [simp]: "[| evs \<in> p; regular p |] ==>
+(Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
by (auto simp: regular_def)
-lemma priK_analz_iff_bad [simp]: "[| evs:p; regular p |] ==>
-(Key (priK A):analz (spies evs)) = (A:bad)"
+lemma priK_analz_iff_bad [simp]: "[| evs \<in> p; regular p |] ==>
+(Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
by auto
-lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs:p;
-priK_set Ks; good Ks; regular p |] ==> Nonce n ~:analz (spies evs)"
+lemma Guard_Nonce_analz: "[| Guard n Ks (spies evs); evs \<in> p;
+priK_set Ks; good Ks; regular p |] ==> Nonce n \<notin> analz (spies evs)"
apply (clarify, simp only: knows_decomp)
apply (drule Guard_invKey_keyset, simp+, safe)
apply (drule in_good, simp)