modernized translations;
authorwenzelm
Wed Feb 10 00:46:56 2010 +0100 (2010-02-10)
changeset 35068544867142ea4
parent 35067 af4c18c30593
child 35069 09154b995ed8
modernized translations;
src/HOL/SET_Protocol/Message_SET.thy
src/HOL/SET_Protocol/Public_SET.thy
src/HOL/TLA/Memory/ProcedureInterface.thy
src/HOL/TLA/TLA.thy
src/HOL/UNITY/Union.thy
src/HOL/Word/WordDefinition.thy
src/ZF/IMP/Com.thy
src/ZF/Induct/Comb.thy
src/ZF/Induct/PropLog.thy
src/ZF/List_ZF.thy
src/ZF/ZF.thy
     1.1 --- a/src/HOL/SET_Protocol/Message_SET.thy	Wed Feb 10 00:45:16 2010 +0100
     1.2 +++ b/src/HOL/SET_Protocol/Message_SET.thy	Wed Feb 10 00:46:56 2010 +0100
     1.3 @@ -71,14 +71,14 @@
     1.4  
     1.5  (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*)
     1.6  syntax
     1.7 -  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     1.8 +  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
     1.9  
    1.10  syntax (xsymbols)
    1.11 -  "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    1.12 +  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
    1.13  
    1.14  translations
    1.15    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    1.16 -  "{|x, y|}"      == "MPair x y"
    1.17 +  "{|x, y|}"      == "CONST MPair x y"
    1.18  
    1.19  
    1.20  constdefs
     2.1 --- a/src/HOL/SET_Protocol/Public_SET.thy	Wed Feb 10 00:45:16 2010 +0100
     2.2 +++ b/src/HOL/SET_Protocol/Public_SET.thy	Wed Feb 10 00:46:56 2010 +0100
     2.3 @@ -23,19 +23,12 @@
     2.4    publicKey :: "[bool, agent] => key"
     2.5      --{*the boolean is TRUE if a signing key*}
     2.6  
     2.7 -syntax
     2.8 -  pubEK :: "agent => key"
     2.9 -  pubSK :: "agent => key"
    2.10 -  priEK :: "agent => key"
    2.11 -  priSK :: "agent => key"
    2.12 +abbreviation "pubEK == publicKey False"
    2.13 +abbreviation "pubSK == publicKey True"
    2.14  
    2.15 -translations
    2.16 -  "pubEK"  == "publicKey False"
    2.17 -  "pubSK"  == "publicKey True"
    2.18 -
    2.19 -  (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
    2.20 -  "priEK A"  == "invKey (pubEK A)"
    2.21 -  "priSK A"  == "invKey (pubSK A)"
    2.22 +(*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
    2.23 +abbreviation "priEK A == invKey (pubEK A)"
    2.24 +abbreviation "priSK A == invKey (pubSK A)"
    2.25  
    2.26  text{*By freeness of agents, no two agents have the same key. Since
    2.27   @{term "True\<noteq>False"}, no agent has the same signing and encryption keys.*}
    2.28 @@ -159,18 +152,12 @@
    2.29      "certC PAN Ka PS T signK ==
    2.30       signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}"
    2.31  
    2.32 -  (*cert and certA have no repeated elements, so they could be translations,
    2.33 -    but that's tricky and makes proofs slower*)
    2.34 +(*cert and certA have no repeated elements, so they could be abbreviations,
    2.35 +  but that's tricky and makes proofs slower*)
    2.36  
    2.37 -syntax
    2.38 -  "onlyEnc" :: msg      
    2.39 -  "onlySig" :: msg
    2.40 -  "authCode" :: msg
    2.41 -
    2.42 -translations
    2.43 -  "onlyEnc"   == "Number 0"
    2.44 -  "onlySig"  == "Number (Suc 0)"
    2.45 -  "authCode" == "Number (Suc (Suc 0))"
    2.46 +abbreviation "onlyEnc == Number 0"
    2.47 +abbreviation "onlySig == Number (Suc 0)"
    2.48 +abbreviation "authCode == Number (Suc (Suc 0))"
    2.49  
    2.50  subsection{*Encryption Primitives*}
    2.51  
     3.1 --- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Wed Feb 10 00:45:16 2010 +0100
     3.2 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Wed Feb 10 00:46:56 2010 +0100
     3.3 @@ -55,10 +55,10 @@
     3.4    "_Return"   :: "['a, 'b, lift] => lift"    ("(Return _ _ _)" [90,90,90] 90)
     3.5  
     3.6  translations
     3.7 -  "_slice"  ==  "slice"
     3.8 +  "_slice"  ==  "CONST slice"
     3.9  
    3.10 -  "_Call"   ==  "ACall"
    3.11 -  "_Return" ==  "AReturn"
    3.12 +  "_Call"   ==  "CONST ACall"
    3.13 +  "_Return" ==  "CONST AReturn"
    3.14  
    3.15  defs
    3.16    slice_def:     "(PRED (x!i)) s == x s i"
     4.1 --- a/src/HOL/TLA/TLA.thy	Wed Feb 10 00:45:16 2010 +0100
     4.2 +++ b/src/HOL/TLA/TLA.thy	Wed Feb 10 00:46:56 2010 +0100
     4.3 @@ -37,12 +37,12 @@
     4.4    "_AAll"    :: "[idts, lift] => lift"                ("(3AALL _./ _)" [0,10] 10)
     4.5  
     4.6  translations
     4.7 -  "_Box"      ==   "Box"
     4.8 -  "_Dmd"      ==   "Dmd"
     4.9 -  "_leadsto"  ==   "leadsto"
    4.10 -  "_stable"   ==   "Stable"
    4.11 -  "_WF"       ==   "WF"
    4.12 -  "_SF"       ==   "SF"
    4.13 +  "_Box"      ==   "CONST Box"
    4.14 +  "_Dmd"      ==   "CONST Dmd"
    4.15 +  "_leadsto"  ==   "CONST leadsto"
    4.16 +  "_stable"   ==   "CONST Stable"
    4.17 +  "_WF"       ==   "CONST WF"
    4.18 +  "_SF"       ==   "CONST SF"
    4.19    "_EEx v A"  ==   "Eex v. A"
    4.20    "_AAll v A" ==   "Aall v. A"
    4.21  
     5.1 --- a/src/HOL/UNITY/Union.thy	Wed Feb 10 00:45:16 2010 +0100
     5.2 +++ b/src/HOL/UNITY/Union.thy	Wed Feb 10 00:46:56 2010 +0100
     5.3 @@ -42,7 +42,7 @@
     5.4  translations
     5.5    "JN x: A. B" == "CONST JOIN A (%x. B)"
     5.6    "JN x y. B" == "JN x. JN y. B"
     5.7 -  "JN x. B" == "JOIN CONST UNIV (%x. B)"
     5.8 +  "JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)"
     5.9  
    5.10  syntax (xsymbols)
    5.11    SKIP     :: "'a program"                              ("\<bottom>")
     6.1 --- a/src/HOL/Word/WordDefinition.thy	Wed Feb 10 00:45:16 2010 +0100
     6.2 +++ b/src/HOL/Word/WordDefinition.thy	Wed Feb 10 00:46:56 2010 +0100
     6.3 @@ -94,7 +94,7 @@
     6.4  syntax
     6.5    of_int :: "int => 'a"
     6.6  translations
     6.7 -  "case x of of_int y => b" == "CONST word_int_case (%y. b) x"
     6.8 +  "case x of CONST of_int y => b" == "CONST word_int_case (%y. b) x"
     6.9  
    6.10  
    6.11  subsection  "Arithmetic operations"
     7.1 --- a/src/ZF/IMP/Com.thy	Wed Feb 10 00:45:16 2010 +0100
     7.2 +++ b/src/ZF/IMP/Com.thy	Wed Feb 10 00:46:56 2010 +0100
     7.3 @@ -22,8 +22,10 @@
     7.4  
     7.5  
     7.6  consts evala :: i
     7.7 -syntax "_evala" :: "[i, i] => o"    (infixl "-a->" 50)
     7.8 -translations "p -a-> n" == "<p,n> \<in> evala"
     7.9 +
    7.10 +abbreviation
    7.11 +  evala_syntax :: "[i, i] => o"    (infixl "-a->" 50)
    7.12 +  where "p -a-> n == <p,n> \<in> evala"
    7.13  
    7.14  inductive
    7.15    domains "evala" \<subseteq> "(aexp \<times> (loc -> nat)) \<times> nat"
    7.16 @@ -50,8 +52,10 @@
    7.17  
    7.18  
    7.19  consts evalb :: i
    7.20 -syntax "_evalb" :: "[i,i] => o"    (infixl "-b->" 50)
    7.21 -translations "p -b-> b" == "<p,b> \<in> evalb"
    7.22 +
    7.23 +abbreviation
    7.24 +  evalb_syntax :: "[i,i] => o"    (infixl "-b->" 50)
    7.25 +  where "p -b-> b == <p,b> \<in> evalb"
    7.26  
    7.27  inductive
    7.28    domains "evalb" \<subseteq> "(bexp \<times> (loc -> nat)) \<times> bool"
    7.29 @@ -82,8 +86,10 @@
    7.30  
    7.31  
    7.32  consts evalc :: i
    7.33 -syntax "_evalc" :: "[i, i] => o"    (infixl "-c->" 50)
    7.34 -translations "p -c-> s" == "<p,s> \<in> evalc"
    7.35 +
    7.36 +abbreviation
    7.37 +  evalc_syntax :: "[i, i] => o"    (infixl "-c->" 50)
    7.38 +  where "p -c-> s == <p,s> \<in> evalc"
    7.39  
    7.40  inductive
    7.41    domains "evalc" \<subseteq> "(com \<times> (loc -> nat)) \<times> (loc -> nat)"
     8.1 --- a/src/ZF/Induct/Comb.thy	Wed Feb 10 00:45:16 2010 +0100
     8.2 +++ b/src/ZF/Induct/Comb.thy	Wed Feb 10 00:46:56 2010 +0100
     8.3 @@ -30,12 +30,14 @@
     8.4  
     8.5  consts
     8.6    contract  :: i
     8.7 -syntax
     8.8 -  "_contract"       :: "[i,i] => o"    (infixl "-1->" 50)
     8.9 -  "_contract_multi" :: "[i,i] => o"    (infixl "--->" 50)
    8.10 -translations
    8.11 -  "p -1-> q" == "<p,q> \<in> contract"
    8.12 -  "p ---> q" == "<p,q> \<in> contract^*"
    8.13 +
    8.14 +abbreviation
    8.15 +  contract_syntax :: "[i,i] => o"    (infixl "-1->" 50)
    8.16 +  where "p -1-> q == <p,q> \<in> contract"
    8.17 +
    8.18 +abbreviation
    8.19 +  contract_multi :: "[i,i] => o"    (infixl "--->" 50)
    8.20 +  where "p ---> q == <p,q> \<in> contract^*"
    8.21  
    8.22  syntax (xsymbols)
    8.23    "comb.app"    :: "[i, i] => i"             (infixl "\<bullet>" 90)
    8.24 @@ -56,12 +58,14 @@
    8.25  
    8.26  consts
    8.27    parcontract :: i
    8.28 -syntax
    8.29 -  "_parcontract" :: "[i,i] => o"    (infixl "=1=>" 50)
    8.30 -  "_parcontract_multi" :: "[i,i] => o"    (infixl "===>" 50)
    8.31 -translations
    8.32 -  "p =1=> q" == "<p,q> \<in> parcontract"
    8.33 -  "p ===> q" == "<p,q> \<in> parcontract^+"
    8.34 +
    8.35 +abbreviation
    8.36 +  parcontract_syntax :: "[i,i] => o"    (infixl "=1=>" 50)
    8.37 +  where "p =1=> q == <p,q> \<in> parcontract"
    8.38 +
    8.39 +abbreviation
    8.40 +  parcontract_multi :: "[i,i] => o"    (infixl "===>" 50)
    8.41 +  where "p ===> q == <p,q> \<in> parcontract^+"
    8.42  
    8.43  inductive
    8.44    domains "parcontract" \<subseteq> "comb \<times> comb"
     9.1 --- a/src/ZF/Induct/PropLog.thy	Wed Feb 10 00:45:16 2010 +0100
     9.2 +++ b/src/ZF/Induct/PropLog.thy	Wed Feb 10 00:46:56 2010 +0100
     9.3 @@ -34,8 +34,10 @@
     9.4  subsection {* The proof system *}
     9.5  
     9.6  consts thms     :: "i => i"
     9.7 -syntax "_thms"  :: "[i,i] => o"    (infixl "|-" 50)
     9.8 -translations "H |- p" == "p \<in> thms(H)"
     9.9 +
    9.10 +abbreviation
    9.11 +  thms_syntax :: "[i,i] => o"    (infixl "|-" 50)
    9.12 +  where "H |- p == p \<in> thms(H)"
    9.13  
    9.14  inductive
    9.15    domains "thms(H)" \<subseteq> "propn"
    10.1 --- a/src/ZF/List_ZF.thy	Wed Feb 10 00:45:16 2010 +0100
    10.2 +++ b/src/ZF/List_ZF.thy	Wed Feb 10 00:46:56 2010 +0100
    10.3 @@ -19,9 +19,9 @@
    10.4   "@List"     :: "is => i"                                 ("[(_)]")
    10.5  
    10.6  translations
    10.7 -  "[x, xs]"     == "Cons(x, [xs])"
    10.8 -  "[x]"         == "Cons(x, [])"
    10.9 -  "[]"          == "Nil"
   10.10 +  "[x, xs]"     == "CONST Cons(x, [xs])"
   10.11 +  "[x]"         == "CONST Cons(x, [])"
   10.12 +  "[]"          == "CONST Nil"
   10.13  
   10.14  
   10.15  consts
    11.1 --- a/src/ZF/ZF.thy	Wed Feb 10 00:45:16 2010 +0100
    11.2 +++ b/src/ZF/ZF.thy	Wed Feb 10 00:46:56 2010 +0100
    11.3 @@ -127,23 +127,23 @@
    11.4    "@patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
    11.5  
    11.6  translations
    11.7 -  "{x, xs}"     == "cons(x, {xs})"
    11.8 -  "{x}"         == "cons(x, 0)"
    11.9 -  "{x:A. P}"    == "Collect(A, %x. P)"
   11.10 -  "{y. x:A, Q}" == "Replace(A, %x y. Q)"
   11.11 -  "{b. x:A}"    == "RepFun(A, %x. b)"
   11.12 -  "INT x:A. B"  == "Inter({B. x:A})"
   11.13 -  "UN x:A. B"   == "Union({B. x:A})"
   11.14 -  "PROD x:A. B" == "Pi(A, %x. B)"
   11.15 -  "SUM x:A. B"  == "Sigma(A, %x. B)"
   11.16 -  "lam x:A. f"  == "Lambda(A, %x. f)"
   11.17 -  "ALL x:A. P"  == "Ball(A, %x. P)"
   11.18 -  "EX x:A. P"   == "Bex(A, %x. P)"
   11.19 +  "{x, xs}"     == "CONST cons(x, {xs})"
   11.20 +  "{x}"         == "CONST cons(x, 0)"
   11.21 +  "{x:A. P}"    == "CONST Collect(A, %x. P)"
   11.22 +  "{y. x:A, Q}" == "CONST Replace(A, %x y. Q)"
   11.23 +  "{b. x:A}"    == "CONST RepFun(A, %x. b)"
   11.24 +  "INT x:A. B"  == "CONST Inter({B. x:A})"
   11.25 +  "UN x:A. B"   == "CONST Union({B. x:A})"
   11.26 +  "PROD x:A. B" == "CONST Pi(A, %x. B)"
   11.27 +  "SUM x:A. B"  == "CONST Sigma(A, %x. B)"
   11.28 +  "lam x:A. f"  == "CONST Lambda(A, %x. f)"
   11.29 +  "ALL x:A. P"  == "CONST Ball(A, %x. P)"
   11.30 +  "EX x:A. P"   == "CONST Bex(A, %x. P)"
   11.31  
   11.32    "<x, y, z>"   == "<x, <y, z>>"
   11.33 -  "<x, y>"      == "Pair(x, y)"
   11.34 -  "%<x,y,zs>.b" == "split(%x <y,zs>.b)"
   11.35 -  "%<x,y>.b"    == "split(%x y. b)"
   11.36 +  "<x, y>"      == "CONST Pair(x, y)"
   11.37 +  "%<x,y,zs>.b" == "CONST split(%x <y,zs>.b)"
   11.38 +  "%<x,y>.b"    == "CONST split(%x y. b)"
   11.39  
   11.40  
   11.41  notation (xsymbols)