src/HOL/Auth/Guard/Proto.thy

--- a/src/HOL/Auth/Guard/Proto.thy	Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Proto.thy	Thu Sep 28 23:42:35 2006 +0200
@@ -17,9 +17,9 @@
 
 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"
 
@@ -76,17 +76,18 @@
 "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"
+abbreviation
+  ap' :: "subs => rule => event"
+  "ap' s R == ap s (snd R)"
 
-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)"
+  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*}
 
@@ -377,32 +378,31 @@
 
 consts
 ns :: proto
-ns1 :: rule
-ns2 :: rule
-ns3 :: rule
 
-translations
-"ns1" == "({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
+abbreviation
+  ns1 :: rule
+  "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|}))"
+  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" == "({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)))"
+  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
+abbreviation (input)
+  ns3a :: event
+  "ns3a == Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
 
-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|})"
+  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}"