1.1 --- a/doc-src/Intro/advanced.tex Wed Dec 06 14:53:55 1995 +0100
1.2 +++ b/doc-src/Intro/advanced.tex Thu Dec 07 14:24:32 1995 +0100
1.3 @@ -395,17 +395,18 @@
1.4 Most theories simply declare constants, definitions and rules. The {\bf
1.5 constant declaration part} has the form
1.6 \begin{ttbox}
1.7 -consts \(c@1\) :: "\(\tau@1\)"
1.8 +consts \(c@1\) :: \(\tau@1\)
1.9 \vdots
1.10 - \(c@n\) :: "\(\tau@n\)"
1.11 + \(c@n\) :: \(\tau@n\)
1.12 \end{ttbox}
1.13 where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are
1.14 -types. Each type {\em must\/} be enclosed in quotation marks. Each
1.15 +types. The types must be enclosed in quotation marks if they contain
1.16 +user-declared infix type constructors like {\tt *}. Each
1.17 constant must be enclosed in quotation marks unless it is a valid
1.18 identifier. To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$,
1.19 the $n$ declarations may be abbreviated to a single line:
1.20 \begin{ttbox}
1.21 - \(c@1\), \ldots, \(c@n\) :: "\(\tau\)"
1.22 + \(c@1\), \ldots, \(c@n\) :: \(\tau\)
1.23 \end{ttbox}
1.24 The {\bf rule declaration part} has the form
1.25 \begin{ttbox}
1.26 @@ -431,7 +432,7 @@
1.27 {\em nand} and {\em xor}:
1.28 \begin{ttbox}
1.29 Gate = FOL +
1.30 -consts nand,xor :: "[o,o] => o"
1.31 +consts nand,xor :: [o,o] => o
1.32 defs nand_def "nand(P,Q) == ~(P & Q)"
1.33 xor_def "xor(P,Q) == P & ~Q | ~P & Q"
1.34 end
1.35 @@ -493,7 +494,7 @@
1.36 Bool = FOL +
1.37 types bool
1.38 arities bool :: term
1.39 -consts tt,ff :: "bool"
1.40 +consts tt,ff :: bool
1.41 end
1.42 \end{ttbox}
1.43 A $k$-place type constructor may have arities of the form
1.44 @@ -521,8 +522,8 @@
1.45 List = FOL +
1.46 types 'a list
1.47 arities list :: (term)term
1.48 -consts Nil :: "'a list"
1.49 - Cons :: "['a, 'a list] => 'a list"
1.50 +consts Nil :: 'a list
1.51 + Cons :: ['a, 'a list] => 'a list
1.52 end
1.53 \end{ttbox}
1.54 Multiple arity declarations may be abbreviated to a single line:
1.55 @@ -541,15 +542,15 @@
1.56 to those found in \ML. Such synonyms are defined in the type declaration part
1.57 and are fairly self explanatory:
1.58 \begin{ttbox}
1.59 -types gate = "[o,o] => o"
1.60 - 'a pred = "'a => o"
1.61 - ('a,'b)nuf = "'b => 'a"
1.62 +types gate = [o,o] => o
1.63 + 'a pred = 'a => o
1.64 + ('a,'b)nuf = 'b => 'a
1.65 \end{ttbox}
1.66 Type declarations and synonyms can be mixed arbitrarily:
1.67 \begin{ttbox}
1.68 types nat
1.69 - 'a stream = "nat => 'a"
1.70 - signal = "nat stream"
1.71 + 'a stream = nat => 'a
1.72 + signal = nat stream
1.73 'a list
1.74 \end{ttbox}
1.75 A synonym is merely an abbreviation for some existing type expression. Hence
1.76 @@ -558,8 +559,8 @@
1.77 to improve the readability of theories. Synonyms can be used just like any
1.78 other type:
1.79 \begin{ttbox}
1.80 -consts and,or :: "gate"
1.81 - negate :: "signal => signal"
1.82 +consts and,or :: gate
1.83 + negate :: signal => signal
1.84 \end{ttbox}
1.85
1.86 \subsection{Infix and mixfix operators}
1.87 @@ -569,8 +570,8 @@
1.88 following theory:
1.89 \begin{ttbox}
1.90 Gate2 = FOL +
1.91 -consts "~&" :: "[o,o] => o" (infixl 35)
1.92 - "#" :: "[o,o] => o" (infixl 30)
1.93 +consts "~&" :: [o,o] => o (infixl 35)
1.94 + "#" :: [o,o] => o (infixl 30)
1.95 defs nand_def "P ~& Q == ~(P & Q)"
1.96 xor_def "P # Q == P & ~Q | ~P & Q"
1.97 end
1.98 @@ -590,7 +591,7 @@
1.99 {\bf Mixfix} operators may have arbitrary context-free syntaxes. Let us
1.100 add a line to the constant declaration part:
1.101 \begin{ttbox}
1.102 - If :: "[o,o,o] => o" ("if _ then _ else _")
1.103 + If :: [o,o,o] => o ("if _ then _ else _")
1.104 \end{ttbox}
1.105 This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt
1.106 if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores
1.107 @@ -607,7 +608,7 @@
1.108 Mixfix declarations can be annotated with priorities, just like
1.109 infixes. The example above is just a shorthand for
1.110 \begin{ttbox}
1.111 - If :: "[o,o,o] => o" ("if _ then _ else _" [0,0,0] 1000)
1.112 + If :: [o,o,o] => o ("if _ then _ else _" [0,0,0] 1000)
1.113 \end{ttbox}
1.114 The numeric components determine priorities. The list of integers
1.115 defines, for each argument position, the minimal priority an expression
1.116 @@ -617,7 +618,7 @@
1.117 appear everywhere because 1000 is the highest priority. On the other
1.118 hand, the declaration
1.119 \begin{ttbox}
1.120 - If :: "[o,o,o] => o" ("if _ then _ else _" [100,0,0] 99)
1.121 + If :: [o,o,o] => o ("if _ then _ else _" [100,0,0] 99)
1.122 \end{ttbox}
1.123 defines concrete syntax for a conditional whose first argument cannot have
1.124 the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a priority
1.125 @@ -675,9 +676,9 @@
1.126 \begin{ttbox}
1.127 Arith = FOL +
1.128 classes arith < term
1.129 -consts "0" :: "'a::arith" ("0")
1.130 - "1" :: "'a::arith" ("1")
1.131 - "+" :: "['a::arith,'a] => 'a" (infixl 60)
1.132 +consts "0" :: 'a::arith ("0")
1.133 + "1" :: 'a::arith ("1")
1.134 + "+" :: ['a::arith,'a] => 'a (infixl 60)
1.135 end
1.136 \end{ttbox}
1.137 No rules are declared for these constants: we merely introduce their
1.138 @@ -693,7 +694,7 @@
1.139 BoolNat = Arith +
1.140 types bool nat
1.141 arities bool, nat :: arith
1.142 -consts Suc :: "nat=>nat"
1.143 +consts Suc :: nat=>nat
1.144 \ttbreak
1.145 rules add0 "0 + n = n::nat"
1.146 addS "Suc(m)+n = Suc(m+n)"
1.147 @@ -785,10 +786,10 @@
1.148 Nat = FOL +
1.149 types nat
1.150 arities nat :: term
1.151 -consts "0" :: "nat" ("0")
1.152 - Suc :: "nat=>nat"
1.153 - rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
1.154 - "+" :: "[nat, nat] => nat" (infixl 60)
1.155 +consts "0" :: nat ("0")
1.156 + Suc :: nat=>nat
1.157 + rec :: [nat, 'a, [nat,'a]=>'a] => 'a
1.158 + "+" :: [nat, nat] => nat (infixl 60)
1.159 rules Suc_inject "Suc(m)=Suc(n) ==> m=n"
1.160 Suc_neq_0 "Suc(m)=0 ==> R"
1.161 induct "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
1.162 @@ -1077,10 +1078,10 @@
1.163 Prolog = FOL +
1.164 types 'a list
1.165 arities list :: (term)term
1.166 -consts Nil :: "'a list"
1.167 - ":" :: "['a, 'a list]=> 'a list" (infixr 60)
1.168 - app :: "['a list, 'a list, 'a list] => o"
1.169 - rev :: "['a list, 'a list] => o"
1.170 +consts Nil :: 'a list
1.171 + ":" :: ['a, 'a list]=> 'a list (infixr 60)
1.172 + app :: ['a list, 'a list, 'a list] => o
1.173 + rev :: ['a list, 'a list] => o
1.174 rules appNil "app(Nil,ys,ys)"
1.175 appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
1.176 revNil "rev(Nil,Nil)"
2.1 --- a/doc-src/Ref/defining.tex Wed Dec 06 14:53:55 1995 +0100
2.2 +++ b/doc-src/Ref/defining.tex Thu Dec 07 14:24:32 1995 +0100
2.3 @@ -487,10 +487,10 @@
2.4 types
2.5 exp
2.6 syntax
2.7 - "0" :: "exp" ("0" 9)
2.8 - "+" :: "[exp, exp] => exp" ("_ + _" [0, 1] 0)
2.9 - "*" :: "[exp, exp] => exp" ("_ * _" [3, 2] 2)
2.10 - "-" :: "exp => exp" ("- _" [3] 3)
2.11 + "0" :: exp ("0" 9)
2.12 + "+" :: [exp, exp] => exp ("_ + _" [0, 1] 0)
2.13 + "*" :: [exp, exp] => exp ("_ * _" [3, 2] 2)
2.14 + "-" :: exp => exp ("- _" [3] 3)
2.15 end
2.16 \end{ttbox}
2.17 If you put this into a file {\tt EXP.thy} and load it via {\tt use_thy"EXP"},
2.18 @@ -578,16 +578,16 @@
2.19
2.20 Infix operators associating to the left or right can be declared
2.21 using {\tt infixl} or {\tt infixr}.
2.22 -Roughly speaking, the form {\tt $c$ ::\ "$\sigma$" (infixl $p$)}
2.23 +Roughly speaking, the form {\tt $c$ ::\ $\sigma$ (infixl $p$)}
2.24 abbreviates the mixfix declarations
2.25 \begin{ttbox}
2.26 -"op \(c\)" :: "\(\sigma\)" ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\))
2.27 -"op \(c\)" :: "\(\sigma\)" ("op \(c\)")
2.28 +"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\))
2.29 +"op \(c\)" :: \(\sigma\) ("op \(c\)")
2.30 \end{ttbox}
2.31 -and {\tt $c$ ::\ "$\sigma$" (infixr $p$)} abbreviates the mixfix declarations
2.32 +and {\tt $c$ ::\ $\sigma$ (infixr $p$)} abbreviates the mixfix declarations
2.33 \begin{ttbox}
2.34 -"op \(c\)" :: "\(\sigma\)" ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\))
2.35 -"op \(c\)" :: "\(\sigma\)" ("op \(c\)")
2.36 +"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\))
2.37 +"op \(c\)" :: \(\sigma\) ("op \(c\)")
2.38 \end{ttbox}
2.39 The infix operator is declared as a constant with the prefix {\tt op}.
2.40 Thus, prefixing infixes with \sdx{op} makes them behave like ordinary
2.41 @@ -602,7 +602,7 @@
2.42 A {\bf binder} is a variable-binding construct such as a quantifier. The
2.43 constant declaration
2.44 \begin{ttbox}
2.45 -\(c\) :: "\(\sigma\)" (binder "\(\Q\)" [\(pb\)] \(p\))
2.46 +\(c\) :: \(\sigma\) (binder "\(\Q\)" [\(pb\)] \(p\))
2.47 \end{ttbox}
2.48 introduces a constant~$c$ of type~$\sigma$, which must have the form
2.49 $(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where
2.50 @@ -613,8 +613,8 @@
2.51
2.52 The declaration is expanded internally to something like
2.53 \begin{ttbox}
2.54 -\(c\) :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)"
2.55 -"\(\Q\)"\hskip-3pt :: "[idts, \(\tau@2\)] => \(\tau@3\)" ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\))
2.56 +\(c\) :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)
2.57 +"\(\Q\)"\hskip-3pt :: [idts, \(\tau@2\)] => \(\tau@3\) ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\))
2.58 \end{ttbox}
2.59 Here \ndx{idts} is the nonterminal symbol for a list of identifiers with
2.60 \index{type constraints}
2.61 @@ -631,7 +631,7 @@
2.62 \medskip
2.63 For example, let us declare the quantifier~$\forall$:\index{quantifiers}
2.64 \begin{ttbox}
2.65 -All :: "('a => o) => o" (binder "ALL " 10)
2.66 +All :: ('a => o) => o (binder "ALL " 10)
2.67 \end{ttbox}
2.68 This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL
2.69 $x$.$P$}. When printing, Isabelle prefers the latter form, but must fall
2.70 @@ -712,7 +712,7 @@
2.71 arities
2.72 o :: logic
2.73 consts
2.74 - Trueprop :: "o => prop" ("_" 5)
2.75 + Trueprop :: o => prop ("_" 5)
2.76 end
2.77 \end{ttbox}
2.78 The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible
2.79 @@ -725,7 +725,7 @@
2.80 \begin{ttbox}
2.81 Hilbert = Base +
2.82 consts
2.83 - "-->" :: "[o, o] => o" (infixr 10)
2.84 + "-->" :: [o, o] => o (infixr 10)
2.85 rules
2.86 K "P --> Q --> P"
2.87 S "(P --> Q --> R) --> (P --> Q) --> P --> R"
2.88 @@ -775,7 +775,7 @@
2.89 \begin{ttbox}
2.90 MinI = Base +
2.91 consts
2.92 - "-->" :: "[o, o] => o" (infixr 10)
2.93 + "-->" :: [o, o] => o (infixr 10)
2.94 rules
2.95 impI "(P ==> Q) ==> P --> Q"
2.96 impE "[| P --> Q; P |] ==> Q"
2.97 @@ -792,7 +792,7 @@
2.98 \begin{ttbox}
2.99 MinIF = MinI +
2.100 consts
2.101 - False :: "o"
2.102 + False :: o
2.103 rules
2.104 FalseE "False ==> P"
2.105 end
2.106 @@ -801,7 +801,7 @@
2.107 \begin{ttbox}
2.108 MinC = Base +
2.109 consts
2.110 - "&" :: "[o, o] => o" (infixr 30)
2.111 + "&" :: [o, o] => o (infixr 30)
2.112 \ttbreak
2.113 rules
2.114 conjI "[| P; Q |] ==> P & Q"
3.1 --- a/doc-src/Ref/simplifier.tex Wed Dec 06 14:53:55 1995 +0100
3.2 +++ b/doc-src/Ref/simplifier.tex Thu Dec 07 14:24:32 1995 +0100
3.3 @@ -515,7 +515,7 @@
3.4 Arith} using a theory file:
3.5 \begin{ttbox}
3.6 NatSum = Arith +
3.7 -consts sum :: "[nat=>nat, nat] => nat"
3.8 +consts sum :: [nat=>nat, nat] => nat
3.9 rules sum_0 "sum(f,0) = 0"
3.10 sum_Suc "sum(f,Suc(n)) = f(n) + sum(f,n)"
3.11 end
4.1 --- a/doc-src/Ref/syntax.tex Wed Dec 06 14:53:55 1995 +0100
4.2 +++ b/doc-src/Ref/syntax.tex Thu Dec 07 14:24:32 1995 +0100
4.3 @@ -356,14 +356,14 @@
4.4 arities
4.5 i, o :: logic
4.6 consts
4.7 - Trueprop :: "o => prop" ("_" 5)
4.8 - Collect :: "[i, i => o] => i"
4.9 - Replace :: "[i, [i, i] => o] => i"
4.10 - Ball :: "[i, i => o] => o"
4.11 + Trueprop :: o => prop ("_" 5)
4.12 + Collect :: [i, i => o] => i
4.13 + Replace :: [i, [i, i] => o] => i
4.14 + Ball :: [i, i => o] => o
4.15 syntax
4.16 - "{\at}Collect" :: "[idt, i, o] => i" ("(1{\ttlbrace}_:_./ _{\ttrbrace})")
4.17 - "{\at}Replace" :: "[idt, idt, i, o] => i" ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})")
4.18 - "{\at}Ball" :: "[idt, i, o] => o" ("(3ALL _:_./ _)" 10)
4.19 + "{\at}Collect" :: [idt, i, o] => i ("(1{\ttlbrace}_:_./ _{\ttrbrace})")
4.20 + "{\at}Replace" :: [idt, idt, i, o] => i ("(1{\ttlbrace}_./ _:_, _{\ttrbrace})")
4.21 + "{\at}Ball" :: [idt, i, o] => o ("(3ALL _:_./ _)" 10)
4.22 translations
4.23 "{\ttlbrace}x:A. P{\ttrbrace}" == "Collect(A, \%x. P)"
4.24 "{\ttlbrace}y. x:A, Q{\ttrbrace}" == "Replace(A, \%x y. Q)"
4.25 @@ -542,9 +542,9 @@
4.26 types
4.27 Nil
4.28 consts
4.29 - Nil :: "'a list"
4.30 + Nil :: 'a list
4.31 syntax
4.32 - "[]" :: "'a list" ("[]")
4.33 + "[]" :: 'a list ("[]")
4.34 translations
4.35 "[]" == "Nil"
4.36 \end{ttbox}
4.37 @@ -578,13 +578,13 @@
4.38 types
4.39 is
4.40 syntax
4.41 - "" :: "i => is" ("_")
4.42 - "{\at}Enum" :: "[i, is] => is" ("_,/ _")
4.43 + "" :: i => is ("_")
4.44 + "{\at}Enum" :: [i, is] => is ("_,/ _")
4.45 consts
4.46 - empty :: "i" ("{\ttlbrace}{\ttrbrace}")
4.47 - insert :: "[i, i] => i"
4.48 + empty :: i ("{\ttlbrace}{\ttrbrace}")
4.49 + insert :: [i, i] => i
4.50 syntax
4.51 - "{\at}Finset" :: "is => i" ("{\ttlbrace}(_){\ttrbrace}")
4.52 + "{\at}Finset" :: is => i ("{\ttlbrace}(_){\ttrbrace}")
4.53 translations
4.54 "{\ttlbrace}x, xs{\ttrbrace}" == "insert(x, {\ttlbrace}xs{\ttrbrace})"
4.55 "{\ttlbrace}x{\ttrbrace}" == "insert(x, {\ttlbrace}{\ttrbrace})"
4.56 @@ -656,10 +656,10 @@
4.57 \begin{ttbox}
4.58 PROD = FINSET +
4.59 consts
4.60 - Pi :: "[i, i => i] => i"
4.61 + Pi :: [i, i => i] => i
4.62 syntax
4.63 - "{\at}PROD" :: "[idt, i, i] => i" ("(3PROD _:_./ _)" 10)
4.64 - "{\at}->" :: "[i, i] => i" ("(_ ->/ _)" [51, 50] 50)
4.65 + "{\at}PROD" :: [idt, i, i] => i ("(3PROD _:_./ _)" 10)
4.66 + "{\at}->" :: [i, i] => i ("(_ ->/ _)" [51, 50] 50)
4.67 \ttbreak
4.68 translations
4.69 "PROD x:A. B" => "Pi(A, \%x. B)"
5.1 --- a/doc-src/Ref/theories.tex Wed Dec 06 14:53:55 1995 +0100
5.2 +++ b/doc-src/Ref/theories.tex Thu Dec 07 14:24:32 1995 +0100
5.3 @@ -68,8 +68,8 @@
5.4 indicate the number~$n$.
5.5
5.6 A {\bf type synonym}\indexbold{type synonyms} is an abbreviation
5.7 - $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$, where
5.8 - $name$ can be a string and $\tau$ must be enclosed in quotation marks.
5.9 + $(\alpha@1,\dots,\alpha@n)name = \tau$, where $name$ and $\tau$ can
5.10 + be strings.
5.11
5.12 \item[$infix$]
5.13 declares a type or constant to be an infix operator of priority $nat$