diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/SET_Protocol/Public_SET.thy
--- a/src/HOL/SET_Protocol/Public_SET.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/SET_Protocol/Public_SET.thy	Thu May 26 17:51:22 2016 +0200
@@ -4,24 +4,24 @@
     Author:     Lawrence C Paulson
 *)
 
-section{*The Public-Key Theory, Modified for SET*}
+section\<open>The Public-Key Theory, Modified for SET\<close>
 
 theory Public_SET
 imports Event_SET
 begin
 
-subsection{*Symmetric and Asymmetric Keys*}
+subsection\<open>Symmetric and Asymmetric Keys\<close>
 
-text{*definitions influenced by the wish to assign asymmetric keys 
+text\<open>definitions influenced by the wish to assign asymmetric keys 
   - since the beginning - only to RCA and CAs, namely we need a partial 
-  function on type Agent*}
+  function on type Agent\<close>
 
 
-text{*The SET specs mention two signature keys for CAs - we only have one*}
+text\<open>The SET specs mention two signature keys for CAs - we only have one\<close>
 
 consts
   publicKey :: "[bool, agent] => key"
-    --{*the boolean is TRUE if a signing key*}
+    \<comment>\<open>the boolean is TRUE if a signing key\<close>
 
 abbreviation "pubEK == publicKey False"
 abbreviation "pubSK == publicKey True"
@@ -30,8 +30,8 @@
 abbreviation "priEK A == invKey (pubEK A)"
 abbreviation "priSK A == invKey (pubSK A)"
 
-text{*By freeness of agents, no two agents have the same key. Since
- @{term "True\<noteq>False"}, no agent has the same signing and encryption keys.*}
+text\<open>By freeness of agents, no two agents have the same key. Since
+ @{term "True\<noteq>False"}, no agent has the same signing and encryption keys.\<close>
 
 specification (publicKey)
   injective_publicKey:
@@ -55,15 +55,15 @@
 declare privateKey_neq_publicKey [THEN not_sym, iff]
 
   
-subsection{*Initial Knowledge*}
+subsection\<open>Initial Knowledge\<close>
 
-text{*This information is not necessary.  Each protocol distributes any needed
+text\<open>This information is not necessary.  Each protocol distributes any needed
 certificates, and anyway our proofs require a formalization of the Spy's 
 knowledge only.  However, the initial knowledge is as follows:
    All agents know RCA's public keys;
    RCA and CAs know their own respective keys;
    RCA (has already certified and therefore) knows all CAs public keys; 
-   Spy knows all keys of all bad agents.*}
+   Spy knows all keys of all bad agents.\<close>
 
 overloading initState \<equiv> "initState"
 begin
@@ -104,13 +104,13 @@
 end
 
 
-text{*Injective mapping from agents to PANs: an agent can have only one card*}
+text\<open>Injective mapping from agents to PANs: an agent can have only one card\<close>
 
 consts  pan :: "agent => nat"
 
 specification (pan)
   inj_pan: "inj pan"
-  --{*No two agents have the same PAN*}
+  \<comment>\<open>No two agents have the same PAN\<close>
 (*<*)
    apply (rule exI [of _ "nat_of_agent"]) 
    apply (simp add: inj_on_def inj_nat_of_agent [THEN inj_eq]) 
@@ -120,10 +120,10 @@
 declare inj_pan [THEN inj_eq, iff]
 
 consts
-  XOR :: "nat*nat => nat"  --{*no properties are assumed of exclusive-or*}
+  XOR :: "nat*nat => nat"  \<comment>\<open>no properties are assumed of exclusive-or\<close>
 
 
-subsection{*Signature Primitives*}
+subsection\<open>Signature Primitives\<close>
 
 definition
  (* Signature = Message + signed Digest *)
@@ -167,22 +167,22 @@
 abbreviation "onlySig == Number (Suc 0)"
 abbreviation "authCode == Number (Suc (Suc 0))"
 
-subsection{*Encryption Primitives*}
+subsection\<open>Encryption Primitives\<close>
 
 definition EXcrypt :: "[key,key,msg,msg] => msg" where
-  --{*Extra Encryption*}
+  \<comment>\<open>Extra Encryption\<close>
     (*K: the symmetric key   EK: the public encryption key*)
     "EXcrypt K EK M m =
        \<lbrace>Crypt K \<lbrace>M, Hash m\<rbrace>, Crypt EK \<lbrace>Key K, m\<rbrace>\<rbrace>"
 
 definition EXHcrypt :: "[key,key,msg,msg] => msg" where
-  --{*Extra Encryption with Hashing*}
+  \<comment>\<open>Extra Encryption with Hashing\<close>
     (*K: the symmetric key   EK: the public encryption key*)
     "EXHcrypt K EK M m =
        \<lbrace>Crypt K \<lbrace>M, Hash m\<rbrace>, Crypt EK \<lbrace>Key K, m, Hash M\<rbrace>\<rbrace>"
 
 definition Enc :: "[key,key,key,msg] => msg" where
-  --{*Simple Encapsulation with SIGNATURE*}
+  \<comment>\<open>Simple Encapsulation with SIGNATURE\<close>
     (*SK: the sender's signing key
       K: the symmetric key
       EK: the public encryption key*)
@@ -190,12 +190,12 @@
        \<lbrace>Crypt K (sign SK M), Crypt EK (Key K)\<rbrace>"
 
 definition EncB :: "[key,key,key,msg,msg] => msg" where
-  --{*Encapsulation with Baggage.  Keys as above, and baggage b.*}
+  \<comment>\<open>Encapsulation with Baggage.  Keys as above, and baggage b.\<close>
     "EncB SK K EK M b =
        \<lbrace>Enc SK K EK \<lbrace>M, Hash b\<rbrace>, b\<rbrace>"
 
 
-subsection{*Basic Properties of pubEK, pubSK, priEK and priSK *}
+subsection\<open>Basic Properties of pubEK, pubSK, priEK and priSK\<close>
 
 lemma publicKey_eq_iff [iff]:
      "(publicKey b A = publicKey b' A') = (b=b' & A=A')"
@@ -217,12 +217,12 @@
 lemma symKeys_invKey_iff [simp]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
 by (unfold symKeys_def, auto)
 
-text{*Can be slow (or even loop) as a simprule*}
+text\<open>Can be slow (or even loop) as a simprule\<close>
 lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'"
 by blast
 
-text{*These alternatives to @{text symKeys_neq_imp_neq} don't seem any better
-in practice.*}
+text\<open>These alternatives to \<open>symKeys_neq_imp_neq\<close> don't seem any better
+in practice.\<close>
 lemma publicKey_neq_symKey: "K \<in> symKeys ==> publicKey b A \<noteq> K"
 by blast
 
@@ -241,12 +241,12 @@
 by auto
 
 
-subsection{*"Image" Equations That Hold for Injective Functions *}
+subsection\<open>"Image" Equations That Hold for Injective Functions\<close>
 
 lemma invKey_image_eq [iff]: "(invKey x \<in> invKey`A) = (x\<in>A)"
 by auto
 
-text{*holds because invKey is injective*}
+text\<open>holds because invKey is injective\<close>
 lemma publicKey_image_eq [iff]:
      "(publicKey b A \<in> publicKey c ` AS) = (b=c & A\<in>AS)"
 by auto
@@ -269,7 +269,7 @@
 apply (auto intro: range_eqI)
 done
 
-text{*for proving @{text new_keys_not_used}*}
+text\<open>for proving \<open>new_keys_not_used\<close>\<close>
 lemma keysFor_parts_insert:
      "[| K \<in> keysFor (parts (insert X H));  X \<in> synth (analz H) |]  
       ==> K \<in> keysFor (parts H) | Key (invKey K) \<in> parts H"
@@ -282,22 +282,22 @@
      "[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H"
 by (drule Crypt_imp_invKey_keysFor, simp)
 
-text{*Agents see their own private keys!*}
+text\<open>Agents see their own private keys!\<close>
 lemma privateKey_in_initStateCA [iff]:
      "Key (invKey (publicKey b A)) \<in> initState A"
 by (case_tac "A", auto)
 
-text{*Agents see their own public keys!*}
+text\<open>Agents see their own public keys!\<close>
 lemma publicKey_in_initStateCA [iff]: "Key (publicKey b A) \<in> initState A"
 by (case_tac "A", auto)
 
-text{*RCA sees CAs' public keys! *}
+text\<open>RCA sees CAs' public keys!\<close>
 lemma pubK_CA_in_initState_RCA [iff]:
      "Key (publicKey b (CA i)) \<in> initState RCA"
 by auto
 
 
-text{*Spy knows all public keys*}
+text\<open>Spy knows all public keys\<close>
 lemma knows_Spy_pubEK_i [iff]: "Key (publicKey b A) \<in> knows Spy evs"
 apply (induct_tac "evs")
 apply (simp_all add: imageI knows_Cons split add: event.split)
@@ -306,13 +306,13 @@
 declare knows_Spy_pubEK_i [THEN analz.Inj, iff]
                             (*needed????*)
 
-text{*Spy sees private keys of bad agents! [and obviously public keys too]*}
+text\<open>Spy sees private keys of bad agents! [and obviously public keys too]\<close>
 lemma knows_Spy_bad_privateKey [intro!]:
      "A \<in> bad ==> Key (invKey (publicKey b A)) \<in> knows Spy evs"
 by (rule initState_subset_knows [THEN subsetD], simp)
 
 
-subsection{*Fresh Nonces for Possibility Theorems*}
+subsection\<open>Fresh Nonces for Possibility Theorems\<close>
 
 lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)"
 by (induct_tac "B", auto)
@@ -320,7 +320,7 @@
 lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []"
 by (simp add: used_Nil)
 
-text{*In any trace, there is an upper bound N on the greatest nonce in use.*}
+text\<open>In any trace, there is an upper bound N on the greatest nonce in use.\<close>
 lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N<=n --> Nonce n \<notin> used evs"
 apply (induct_tac "evs")
 apply (rule_tac x = 0 in exI)
@@ -337,10 +337,10 @@
 done
 
 
-subsection{*Specialized Methods for Possibility Theorems*}
+subsection\<open>Specialized Methods for Possibility Theorems\<close>
 
 ML
-{*
+\<open>
 (*Tactic for possibility theorems*)
 fun possibility_tac ctxt =
     REPEAT (*omit used_Says so that Nonces start from different traces!*)
@@ -356,18 +356,18 @@
     (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
      THEN
      REPEAT_FIRST (resolve_tac ctxt [refl, conjI]))
-*}
+\<close>
 
-method_setup possibility = {*
-    Scan.succeed (SIMPLE_METHOD o possibility_tac) *}
+method_setup possibility = \<open>
+    Scan.succeed (SIMPLE_METHOD o possibility_tac)\<close>
     "for proving possibility theorems"
 
-method_setup basic_possibility = {*
-    Scan.succeed (SIMPLE_METHOD o basic_possibility_tac) *}
+method_setup basic_possibility = \<open>
+    Scan.succeed (SIMPLE_METHOD o basic_possibility_tac)\<close>
     "for proving possibility theorems"
 
 
-subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*}
+subsection\<open>Specialized Rewriting for Theorems About @{term analz} and Image\<close>
 
 lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H"
 by blast
@@ -376,17 +376,17 @@
      "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"
 by blast
 
-text{*Needed for @{text DK_fresh_not_KeyCryptKey}*}
+text\<open>Needed for \<open>DK_fresh_not_KeyCryptKey\<close>\<close>
 lemma publicKey_in_used [iff]: "Key (publicKey b A) \<in> used evs"
 by auto
 
 lemma privateKey_in_used [iff]: "Key (invKey (publicKey b A)) \<in> used evs"
 by (blast intro!: initState_into_used)
 
-text{*Reverse the normal simplification of "image" to build up (not break down)
-  the set of keys.  Based on @{text analz_image_freshK_ss}, but simpler.*}
+text\<open>Reverse the normal simplification of "image" to build up (not break down)
+  the set of keys.  Based on \<open>analz_image_freshK_ss\<close>, but simpler.\<close>
 lemmas analz_image_keys_simps =
-       simp_thms mem_simps --{*these two allow its use with @{text "only:"}*}
+       simp_thms mem_simps \<comment>\<open>these two allow its use with \<open>only:\<close>\<close>
        image_insert [THEN sym] image_Un [THEN sym] 
        rangeI symKeys_neq_imp_neq
        insert_Key_singleton insert_Key_image Un_assoc [THEN sym]
@@ -394,16 +394,16 @@
 
 (*General lemmas proved by Larry*)
 
-subsection{*Controlled Unfolding of Abbreviations*}
+subsection\<open>Controlled Unfolding of Abbreviations\<close>
 
-text{*A set is expanded only if a relation is applied to it*}
+text\<open>A set is expanded only if a relation is applied to it\<close>
 lemma def_abbrev_simp_relation:
      "A = B ==> (A \<in> X) = (B \<in> X) &  
                  (u = A) = (u = B) &  
                  (A = u) = (B = u)"
 by auto
 
-text{*A set is expanded only if one of the given functions is applied to it*}
+text\<open>A set is expanded only if one of the given functions is applied to it\<close>
 lemma def_abbrev_simp_function:
      "A = B  
       ==> parts (insert A X) = parts (insert B X) &  
@@ -411,15 +411,15 @@
           keysFor (insert A X) = keysFor (insert B X)"
 by auto
 
-subsubsection{*Special Simplification Rules for @{term signCert}*}
+subsubsection\<open>Special Simplification Rules for @{term signCert}\<close>
 
-text{*Avoids duplicating X and its components!*}
+text\<open>Avoids duplicating X and its components!\<close>
 lemma parts_insert_signCert:
      "parts (insert (signCert K X) H) =  
       insert \<lbrace>X, Crypt K X\<rbrace> (parts (insert (Crypt K X) H))"
 by (simp add: signCert_def insert_commute [of X])
 
-text{*Avoids a case split! [X is always available]*}
+text\<open>Avoids a case split! [X is always available]\<close>
 lemma analz_insert_signCert:
      "analz (insert (signCert K X) H) =  
       insert \<lbrace>X, Crypt K X\<rbrace> (insert (Crypt K X) (analz (insert X H)))"
@@ -428,9 +428,9 @@
 lemma keysFor_insert_signCert: "keysFor (insert (signCert K X) H) = keysFor H"
 by (simp add: signCert_def)
 
-text{*Controlled rewrite rules for @{term signCert}, just the definitions
+text\<open>Controlled rewrite rules for @{term signCert}, just the definitions
   of the others. Encryption primitives are just expanded, despite their huge
-  redundancy!*}
+  redundancy!\<close>
 lemmas abbrev_simps [simp] =
     parts_insert_signCert analz_insert_signCert keysFor_insert_signCert
     sign_def     [THEN def_abbrev_simp_relation]
@@ -451,7 +451,7 @@
     EncB_def     [THEN def_abbrev_simp_function]
 
 
-subsubsection{*Elimination Rules for Controlled Rewriting *}
+subsubsection\<open>Elimination Rules for Controlled Rewriting\<close>
 
 lemma Enc_partsE: 
      "!!R. [|Enc SK K EK M \<in> parts H;  
@@ -477,7 +477,7 @@
 by (unfold EXcrypt_def, blast)
 
 
-subsection{*Lemmas to Simplify Expressions Involving @{term analz} *}
+subsection\<open>Lemmas to Simplify Expressions Involving @{term analz}\<close>
 
 lemma analz_knows_absorb:
      "Key K \<in> analz (knows Spy evs)  
@@ -505,13 +505,13 @@
          subset_insertI [THEN [2] subset_trans] 
 
 
-subsection{*Freshness Lemmas*}
+subsection\<open>Freshness Lemmas\<close>
 
 lemma in_parts_Says_imp_used:
      "[|Key K \<in> parts {X}; Says A B X \<in> set evs|] ==> Key K \<in> used evs"
 by (blast intro: parts_trans dest!: Says_imp_knows_Spy [THEN parts.Inj])
 
-text{*A useful rewrite rule with @{term analz_image_keys_simps}*}
+text\<open>A useful rewrite rule with @{term analz_image_keys_simps}\<close>
 lemma Crypt_notin_image_Key: "Crypt K X \<notin> Key ` KK"
 by auto