971 \item[Quantifiers:] {\tt !~{\it pattern}:$A$.~$P$} |
971 \item[Quantifiers:] {\tt !~{\it pattern}:$A$.~$P$} |
972 \item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$} |
972 \item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$} |
973 \item[Set operations:] {\tt UN~{\it pattern}:$A$.~$B$} |
973 \item[Set operations:] {\tt UN~{\it pattern}:$A$.~$B$} |
974 \item[Sets:] {\tt \{~{\it pattern}~.~$P$~\}} |
974 \item[Sets:] {\tt \{~{\it pattern}~.~$P$~\}} |
975 \end{description} |
975 \end{description} |
976 % FIXME: remove comment in HOL/Prod.thy concerning printing |
976 |
977 % FIXME: remove ML code from HOL/Prod.thy |
977 There is a simple tactic which supports reasoning about patterns: |
|
978 \begin{ttdescription} |
|
979 \item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all |
|
980 {\tt!!}-quantified variables of product type by individual variables for |
|
981 each component. A simple example: |
|
982 \begin{ttbox} |
|
983 {\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p} |
|
984 by(split_all_tac 1); |
|
985 {\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)} |
|
986 \end{ttbox} |
|
987 \end{ttdescription} |
978 |
988 |
979 Theory {\tt Prod} also introduces the degenerate product type {\tt unit} |
989 Theory {\tt Prod} also introduces the degenerate product type {\tt unit} |
980 which contains only a single element named {\tt()} with the property |
990 which contains only a single element named {\tt()} with the property |
981 \begin{ttbox} |
991 \begin{ttbox} |
982 \tdx{unit_eq} u = () |
992 \tdx{unit_eq} u = () |