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)"