# HG changeset patch # User clasohm # Date 818342672 -3600 # Node ID 9bcad9c22fd493ca88c99ca453c1c0dbf8ec923f # Parent cf066d9b4c4ff92d272a77925182689aa1b2e188 removed quotes from syntax and consts sections diff -r cf066d9b4c4f -r 9bcad9c22fd4 doc-src/Intro/advanced.tex --- a/doc-src/Intro/advanced.tex Wed Dec 06 14:53:55 1995 +0100 +++ b/doc-src/Intro/advanced.tex Thu Dec 07 14:24:32 1995 +0100 @@ -395,17 +395,18 @@ Most theories simply declare constants, definitions and rules. The {\bf constant declaration part} has the form \begin{ttbox} -consts \(c@1\) :: "\(\tau@1\)" +consts \(c@1\) :: \(\tau@1\) \vdots - \(c@n\) :: "\(\tau@n\)" + \(c@n\) :: \(\tau@n\) \end{ttbox} where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are -types. Each type {\em must\/} be enclosed in quotation marks. Each +types. The types must be enclosed in quotation marks if they contain +user-declared infix type constructors like {\tt *}. Each constant must be enclosed in quotation marks unless it is a valid identifier. To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$, the $n$ declarations may be abbreviated to a single line: \begin{ttbox} - \(c@1\), \ldots, \(c@n\) :: "\(\tau\)" + \(c@1\), \ldots, \(c@n\) :: \(\tau\) \end{ttbox} The {\bf rule declaration part} has the form \begin{ttbox} @@ -431,7 +432,7 @@ {\em nand} and {\em xor}: \begin{ttbox} Gate = FOL + -consts nand,xor :: "[o,o] => o" +consts nand,xor :: [o,o] => o defs nand_def "nand(P,Q) == ~(P & Q)" xor_def "xor(P,Q) == P & ~Q | ~P & Q" end @@ -493,7 +494,7 @@ Bool = FOL + types bool arities bool :: term -consts tt,ff :: "bool" +consts tt,ff :: bool end \end{ttbox} A $k$-place type constructor may have arities of the form @@ -521,8 +522,8 @@ List = FOL + types 'a list arities list :: (term)term -consts Nil :: "'a list" - Cons :: "['a, 'a list] => 'a list" +consts Nil :: 'a list + Cons :: ['a, 'a list] => 'a list end \end{ttbox} Multiple arity declarations may be abbreviated to a single line: @@ -541,15 +542,15 @@ to those found in \ML. Such synonyms are defined in the type declaration part and are fairly self explanatory: \begin{ttbox} -types gate = "[o,o] => o" - 'a pred = "'a => o" - ('a,'b)nuf = "'b => 'a" +types gate = [o,o] => o + 'a pred = 'a => o + ('a,'b)nuf = 'b => 'a \end{ttbox} Type declarations and synonyms can be mixed arbitrarily: \begin{ttbox} types nat - 'a stream = "nat => 'a" - signal = "nat stream" + 'a stream = nat => 'a + signal = nat stream 'a list \end{ttbox} A synonym is merely an abbreviation for some existing type expression. Hence @@ -558,8 +559,8 @@ to improve the readability of theories. Synonyms can be used just like any other type: \begin{ttbox} -consts and,or :: "gate" - negate :: "signal => signal" +consts and,or :: gate + negate :: signal => signal \end{ttbox} \subsection{Infix and mixfix operators} @@ -569,8 +570,8 @@ following theory: \begin{ttbox} Gate2 = FOL + -consts "~&" :: "[o,o] => o" (infixl 35) - "#" :: "[o,o] => o" (infixl 30) +consts "~&" :: [o,o] => o (infixl 35) + "#" :: [o,o] => o (infixl 30) defs nand_def "P ~& Q == ~(P & Q)" xor_def "P # Q == P & ~Q | ~P & Q" end @@ -590,7 +591,7 @@ {\bf Mixfix} operators may have arbitrary context-free syntaxes. Let us add a line to the constant declaration part: \begin{ttbox} - If :: "[o,o,o] => o" ("if _ then _ else _") + If :: [o,o,o] => o ("if _ then _ else _") \end{ttbox} This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores @@ -607,7 +608,7 @@ Mixfix declarations can be annotated with priorities, just like infixes. The example above is just a shorthand for \begin{ttbox} - If :: "[o,o,o] => o" ("if _ then _ else _" [0,0,0] 1000) + If :: [o,o,o] => o ("if _ then _ else _" [0,0,0] 1000) \end{ttbox} The numeric components determine priorities. The list of integers defines, for each argument position, the minimal priority an expression @@ -617,7 +618,7 @@ appear everywhere because 1000 is the highest priority. On the other hand, the declaration \begin{ttbox} - If :: "[o,o,o] => o" ("if _ then _ else _" [100,0,0] 99) + If :: [o,o,o] => o ("if _ then _ else _" [100,0,0] 99) \end{ttbox} defines concrete syntax for a conditional whose first argument cannot have the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a priority @@ -675,9 +676,9 @@ \begin{ttbox} Arith = FOL + classes arith < term -consts "0" :: "'a::arith" ("0") - "1" :: "'a::arith" ("1") - "+" :: "['a::arith,'a] => 'a" (infixl 60) +consts "0" :: 'a::arith ("0") + "1" :: 'a::arith ("1") + "+" :: ['a::arith,'a] => 'a (infixl 60) end \end{ttbox} No rules are declared for these constants: we merely introduce their @@ -693,7 +694,7 @@ BoolNat = Arith + types bool nat arities bool, nat :: arith -consts Suc :: "nat=>nat" +consts Suc :: nat=>nat \ttbreak rules add0 "0 + n = n::nat" addS "Suc(m)+n = Suc(m+n)" @@ -785,10 +786,10 @@ Nat = FOL + types nat arities nat :: term -consts "0" :: "nat" ("0") - Suc :: "nat=>nat" - rec :: "[nat, 'a, [nat,'a]=>'a] => 'a" - "+" :: "[nat, nat] => nat" (infixl 60) +consts "0" :: nat ("0") + Suc :: nat=>nat + rec :: [nat, 'a, [nat,'a]=>'a] => 'a + "+" :: [nat, nat] => nat (infixl 60) rules Suc_inject "Suc(m)=Suc(n) ==> m=n" Suc_neq_0 "Suc(m)=0 ==> R" induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" @@ -1077,10 +1078,10 @@ Prolog = FOL + types 'a list arities list :: (term)term -consts Nil :: "'a list" - ":" :: "['a, 'a list]=> 'a list" (infixr 60) - app :: "['a list, 'a list, 'a list] => o" - rev :: "['a list, 'a list] => o" +consts Nil :: 'a list + ":" :: ['a, 'a list]=> 'a list (infixr 60) + app :: ['a list, 'a list, 'a list] => o + rev :: ['a list, 'a list] => o rules appNil "app(Nil,ys,ys)" appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" revNil "rev(Nil,Nil)" diff -r cf066d9b4c4f -r 9bcad9c22fd4 doc-src/Ref/defining.tex --- a/doc-src/Ref/defining.tex Wed Dec 06 14:53:55 1995 +0100 +++ b/doc-src/Ref/defining.tex Thu Dec 07 14:24:32 1995 +0100 @@ -487,10 +487,10 @@ types exp syntax - "0" :: "exp" ("0" 9) - "+" :: "[exp, exp] => exp" ("_ + _" [0, 1] 0) - "*" :: "[exp, exp] => exp" ("_ * _" [3, 2] 2) - "-" :: "exp => exp" ("- _" [3] 3) + "0" :: exp ("0" 9) + "+" :: [exp, exp] => exp ("_ + _" [0, 1] 0) + "*" :: [exp, exp] => exp ("_ * _" [3, 2] 2) + "-" :: exp => exp ("- _" [3] 3) end \end{ttbox} If you put this into a file {\tt EXP.thy} and load it via {\tt use_thy"EXP"}, @@ -578,16 +578,16 @@ Infix operators associating to the left or right can be declared using {\tt infixl} or {\tt infixr}. -Roughly speaking, the form {\tt $c$ ::\ "$\sigma$" (infixl $p$)} +Roughly speaking, the form {\tt $c$ ::\ $\sigma$ (infixl $p$)} abbreviates the mixfix declarations \begin{ttbox} -"op \(c\)" :: "\(\sigma\)" ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\)) -"op \(c\)" :: "\(\sigma\)" ("op \(c\)") +"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\)) +"op \(c\)" :: \(\sigma\) ("op \(c\)") \end{ttbox} -and {\tt $c$ ::\ "$\sigma$" (infixr $p$)} abbreviates the mixfix declarations +and {\tt $c$ ::\ $\sigma$ (infixr $p$)} abbreviates the mixfix declarations \begin{ttbox} -"op \(c\)" :: "\(\sigma\)" ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\)) -"op \(c\)" :: "\(\sigma\)" ("op \(c\)") +"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\)) +"op \(c\)" :: \(\sigma\) ("op \(c\)") \end{ttbox} The infix operator is declared as a constant with the prefix {\tt op}. Thus, prefixing infixes with \sdx{op} makes them behave like ordinary @@ -602,7 +602,7 @@ A {\bf binder} is a variable-binding construct such as a quantifier. The constant declaration \begin{ttbox} -\(c\) :: "\(\sigma\)" (binder "\(\Q\)" [\(pb\)] \(p\)) +\(c\) :: \(\sigma\) (binder "\(\Q\)" [\(pb\)] \(p\)) \end{ttbox} introduces a constant~$c$ of type~$\sigma$, which must have the form $(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where @@ -613,8 +613,8 @@ The declaration is expanded internally to something like \begin{ttbox} -\(c\) :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)" -"\(\Q\)"\hskip-3pt :: "[idts, \(\tau@2\)] => \(\tau@3\)" ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\)) +\(c\) :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\) +"\(\Q\)"\hskip-3pt :: [idts, \(\tau@2\)] => \(\tau@3\) ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\)) \end{ttbox} Here \ndx{idts} is the nonterminal symbol for a list of identifiers with \index{type constraints} @@ -631,7 +631,7 @@ \medskip For example, let us declare the quantifier~$\forall$:\index{quantifiers} \begin{ttbox} -All :: "('a => o) => o" (binder "ALL " 10) +All :: ('a => o) => o (binder "ALL " 10) \end{ttbox} This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL $x$.$P$}. When printing, Isabelle prefers the latter form, but must fall @@ -712,7 +712,7 @@ arities o :: logic consts - Trueprop :: "o => prop" ("_" 5) + Trueprop :: o => prop ("_" 5) end \end{ttbox} The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible @@ -725,7 +725,7 @@ \begin{ttbox} Hilbert = Base + consts - "-->" :: "[o, o] => o" (infixr 10) + "-->" :: [o, o] => o (infixr 10) rules K "P --> Q --> P" S "(P --> Q --> R) --> (P --> Q) --> P --> R" @@ -775,7 +775,7 @@ \begin{ttbox} MinI = Base + consts - "-->" :: "[o, o] => o" (infixr 10) + "-->" :: [o, o] => o (infixr 10) rules impI "(P ==> Q) ==> P --> Q" impE "[| P --> Q; P |] ==> Q" @@ -792,7 +792,7 @@ \begin{ttbox} MinIF = MinI + consts - False :: "o" + False :: o rules FalseE "False ==> P" end @@ -801,7 +801,7 @@ \begin{ttbox} MinC = Base + consts - "&" :: "[o, o] => o" (infixr 30) + "&" :: [o, o] => o (infixr 30) \ttbreak rules conjI "[| P; Q |] ==> P & Q" diff -r cf066d9b4c4f -r 9bcad9c22fd4 doc-src/Ref/simplifier.tex --- a/doc-src/Ref/simplifier.tex Wed Dec 06 14:53:55 1995 +0100 +++ b/doc-src/Ref/simplifier.tex Thu Dec 07 14:24:32 1995 +0100 @@ -515,7 +515,7 @@ Arith} using a theory file: \begin{ttbox} NatSum = Arith + -consts sum :: "[nat=>nat, nat] => nat" +consts sum :: [nat=>nat, nat] => nat rules sum_0 "sum(f,0) = 0" sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)" end diff -r cf066d9b4c4f -r 9bcad9c22fd4 doc-src/Ref/syntax.tex --- a/doc-src/Ref/syntax.tex Wed Dec 06 14:53:55 1995 +0100 +++ b/doc-src/Ref/syntax.tex Thu Dec 07 14:24:32 1995 +0100 @@ -356,14 +356,14 @@ arities i, o :: logic consts - Trueprop :: "o => prop" ("_" 5) - Collect :: "[i, i => o] => i" - Replace :: "[i, [i, i] => o] => i" - Ball :: "[i, i => o] => o" + Trueprop :: o => prop ("_" 5) + Collect :: [i, i => o] => i + Replace :: [i, [i, i] => o] => i + Ball :: [i, i => o] => o syntax - "{\at}Collect" :: "[idt, i, o] => i" ("(1{\ttlbrace}_:_./ _{\ttrbrace})") - "{\at}Replace" :: "[idt, idt, i, o] => i" ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})") - "{\at}Ball" :: "[idt, i, o] => o" ("(3ALL _:_./ _)" 10) + "{\at}Collect" :: [idt, i, o] => i ("(1{\ttlbrace}_:_./ _{\ttrbrace})") + "{\at}Replace" :: [idt, idt, i, o] => i ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})") + "{\at}Ball" :: [idt, i, o] => o ("(3ALL _:_./ _)" 10) translations "{\ttlbrace}x:A. P{\ttrbrace}" == "Collect(A, \%x. P)" "{\ttlbrace}y. x:A, Q{\ttrbrace}" == "Replace(A, \%x y. Q)" @@ -542,9 +542,9 @@ types Nil consts - Nil :: "'a list" + Nil :: 'a list syntax - "[]" :: "'a list" ("[]") + "[]" :: 'a list ("[]") translations "[]" == "Nil" \end{ttbox} @@ -578,13 +578,13 @@ types is syntax - "" :: "i => is" ("_") - "{\at}Enum" :: "[i, is] => is" ("_,/ _") + "" :: i => is ("_") + "{\at}Enum" :: [i, is] => is ("_,/ _") consts - empty :: "i" ("{\ttlbrace}{\ttrbrace}") - insert :: "[i, i] => i" + empty :: i ("{\ttlbrace}{\ttrbrace}") + insert :: [i, i] => i syntax - "{\at}Finset" :: "is => i" ("{\ttlbrace}(_){\ttrbrace}") + "{\at}Finset" :: is => i ("{\ttlbrace}(_){\ttrbrace}") translations "{\ttlbrace}x, xs{\ttrbrace}" == "insert(x, {\ttlbrace}xs{\ttrbrace})" "{\ttlbrace}x{\ttrbrace}" == "insert(x, {\ttlbrace}{\ttrbrace})" @@ -656,10 +656,10 @@ \begin{ttbox} PROD = FINSET + consts - Pi :: "[i, i => i] => i" + Pi :: [i, i => i] => i syntax - "{\at}PROD" :: "[idt, i, i] => i" ("(3PROD _:_./ _)" 10) - "{\at}->" :: "[i, i] => i" ("(_ ->/ _)" [51, 50] 50) + "{\at}PROD" :: [idt, i, i] => i ("(3PROD _:_./ _)" 10) + "{\at}->" :: [i, i] => i ("(_ ->/ _)" [51, 50] 50) \ttbreak translations "PROD x:A. B" => "Pi(A, \%x. B)" diff -r cf066d9b4c4f -r 9bcad9c22fd4 doc-src/Ref/theories.tex --- a/doc-src/Ref/theories.tex Wed Dec 06 14:53:55 1995 +0100 +++ b/doc-src/Ref/theories.tex Thu Dec 07 14:24:32 1995 +0100 @@ -68,8 +68,8 @@ indicate the number~$n$. A {\bf type synonym}\indexbold{type synonyms} is an abbreviation - $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$, where - $name$ can be a string and $\tau$ must be enclosed in quotation marks. + $(\alpha@1,\dots,\alpha@n)name = \tau$, where $name$ and $\tau$ can + be strings. \item[$infix$] declares a type or constant to be an infix operator of priority $nat$