replaced syntax/translations by abbreviation;
authorwenzelm
Thu Sep 28 23:42:35 2006 +0200 (2006-09-28)
changeset 207681d478c2d621f
parent 20767 9bc632ae588f
child 20769 5d538d3d5e2a
replaced syntax/translations by abbreviation;
src/HOL/Auth/CertifiedEmail.thy
src/HOL/Auth/Event.thy
src/HOL/Auth/Guard/Extensions.thy
src/HOL/Auth/Guard/Guard.thy
src/HOL/Auth/Guard/GuardK.thy
src/HOL/Auth/Guard/Guard_NS_Public.thy
src/HOL/Auth/Guard/Guard_OtwayRees.thy
src/HOL/Auth/Guard/Guard_Yahalom.thy
src/HOL/Auth/Guard/List_Msg.thy
src/HOL/Auth/Guard/Proto.thy
src/HOL/Auth/KerberosIV.thy
src/HOL/Auth/KerberosIV_Gets.thy
src/HOL/Auth/KerberosV.thy
src/HOL/Auth/Kerberos_BAN.thy
src/HOL/Auth/Kerberos_BAN_Gets.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Recur.thy
src/HOL/Auth/Smartcard/EventSC.thy
src/HOL/Auth/TLS.thy
src/HOL/Auth/ZhouGollmann.thy
src/HOL/MicroJava/J/Example.thy
     1.1 --- a/src/HOL/Auth/CertifiedEmail.thy	Thu Sep 28 23:42:32 2006 +0200
     1.2 +++ b/src/HOL/Auth/CertifiedEmail.thy	Thu Sep 28 23:42:35 2006 +0200
     1.3 @@ -7,13 +7,12 @@
     1.4  
     1.5  theory CertifiedEmail imports Public begin
     1.6  
     1.7 -syntax
     1.8 -  TTP        :: agent
     1.9 -  RPwd       :: "agent => key"
    1.10 +abbreviation
    1.11 +  TTP :: agent
    1.12 +  "TTP == Server"
    1.13  
    1.14 -translations
    1.15 -  "TTP"   == "Server "
    1.16 -  "RPwd"  == "shrK "
    1.17 +  RPwd :: "agent => key"
    1.18 +  "RPwd == shrK"
    1.19  
    1.20   
    1.21  (*FIXME: the four options should be represented by pairs of 0 or 1.
     2.1 --- a/src/HOL/Auth/Event.thy	Thu Sep 28 23:42:32 2006 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Thu Sep 28 23:42:35 2006 +0200
     2.3 @@ -27,11 +27,10 @@
     2.4  
     2.5  
     2.6  text{*The constant "spies" is retained for compatibility's sake*}
     2.7 -syntax
     2.8 +
     2.9 +abbreviation (input)
    2.10    spies  :: "event list => msg set"
    2.11 -
    2.12 -translations
    2.13 -  "spies"   => "knows Spy"
    2.14 +  "spies == knows Spy"
    2.15  
    2.16  text{*Spy has access to his own key for spoof messages, but Server is secure*}
    2.17  specification (bad)
     3.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Thu Sep 28 23:42:32 2006 +0200
     3.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Thu Sep 28 23:42:35 2006 +0200
     3.3 @@ -85,9 +85,9 @@
     3.4  lemma Crypt_isnt_MPair [iff]: "~ is_MPair (Crypt K X)"
     3.5  by simp
     3.6  
     3.7 -syntax not_MPair :: "msg => bool"
     3.8 -
     3.9 -translations "not_MPair X" == "~ is_MPair X"
    3.10 +abbreviation
    3.11 +  not_MPair :: "msg => bool"
    3.12 +  "not_MPair X == ~ is_MPair X"
    3.13  
    3.14  lemma is_MPairE: "[| is_MPair X ==> P; not_MPair X ==> P |] ==> P"
    3.15  by auto
    3.16 @@ -369,11 +369,9 @@
    3.17       | Notes A' X => if A=A' then insert X (knows' A evs) else knows' A evs
    3.18     ))"
    3.19  
    3.20 -translations "spies" == "knows Spy"
    3.21 -
    3.22 -syntax spies' :: "event list => msg set"
    3.23 -
    3.24 -translations "spies'" == "knows' Spy"
    3.25 +abbreviation
    3.26 +  spies' :: "event list => msg set"
    3.27 +  "spies' == knows' Spy"
    3.28  
    3.29  subsubsection{*decomposition of knows into knows' and initState*}
    3.30  
    3.31 @@ -453,9 +451,9 @@
    3.32  constdefs knows_max :: "agent => event list => msg set"
    3.33  "knows_max A evs == knows_max' A evs Un initState A"
    3.34  
    3.35 -consts spies_max :: "event list => msg set"
    3.36 -
    3.37 -translations "spies_max evs" == "knows_max Spy evs"
    3.38 +abbreviation
    3.39 +  spies_max :: "event list => msg set"
    3.40 +  "spies_max evs == knows_max Spy evs"
    3.41  
    3.42  subsubsection{*basic facts about @{term knows_max}*}
    3.43  
     4.1 --- a/src/HOL/Auth/Guard/Guard.thy	Thu Sep 28 23:42:32 2006 +0200
     4.2 +++ b/src/HOL/Auth/Guard/Guard.thy	Thu Sep 28 23:42:35 2006 +0200
     4.3 @@ -162,9 +162,9 @@
     4.4  
     4.5  subsection{*set obtained by decrypting a message*}
     4.6  
     4.7 -syntax decrypt :: "msg set => key => msg => msg set"
     4.8 -
     4.9 -translations "decrypt H K Y" => "insert Y (H - {Crypt K Y})"
    4.10 +abbreviation (input)
    4.11 +  decrypt :: "msg set => key => msg => msg set"
    4.12 +  "decrypt H K Y == insert Y (H - {Crypt K Y})"
    4.13  
    4.14  lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Nonce n:analz H |]
    4.15  ==> Nonce n:analz (decrypt H K Y)"
     5.1 --- a/src/HOL/Auth/Guard/GuardK.thy	Thu Sep 28 23:42:32 2006 +0200
     5.2 +++ b/src/HOL/Auth/Guard/GuardK.thy	Thu Sep 28 23:42:35 2006 +0200
     5.3 @@ -158,9 +158,9 @@
     5.4  
     5.5  subsection{*set obtained by decrypting a message*}
     5.6  
     5.7 -syntax decrypt :: "msg set => key => msg => msg set"
     5.8 -
     5.9 -translations "decrypt H K Y" => "insert Y (H - {Crypt K Y})"
    5.10 +abbreviation (input)
    5.11 +  decrypt :: "msg set => key => msg => msg set"
    5.12 +  "decrypt H K Y == insert Y (H - {Crypt K Y})"
    5.13  
    5.14  lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Key n:analz H |]
    5.15  ==> Key n:analz (decrypt H K Y)"
     6.1 --- a/src/HOL/Auth/Guard/Guard_NS_Public.thy	Thu Sep 28 23:42:32 2006 +0200
     6.2 +++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Thu Sep 28 23:42:35 2006 +0200
     6.3 @@ -17,28 +17,22 @@
     6.4  
     6.5  subsection{*messages used in the protocol*}
     6.6  
     6.7 -syntax ns1 :: "agent => agent => nat => event"
     6.8 -
     6.9 -translations "ns1 A B NA" => "Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
    6.10 +abbreviation (input)
    6.11 +  ns1 :: "agent => agent => nat => event"
    6.12 +  "ns1 A B NA == Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
    6.13  
    6.14 -syntax ns1' :: "agent => agent => agent => nat => event"
    6.15 -
    6.16 -translations "ns1' A' A B NA"
    6.17 -=> "Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
    6.18 -
    6.19 -syntax ns2 :: "agent => agent => nat => nat => event"
    6.20 +  ns1' :: "agent => agent => agent => nat => event"
    6.21 +  "ns1' A' A B NA == Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
    6.22  
    6.23 -translations "ns2 B A NA NB"
    6.24 -=> "Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
    6.25 -
    6.26 -syntax ns2' :: "agent => agent => agent => nat => nat => event"
    6.27 +  ns2 :: "agent => agent => nat => nat => event"
    6.28 +  "ns2 B A NA NB == Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
    6.29  
    6.30 -translations "ns2' B' B A NA NB"
    6.31 -=> "Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
    6.32 +  ns2' :: "agent => agent => agent => nat => nat => event"
    6.33 +  "ns2' B' B A NA NB == Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
    6.34  
    6.35 -syntax ns3 :: "agent => agent => nat => event"
    6.36 +  ns3 :: "agent => agent => nat => event"
    6.37 +  "ns3 A B NB == Says A B (Crypt (pubK B) (Nonce NB))"
    6.38  
    6.39 -translations "ns3 A B NB" => "Says A B (Crypt (pubK B) (Nonce NB))"
    6.40  
    6.41  subsection{*definition of the protocol*}
    6.42  
     7.1 --- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Thu Sep 28 23:42:32 2006 +0200
     7.2 +++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Thu Sep 28 23:42:35 2006 +0200
     7.3 @@ -15,53 +15,42 @@
     7.4  
     7.5  subsection{*messages used in the protocol*}
     7.6  
     7.7 -syntax nil :: "msg"
     7.8 -
     7.9 -translations "nil" == "Number 0"
    7.10 -
    7.11 -syntax or1 :: "agent => agent => nat => event"
    7.12 -
    7.13 -translations "or1 A B NA"
    7.14 -=> "Says A B {|Nonce NA, Agent A, Agent B,
    7.15 -               Ciph A {|Nonce NA, Agent A, Agent B|}|}"
    7.16 +abbreviation
    7.17 +  nil :: "msg"
    7.18 +  "nil == Number 0"
    7.19  
    7.20 -syntax or1' :: "agent => agent => agent => nat => msg => event"
    7.21 -
    7.22 -translations "or1' A' A B NA X"
    7.23 -=> "Says A' B {|Nonce NA, Agent A, Agent B, X|}"
    7.24 +  or1 :: "agent => agent => nat => event"
    7.25 +  "or1 A B NA ==
    7.26 +    Says A B {|Nonce NA, Agent A, Agent B, Ciph A {|Nonce NA, Agent A, Agent B|}|}"
    7.27  
    7.28 -syntax or2 :: "agent => agent => nat => nat => msg => event"
    7.29 +  or1' :: "agent => agent => agent => nat => msg => event"
    7.30 +  "or1' A' A B NA X == Says A' B {|Nonce NA, Agent A, Agent B, X|}"
    7.31  
    7.32 -translations "or2 A B NA NB X"
    7.33 -=> "Says B Server {|Nonce NA, Agent A, Agent B, X,
    7.34 +  or2 :: "agent => agent => nat => nat => msg => event"
    7.35 +  "or2 A B NA NB X ==
    7.36 +    Says B Server {|Nonce NA, Agent A, Agent B, X,
    7.37                      Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
    7.38  
    7.39 -syntax or2' :: "agent => agent => agent => nat => nat => event"
    7.40 -
    7.41 -translations "or2' B' A B NA NB"
    7.42 -=> "Says B' Server {|Nonce NA, Agent A, Agent B,
    7.43 +  or2' :: "agent => agent => agent => nat => nat => event"
    7.44 +  "or2' B' A B NA NB ==
    7.45 +    Says B' Server {|Nonce NA, Agent A, Agent B,
    7.46                       Ciph A {|Nonce NA, Agent A, Agent B|},
    7.47                       Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
    7.48  
    7.49 -syntax or3 :: "agent => agent => nat => nat => key => event"
    7.50 -
    7.51 -translations "or3 A B NA NB K"
    7.52 -=> "Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
    7.53 +  or3 :: "agent => agent => nat => nat => key => event"
    7.54 +  "or3 A B NA NB K ==
    7.55 +    Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
    7.56                      Ciph B {|Nonce NB, Key K|}|}"
    7.57  
    7.58 -syntax or3':: "agent => msg => agent => agent => nat => nat => key => event"
    7.59 -
    7.60 -translations "or3' S Y A B NA NB K"
    7.61 -=> "Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
    7.62 -
    7.63 -syntax or4 :: "agent => agent => nat => msg => event"
    7.64 +  or3':: "agent => msg => agent => agent => nat => nat => key => event"
    7.65 +  "or3' S Y A B NA NB K ==
    7.66 +    Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
    7.67  
    7.68 -translations "or4 A B NA X" => "Says B A {|Nonce NA, X, nil|}"
    7.69 +  or4 :: "agent => agent => nat => msg => event"
    7.70 +  "or4 A B NA X == Says B A {|Nonce NA, X, nil|}"
    7.71  
    7.72 -syntax or4' :: "agent => agent => nat => msg => event"
    7.73 -
    7.74 -translations "or4' B' A NA K" =>
    7.75 -"Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
    7.76 +  or4' :: "agent => agent => nat => key => event"
    7.77 +  "or4' B' A NA K == Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
    7.78  
    7.79  subsection{*definition of the protocol*}
    7.80  
     8.1 --- a/src/HOL/Auth/Guard/Guard_Yahalom.thy	Thu Sep 28 23:42:32 2006 +0200
     8.2 +++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Thu Sep 28 23:42:35 2006 +0200
     8.3 @@ -15,42 +15,34 @@
     8.4  
     8.5  subsection{*messages used in the protocol*}
     8.6  
     8.7 -syntax ya1 :: "agent => agent => nat => event"
     8.8 -
     8.9 -translations "ya1 A B NA" => "Says A B {|Agent A, Nonce NA|}"
    8.10 +abbreviation (input)
    8.11 +  ya1 :: "agent => agent => nat => event"
    8.12 +  "ya1 A B NA == Says A B {|Agent A, Nonce NA|}"
    8.13  
    8.14 -syntax ya1' :: "agent => agent => agent => nat => event"
    8.15 -
    8.16 -translations "ya1' A' A B NA" => "Says A' B {|Agent A, Nonce NA|}"
    8.17 -
    8.18 -syntax ya2 :: "agent => agent => nat => nat => event"
    8.19 +  ya1' :: "agent => agent => agent => nat => event"
    8.20 +  "ya1' A' A B NA == Says A' B {|Agent A, Nonce NA|}"
    8.21  
    8.22 -translations "ya2 A B NA NB"
    8.23 -=> "Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
    8.24 -
    8.25 -syntax ya2' :: "agent => agent => agent => nat => nat => event"
    8.26 +  ya2 :: "agent => agent => nat => nat => event"
    8.27 +  "ya2 A B NA NB == Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
    8.28  
    8.29 -translations "ya2' B' A B NA NB"
    8.30 -=> "Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
    8.31 +  ya2' :: "agent => agent => agent => nat => nat => event"
    8.32 +  "ya2' B' A B NA NB == Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
    8.33  
    8.34 -syntax ya3 :: "agent => agent => nat => nat => key => event"
    8.35 -
    8.36 -translations "ya3 A B NA NB K"
    8.37 -=> "Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
    8.38 +  ya3 :: "agent => agent => nat => nat => key => event"
    8.39 +  "ya3 A B NA NB K ==
    8.40 +    Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
    8.41                      Ciph B {|Agent A, Key K|}|}"
    8.42  
    8.43 -syntax ya3':: "agent => msg => agent => agent => nat => nat => key => event"
    8.44 -
    8.45 -translations "ya3' S Y A B NA NB K"
    8.46 -=> "Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
    8.47 +  ya3':: "agent => msg => agent => agent => nat => nat => key => event"
    8.48 +  "ya3' S Y A B NA NB K ==
    8.49 +    Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
    8.50  
    8.51 -syntax ya4 :: "agent => agent => nat => nat => msg => event"
    8.52 -
    8.53 -translations "ya4 A B K NB Y" => "Says A B {|Y, Crypt K (Nonce NB)|}"
    8.54 +  ya4 :: "agent => agent => nat => nat => msg => event"
    8.55 +  "ya4 A B K NB Y == Says A B {|Y, Crypt K (Nonce NB)|}"
    8.56  
    8.57 -syntax ya4' :: "agent => agent => nat => nat => msg => event"
    8.58 +  ya4' :: "agent => agent => nat => nat => msg => event"
    8.59 +  "ya4' A' B K NB Y == Says A' B {|Y, Crypt K (Nonce NB)|}"
    8.60  
    8.61 -translations "ya4' A' B K NB Y" => "Says A' B {|Y, Crypt K (Nonce NB)|}"
    8.62  
    8.63  subsection{*definition of the protocol*}
    8.64  
     9.1 --- a/src/HOL/Auth/Guard/List_Msg.thy	Thu Sep 28 23:42:32 2006 +0200
     9.2 +++ b/src/HOL/Auth/Guard/List_Msg.thy	Thu Sep 28 23:42:35 2006 +0200
     9.3 @@ -17,15 +17,15 @@
     9.4  
     9.5  subsubsection{*nil is represented by any message which is not a pair*}
     9.6  
     9.7 -syntax cons :: "msg => msg => msg"
     9.8 -
     9.9 -translations "cons x l" => "{|x,l|}"
    9.10 +abbreviation (input)
    9.11 +  cons :: "msg => msg => msg"
    9.12 +  "cons x l == {|x,l|}"
    9.13  
    9.14  subsubsection{*induction principle*}
    9.15  
    9.16  lemma lmsg_induct: "[| !!x. not_MPair x ==> P x; !!x l. P l ==> P (cons x l) |]
    9.17  ==> P l"
    9.18 -by (induct l, auto)
    9.19 +by (induct l) auto
    9.20  
    9.21  subsubsection{*head*}
    9.22  
    9.23 @@ -50,7 +50,7 @@
    9.24  "len other = 0"
    9.25  
    9.26  lemma len_not_empty: "n < len l ==> EX x l'. l = cons x l'"
    9.27 -by (cases l, auto)
    9.28 +by (cases l) auto
    9.29  
    9.30  subsubsection{*membership*}
    9.31  
    9.32 @@ -69,10 +69,10 @@
    9.33  "del (x, other) = other"
    9.34  
    9.35  lemma notin_del [simp]: "~ isin (x,l) ==> del (x,l) = l"
    9.36 -by (induct l, auto)
    9.37 +by (induct l) auto
    9.38  
    9.39  lemma isin_del [rule_format]: "isin (y, del (x,l)) --> isin (y,l)"
    9.40 -by (induct l, auto)
    9.41 +by (induct l) auto
    9.42  
    9.43  subsubsection{*concatenation*}
    9.44  
    9.45 @@ -83,7 +83,7 @@
    9.46  "app (other, l') = l'"
    9.47  
    9.48  lemma isin_app [iff]: "isin (x, app(l,l')) = (isin (x,l) | isin (x,l'))"
    9.49 -by (induct l, auto)
    9.50 +by (induct l) auto
    9.51  
    9.52  subsubsection{*replacement*}
    9.53  
    9.54 @@ -104,7 +104,7 @@
    9.55  "ith (other, i) = other"
    9.56  
    9.57  lemma ith_head: "0 < len l ==> ith (l,0) = head l"
    9.58 -by (cases l, auto)
    9.59 +by (cases l) auto
    9.60  
    9.61  subsubsection{*insertion*}
    9.62  
    9.63 @@ -115,7 +115,7 @@
    9.64  "ins (l, 0, y) = cons y l"
    9.65  
    9.66  lemma ins_head [simp]: "ins (l,0,y) = cons y l"
    9.67 -by (cases l, auto)
    9.68 +by (cases l) auto
    9.69  
    9.70  subsubsection{*truncation*}
    9.71  
    9.72 @@ -126,16 +126,16 @@
    9.73  "trunc (cons x l, Suc i) = trunc (l,i)"
    9.74  
    9.75  lemma trunc_zero [simp]: "trunc (l,0) = l"
    9.76 -by (cases l, auto)
    9.77 +by (cases l) auto
    9.78  
    9.79  
    9.80  subsection{*Agent Lists*}
    9.81  
    9.82  subsubsection{*set of well-formed agent-list messages*}
    9.83  
    9.84 -syntax nil :: msg
    9.85 -
    9.86 -translations "nil" == "Number 0"
    9.87 +abbreviation
    9.88 +  nil :: msg
    9.89 +  "nil == Number 0"
    9.90  
    9.91  consts agl :: "msg set"
    9.92  
    10.1 --- a/src/HOL/Auth/Guard/Proto.thy	Thu Sep 28 23:42:32 2006 +0200
    10.2 +++ b/src/HOL/Auth/Guard/Proto.thy	Thu Sep 28 23:42:35 2006 +0200
    10.3 @@ -17,9 +17,9 @@
    10.4  
    10.5  types rule = "event set * event"
    10.6  
    10.7 -syntax msg' :: "rule => msg"
    10.8 -
    10.9 -translations "msg' R" == "msg (snd R)"
   10.10 +abbreviation
   10.11 +  msg' :: "rule => msg"
   10.12 +  "msg' R == msg (snd R)"
   10.13  
   10.14  types proto = "rule set"
   10.15  
   10.16 @@ -76,17 +76,18 @@
   10.17  "ap s (Gets A X) = Gets (agent s A) (apm s X)"
   10.18  "ap s (Notes A X) = Notes (agent s A) (apm s X)"
   10.19  
   10.20 -syntax
   10.21 -ap' :: "rule => msg"
   10.22 -apm' :: "rule => msg"
   10.23 -priK' :: "subs => agent => key"
   10.24 -pubK' :: "subs => agent => key"
   10.25 +abbreviation
   10.26 +  ap' :: "subs => rule => event"
   10.27 +  "ap' s R == ap s (snd R)"
   10.28  
   10.29 -translations
   10.30 -"ap' s R" == "ap s (snd R)"
   10.31 -"apm' s R" == "apm s (msg' R)"
   10.32 -"priK' s A" == "priK (agent s A)"
   10.33 -"pubK' s A" == "pubK (agent s A)"
   10.34 +  apm' :: "subs => rule => msg"
   10.35 +  "apm' s R == apm s (msg' R)"
   10.36 +
   10.37 +  priK' :: "subs => agent => key"
   10.38 +  "priK' s A == priK (agent s A)"
   10.39 +
   10.40 +  pubK' :: "subs => agent => key"
   10.41 +  "pubK' s A == pubK (agent s A)"
   10.42  
   10.43  subsection{*nonces generated by a rule*}
   10.44  
   10.45 @@ -377,32 +378,31 @@
   10.46  
   10.47  consts
   10.48  ns :: proto
   10.49 -ns1 :: rule
   10.50 -ns2 :: rule
   10.51 -ns3 :: rule
   10.52  
   10.53 -translations
   10.54 -"ns1" == "({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
   10.55 +abbreviation
   10.56 +  ns1 :: rule
   10.57 +  "ns1 == ({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
   10.58  
   10.59 -"ns2" == "({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})},
   10.60 -Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))"
   10.61 +  ns2 :: rule
   10.62 +  "ns2 == ({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})},
   10.63 +    Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))"
   10.64  
   10.65 -"ns3" == "({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}),
   10.66 -Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})},
   10.67 -Says a b (Crypt (pubK b) (Nonce Nb)))"
   10.68 +  ns3 :: rule
   10.69 +  "ns3 == ({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}),
   10.70 +    Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})},
   10.71 +    Says a b (Crypt (pubK b) (Nonce Nb)))"
   10.72  
   10.73  inductive ns intros
   10.74  [iff]: "ns1:ns"
   10.75  [iff]: "ns2:ns"
   10.76  [iff]: "ns3:ns"
   10.77  
   10.78 -syntax
   10.79 -ns3a :: msg
   10.80 -ns3b :: msg
   10.81 +abbreviation (input)
   10.82 +  ns3a :: event
   10.83 +  "ns3a == Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
   10.84  
   10.85 -translations
   10.86 -"ns3a" => "Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
   10.87 -"ns3b" => "Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})"
   10.88 +  ns3b :: event
   10.89 +  "ns3b == Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})"
   10.90  
   10.91  constdefs keys :: "keyfun"
   10.92  "keys R' s' n evs == {priK' s' a, priK' s' b}"
    11.1 --- a/src/HOL/Auth/KerberosIV.thy	Thu Sep 28 23:42:32 2006 +0200
    11.2 +++ b/src/HOL/Auth/KerberosIV.thy	Thu Sep 28 23:42:35 2006 +0200
    11.3 @@ -10,33 +10,18 @@
    11.4  
    11.5  text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
    11.6  
    11.7 -syntax
    11.8 +abbreviation
    11.9    Kas :: agent
   11.10 -  Tgs :: agent  --{*the two servers are translations...*}
   11.11 +  "Kas == Server"
   11.12  
   11.13 -
   11.14 -translations
   11.15 -  "Kas"       == "Server "
   11.16 -  "Tgs"       == "Friend 0"
   11.17 +  Tgs :: agent
   11.18 +  "Tgs == Friend 0"
   11.19  
   11.20  
   11.21  axioms
   11.22    Tgs_not_bad [iff]: "Tgs \<notin> bad"
   11.23     --{*Tgs is secure --- we already know that Kas is secure*}
   11.24  
   11.25 -(*The current time is the length of the trace*)
   11.26 -syntax
   11.27 -    CT :: "event list=>nat"
   11.28 -
   11.29 -    expiredAK :: "[nat, event list] => bool"
   11.30 -
   11.31 -    expiredSK :: "[nat, event list] => bool"
   11.32 -
   11.33 -    expiredA :: "[nat, event list] => bool"
   11.34 -
   11.35 -    valid :: "[nat, nat] => bool" ("valid _ wrt _")
   11.36 -
   11.37 -
   11.38  constdefs
   11.39   (* authKeys are those contained in an authTicket *)
   11.40      authKeys :: "event list => key set"
   11.41 @@ -92,16 +77,22 @@
   11.42    replylife_LB [iff]: "Suc 0 \<le> replylife"
   11.43      by blast
   11.44  
   11.45 -translations
   11.46 -   "CT" == "length "
   11.47 +abbreviation
   11.48 +  (*The current time is the length of the trace*)
   11.49 +  CT :: "event list=>nat"
   11.50 +  "CT == length"
   11.51  
   11.52 -   "expiredAK Ta evs" == "authKlife + Ta < CT evs"
   11.53 +  expiredAK :: "[nat, event list] => bool"
   11.54 +  "expiredAK Ta evs == authKlife + Ta < CT evs"
   11.55  
   11.56 -   "expiredSK Ts evs" == "servKlife + Ts < CT evs"
   11.57 +  expiredSK :: "[nat, event list] => bool"
   11.58 +  "expiredSK Ts evs == servKlife + Ts < CT evs"
   11.59  
   11.60 -   "expiredA T evs" == "authlife + T < CT evs"
   11.61 +  expiredA :: "[nat, event list] => bool"
   11.62 +  "expiredA T evs == authlife + T < CT evs"
   11.63  
   11.64 -   "valid T1 wrt T2" == "T1 <= replylife + T2"
   11.65 +  valid :: "[nat, nat] => bool" ("valid _ wrt _")
   11.66 +  "valid T1 wrt T2 == T1 <= replylife + T2"
   11.67  
   11.68  (*---------------------------------------------------------------------*)
   11.69  
    12.1 --- a/src/HOL/Auth/KerberosIV_Gets.thy	Thu Sep 28 23:42:32 2006 +0200
    12.2 +++ b/src/HOL/Auth/KerberosIV_Gets.thy	Thu Sep 28 23:42:35 2006 +0200
    12.3 @@ -10,33 +10,18 @@
    12.4  
    12.5  text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
    12.6  
    12.7 -syntax
    12.8 +abbreviation
    12.9    Kas :: agent
   12.10 -  Tgs :: agent  --{*the two servers are translations...*}
   12.11 +  "Kas == Server"
   12.12  
   12.13 -
   12.14 -translations
   12.15 -  "Kas"       == "Server "
   12.16 -  "Tgs"       == "Friend 0"
   12.17 +  Tgs :: agent
   12.18 +  "Tgs == Friend 0"
   12.19  
   12.20  
   12.21  axioms
   12.22    Tgs_not_bad [iff]: "Tgs \<notin> bad"
   12.23     --{*Tgs is secure --- we already know that Kas is secure*}
   12.24  
   12.25 -(*The current time is just the length of the trace!*)
   12.26 -syntax
   12.27 -    CT :: "event list=>nat"
   12.28 -
   12.29 -    expiredAK :: "[nat, event list] => bool"
   12.30 -
   12.31 -    expiredSK :: "[nat, event list] => bool"
   12.32 -
   12.33 -    expiredA :: "[nat, event list] => bool"
   12.34 -
   12.35 -    valid :: "[nat, nat] => bool" ("valid _ wrt _")
   12.36 -
   12.37 -
   12.38  constdefs
   12.39   (* authKeys are those contained in an authTicket *)
   12.40      authKeys :: "event list => key set"
   12.41 @@ -80,16 +65,22 @@
   12.42    replylife_LB [iff]: "Suc 0 \<le> replylife"
   12.43      by blast
   12.44  
   12.45 -translations
   12.46 -   "CT" == "length "
   12.47 +abbreviation
   12.48 +  (*The current time is just the length of the trace!*)
   12.49 +  CT :: "event list=>nat"
   12.50 +  "CT == length"
   12.51  
   12.52 -   "expiredAK Ta evs" == "authKlife + Ta < CT evs"
   12.53 +  expiredAK :: "[nat, event list] => bool"
   12.54 +  "expiredAK Ta evs == authKlife + Ta < CT evs"
   12.55  
   12.56 -   "expiredSK Ts evs" == "servKlife + Ts < CT evs"
   12.57 +  expiredSK :: "[nat, event list] => bool"
   12.58 +  "expiredSK Ts evs == servKlife + Ts < CT evs"
   12.59  
   12.60 -   "expiredA T evs" == "authlife + T < CT evs"
   12.61 +  expiredA :: "[nat, event list] => bool"
   12.62 +  "expiredA T evs == authlife + T < CT evs"
   12.63  
   12.64 -   "valid T1 wrt T2" == "T1 <= replylife + T2"
   12.65 +  valid :: "[nat, nat] => bool" ("valid _ wrt _")
   12.66 +  "valid T1 wrt T2 == T1 <= replylife + T2"
   12.67  
   12.68  (*---------------------------------------------------------------------*)
   12.69  
    13.1 --- a/src/HOL/Auth/KerberosV.thy	Thu Sep 28 23:42:32 2006 +0200
    13.2 +++ b/src/HOL/Auth/KerberosV.thy	Thu Sep 28 23:42:35 2006 +0200
    13.3 @@ -8,33 +8,18 @@
    13.4  
    13.5  text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
    13.6  
    13.7 -syntax
    13.8 +abbreviation
    13.9    Kas :: agent
   13.10 -  Tgs :: agent  --{*the two servers are translations...*}
   13.11 +  "Kas == Server"
   13.12  
   13.13 -
   13.14 -translations
   13.15 -  "Kas"       == "Server "
   13.16 -  "Tgs"       == "Friend 0"
   13.17 +  Tgs :: agent
   13.18 +  "Tgs == Friend 0"
   13.19  
   13.20  
   13.21  axioms
   13.22    Tgs_not_bad [iff]: "Tgs \<notin> bad"
   13.23     --{*Tgs is secure --- we already know that Kas is secure*}
   13.24  
   13.25 -(*The current time is just the length of the trace!*)
   13.26 -syntax
   13.27 -    CT :: "event list=>nat"
   13.28 -
   13.29 -    expiredAK :: "[nat, event list] => bool"
   13.30 -
   13.31 -    expiredSK :: "[nat, event list] => bool"
   13.32 -
   13.33 -    expiredA :: "[nat, event list] => bool"
   13.34 -
   13.35 -    valid :: "[nat, nat] => bool"  ("valid _ wrt _")
   13.36 -
   13.37 -
   13.38  constdefs
   13.39   (* authKeys are those contained in an authTicket *)
   13.40      authKeys :: "event list => key set"
   13.41 @@ -81,16 +66,22 @@
   13.42    replylife_LB [iff]: "Suc 0 \<le> replylife"
   13.43      by blast
   13.44  
   13.45 -translations
   13.46 -   "CT" == "length "
   13.47 +abbreviation
   13.48 +  (*The current time is just the length of the trace!*)
   13.49 +  CT :: "event list=>nat"
   13.50 +  "CT == length"
   13.51  
   13.52 -   "expiredAK T evs" == "authKlife + T < CT evs"
   13.53 +  expiredAK :: "[nat, event list] => bool"
   13.54 +  "expiredAK T evs == authKlife + T < CT evs"
   13.55  
   13.56 -   "expiredSK T evs" == "servKlife + T < CT evs"
   13.57 +  expiredSK :: "[nat, event list] => bool"
   13.58 +  "expiredSK T evs == servKlife + T < CT evs"
   13.59  
   13.60 -   "expiredA T evs" == "authlife + T < CT evs"
   13.61 +  expiredA :: "[nat, event list] => bool"
   13.62 +  "expiredA T evs == authlife + T < CT evs"
   13.63  
   13.64 -   "valid T1 wrt T2" == "T1 <= replylife + T2"
   13.65 +  valid :: "[nat, nat] => bool"  ("valid _ wrt _")
   13.66 +  "valid T1 wrt T2 == T1 <= replylife + T2"
   13.67  
   13.68  (*---------------------------------------------------------------------*)
   13.69  
    14.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Thu Sep 28 23:42:32 2006 +0200
    14.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Thu Sep 28 23:42:35 2006 +0200
    14.3 @@ -20,11 +20,6 @@
    14.4  (* Temporal model of accidents: session keys can be leaked
    14.5                                  ONLY when they have expired *)
    14.6  
    14.7 -syntax
    14.8 -    CT :: "event list=>nat"
    14.9 -    expiredK :: "[nat, event list] => bool"
   14.10 -    expiredA :: "[nat, event list] => bool"
   14.11 -
   14.12  consts
   14.13  
   14.14      (*Duration of the session key*)
   14.15 @@ -43,13 +38,15 @@
   14.16    authlife_LB [iff]:    "0 < authlife"
   14.17      by blast
   14.18  
   14.19 -
   14.20 -translations
   14.21 -   "CT" == "length "
   14.22 +abbreviation
   14.23 +  CT :: "event list=>nat"
   14.24 +  "CT == length "
   14.25  
   14.26 -   "expiredK T evs" == "sesKlife + T < CT evs"
   14.27 +  expiredK :: "[nat, event list] => bool"
   14.28 +  "expiredK T evs == sesKlife + T < CT evs"
   14.29  
   14.30 -   "expiredA T evs" == "authlife + T < CT evs"
   14.31 +  expiredA :: "[nat, event list] => bool"
   14.32 +  "expiredA T evs == authlife + T < CT evs"
   14.33  
   14.34  
   14.35  constdefs
    15.1 --- a/src/HOL/Auth/Kerberos_BAN_Gets.thy	Thu Sep 28 23:42:32 2006 +0200
    15.2 +++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy	Thu Sep 28 23:42:35 2006 +0200
    15.3 @@ -18,11 +18,6 @@
    15.4  (* Temporal modelization: session keys can be leaked
    15.5                            ONLY when they have expired *)
    15.6  
    15.7 -syntax
    15.8 -    CT :: "event list=>nat"
    15.9 -    expiredK :: "[nat, event list] => bool"
   15.10 -    expiredA :: "[nat, event list] => bool"
   15.11 -
   15.12  consts
   15.13  
   15.14      (*Duration of the session key*)
   15.15 @@ -44,12 +39,15 @@
   15.16      by blast
   15.17  
   15.18  
   15.19 -translations
   15.20 -   "CT" == "length "
   15.21 +abbreviation
   15.22 +  CT :: "event list=>nat"
   15.23 +  "CT == length"
   15.24  
   15.25 -   "expiredK T evs" == "sesKlife + T < CT evs"
   15.26 +  expiredK :: "[nat, event list] => bool"
   15.27 +  "expiredK T evs == sesKlife + T < CT evs"
   15.28  
   15.29 -   "expiredA T evs" == "authlife + T < CT evs"
   15.30 +  expiredA :: "[nat, event list] => bool"
   15.31 +  "expiredA T evs == authlife + T < CT evs"
   15.32  
   15.33  
   15.34  constdefs
    16.1 --- a/src/HOL/Auth/Public.thy	Thu Sep 28 23:42:32 2006 +0200
    16.2 +++ b/src/HOL/Auth/Public.thy	Thu Sep 28 23:42:35 2006 +0200
    16.3 @@ -20,33 +20,32 @@
    16.4  consts
    16.5    publicKey :: "[keymode,agent] => key"
    16.6  
    16.7 -syntax
    16.8 +abbreviation
    16.9    pubEK :: "agent => key"
   16.10 -  pubSK :: "agent => key"
   16.11 +  "pubEK == publicKey Encryption"
   16.12  
   16.13 -  privateKey :: "[bool,agent] => key"
   16.14 -  priEK :: "agent => key"
   16.15 -  priSK :: "agent => key"
   16.16 +  pubSK :: "agent => key"
   16.17 +  "pubSK == publicKey Signature"
   16.18  
   16.19 -translations
   16.20 -  "pubEK"  == "publicKey Encryption"
   16.21 -  "pubSK"  == "publicKey Signature"
   16.22 +  privateKey :: "[keymode, agent] => key"
   16.23 +  "privateKey b A == invKey (publicKey b A)"
   16.24  
   16.25    (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
   16.26 -  "privateKey b A" == "invKey (publicKey b A)"
   16.27 -  "priEK A"  == "privateKey Encryption A"
   16.28 -  "priSK A"  == "privateKey Signature A"
   16.29 +  priEK :: "agent => key"
   16.30 +  "priEK A == privateKey Encryption A"
   16.31 +  priSK :: "agent => key"
   16.32 +  "priSK A == privateKey Signature A"
   16.33  
   16.34  
   16.35 -text{*These translations give backward compatibility.  They represent the
   16.36 +text{*These abbreviations give backward compatibility.  They represent the
   16.37  simple situation where the signature and encryption keys are the same.*}
   16.38 -syntax
   16.39 +
   16.40 +abbreviation
   16.41    pubK :: "agent => key"
   16.42 +  "pubK A == pubEK A"
   16.43 +
   16.44    priK :: "agent => key"
   16.45 -
   16.46 -translations
   16.47 -  "pubK A" == "pubEK A"
   16.48 -  "priK A" == "invKey (pubEK A)"
   16.49 +  "priK A == invKey (pubEK A)"
   16.50  
   16.51  
   16.52  text{*By freeness of agents, no two agents have the same key.  Since
    17.1 --- a/src/HOL/Auth/Recur.thy	Thu Sep 28 23:42:32 2006 +0200
    17.2 +++ b/src/HOL/Auth/Recur.thy	Thu Sep 28 23:42:35 2006 +0200
    17.3 @@ -9,8 +9,9 @@
    17.4  theory Recur imports Public begin
    17.5  
    17.6  text{*End marker for message bundles*}
    17.7 -syntax        END :: "msg"
    17.8 -translations "END" == "Number 0"
    17.9 +abbreviation
   17.10 +  END :: "msg"
   17.11 +  "END == Number 0"
   17.12  
   17.13  (*Two session keys are distributed to each agent except for the initiator,
   17.14          who receives one.
    18.1 --- a/src/HOL/Auth/Smartcard/EventSC.thy	Thu Sep 28 23:42:32 2006 +0200
    18.2 +++ b/src/HOL/Auth/Smartcard/EventSC.thy	Thu Sep 28 23:42:35 2006 +0200
    18.3 @@ -24,10 +24,9 @@
    18.4   cloned  :: "card set"   (* cloned smart cards*)
    18.5   secureM :: "bool"(*assumption of secure means between agents and their cards*)
    18.6  
    18.7 -syntax
    18.8 +abbreviation
    18.9    insecureM :: bool (*certain protocols make no assumption of secure means*)
   18.10 -translations
   18.11 -  "insecureM" == "\<not>secureM"
   18.12 +  "insecureM == \<not>secureM"
   18.13  
   18.14  
   18.15  text{*Spy has access to his own key for spoof messages, but Server is secure*}
    19.1 --- a/src/HOL/Auth/TLS.thy	Thu Sep 28 23:42:32 2006 +0200
    19.2 +++ b/src/HOL/Auth/TLS.thy	Thu Sep 28 23:42:35 2006 +0200
    19.3 @@ -63,13 +63,13 @@
    19.4      Session keys implicitly include MAC secrets.*)
    19.5    sessionK :: "(nat*nat*nat) * role => key"
    19.6  
    19.7 -syntax
    19.8 -    clientK :: "nat*nat*nat => key"
    19.9 -    serverK :: "nat*nat*nat => key"
   19.10 +abbreviation
   19.11 +  clientK :: "nat*nat*nat => key"
   19.12 +  "clientK X == sessionK(X, ClientRole)"
   19.13  
   19.14 -translations
   19.15 -  "clientK X" == "sessionK(X, ClientRole)"
   19.16 -  "serverK X" == "sessionK(X, ServerRole)"
   19.17 +  serverK :: "nat*nat*nat => key"
   19.18 +  "serverK X == sessionK(X, ServerRole)"
   19.19 +
   19.20  
   19.21  specification (PRF)
   19.22    inj_PRF: "inj PRF"
    20.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Thu Sep 28 23:42:32 2006 +0200
    20.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Thu Sep 28 23:42:35 2006 +0200
    20.3 @@ -12,23 +12,18 @@
    20.4  
    20.5  theory ZhouGollmann imports Public begin
    20.6  
    20.7 -syntax
    20.8 +abbreviation
    20.9    TTP :: agent
   20.10 +  "TTP == Server"
   20.11  
   20.12 -translations
   20.13 -  "TTP" == " Server "
   20.14 -
   20.15 -syntax
   20.16    f_sub :: nat
   20.17 +  "f_sub == 5"
   20.18    f_nro :: nat
   20.19 +  "f_nro == 2"
   20.20    f_nrr :: nat
   20.21 +  "f_nrr == 3"
   20.22    f_con :: nat
   20.23 -
   20.24 -translations
   20.25 -  "f_sub" == " 5 "
   20.26 -  "f_nro" == " 2 "
   20.27 -  "f_nrr" == " 3 "
   20.28 -  "f_con" == " 4 "
   20.29 +  "f_con == 4"
   20.30  
   20.31  
   20.32  constdefs
    21.1 --- a/src/HOL/MicroJava/J/Example.thy	Thu Sep 28 23:42:32 2006 +0200
    21.2 +++ b/src/HOL/MicroJava/J/Example.thy	Thu Sep 28 23:42:35 2006 +0200
    21.3 @@ -110,28 +110,20 @@
    21.4                      Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
    21.5  
    21.6  
    21.7 -syntax
    21.8 +abbreviation
    21.9 +  NP  :: xcpt
   21.10 +  "NP == NullPointer"
   21.11  
   21.12 -  NP  :: xcpt
   21.13    tprg  ::"java_mb prog"
   21.14 +  "tprg == [ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
   21.15 +
   21.16    obj1  :: obj
   21.17 -  obj2  :: obj
   21.18 -  s0  :: state
   21.19 -  s1  :: state
   21.20 -  s2  :: state
   21.21 -  s3  :: state
   21.22 -  s4  :: state
   21.23 +  "obj1 == (Ext, empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))"
   21.24  
   21.25 -translations
   21.26 -  "NP"   == "NullPointer"
   21.27 -  "tprg" == "[ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
   21.28 -  "obj1"    <= "(Ext, empty((vee, Base)\<mapsto>Bool False)
   21.29 -         ((vee, Ext )\<mapsto>Intg 0))"
   21.30 -  "s0" == " Norm    (empty, empty)"
   21.31 -  "s1" == " Norm    (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
   21.32 -  "s2" == " Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
   21.33 -  "s3" == "(Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
   21.34 -
   21.35 +  "s0 == Norm    (empty, empty)"
   21.36 +  "s1 == Norm    (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
   21.37 +  "s2 == Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
   21.38 +  "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
   21.39  
   21.40  ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *}
   21.41  lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb"