doc-src/Intro/advanced.tex
changeset 1366 3f3c25d3ec04
parent 1185 9968989790e2
child 1387 9bcad9c22fd4
equal deleted inserted replaced
1365:0defae128e43 1366:3f3c25d3ec04
   435 defs    nand_def "nand(P,Q) == ~(P & Q)"
   435 defs    nand_def "nand(P,Q) == ~(P & Q)"
   436         xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
   436         xor_def  "xor(P,Q)  == P & ~Q | ~P & Q"
   437 end
   437 end
   438 \end{ttbox}
   438 \end{ttbox}
   439 
   439 
       
   440 \begin{warn}
       
   441 A common mistake when writing definitions is to introduce extra free variables
       
   442 on the right-hard side as in the following fictitious definition:
       
   443 \begin{ttbox}
       
   444 defs  prime_def "prime(p) == (m divides p) --> (m=1 | m=p)"
       
   445 \end{ttbox}
       
   446 Isabelle rejects this ``definition'' because of the extra {\tt m} on the
       
   447 right-hard side, which would introduce an inconsistency. What you should have
       
   448 written is
       
   449 \begin{ttbox}
       
   450 defs  prime_def "prime(p) == ALL m. (m divides p) --> (m=1 | m=p)"
       
   451 \end{ttbox}
       
   452 \end{warn}
   440 
   453 
   441 \subsection{Declaring type constructors}
   454 \subsection{Declaring type constructors}
   442 \indexbold{types!declaring}\indexbold{arities!declaring}
   455 \indexbold{types!declaring}\indexbold{arities!declaring}
   443 %
   456 %
   444 Types are composed of type variables and {\bf type constructors}.  Each
   457 Types are composed of type variables and {\bf type constructors}.  Each