src/HOL/Auth/Guard/Guard_Yahalom.thy

--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy	Thu Oct 13 14:49:15 2022 +0200
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Thu Oct 13 15:38:32 2022 +0100
@@ -52,18 +52,18 @@
 
   Nil: "[] \<in> ya"
 
-| Fake: "[| evs \<in> ya; X \<in> synth (analz (spies evs)) |] ==> Says Spy B X # evs \<in> ya"
+| Fake: "\<lbrakk>evs \<in> ya; X \<in> synth (analz (spies evs))\<rbrakk> \<Longrightarrow> Says Spy B X # evs \<in> ya"
 
-| YA1: "[| evs1 \<in> ya; Nonce NA \<notin> used evs1 |] ==> ya1 A B NA # evs1 \<in> ya"
+| YA1: "\<lbrakk>evs1 \<in> ya; Nonce NA \<notin> used evs1\<rbrakk> \<Longrightarrow> ya1 A B NA # evs1 \<in> ya"
 
-| YA2: "[| evs2 \<in> ya; ya1' A' A B NA \<in> set evs2; Nonce NB \<notin> used evs2 |]
-  ==> ya2 A B NA NB # evs2 \<in> ya"
+| YA2: "\<lbrakk>evs2 \<in> ya; ya1' A' A B NA \<in> set evs2; Nonce NB \<notin> used evs2\<rbrakk>
+  \<Longrightarrow> ya2 A B NA NB # evs2 \<in> ya"
 
-| YA3: "[| evs3 \<in> ya; ya2' B' A B NA NB \<in> set evs3; Key K \<notin> used evs3 |]
-  ==> ya3 A B NA NB K # evs3 \<in> ya"
+| YA3: "\<lbrakk>evs3 \<in> ya; ya2' B' A B NA NB \<in> set evs3; Key K \<notin> used evs3\<rbrakk>
+  \<Longrightarrow> ya3 A B NA NB K # evs3 \<in> ya"
 
-| YA4: "[| evs4 \<in> ya; ya1 A B NA \<in> set evs4; ya3' S Y A B NA NB K \<in> set evs4 |]
-  ==> ya4 A B K NB Y # evs4 \<in> ya"
+| YA4: "\<lbrakk>evs4 \<in> ya; ya1 A B NA \<in> set evs4; ya3' S Y A B NA NB K \<in> set evs4\<rbrakk>
+  \<Longrightarrow> ya4 A B K NB Y # evs4 \<in> ya"
 
 subsection\<open>declarations for tactics\<close>
 
@@ -96,7 +96,7 @@
 
 subsection\<open>guardedness of KAB\<close>
 
-lemma Guard_KAB [rule_format]: "[| evs \<in> ya; A \<notin> bad; B \<notin> bad |] ==>
+lemma Guard_KAB [rule_format]: "\<lbrakk>evs \<in> ya; A \<notin> bad; B \<notin> bad\<rbrakk> \<Longrightarrow>
 ya3 A B NA NB K \<in> set evs \<longrightarrow> GuardK K {shrK A,shrK B} (spies evs)" 
 apply (erule ya.induct)
 (* Nil *)
@@ -127,18 +127,18 @@
 subsection\<open>ya2' implies ya1'\<close>
 
 lemma ya2'_parts_imp_ya1'_parts [rule_format]:
-     "[| evs \<in> ya; B \<notin> bad |] ==>
+     "\<lbrakk>evs \<in> ya; B \<notin> bad\<rbrakk> \<Longrightarrow>
       Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
       \<lbrace>Agent A, Nonce NA\<rbrace> \<in> spies evs"
 by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts)
 
-lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB \<in> set evs; evs \<in> ya; B \<notin> bad |]
-==> \<lbrace>Agent A, Nonce NA\<rbrace> \<in> spies evs"
+lemma ya2'_imp_ya1'_parts: "\<lbrakk>ya2' B' A B NA NB \<in> set evs; evs \<in> ya; B \<notin> bad\<rbrakk>
+\<Longrightarrow> \<lbrace>Agent A, Nonce NA\<rbrace> \<in> spies evs"
 by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts)
 
 subsection\<open>uniqueness of NB\<close>
 
-lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs \<in> ya; B \<notin> bad; B' \<notin> bad |] ==>
+lemma NB_is_uniq_in_ya2'_parts [rule_format]: "\<lbrakk>evs \<in> ya; B \<notin> bad; B' \<notin> bad\<rbrakk> \<Longrightarrow>
 Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
 Ciph B' \<lbrace>Agent A', Nonce NA', Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
 A=A' \<and> B=B' \<and> NA=NA'"
@@ -148,14 +148,14 @@
 apply (drule not_used_parts_false, simp+)+
 by (drule Says_not_parts, simp+)+
 
-lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB \<in> set evs;
-ya2' C' A' B' NA' NB \<in> set evs; evs \<in> ya; B \<notin> bad; B' \<notin> bad |]
-==> A=A' \<and> B=B' \<and> NA=NA'"
+lemma NB_is_uniq_in_ya2': "\<lbrakk>ya2' C A B NA NB \<in> set evs;
+ya2' C' A' B' NA' NB \<in> set evs; evs \<in> ya; B \<notin> bad; B' \<notin> bad\<rbrakk>
+\<Longrightarrow> A=A' \<and> B=B' \<and> NA=NA'"
 by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies)
 
 subsection\<open>ya3' implies ya2'\<close>
 
-lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs \<in> ya; A \<notin> bad |] ==>
+lemma ya3'_parts_imp_ya2'_parts [rule_format]: "\<lbrakk>evs \<in> ya; A \<notin> bad\<rbrakk> \<Longrightarrow>
 Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs)
 \<longrightarrow> Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs)"
 apply (erule ya.induct, simp_all)
@@ -163,7 +163,7 @@
 apply (blast intro: parts_sub, blast)
 by (auto dest: Says_imp_spies parts_parts)
 
-lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs \<in> ya; A \<notin> bad |] ==>
+lemma ya3'_parts_imp_ya2' [rule_format]: "\<lbrakk>evs \<in> ya; A \<notin> bad\<rbrakk> \<Longrightarrow>
 Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs)
 \<longrightarrow> (\<exists>B'. ya2' B' A B NA NB \<in> set evs)"
 apply (erule ya.induct, simp_all, safe)
@@ -173,21 +173,21 @@
 apply blast
 by (auto dest: Says_imp_spies2 parts_parts)
 
-lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K \<in> set evs; evs \<in> ya; A \<notin> bad |]
-==> (\<exists>B'. ya2' B' A B NA NB \<in> set evs)"
+lemma ya3'_imp_ya2': "\<lbrakk>ya3' S Y A B NA NB K \<in> set evs; evs \<in> ya; A \<notin> bad\<rbrakk>
+\<Longrightarrow> (\<exists>B'. ya2' B' A B NA NB \<in> set evs)"
 by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies)
 
 subsection\<open>ya3' implies ya3\<close>
 
-lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs \<in> ya; A \<notin> bad |] ==>
+lemma ya3'_parts_imp_ya3 [rule_format]: "\<lbrakk>evs \<in> ya; A \<notin> bad\<rbrakk> \<Longrightarrow>
 Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace> \<in> parts(spies evs)
 \<longrightarrow> ya3 A B NA NB K \<in> set evs"
 apply (erule ya.induct, simp_all, safe)
 apply (drule Crypt_synth_insert, simp+)
 by (blast dest: Says_imp_spies2 parts_parts)
 
-lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K \<in> set evs; evs \<in> ya; A \<notin> bad |]
-==> ya3 A B NA NB K \<in> set evs"
+lemma ya3'_imp_ya3: "\<lbrakk>ya3' S Y A B NA NB K \<in> set evs; evs \<in> ya; A \<notin> bad\<rbrakk>
+\<Longrightarrow> ya3 A B NA NB K \<in> set evs"
 by (blast dest: Says_imp_spies ya3'_parts_imp_ya3)
 
 subsection\<open>guardedness of NB\<close>
@@ -195,7 +195,7 @@
 definition ya_keys :: "agent \<Rightarrow> agent \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> event list \<Rightarrow> key set" where
 "ya_keys A B NA NB evs \<equiv> {shrK A,shrK B} \<union> {K. ya3 A B NA NB K \<in> set evs}"
 
-lemma Guard_NB [rule_format]: "[| evs \<in> ya; A \<notin> bad; B \<notin> bad |] ==>
+lemma Guard_NB [rule_format]: "\<lbrakk>evs \<in> ya; A \<notin> bad; B \<notin> bad\<rbrakk> \<Longrightarrow>
 ya2 A B NA NB \<in> set evs \<longrightarrow> Guard NB (ya_keys A B NA NB evs) (spies evs)"
 apply (erule ya.induct)
 (* Nil *)