485 \begin{ttbox} |
485 \begin{ttbox} |
486 EXP = Pure + |
486 EXP = Pure + |
487 types |
487 types |
488 exp |
488 exp |
489 syntax |
489 syntax |
490 "0" :: "exp" ("0" 9) |
490 "0" :: exp ("0" 9) |
491 "+" :: "[exp, exp] => exp" ("_ + _" [0, 1] 0) |
491 "+" :: [exp, exp] => exp ("_ + _" [0, 1] 0) |
492 "*" :: "[exp, exp] => exp" ("_ * _" [3, 2] 2) |
492 "*" :: [exp, exp] => exp ("_ * _" [3, 2] 2) |
493 "-" :: "exp => exp" ("- _" [3] 3) |
493 "-" :: exp => exp ("- _" [3] 3) |
494 end |
494 end |
495 \end{ttbox} |
495 \end{ttbox} |
496 If you put this into a file {\tt EXP.thy} and load it via {\tt use_thy"EXP"}, |
496 If you put this into a file {\tt EXP.thy} and load it via {\tt use_thy"EXP"}, |
497 you can run some tests: |
497 you can run some tests: |
498 \begin{ttbox} |
498 \begin{ttbox} |
576 \subsection{Infixes} |
576 \subsection{Infixes} |
577 \indexbold{infixes} |
577 \indexbold{infixes} |
578 |
578 |
579 Infix operators associating to the left or right can be declared |
579 Infix operators associating to the left or right can be declared |
580 using {\tt infixl} or {\tt infixr}. |
580 using {\tt infixl} or {\tt infixr}. |
581 Roughly speaking, the form {\tt $c$ ::\ "$\sigma$" (infixl $p$)} |
581 Roughly speaking, the form {\tt $c$ ::\ $\sigma$ (infixl $p$)} |
582 abbreviates the mixfix declarations |
582 abbreviates the mixfix declarations |
583 \begin{ttbox} |
583 \begin{ttbox} |
584 "op \(c\)" :: "\(\sigma\)" ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\)) |
584 "op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\)) |
585 "op \(c\)" :: "\(\sigma\)" ("op \(c\)") |
585 "op \(c\)" :: \(\sigma\) ("op \(c\)") |
586 \end{ttbox} |
586 \end{ttbox} |
587 and {\tt $c$ ::\ "$\sigma$" (infixr $p$)} abbreviates the mixfix declarations |
587 and {\tt $c$ ::\ $\sigma$ (infixr $p$)} abbreviates the mixfix declarations |
588 \begin{ttbox} |
588 \begin{ttbox} |
589 "op \(c\)" :: "\(\sigma\)" ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\)) |
589 "op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\)) |
590 "op \(c\)" :: "\(\sigma\)" ("op \(c\)") |
590 "op \(c\)" :: \(\sigma\) ("op \(c\)") |
591 \end{ttbox} |
591 \end{ttbox} |
592 The infix operator is declared as a constant with the prefix {\tt op}. |
592 The infix operator is declared as a constant with the prefix {\tt op}. |
593 Thus, prefixing infixes with \sdx{op} makes them behave like ordinary |
593 Thus, prefixing infixes with \sdx{op} makes them behave like ordinary |
594 function symbols, as in \ML. Special characters occurring in~$c$ must be |
594 function symbols, as in \ML. Special characters occurring in~$c$ must be |
595 escaped, as in delimiters, using a single quote. |
595 escaped, as in delimiters, using a single quote. |
600 \begingroup |
600 \begingroup |
601 \def\Q{{\cal Q}} |
601 \def\Q{{\cal Q}} |
602 A {\bf binder} is a variable-binding construct such as a quantifier. The |
602 A {\bf binder} is a variable-binding construct such as a quantifier. The |
603 constant declaration |
603 constant declaration |
604 \begin{ttbox} |
604 \begin{ttbox} |
605 \(c\) :: "\(\sigma\)" (binder "\(\Q\)" [\(pb\)] \(p\)) |
605 \(c\) :: \(\sigma\) (binder "\(\Q\)" [\(pb\)] \(p\)) |
606 \end{ttbox} |
606 \end{ttbox} |
607 introduces a constant~$c$ of type~$\sigma$, which must have the form |
607 introduces a constant~$c$ of type~$\sigma$, which must have the form |
608 $(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where |
608 $(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where |
609 $x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$ |
609 $x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$ |
610 and the whole term has type~$\tau@3$. The optional integer $pb$ |
610 and the whole term has type~$\tau@3$. The optional integer $pb$ |
611 specifies the body's priority, by default~$p$. Special characters |
611 specifies the body's priority, by default~$p$. Special characters |
612 in $\Q$ must be escaped using a single quote. |
612 in $\Q$ must be escaped using a single quote. |
613 |
613 |
614 The declaration is expanded internally to something like |
614 The declaration is expanded internally to something like |
615 \begin{ttbox} |
615 \begin{ttbox} |
616 \(c\) :: "(\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)" |
616 \(c\) :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\) |
617 "\(\Q\)"\hskip-3pt :: "[idts, \(\tau@2\)] => \(\tau@3\)" ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\)) |
617 "\(\Q\)"\hskip-3pt :: [idts, \(\tau@2\)] => \(\tau@3\) ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\)) |
618 \end{ttbox} |
618 \end{ttbox} |
619 Here \ndx{idts} is the nonterminal symbol for a list of identifiers with |
619 Here \ndx{idts} is the nonterminal symbol for a list of identifiers with |
620 \index{type constraints} |
620 \index{type constraints} |
621 optional type constraints (see Fig.\ts\ref{fig:pure_gram}). The |
621 optional type constraints (see Fig.\ts\ref{fig:pure_gram}). The |
622 declaration also installs a parse translation\index{translations!parse} |
622 declaration also installs a parse translation\index{translations!parse} |
629 \[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)). \] |
629 \[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)). \] |
630 |
630 |
631 \medskip |
631 \medskip |
632 For example, let us declare the quantifier~$\forall$:\index{quantifiers} |
632 For example, let us declare the quantifier~$\forall$:\index{quantifiers} |
633 \begin{ttbox} |
633 \begin{ttbox} |
634 All :: "('a => o) => o" (binder "ALL " 10) |
634 All :: ('a => o) => o (binder "ALL " 10) |
635 \end{ttbox} |
635 \end{ttbox} |
636 This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL |
636 This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL |
637 $x$.$P$}. When printing, Isabelle prefers the latter form, but must fall |
637 $x$.$P$}. When printing, Isabelle prefers the latter form, but must fall |
638 back on ${\tt All}(P)$ if $P$ is not an abstraction. Both $P$ and {\tt ALL |
638 back on ${\tt All}(P)$ if $P$ is not an abstraction. Both $P$ and {\tt ALL |
639 $x$.$P$} have type~$o$, the type of formulae, while the bound variable |
639 $x$.$P$} have type~$o$, the type of formulae, while the bound variable |
710 types |
710 types |
711 o |
711 o |
712 arities |
712 arities |
713 o :: logic |
713 o :: logic |
714 consts |
714 consts |
715 Trueprop :: "o => prop" ("_" 5) |
715 Trueprop :: o => prop ("_" 5) |
716 end |
716 end |
717 \end{ttbox} |
717 \end{ttbox} |
718 The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible |
718 The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible |
719 coercion function. Assuming this definition resides in a file {\tt Base.thy}, |
719 coercion function. Assuming this definition resides in a file {\tt Base.thy}, |
720 you have to load it with the command {\tt use_thy "Base"}. |
720 you have to load it with the command {\tt use_thy "Base"}. |
723 implication. Its definition in Isabelle needs no advanced features but |
723 implication. Its definition in Isabelle needs no advanced features but |
724 illustrates the overall mechanism nicely: |
724 illustrates the overall mechanism nicely: |
725 \begin{ttbox} |
725 \begin{ttbox} |
726 Hilbert = Base + |
726 Hilbert = Base + |
727 consts |
727 consts |
728 "-->" :: "[o, o] => o" (infixr 10) |
728 "-->" :: [o, o] => o (infixr 10) |
729 rules |
729 rules |
730 K "P --> Q --> P" |
730 K "P --> Q --> P" |
731 S "(P --> Q --> R) --> (P --> Q) --> P --> R" |
731 S "(P --> Q --> R) --> (P --> Q) --> P --> R" |
732 MP "[| P --> Q; P |] ==> Q" |
732 MP "[| P --> Q; P |] ==> Q" |
733 end |
733 end |
790 |
790 |
791 We may easily extend minimal logic with falsity: |
791 We may easily extend minimal logic with falsity: |
792 \begin{ttbox} |
792 \begin{ttbox} |
793 MinIF = MinI + |
793 MinIF = MinI + |
794 consts |
794 consts |
795 False :: "o" |
795 False :: o |
796 rules |
796 rules |
797 FalseE "False ==> P" |
797 FalseE "False ==> P" |
798 end |
798 end |
799 \end{ttbox} |
799 \end{ttbox} |
800 On the other hand, we may wish to introduce conjunction only: |
800 On the other hand, we may wish to introduce conjunction only: |
801 \begin{ttbox} |
801 \begin{ttbox} |
802 MinC = Base + |
802 MinC = Base + |
803 consts |
803 consts |
804 "&" :: "[o, o] => o" (infixr 30) |
804 "&" :: [o, o] => o (infixr 30) |
805 \ttbreak |
805 \ttbreak |
806 rules |
806 rules |
807 conjI "[| P; Q |] ==> P & Q" |
807 conjI "[| P; Q |] ==> P & Q" |
808 conjE1 "P & Q ==> P" |
808 conjE1 "P & Q ==> P" |
809 conjE2 "P & Q ==> Q" |
809 conjE2 "P & Q ==> Q" |