# HG changeset patch # User wenzelm # Date 1265759216 -3600 # Node ID 544867142ea402febae05d94f2e350846992aac2 # Parent af4c18c30593626654dcdd21b27581d71fc05e1c modernized translations; diff -r af4c18c30593 -r 544867142ea4 src/HOL/SET_Protocol/Message_SET.thy --- a/src/HOL/SET_Protocol/Message_SET.thy Wed Feb 10 00:45:16 2010 +0100 +++ b/src/HOL/SET_Protocol/Message_SET.thy Wed Feb 10 00:46:56 2010 +0100 @@ -71,14 +71,14 @@ (*Concrete syntax: messages appear as {|A,B,NA|}, etc...*) syntax - "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") + "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") syntax (xsymbols) - "@MTuple" :: "['a, args] => 'a * 'b" ("(2\_,/ _\)") + "_MTuple" :: "['a, args] => 'a * 'b" ("(2\_,/ _\)") translations "{|x, y, z|}" == "{|x, {|y, z|}|}" - "{|x, y|}" == "MPair x y" + "{|x, y|}" == "CONST MPair x y" constdefs diff -r af4c18c30593 -r 544867142ea4 src/HOL/SET_Protocol/Public_SET.thy --- a/src/HOL/SET_Protocol/Public_SET.thy Wed Feb 10 00:45:16 2010 +0100 +++ b/src/HOL/SET_Protocol/Public_SET.thy Wed Feb 10 00:46:56 2010 +0100 @@ -23,19 +23,12 @@ publicKey :: "[bool, agent] => key" --{*the boolean is TRUE if a signing key*} -syntax - pubEK :: "agent => key" - pubSK :: "agent => key" - priEK :: "agent => key" - priSK :: "agent => key" +abbreviation "pubEK == publicKey False" +abbreviation "pubSK == publicKey True" -translations - "pubEK" == "publicKey False" - "pubSK" == "publicKey True" - - (*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*) - "priEK A" == "invKey (pubEK A)" - "priSK A" == "invKey (pubSK A)" +(*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*) +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\False"}, no agent has the same signing and encryption keys.*} @@ -159,18 +152,12 @@ "certC PAN Ka PS T signK == signCert signK {|Hash {|Nonce PS, Pan PAN|}, Key Ka, T|}" - (*cert and certA have no repeated elements, so they could be translations, - but that's tricky and makes proofs slower*) +(*cert and certA have no repeated elements, so they could be abbreviations, + but that's tricky and makes proofs slower*) -syntax - "onlyEnc" :: msg - "onlySig" :: msg - "authCode" :: msg - -translations - "onlyEnc" == "Number 0" - "onlySig" == "Number (Suc 0)" - "authCode" == "Number (Suc (Suc 0))" +abbreviation "onlyEnc == Number 0" +abbreviation "onlySig == Number (Suc 0)" +abbreviation "authCode == Number (Suc (Suc 0))" subsection{*Encryption Primitives*} diff -r af4c18c30593 -r 544867142ea4 src/HOL/TLA/Memory/ProcedureInterface.thy --- a/src/HOL/TLA/Memory/ProcedureInterface.thy Wed Feb 10 00:45:16 2010 +0100 +++ b/src/HOL/TLA/Memory/ProcedureInterface.thy Wed Feb 10 00:46:56 2010 +0100 @@ -55,10 +55,10 @@ "_Return" :: "['a, 'b, lift] => lift" ("(Return _ _ _)" [90,90,90] 90) translations - "_slice" == "slice" + "_slice" == "CONST slice" - "_Call" == "ACall" - "_Return" == "AReturn" + "_Call" == "CONST ACall" + "_Return" == "CONST AReturn" defs slice_def: "(PRED (x!i)) s == x s i" diff -r af4c18c30593 -r 544867142ea4 src/HOL/TLA/TLA.thy --- a/src/HOL/TLA/TLA.thy Wed Feb 10 00:45:16 2010 +0100 +++ b/src/HOL/TLA/TLA.thy Wed Feb 10 00:46:56 2010 +0100 @@ -37,12 +37,12 @@ "_AAll" :: "[idts, lift] => lift" ("(3AALL _./ _)" [0,10] 10) translations - "_Box" == "Box" - "_Dmd" == "Dmd" - "_leadsto" == "leadsto" - "_stable" == "Stable" - "_WF" == "WF" - "_SF" == "SF" + "_Box" == "CONST Box" + "_Dmd" == "CONST Dmd" + "_leadsto" == "CONST leadsto" + "_stable" == "CONST Stable" + "_WF" == "CONST WF" + "_SF" == "CONST SF" "_EEx v A" == "Eex v. A" "_AAll v A" == "Aall v. A" diff -r af4c18c30593 -r 544867142ea4 src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Wed Feb 10 00:45:16 2010 +0100 +++ b/src/HOL/UNITY/Union.thy Wed Feb 10 00:46:56 2010 +0100 @@ -42,7 +42,7 @@ translations "JN x: A. B" == "CONST JOIN A (%x. B)" "JN x y. B" == "JN x. JN y. B" - "JN x. B" == "JOIN CONST UNIV (%x. B)" + "JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)" syntax (xsymbols) SKIP :: "'a program" ("\") diff -r af4c18c30593 -r 544867142ea4 src/HOL/Word/WordDefinition.thy --- a/src/HOL/Word/WordDefinition.thy Wed Feb 10 00:45:16 2010 +0100 +++ b/src/HOL/Word/WordDefinition.thy Wed Feb 10 00:46:56 2010 +0100 @@ -94,7 +94,7 @@ syntax of_int :: "int => 'a" translations - "case x of of_int y => b" == "CONST word_int_case (%y. b) x" + "case x of CONST of_int y => b" == "CONST word_int_case (%y. b) x" subsection "Arithmetic operations" diff -r af4c18c30593 -r 544867142ea4 src/ZF/IMP/Com.thy --- a/src/ZF/IMP/Com.thy Wed Feb 10 00:45:16 2010 +0100 +++ b/src/ZF/IMP/Com.thy Wed Feb 10 00:46:56 2010 +0100 @@ -22,8 +22,10 @@ consts evala :: i -syntax "_evala" :: "[i, i] => o" (infixl "-a->" 50) -translations "p -a-> n" == " \ evala" + +abbreviation + evala_syntax :: "[i, i] => o" (infixl "-a->" 50) + where "p -a-> n == \ evala" inductive domains "evala" \ "(aexp \ (loc -> nat)) \ nat" @@ -50,8 +52,10 @@ consts evalb :: i -syntax "_evalb" :: "[i,i] => o" (infixl "-b->" 50) -translations "p -b-> b" == " \ evalb" + +abbreviation + evalb_syntax :: "[i,i] => o" (infixl "-b->" 50) + where "p -b-> b == \ evalb" inductive domains "evalb" \ "(bexp \ (loc -> nat)) \ bool" @@ -82,8 +86,10 @@ consts evalc :: i -syntax "_evalc" :: "[i, i] => o" (infixl "-c->" 50) -translations "p -c-> s" == " \ evalc" + +abbreviation + evalc_syntax :: "[i, i] => o" (infixl "-c->" 50) + where "p -c-> s == \ evalc" inductive domains "evalc" \ "(com \ (loc -> nat)) \ (loc -> nat)" diff -r af4c18c30593 -r 544867142ea4 src/ZF/Induct/Comb.thy --- a/src/ZF/Induct/Comb.thy Wed Feb 10 00:45:16 2010 +0100 +++ b/src/ZF/Induct/Comb.thy Wed Feb 10 00:46:56 2010 +0100 @@ -30,12 +30,14 @@ consts contract :: i -syntax - "_contract" :: "[i,i] => o" (infixl "-1->" 50) - "_contract_multi" :: "[i,i] => o" (infixl "--->" 50) -translations - "p -1-> q" == " \ contract" - "p ---> q" == " \ contract^*" + +abbreviation + contract_syntax :: "[i,i] => o" (infixl "-1->" 50) + where "p -1-> q == \ contract" + +abbreviation + contract_multi :: "[i,i] => o" (infixl "--->" 50) + where "p ---> q == \ contract^*" syntax (xsymbols) "comb.app" :: "[i, i] => i" (infixl "\" 90) @@ -56,12 +58,14 @@ consts parcontract :: i -syntax - "_parcontract" :: "[i,i] => o" (infixl "=1=>" 50) - "_parcontract_multi" :: "[i,i] => o" (infixl "===>" 50) -translations - "p =1=> q" == " \ parcontract" - "p ===> q" == " \ parcontract^+" + +abbreviation + parcontract_syntax :: "[i,i] => o" (infixl "=1=>" 50) + where "p =1=> q == \ parcontract" + +abbreviation + parcontract_multi :: "[i,i] => o" (infixl "===>" 50) + where "p ===> q == \ parcontract^+" inductive domains "parcontract" \ "comb \ comb" diff -r af4c18c30593 -r 544867142ea4 src/ZF/Induct/PropLog.thy --- a/src/ZF/Induct/PropLog.thy Wed Feb 10 00:45:16 2010 +0100 +++ b/src/ZF/Induct/PropLog.thy Wed Feb 10 00:46:56 2010 +0100 @@ -34,8 +34,10 @@ subsection {* The proof system *} consts thms :: "i => i" -syntax "_thms" :: "[i,i] => o" (infixl "|-" 50) -translations "H |- p" == "p \ thms(H)" + +abbreviation + thms_syntax :: "[i,i] => o" (infixl "|-" 50) + where "H |- p == p \ thms(H)" inductive domains "thms(H)" \ "propn" diff -r af4c18c30593 -r 544867142ea4 src/ZF/List_ZF.thy --- a/src/ZF/List_ZF.thy Wed Feb 10 00:45:16 2010 +0100 +++ b/src/ZF/List_ZF.thy Wed Feb 10 00:46:56 2010 +0100 @@ -19,9 +19,9 @@ "@List" :: "is => i" ("[(_)]") translations - "[x, xs]" == "Cons(x, [xs])" - "[x]" == "Cons(x, [])" - "[]" == "Nil" + "[x, xs]" == "CONST Cons(x, [xs])" + "[x]" == "CONST Cons(x, [])" + "[]" == "CONST Nil" consts diff -r af4c18c30593 -r 544867142ea4 src/ZF/ZF.thy --- a/src/ZF/ZF.thy Wed Feb 10 00:45:16 2010 +0100 +++ b/src/ZF/ZF.thy Wed Feb 10 00:46:56 2010 +0100 @@ -127,23 +127,23 @@ "@patterns" :: "[pttrn, patterns] => patterns" ("_,/_") translations - "{x, xs}" == "cons(x, {xs})" - "{x}" == "cons(x, 0)" - "{x:A. P}" == "Collect(A, %x. P)" - "{y. x:A, Q}" == "Replace(A, %x y. Q)" - "{b. x:A}" == "RepFun(A, %x. b)" - "INT x:A. B" == "Inter({B. x:A})" - "UN x:A. B" == "Union({B. x:A})" - "PROD x:A. B" == "Pi(A, %x. B)" - "SUM x:A. B" == "Sigma(A, %x. B)" - "lam x:A. f" == "Lambda(A, %x. f)" - "ALL x:A. P" == "Ball(A, %x. P)" - "EX x:A. P" == "Bex(A, %x. P)" + "{x, xs}" == "CONST cons(x, {xs})" + "{x}" == "CONST cons(x, 0)" + "{x:A. P}" == "CONST Collect(A, %x. P)" + "{y. x:A, Q}" == "CONST Replace(A, %x y. Q)" + "{b. x:A}" == "CONST RepFun(A, %x. b)" + "INT x:A. B" == "CONST Inter({B. x:A})" + "UN x:A. B" == "CONST Union({B. x:A})" + "PROD x:A. B" == "CONST Pi(A, %x. B)" + "SUM x:A. B" == "CONST Sigma(A, %x. B)" + "lam x:A. f" == "CONST Lambda(A, %x. f)" + "ALL x:A. P" == "CONST Ball(A, %x. P)" + "EX x:A. P" == "CONST Bex(A, %x. P)" "" == ">" - "" == "Pair(x, y)" - "%.b" == "split(%x .b)" - "%.b" == "split(%x y. b)" + "" == "CONST Pair(x, y)" + "%.b" == "CONST split(%x .b)" + "%.b" == "CONST split(%x y. b)" notation (xsymbols)