src/HOL/Auth/Guard/Proto.thy

 
 subsection{*protocols*}
 
 types rule = "event set * event"
 
-syntax msg' :: "rule => msg"
-
-translations "msg' R" == "msg (snd R)"
+abbreviation
+  msg' :: "rule => msg"
+  "msg' R == msg (snd R)"
 
 types proto = "rule set"
 
 constdefs wdef :: "proto => bool"
 "wdef p == ALL R k. R:p --> Number k:parts {msg' R}

 primrec
 "ap s (Says A B X) = Says (agent s A) (agent s B) (apm s X)"
 "ap s (Gets A X) = Gets (agent s A) (apm s X)"
 "ap s (Notes A X) = Notes (agent s A) (apm s X)"
 
-syntax
-ap' :: "rule => msg"
-apm' :: "rule => msg"
-priK' :: "subs => agent => key"
-pubK' :: "subs => agent => key"
-
-translations
-"ap' s R" == "ap s (snd R)"
-"apm' s R" == "apm s (msg' R)"
-"priK' s A" == "priK (agent s A)"
-"pubK' s A" == "pubK (agent s A)"
+abbreviation
+  ap' :: "subs => rule => event"
+  "ap' s R == ap s (snd R)"
+
+  apm' :: "subs => rule => msg"
+  "apm' s R == apm s (msg' R)"
+
+  priK' :: "subs => agent => key"
+  "priK' s A == priK (agent s A)"
+
+  pubK' :: "subs => agent => key"
+  "pubK' s A == pubK (agent s A)"
 
 subsection{*nonces generated by a rule*}
 
 constdefs newn :: "rule => nat set"
 "newn R == {n. Nonce n:parts {msg (snd R)} & Nonce n ~:parts (msg`(fst R))}"

 Na :: nat "Na == 0"
 Nb :: nat "Nb == 1"
 
 consts
 ns :: proto
-ns1 :: rule
-ns2 :: rule
-ns3 :: rule
-
-translations
-"ns1" == "({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
-
-"ns2" == "({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})},
-Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))"
-
-"ns3" == "({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}),
-Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})},
-Says a b (Crypt (pubK b) (Nonce Nb)))"
+
+abbreviation
+  ns1 :: rule
+  "ns1 == ({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
+
+  ns2 :: rule
+  "ns2 == ({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})},
+    Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))"
+
+  ns3 :: rule
+  "ns3 == ({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}),
+    Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})},
+    Says a b (Crypt (pubK b) (Nonce Nb)))"
 
 inductive ns intros
 [iff]: "ns1:ns"
 [iff]: "ns2:ns"
 [iff]: "ns3:ns"
 
-syntax
-ns3a :: msg
-ns3b :: msg
-
-translations
-"ns3a" => "Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
-"ns3b" => "Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})"
+abbreviation (input)
+  ns3a :: event
+  "ns3a == Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
+
+  ns3b :: event
+  "ns3b == Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})"
 
 constdefs keys :: "keyfun"
 "keys R' s' n evs == {priK' s' a, priK' s' b}"
 
 lemma "monoton ns keys"