author  nipkow 
Thu, 16 Oct 1997 13:13:03 +0200  
changeset 3881  73be08b4da3f 
parent 3489  afa802078173 
child 3959  033633d9a032 
permissions  rwrr 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1 
%% $Id$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

2 
\chapter{HigherOrder Logic} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

3 
\index{higherorder logic(} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

4 
\index{HOL system@{\sc hol} system} 
1162  5 

6 
The theory~\thydx{HOL} implements higherorder logic. It is based on 

7 
Gordon's~{\sc hol} system~\cite{mgordonhol}, which itself is based on 

3152  8 
Church's original paper~\cite{church40}. Andrews's 
9 
book~\cite{andrews86} is a full description of the original 

10 
Churchstyle higherorder logic. Experience with the {\sc hol} system 

11 
has demonstrated that higherorder logic is widely applicable in many 

12 
areas of mathematics and computer science, not just hardware 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

13 
verification, {\sc hol}'s original \textit{raison d'\^etre\/}. It is 
3152  14 
weaker than {\ZF} set theory but for most applications this does not 
15 
matter. If you prefer {\ML} to Lisp, you will probably prefer \HOL\ 

16 
to~{\ZF}. 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

17 

2926  18 
The syntax of \HOL\footnote{Earlier versions of Isabelle's \HOL\ used a 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

19 
different syntax. Ancient releases of Isabelle included still another version 
2926  20 
of~\HOL, with explicit type inference rules~\cite{paulsonCOLOG}. This 
21 
version no longer exists, but \thydx{ZF} supports a similar style of 

22 
reasoning.} follows $\lambda$calculus and functional programming. Function 

23 
application is curried. To apply the function~$f$ of type 

24 
$\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in \HOL, you simply 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

25 
write $f\,a\,b$. There is no `apply' operator as in \thydx{ZF}. Note that 
2926  26 
$f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in \HOL. We write ordered 
27 
pairs as $(a,b)$, not $\langle a,b\rangle$ as in {\ZF}. 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

28 

1162  29 
\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

30 
identifies objectlevel types with metalevel types, taking advantage of 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

31 
Isabelle's builtin type checker. It identifies objectlevel functions 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

32 
with metalevel functions, so it uses Isabelle's operations for abstraction 
2926  33 
and application. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

34 

3152  35 
These identifications allow Isabelle to support \HOL\ particularly 
36 
nicely, but they also mean that \HOL\ requires more sophistication 

37 
from the user  in particular, an understanding of Isabelle's type 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

38 
system. Beginners should work with \texttt{show_types} (or even 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

39 
\texttt{show_sorts}) set to \texttt{true}. 
2926  40 
% Gain experience by 
41 
%working in firstorder logic before attempting to use higherorder logic. 

42 
%This chapter assumes familiarity with~{\FOL{}}. 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

43 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

44 

2926  45 
\begin{figure} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

46 
\begin{constants} 
2926  47 
\it name &\it metatype & \it description \\ 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

48 
\cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\ 
2926  49 
\cdx{Not} & $bool\To bool$ & negation ($\neg$) \\ 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

50 
\cdx{True} & $bool$ & tautology ($\top$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

51 
\cdx{False} & $bool$ & absurdity ($\bot$) \\ 
2926  52 
\cdx{If} & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\ 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

53 
\cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

54 
\end{constants} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

55 
\subcaption{Constants} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

56 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

57 
\begin{constants} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

58 
\index{"@@{\tt\at} symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

59 
\index{*"! symbol}\index{*"? symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

60 
\index{*"?"! symbol}\index{*"E"X"! symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

61 
\it symbol &\it name &\it metatype & \it description \\ 
2926  62 
\tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ & 
63 
Hilbert description ($\varepsilon$) \\ 

64 
{\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha\To bool)\To bool$ & 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

65 
universal quantifier ($\forall$) \\ 
2926  66 
{\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha\To bool)\To bool$ & 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

67 
existential quantifier ($\exists$) \\ 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

68 
{\tt?!} or \texttt{EX!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ & 
2926  69 
unique existence ($\exists!$)\\ 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

70 
\texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ & 
2926  71 
least element 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

72 
\end{constants} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

73 
\subcaption{Binders} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

74 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

75 
\begin{constants} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

76 
\index{*"= symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

77 
\index{&@{\tt\&} symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

78 
\index{*" symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

79 
\index{*"""> symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

80 
\it symbol & \it metatype & \it priority & \it description \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

81 
\sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 
1234  82 
Left 55 & composition ($\circ$) \\ 
2926  83 
\tt = & $[\alpha,\alpha]\To bool$ & Left 50 & equality ($=$) \\ 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

84 
\tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

85 
\tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

86 
less than or equals ($\leq$)\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

87 
\tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

88 
\tt  & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

89 
\tt > & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

90 
\end{constants} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

91 
\subcaption{Infixes} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

92 
\caption{Syntax of \texttt{HOL}} \label{holconstants} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

93 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

94 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

95 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

96 
\begin{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

97 
\index{*let symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

98 
\index{*in symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

99 
\dquotes 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

100 
\[\begin{array}{rclcl} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

101 
term & = & \hbox{expression of class~$term$} \\ 
2926  102 
&  & "\at~" id " . " formula \\ 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

103 
&  & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

104 
\multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

105 
&  & 
2926  106 
\multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\ 
107 
&  & "LEAST"~ id " . " formula \\[2ex] 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

108 
formula & = & \hbox{expression of type~$bool$} \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

109 
&  & term " = " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

110 
&  & term " \ttilde= " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

111 
&  & term " < " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

112 
&  & term " <= " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

113 
&  & "\ttilde\ " formula \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

114 
&  & formula " \& " formula \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

115 
&  & formula "  " formula \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

116 
&  & formula " > " formula \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

117 
&  & "!~~~" id~id^* " . " formula 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

118 
&  & "ALL~" id~id^* " . " formula \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

119 
&  & "?~~~" id~id^* " . " formula 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

120 
&  & "EX~~" id~id^* " . " formula \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

121 
&  & "?!~~" id~id^* " . " formula 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

122 
&  & "EX!~" id~id^* " . " formula 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

123 
\end{array} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

124 
\] 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

125 
\caption{Full grammar for \HOL} \label{holgrammar} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

126 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

127 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

128 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

129 
\section{Syntax} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

130 

1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

131 
Figure~\ref{holconstants} lists the constants (including infixes and 
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

132 
binders), while Fig.\ts\ref{holgrammar} presents the grammar of 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

133 
higherorder logic. Note that $a$\verb~=$b$ is translated to 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

134 
$\neg(a=b)$. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

135 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

136 
\begin{warn} 
1162  137 
\HOL\ has no ifandonlyif connective; logical equivalence is expressed 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

138 
using equality. But equality has a high priority, as befitting a 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

139 
relation, while ifandonlyif typically has the lowest priority. Thus, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

140 
$\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

141 
When using $=$ to mean logical equivalence, enclose both operands in 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

142 
parentheses. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

143 
\end{warn} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

144 

2926  145 
\subsection{Types and classes} 
3152  146 
The universal type class of higherorder terms is called~\cldx{term}. 
147 
By default, explicit type variables have class \cldx{term}. In 

148 
particular the equality symbol and quantifiers are polymorphic over 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

149 
class \texttt{term}. 
2926  150 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

151 
The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus, 
3152  152 
formulae are terms. The builtin type~\tydx{fun}, which constructs 
153 
function types, is overloaded with arity {\tt(term,\thinspace 

154 
term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt 

155 
term} if $\sigma$ and~$\tau$ do, allowing quantification over 

156 
functions. 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

157 

3152  158 
\HOL\ offers various methods for introducing new types. 
159 
See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}. 

2926  160 

3152  161 
Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order 
162 
signatures; the relations $<$ and $\leq$ are polymorphic over this 

163 
class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and 

164 
the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass 

165 
\cldx{order} of \cldx{ord} which axiomatizes partially ordered types 

166 
(w.r.t.\ $\le$). 

2926  167 

3152  168 
Three other syntactic type classes  \cldx{plus}, \cldx{minus} and 
169 
\cldx{times}  permit overloading of the operators {\tt+},\index{*"+ 

170 
symbol} {\tt}\index{*" symbol} and {\tt*}.\index{*"* symbol} In 

171 
particular, {\tt} is instantiated for set difference and subtraction 

172 
on natural numbers. 

2926  173 

174 
If you state a goal containing overloaded functions, you may need to include 

175 
type constraints. Type inference may otherwise make the goal more 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

176 
polymorphic than you intended, with confusing results. For example, the 
2926  177 
variables $i$, $j$ and $k$ in the goal $i \le j \Imp i \le j+k$ have type 
178 
$\alpha::\{ord,plus\}$, although you may have expected them to have some 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

179 
numeric type, e.g. $nat$. Instead you should have stated the goal as 
2926  180 
$(i::nat) \le j \Imp i \le j+k$, which causes all three variables to have 
181 
type $nat$. 

182 

183 
\begin{warn} 

184 
If resolution fails for no obvious reason, try setting 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

185 
\ttindex{show_types} to \texttt{true}, causing Isabelle to display 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

186 
types of terms. Possibly set \ttindex{show_sorts} to \texttt{true} as 
3152  187 
well, causing Isabelle to display type classes and sorts. 
2926  188 

189 
\index{unification!incompleteness of} 

190 
Where function types are involved, Isabelle's unification code does not 

191 
guarantee to find instantiations for type variables automatically. Be 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

192 
prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac}, 
2926  193 
possibly instantiating type variables. Setting 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

194 
\ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report 
2926  195 
omitted search paths during unification.\index{tracing!of unification} 
196 
\end{warn} 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

197 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

198 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

199 
\subsection{Binders} 
3160  200 

201 
Hilbert's {\bf description} operator~$\varepsilon x.P[x]$ stands for 

3152  202 
some~$x$ satisfying~$P$, if such exists. Since all terms in \HOL\ 
203 
denote something, a description is always meaningful, but we do not 

204 
know its value unless $P$ defines it uniquely. We may write 

205 
descriptions as \cdx{Eps}($\lambda x.P[x]$) or use the syntax 

206 
\hbox{\tt \at $x$.$P[x]$}. 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

207 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

208 
Existential quantification is defined by 
2926  209 
\[ \exists x.P~x \;\equiv\; P(\varepsilon x.P~x). \] 
210 
The unique existence quantifier, $\exists!x.P$, is defined in terms 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

211 
of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested 
2926  212 
quantifications. For instance, $\exists!x\,y.P\,x\,y$ abbreviates 
3160  213 
$\exists!x. \exists!y.P\,x\,y$; note that this does not mean that there 
214 
exists a unique pair $(x,y)$ satisfying~$P\,x\,y$. 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

215 

1162  216 
\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} 
217 
Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\ 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

218 
uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

219 
existential quantifier must be followed by a space; thus {\tt?x} is an 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

220 
unknown, while \verb'? x.f x=y' is a quantification. Isabelle's usual 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

221 
notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

222 
available. Both notations are accepted for input. The {\ML} reference 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

223 
\ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

224 
true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

225 
to \texttt{false}, then~{\tt ALL} and~{\tt EX} are displayed. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

226 

3152  227 
If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a 
228 
variable of type $\tau$, then the term \cdx{LEAST}~$x.P[x]$ is defined 

229 
to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

230 
Fig.~\ref{holdefs}). The definition uses Hilbert's $\varepsilon$ 
3160  231 
choice operator, so \texttt{Least} is always meaningful, but may yield 
232 
nothing useful in case there is not a unique least element satisfying 

233 
$P$.\footnote{Class $ord$ does not require much of its instances, so 

234 
$\le$ need not be a wellordering, not even an order at all!} 

2926  235 

3152  236 
\medskip All these binders have priority 10. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

237 

2926  238 
\begin{warn} 
239 
The low priority of binders means that they need to be enclosed in 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

240 
parenthesis when they occur in the context of other operations. For example, 
2926  241 
instead of $P \land \forall x.Q$ you need to write $P \land (\forall x.Q)$. 
242 
\end{warn} 

243 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

244 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

245 
\subsection{The \sdx{let} and \sdx{case} constructions} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

246 
Local abbreviations can be introduced by a \texttt{let} construct whose 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

247 
syntax appears in Fig.\ts\ref{holgrammar}. Internally it is translated into 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

248 
the constant~\cdx{Let}. It can be expanded by rewriting with its 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

249 
definition, \tdx{Let_def}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

250 

1162  251 
\HOL\ also defines the basic syntax 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

252 
\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"" \dots ""~c@n~"=>"~e@n\] 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

253 
as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

254 
and \sdx{of} are reserved words. Initially, this is mere syntax and has no 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

255 
logical meaning. By declaring translations, you can cause instances of the 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

256 
{\tt case} construct to denote applications of particular case operators. 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

257 
This is what happens automatically for each \texttt{datatype} definition 
2926  258 
(see~\S\ref{sec:HOL:datatype}). 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

259 

2926  260 
\begin{warn} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

261 
Both \texttt{if} and \texttt{case} constructs have as low a priority as 
3152  262 
quantifiers, which requires additional enclosing parentheses in the context 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

263 
of most other operations. For example, instead of $f~x = if \dots then \dots 
2926  264 
else \dots$ you need to write $f~x = (if \dots then \dots else 
265 
\dots)$. 

266 
\end{warn} 

267 

268 
\section{Rules of inference} 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

269 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

270 
\begin{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

271 
\begin{ttbox}\makeatother 
3152  272 
\tdx{refl} t = (t::'a) 
273 
\tdx{subst} [ s = t; P s ] ==> P (t::'a) 

274 
\tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x.f x) = (\%x.g x) 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

275 
\tdx{impI} (P ==> Q) ==> P>Q 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

276 
\tdx{mp} [ P>Q; P ] ==> Q 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

277 
\tdx{iff} (P>Q) > (Q>P) > (P=Q) 
3152  278 
\tdx{selectI} P(x::'a) ==> P(@x.P x) 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

279 
\tdx{True_or_False} (P=True)  (P=False) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

280 
\end{ttbox} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

281 
\caption{The \texttt{HOL} rules} \label{holrules} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

282 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

283 

3160  284 
Figure~\ref{holrules} shows the primitive inference rules of~\HOL{}, 
285 
with their~{\ML} names. Some of the rules deserve additional 

286 
comments: 

2926  287 
\begin{ttdescription} 
288 
\item[\tdx{ext}] expresses extensionality of functions. 

289 
\item[\tdx{iff}] asserts that logically equivalent formulae are 

290 
equal. 

291 
\item[\tdx{selectI}] gives the defining property of the Hilbert 

292 
$\varepsilon$operator. It is a form of the Axiom of Choice. The derived rule 

293 
\tdx{select_equality} (see below) is often easier to use. 

294 
\item[\tdx{True_or_False}] makes the logic classical.\footnote{In 

295 
fact, the $\varepsilon$operator already makes the logic classical, as 

296 
shown by Diaconescu; see Paulson~\cite{paulsonCOLOG} for details.} 

297 
\end{ttdescription} 

298 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

299 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

300 
\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

301 
\begin{ttbox}\makeatother 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

302 
\tdx{True_def} True == ((\%x::bool.x)=(\%x.x)) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

303 
\tdx{All_def} All == (\%P. P = (\%x.True)) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

304 
\tdx{Ex_def} Ex == (\%P. P(@x.P x)) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

305 
\tdx{False_def} False == (!P.P) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

306 
\tdx{not_def} not == (\%P. P>False) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

307 
\tdx{and_def} op & == (\%P Q. !R. (P>Q>R) > R) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

308 
\tdx{or_def} op  == (\%P Q. !R. (P>R) > (Q>R) > R) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

309 
\tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y > y=x)) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

310 

3152  311 
\tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x)) 
312 
\tdx{if_def} If P x y == 

313 
(\%P x y. @z::'a.(P=True > z=x) & (P=False > z=y)) 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

314 
\tdx{Let_def} Let s f == f s 
3152  315 
\tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) > x <= y)" 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

316 
\end{ttbox} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

317 
\caption{The \texttt{HOL} definitions} \label{holdefs} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

318 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

319 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

320 

1162  321 
\HOL{} follows standard practice in higherorder logic: only a few 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

322 
connectives are taken as primitive, with the remainder defined obscurely 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

323 
(Fig.\ts\ref{holdefs}). Gordon's {\sc hol} system expresses the 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

324 
corresponding definitions \cite[page~270]{mgordonhol} using 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

325 
objectequality~({\tt=}), which is possible because equality in 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

326 
higherorder logic may equate formulae and even functions over formulae. 
1162  327 
But theory~\HOL{}, like all other Isabelle theories, uses 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

328 
metaequality~({\tt==}) for definitions. 
2926  329 
\begin{warn} 
3132
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

330 
The definitions above should never be expanded and are shown for completeness 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

331 
only. Instead users should reason in terms of the derived rules shown below 
2926  332 
or, better still, using highlevel tactics 
333 
(see~\S\ref{sec:HOL:genericpackages}). 

334 
\end{warn} 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

335 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

336 
Some of the rules mention type variables; for example, \texttt{refl} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

337 
mentions the type variable~{\tt'a}. This allows you to instantiate 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

338 
type variables explicitly by calling \texttt{res_inst_tac}. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

339 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

340 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

341 
\begin{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

342 
\begin{ttbox} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

343 
\tdx{sym} s=t ==> t=s 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

344 
\tdx{trans} [ r=s; s=t ] ==> r=t 
1489  345 
\tdx{ssubst} [ t=s; P s ] ==> P t 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

346 
\tdx{box_equals} [ a=b; a=c; b=d ] ==> c=d 
1489  347 
\tdx{arg_cong} x = y ==> f x = f y 
348 
\tdx{fun_cong} f = g ==> f x = g x 

349 
\tdx{cong} [ f = g; x = y ] ==> f x = g y 

350 
\tdx{not_sym} t ~= s ==> s ~= t 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

351 
\subcaption{Equality} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

352 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

353 
\tdx{TrueI} True 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

354 
\tdx{FalseE} False ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

355 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

356 
\tdx{conjI} [ P; Q ] ==> P&Q 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

357 
\tdx{conjunct1} [ P&Q ] ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

358 
\tdx{conjunct2} [ P&Q ] ==> Q 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

359 
\tdx{conjE} [ P&Q; [ P; Q ] ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

360 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

361 
\tdx{disjI1} P ==> PQ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

362 
\tdx{disjI2} Q ==> PQ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

363 
\tdx{disjE} [ P  Q; P ==> R; Q ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

364 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

365 
\tdx{notI} (P ==> False) ==> ~ P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

366 
\tdx{notE} [ ~ P; P ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

367 
\tdx{impE} [ P>Q; P; Q ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

368 
\subcaption{Propositional logic} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

369 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

370 
\tdx{iffI} [ P ==> Q; Q ==> P ] ==> P=Q 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

371 
\tdx{iffD1} [ P=Q; P ] ==> Q 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

372 
\tdx{iffD2} [ P=Q; Q ] ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

373 
\tdx{iffE} [ P=Q; [ P > Q; Q > P ] ==> R ] ==> R 
1489  374 
% 
375 
%\tdx{eqTrueI} P ==> P=True 

376 
%\tdx{eqTrueE} P=True ==> P 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

377 
\subcaption{Logical equivalence} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

378 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

379 
\end{ttbox} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

380 
\caption{Derived rules for \HOL} \label{hollemmas1} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

381 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

382 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

383 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

384 
\begin{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

385 
\begin{ttbox}\makeatother 
1489  386 
\tdx{allI} (!!x. P x) ==> !x. P x 
387 
\tdx{spec} !x.P x ==> P x 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

388 
\tdx{allE} [ !x.P x; P x ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

389 
\tdx{all_dupE} [ !x.P x; [ P x; !x.P x ] ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

390 

1489  391 
\tdx{exI} P x ==> ? x. P x 
392 
\tdx{exE} [ ? x. P x; !!x. P x ==> Q ] ==> Q 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

393 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

394 
\tdx{ex1I} [ P a; !!x. P x ==> x=a ] ==> ?! x. P x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

395 
\tdx{ex1E} [ ?! x.P x; !!x. [ P x; ! y. P y > y=x ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

396 
] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

397 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

398 
\tdx{select_equality} [ P a; !!x. P x ==> x=a ] ==> (@x.P x) = a 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

399 
\subcaption{Quantifiers and descriptions} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

400 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

401 
\tdx{ccontr} (~P ==> False) ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

402 
\tdx{classical} (~P ==> P) ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

403 
\tdx{excluded_middle} ~P  P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

404 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

405 
\tdx{disjCI} (~Q ==> P) ==> PQ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

406 
\tdx{exCI} (! x. ~ P x ==> P a) ==> ? x.P x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

407 
\tdx{impCE} [ P>Q; ~ P ==> R; Q ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

408 
\tdx{iffCE} [ P=Q; [ P;Q ] ==> R; [ ~P; ~Q ] ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

409 
\tdx{notnotD} ~~P ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

410 
\tdx{swap} ~P ==> (~Q ==> P) ==> Q 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

411 
\subcaption{Classical logic} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

412 

1489  413 
%\tdx{if_True} (if True then x else y) = x 
414 
%\tdx{if_False} (if False then x else y) = y 

1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

415 
\tdx{if_P} P ==> (if P then x else y) = x 
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

416 
\tdx{if_not_P} ~ P ==> (if P then x else y) = y 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

417 
\tdx{expand_if} P(if Q then x else y) = ((Q > P x) & (~Q > P y)) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

418 
\subcaption{Conditionals} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

419 
\end{ttbox} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

420 
\caption{More derived rules} \label{hollemmas2} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

421 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

422 

1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

423 
Some derived rules are shown in Figures~\ref{hollemmas1} 
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

424 
and~\ref{hollemmas2}, with their {\ML} names. These include natural rules 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

425 
for the logical connectives, as well as sequentstyle elimination rules for 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

426 
conjunctions, implications, and universal quantifiers. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

427 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

428 
Note the equality rules: \tdx{ssubst} performs substitution in 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

429 
backward proofs, while \tdx{box_equals} supports reasoning by 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

430 
simplifying both sides of an equation. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

431 

1489  432 
The following simple tactics are occasionally useful: 
433 
\begin{ttdescription} 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

434 
\item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI} 
1489  435 
repeatedly to remove all outermost universal quantifiers and implications 
436 
from subgoal $i$. 

437 
\item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction 

438 
on $P$ for subgoal $i$: the latter is replaced by two identical subgoals 

439 
with the added assumptions $P$ and $\neg P$, respectively. 

440 
\end{ttdescription} 

441 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

442 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

443 
\begin{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

444 
\begin{center} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

445 
\begin{tabular}{rrr} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

446 
\it name &\it metatype & \it description \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

447 
\index{{}@\verb'{}' symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

448 
\verb{} & $\alpha\,set$ & the empty set \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

449 
\cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

450 
& insertion of element \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

451 
\cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

452 
& comprehension \\ 
3160  453 
\cdx{Compl} & $\alpha\,set\To\alpha\,set$ 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

454 
& complement \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

455 
\cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

456 
& intersection over a set\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

457 
\cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

458 
& union over a set\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

459 
\cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

460 
&set of sets intersection \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

461 
\cdx{Union} & $(\alpha\,set)set\To\alpha\,set$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

462 
&set of sets union \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

463 
\cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

464 
& powerset \\[1ex] 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

465 
\cdx{range} & $(\alpha\To\beta )\To\beta\,set$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

466 
& range of a function \\[1ex] 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

467 
\cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$ 
2926  468 
& bounded quantifiers 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

469 
\end{tabular} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

470 
\end{center} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

471 
\subcaption{Constants} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

472 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

473 
\begin{center} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

474 
\begin{tabular}{llrrr} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

475 
\it symbol &\it name &\it metatype & \it priority & \it description \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

476 
\sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

477 
intersection over a type\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

478 
\sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

479 
union over a type 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

480 
\end{tabular} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

481 
\end{center} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

482 
\subcaption{Binders} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

483 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

484 
\begin{center} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

485 
\index{*"`"` symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

486 
\index{*": symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

487 
\index{*"<"= symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

488 
\begin{tabular}{rrrr} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

489 
\it symbol & \it metatype & \it priority & \it description \\ 
3161  490 
\tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$ 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

491 
& Left 90 & image \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

492 
\sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ 
3152  493 
& Left 70 & intersection ($\int$) \\ 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

494 
\sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ 
3152  495 
& Left 65 & union ($\un$) \\ 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

496 
\tt: & $[\alpha ,\alpha\,set]\To bool$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

497 
& Left 50 & membership ($\in$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

498 
\tt <= & $[\alpha\,set,\alpha\,set]\To bool$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

499 
& Left 50 & subset ($\subseteq$) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

500 
\end{tabular} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

501 
\end{center} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

502 
\subcaption{Infixes} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

503 
\caption{Syntax of the theory \texttt{Set}} \label{holsetsyntax} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

504 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

505 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

506 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

507 
\begin{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

508 
\begin{center} \tt\frenchspacing 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

509 
\index{*"! symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

510 
\begin{tabular}{rrr} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

511 
\it external & \it internal & \it description \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

512 
$a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm nonmembership\\ 
3152  513 
{\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\ 
514 
{\ttlbrace}$x$.$P[x]${\ttrbrace} & Collect($\lambda x.P[x]$) & 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

515 
\rm comprehension \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

516 
\sdx{INT} $x$:$A$.$B[x]$ & INTER $A$ $\lambda x.B[x]$ & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

517 
\rm intersection \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

518 
\sdx{UN}{\tt\ } $x$:$A$.$B[x]$ & UNION $A$ $\lambda x.B[x]$ & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

519 
\rm union \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

520 
\tt ! $x$:$A$.$P[x]$ or \sdx{ALL} $x$:$A$.$P[x]$ & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

521 
Ball $A$ $\lambda x.P[x]$ & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

522 
\rm bounded $\forall$ \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

523 
\sdx{?} $x$:$A$.$P[x]$ or \sdx{EX}{\tt\ } $x$:$A$.$P[x]$ & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

524 
Bex $A$ $\lambda x.P[x]$ & \rm bounded $\exists$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

525 
\end{tabular} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

526 
\end{center} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

527 
\subcaption{Translations} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

528 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

529 
\dquotes 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

530 
\[\begin{array}{rclcl} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

531 
term & = & \hbox{other terms\ldots} \\ 
3152  532 
&  & "{\ttlbrace}{\ttrbrace}" \\ 
533 
&  & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\ 

534 
&  & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\ 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

535 
&  & term " `` " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

536 
&  & term " Int " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

537 
&  & term " Un " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

538 
&  & "INT~~" id ":" term " . " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

539 
&  & "UN~~~" id ":" term " . " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

540 
&  & "INT~~" id~id^* " . " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

541 
&  & "UN~~~" id~id^* " . " term \\[2ex] 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

542 
formula & = & \hbox{other formulae\ldots} \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

543 
&  & term " : " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

544 
&  & term " \ttilde: " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

545 
&  & term " <= " term \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

546 
&  & "!~" id ":" term " . " formula 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

547 
&  & "ALL " id ":" term " . " formula \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

548 
&  & "?~" id ":" term " . " formula 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

549 
&  & "EX~~" id ":" term " . " formula 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

550 
\end{array} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

551 
\] 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

552 
\subcaption{Full Grammar} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

553 
\caption{Syntax of the theory \texttt{Set} (continued)} \label{holsetsyntax2} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

554 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

555 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

556 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

557 
\section{A formulation of set theory} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

558 
Historically, higherorder logic gives a foundation for Russell and 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

559 
Whitehead's theory of classes. Let us use modern terminology and call them 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

560 
{\bf sets}, but note that these sets are distinct from those of {\ZF} set 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

561 
theory, and behave more like {\ZF} classes. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

562 
\begin{itemize} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

563 
\item 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

564 
Sets are given by predicates over some type~$\sigma$. Types serve to 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

565 
define universes for sets, but type checking is still significant. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

566 
\item 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

567 
There is a universal set (for each type). Thus, sets have complements, and 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

568 
may be defined by absolute comprehension. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

569 
\item 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

570 
Although sets may contain other sets as elements, the containing set must 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

571 
have a more complex type. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

572 
\end{itemize} 
1162  573 
Finite unions and intersections have the same behaviour in \HOL\ as they 
574 
do in~{\ZF}. In \HOL\ the intersection of the empty set is welldefined, 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

575 
denoting the universal set for the given type. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

576 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

577 
\subsection{Syntax of set theory}\index{*set type} 
1162  578 
\HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

579 
essentially the same as $\alpha\To bool$. The new type is defined for 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

580 
clarity and to avoid complications involving function types in unification. 
2926  581 
The isomorphisms between the two types are declared explicitly. They are 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

582 
very natural: \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while 
2926  583 
\hbox{\tt op :} maps in the other direction (ignoring argument order). 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

584 

1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

585 
Figure~\ref{holsetsyntax} lists the constants, infixes, and syntax 
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

586 
translations. Figure~\ref{holsetsyntax2} presents the grammar of the new 
3152  587 
constructs. Infix operators include union and intersection ($A\un B$ 
588 
and $A\int B$), the subset and membership relations, and the image 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

589 
operator~{\tt``}\@. Note that $a$\verb~:$b$ is translated to 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

590 
$\neg(a\in b)$. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

591 

3152  592 
The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in 
593 
the obvious manner using~{\tt insert} and~$\{\}$: 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

594 
\begin{eqnarray*} 
3152  595 
\{a, b, c\} & \equiv & 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

596 
\texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\})) 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

597 
\end{eqnarray*} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

598 

3152  599 
The set \hbox{\tt{\ttlbrace}$x$.$P[x]${\ttrbrace}} consists of all $x$ (of suitable type) 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

600 
that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

601 
occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

602 
x.P[x])$. It defines sets by absolute comprehension, which is impossible 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

603 
in~{\ZF}; the type of~$x$ implicitly restricts the comprehension. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

604 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

605 
The set theory defines two {\bf bounded quantifiers}: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

606 
\begin{eqnarray*} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

607 
\forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

608 
\exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

609 
\end{eqnarray*} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

610 
The constants~\cdx{Ball} and~\cdx{Bex} are defined 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

611 
accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

612 
write\index{*"! symbol}\index{*"? symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

613 
\index{*ALL symbol}\index{*EX symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

614 
% 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

615 
\hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}. Isabelle's 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

616 
usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

617 
for input. As with the primitive quantifiers, the {\ML} reference 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

618 
\ttindex{HOL_quantifiers} specifies which notation to use for output. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

619 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

620 
Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

621 
$\bigcap@{x\in A}B[x]$, are written 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

622 
\sdx{UN}~\hbox{\tt$x$:$A$.$B[x]$} and 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

623 
\sdx{INT}~\hbox{\tt$x$:$A$.$B[x]$}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

624 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

625 
Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

626 
B[x]$, are written \sdx{UN}~\hbox{\tt$x$.$B[x]$} and 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

627 
\sdx{INT}~\hbox{\tt$x$.$B[x]$}. They are equivalent to the previous 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

628 
union and intersection operators when $A$ is the universal set. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

629 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

630 
The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

631 
not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

632 
respectively. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

633 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

634 

2926  635 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

636 
\begin{figure} \underscoreon 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

637 
\begin{ttbox} 
3152  638 
\tdx{mem_Collect_eq} (a : {\ttlbrace}x.P x{\ttrbrace}) = P a 
639 
\tdx{Collect_mem_eq} {\ttlbrace}x.x:A{\ttrbrace} = A 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

640 

3152  641 
\tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x.False{\ttrbrace} 
642 
\tdx{insert_def} insert a B == {\ttlbrace}x.x=a{\ttrbrace} Un B 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

643 
\tdx{Ball_def} Ball A P == ! x. x:A > P x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

644 
\tdx{Bex_def} Bex A P == ? x. x:A & P x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

645 
\tdx{subset_def} A <= B == ! x:A. x:B 
3152  646 
\tdx{Un_def} A Un B == {\ttlbrace}x.x:A  x:B{\ttrbrace} 
647 
\tdx{Int_def} A Int B == {\ttlbrace}x.x:A & x:B{\ttrbrace} 

648 
\tdx{set_diff_def} A  B == {\ttlbrace}x.x:A & x~:B{\ttrbrace} 

649 
\tdx{Compl_def} Compl A == {\ttlbrace}x. ~ x:A{\ttrbrace} 

650 
\tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace} 

651 
\tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace} 

652 
\tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x.True{\ttrbrace} B 

653 
\tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x.True{\ttrbrace} B 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

654 
\tdx{Inter_def} Inter S == (INT x:S. x) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

655 
\tdx{Union_def} Union S == (UN x:S. x) 
3152  656 
\tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace} 
657 
\tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace} 

658 
\tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace} 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

659 
\end{ttbox} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

660 
\caption{Rules of the theory \texttt{Set}} \label{holsetrules} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

661 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

662 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

663 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

664 
\begin{figure} \underscoreon 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

665 
\begin{ttbox} 
3152  666 
\tdx{CollectI} [ P a ] ==> a : {\ttlbrace}x.P x{\ttrbrace} 
667 
\tdx{CollectD} [ a : {\ttlbrace}x.P x{\ttrbrace} ] ==> P a 

668 
\tdx{CollectE} [ a : {\ttlbrace}x.P x{\ttrbrace}; P a ==> W ] ==> W 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

669 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

670 
\tdx{ballI} [ !!x. x:A ==> P x ] ==> ! x:A. P x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

671 
\tdx{bspec} [ ! x:A. P x; x:A ] ==> P x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

672 
\tdx{ballE} [ ! x:A. P x; P x ==> Q; ~ x:A ==> Q ] ==> Q 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

673 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

674 
\tdx{bexI} [ P x; x:A ] ==> ? x:A. P x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

675 
\tdx{bexCI} [ ! x:A. ~ P x ==> P a; a:A ] ==> ? x:A.P x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

676 
\tdx{bexE} [ ? x:A. P x; !!x. [ x:A; P x ] ==> Q ] ==> Q 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

677 
\subcaption{Comprehension and Bounded quantifiers} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

678 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

679 
\tdx{subsetI} (!!x.x:A ==> x:B) ==> A <= B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

680 
\tdx{subsetD} [ A <= B; c:A ] ==> c:B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

681 
\tdx{subsetCE} [ A <= B; ~ (c:A) ==> P; c:B ==> P ] ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

682 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

683 
\tdx{subset_refl} A <= A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

684 
\tdx{subset_trans} [ A<=B; B<=C ] ==> A<=C 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

685 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

686 
\tdx{equalityI} [ A <= B; B <= A ] ==> A = B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

687 
\tdx{equalityD1} A = B ==> A<=B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

688 
\tdx{equalityD2} A = B ==> B<=A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

689 
\tdx{equalityE} [ A = B; [ A<=B; B<=A ] ==> P ] ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

690 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

691 
\tdx{equalityCE} [ A = B; [ c:A; c:B ] ==> P; 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

692 
[ ~ c:A; ~ c:B ] ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

693 
] ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

694 
\subcaption{The subset and equality relations} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

695 
\end{ttbox} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

696 
\caption{Derived rules for set theory} \label{holset1} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

697 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

698 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

699 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

700 
\begin{figure} \underscoreon 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

701 
\begin{ttbox} 
3152  702 
\tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

703 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

704 
\tdx{insertI1} a : insert a B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

705 
\tdx{insertI2} a : B ==> a : insert b B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

706 
\tdx{insertE} [ a : insert b A; a=b ==> P; a:A ==> P ] ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

707 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

708 
\tdx{ComplI} [ c:A ==> False ] ==> c : Compl A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

709 
\tdx{ComplD} [ c : Compl A ] ==> ~ c:A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

710 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

711 
\tdx{UnI1} c:A ==> c : A Un B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

712 
\tdx{UnI2} c:B ==> c : A Un B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

713 
\tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

714 
\tdx{UnE} [ c : A Un B; c:A ==> P; c:B ==> P ] ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

715 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

716 
\tdx{IntI} [ c:A; c:B ] ==> c : A Int B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

717 
\tdx{IntD1} c : A Int B ==> c:A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

718 
\tdx{IntD2} c : A Int B ==> c:B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

719 
\tdx{IntE} [ c : A Int B; [ c:A; c:B ] ==> P ] ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

720 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

721 
\tdx{UN_I} [ a:A; b: B a ] ==> b: (UN x:A. B x) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

722 
\tdx{UN_E} [ b: (UN x:A. B x); !!x.[ x:A; b:B x ] ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

723 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

724 
\tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

725 
\tdx{INT_D} [ b: (INT x:A. B x); a:A ] ==> b: B a 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

726 
\tdx{INT_E} [ b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

727 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

728 
\tdx{UnionI} [ X:C; A:X ] ==> A : Union C 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

729 
\tdx{UnionE} [ A : Union C; !!X.[ A:X; X:C ] ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

730 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

731 
\tdx{InterI} [ !!X. X:C ==> A:X ] ==> A : Inter C 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

732 
\tdx{InterD} [ A : Inter C; X:C ] ==> A:X 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

733 
\tdx{InterE} [ A : Inter C; A:X ==> R; ~ X:C ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

734 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

735 
\tdx{PowI} A<=B ==> A: Pow B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

736 
\tdx{PowD} A: Pow B ==> A<=B 
2926  737 

738 
\tdx{imageI} [ x:A ] ==> f x : f``A 

739 
\tdx{imageE} [ b : f``A; !!x.[ b=f x; x:A ] ==> P ] ==> P 

740 

741 
\tdx{rangeI} f x : range f 

742 
\tdx{rangeE} [ b : range f; !!x.[ b=f x ] ==> P ] ==> P 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

743 
\end{ttbox} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

744 
\caption{Further derived rules for set theory} \label{holset2} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

745 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

746 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

747 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

748 
\subsection{Axioms and rules of set theory} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

749 
Figure~\ref{holsetrules} presents the rules of theory \thydx{Set}. The 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

750 
axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

751 
that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

752 
course, \hbox{\tt op :} also serves as the membership relation. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

753 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

754 
All the other axioms are definitions. They include the empty set, bounded 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

755 
quantifiers, unions, intersections, complements and the subset relation. 
2926  756 
They also include straightforward constructions on functions: image~({\tt``}) 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

757 
and \texttt{range}. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

758 

2926  759 
%The predicate \cdx{inj_onto} is used for simulating type definitions. 
760 
%The statement ${\tt inj_onto}~f~A$ asserts that $f$ is injective on the 

761 
%set~$A$, which specifies a subset of its domain type. In a type 

762 
%definition, $f$ is the abstraction function and $A$ is the set of valid 

763 
%representations; we should not expect $f$ to be injective outside of~$A$. 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

764 

2926  765 
%\begin{figure} \underscoreon 
766 
%\begin{ttbox} 

767 
%\tdx{Inv_f_f} inj f ==> Inv f (f x) = x 

768 
%\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y 

769 
% 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

770 
%\tdx{Inv_injective} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

771 
% [ Inv f x=Inv f y; x: range f; y: range f ] ==> x=y 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

772 
% 
2926  773 
% 
774 
%\tdx{monoI} [ !!A B. A <= B ==> f A <= f B ] ==> mono f 

775 
%\tdx{monoD} [ mono f; A <= B ] ==> f A <= f B 

776 
% 

777 
%\tdx{injI} [ !! x y. f x = f y ==> x=y ] ==> inj f 

778 
%\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f 

779 
%\tdx{injD} [ inj f; f x = f y ] ==> x=y 

780 
% 

781 
%\tdx{inj_ontoI} (!!x y. [ f x=f y; x:A; y:A ] ==> x=y) ==> inj_onto f A 

782 
%\tdx{inj_ontoD} [ inj_onto f A; f x=f y; x:A; y:A ] ==> x=y 

783 
% 

784 
%\tdx{inj_onto_inverseI} 

785 
% (!!x. x:A ==> g(f x) = x) ==> inj_onto f A 

786 
%\tdx{inj_onto_contraD} 

787 
% [ inj_onto f A; x~=y; x:A; y:A ] ==> ~ f x=f y 

788 
%\end{ttbox} 

789 
%\caption{Derived rules involving functions} \label{holfun} 

790 
%\end{figure} 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

791 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

792 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

793 
\begin{figure} \underscoreon 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

794 
\begin{ttbox} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

795 
\tdx{Union_upper} B:A ==> B <= Union A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

796 
\tdx{Union_least} [ !!X. X:A ==> X<=C ] ==> Union A <= C 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

797 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

798 
\tdx{Inter_lower} B:A ==> Inter A <= B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

799 
\tdx{Inter_greatest} [ !!X. X:A ==> C<=X ] ==> C <= Inter A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

800 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

801 
\tdx{Un_upper1} A <= A Un B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

802 
\tdx{Un_upper2} B <= A Un B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

803 
\tdx{Un_least} [ A<=C; B<=C ] ==> A Un B <= C 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

804 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

805 
\tdx{Int_lower1} A Int B <= A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

806 
\tdx{Int_lower2} A Int B <= B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

807 
\tdx{Int_greatest} [ C<=A; C<=B ] ==> C <= A Int B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

808 
\end{ttbox} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

809 
\caption{Derived rules involving subsets} \label{holsubset} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

810 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

811 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

812 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

813 
\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

814 
\begin{ttbox} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

815 
\tdx{Int_absorb} A Int A = A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

816 
\tdx{Int_commute} A Int B = B Int A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

817 
\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

818 
\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

819 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

820 
\tdx{Un_absorb} A Un A = A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

821 
\tdx{Un_commute} A Un B = B Un A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

822 
\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

823 
\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

824 

3152  825 
\tdx{Compl_disjoint} A Int (Compl A) = {\ttlbrace}x.False{\ttrbrace} 
826 
\tdx{Compl_partition} A Un (Compl A) = {\ttlbrace}x.True{\ttrbrace} 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

827 
\tdx{double_complement} Compl(Compl A) = A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

828 
\tdx{Compl_Un} Compl(A Un B) = (Compl A) Int (Compl B) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

829 
\tdx{Compl_Int} Compl(A Int B) = (Compl A) Un (Compl B) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

830 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

831 
\tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

832 
\tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

833 
\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

834 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

835 
\tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

836 
\tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

837 
\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

838 
\end{ttbox} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

839 
\caption{Set equalities} \label{holequalities} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

840 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

841 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

842 

1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

843 
Figures~\ref{holset1} and~\ref{holset2} present derived rules. Most are 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

844 
obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

845 
such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

846 
are designed for classical reasoning; the rules \tdx{subsetD}, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

847 
\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

848 
strictly necessary but yield more natural proofs. Similarly, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

849 
\tdx{equalityCE} supports classical reasoning about extensionality, 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

850 
after the fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

851 
proofs pertaining to set theory. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

852 

1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

853 
Figure~\ref{holsubset} presents lattice properties of the subset relation. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

854 
Unions form least upper bounds; nonempty intersections form greatest lower 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

855 
bounds. Reasoning directly about subsets often yields clearer proofs than 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

856 
reasoning about the membership relation. See the file \texttt{HOL/subset.ML}. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

857 

1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

858 
Figure~\ref{holequalities} presents many common set equalities. They 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

859 
include commutative, associative and distributive laws involving unions, 
2926  860 
intersections and complements. For a complete listing see the file {\tt 
861 
HOL/equalities.ML}. 

862 

863 
\begin{warn} 

3132
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

864 
\texttt{Blast_tac} proves many settheoretic theorems automatically. 
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

865 
Hence you seldom need to refer to the theorems above. 
2926  866 
\end{warn} 
867 

868 
\begin{figure} 

869 
\begin{center} 

870 
\begin{tabular}{rrr} 

871 
\it name &\it metatype & \it description \\ 

872 
\cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$ 

873 
& injective/surjective \\ 

874 
\cdx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$ 

875 
& injective over subset\\ 

876 
\cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function 

877 
\end{tabular} 

878 
\end{center} 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

879 

2926  880 
\underscoreon 
881 
\begin{ttbox} 

882 
\tdx{inj_def} inj f == ! x y. f x=f y > x=y 

883 
\tdx{surj_def} surj f == ! y. ? x. y=f x 

884 
\tdx{inj_onto_def} inj_onto f A == !x:A. !y:A. f x=f y > x=y 

885 
\tdx{inv_def} inv f == (\%y. @x. f(x)=y) 

886 
\end{ttbox} 

887 
\caption{Theory \thydx{Fun}} \label{fig:HOL:Fun} 

888 
\end{figure} 

889 

890 
\subsection{Properties of functions}\nopagebreak 

891 
Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions. 

892 
Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

893 
of~$f$. See the file \texttt{HOL/Fun.ML} for a complete listing of the derived 
2926  894 
rules. Reasoning about function composition (the operator~\sdx{o}) and the 
895 
predicate~\cdx{surj} is done simply by expanding the definitions. 

896 

897 
There is also a large collection of monotonicity theorems for constructions 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

898 
on sets in the file \texttt{HOL/mono.ML}. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

899 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

900 
\section{Generic packages} 
2926  901 
\label{sec:HOL:genericpackages} 
902 

3132
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

903 
\HOL\ instantiates most of Isabelle's generic packages, making available the 
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

904 
simplifier and the classical reasoner. 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

905 

3152  906 
\subsection{Simplification and substitution} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

907 

3152  908 
The simplifier is available in \HOL. Tactics such as {\tt 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

909 
Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset 
3152  910 
({\tt!simpset}), which works for most purposes. A quite minimal 
911 
simplification set for higherorder logic is~\ttindexbold{HOL_ss}, 

912 
even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which 

913 
also expresses logical equivalence, may be used for rewriting. See 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

914 
the file \texttt{HOL/simpdata.ML} for a complete listing of the basic 
3152  915 
simplification rules. 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

916 

bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

917 
See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

918 
{Chaps.\ts\ref{substitution} and~\ref{simpchap}} for details of substitution 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

919 
and simplification. 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

920 

3132
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

921 
\begin{warn}\index{simplification!of conjunctions}% 
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

922 
Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous. The 
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

923 
left part of a conjunction helps in simplifying the right part. This effect 
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

924 
is not available by default: it can be slow. It can be obtained by 
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

925 
including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$. 
1234  926 
\end{warn} 
927 

3152  928 
If the simplifier cannot use a certain rewrite rule  either because 
929 
of nontermination or because its lefthand side is too flexible  

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

930 
then you might try \texttt{stac}: 
1489  931 
\begin{ttdescription} 
932 
\item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$, 

933 
replaces in subgoal $i$ instances of $lhs$ by corresponding instances of 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

934 
$rhs$. In case of multiple instances of $lhs$ in subgoal $i$, backtracking 
1489  935 
may be necessary to select the desired ones. 
2926  936 

937 
If $thm$ is a conditional equality, the instantiated condition becomes an 

938 
additional (first) subgoal. 

1489  939 
\end{ttdescription} 
940 

3132
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

941 
\HOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes 
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

942 
for an equality throughout a subgoal and its hypotheses. This tactic uses 
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

943 
\HOL's general substitution rule. 
2926  944 

1489  945 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

946 
\subsection{Classical reasoning} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

947 

1162  948 
\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

949 
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

950 
rule; recall Fig.\ts\ref{hollemmas2} above. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

951 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

952 
The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and {\tt 
2495  953 
Best_tac} use the default claset ({\tt!claset}), which works for most 
954 
purposes. Named clasets include \ttindexbold{prop_cs}, which includes the 

2926  955 
propositional rules, and \ttindexbold{HOL_cs}, which also includes quantifier 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

956 
rules. See the file \texttt{HOL/cladata.ML} for lists of the classical rules, 
2926  957 
and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% 
958 
{Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods. 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

959 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

960 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

961 
\section{Types}\label{sec:HOL:Types} 
3152  962 
This section describes \HOL's basic predefined types ($\alpha \times 
963 
\beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

964 
introducing new types in general. The most important type 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

965 
construction, the \texttt{datatype}, is treated separately in 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

966 
\S\ref{sec:HOL:datatype}. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

967 

3152  968 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

969 
\subsection{Product and sum types}\index{*"* type}\index{*"+ type} 
2994  970 
\label{subsec:prodsum} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

971 

2926  972 
\begin{figure}[htbp] 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

973 
\begin{constants} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

974 
\it symbol & \it metatype & & \it description \\ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

975 
\cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

976 
& & ordered pairs $(a,b)$ \\ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

977 
\cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

978 
\cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

979 
\cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

980 
& & generalized projection\\ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

981 
\cdx{Sigma} & 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

982 
$[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ & 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

983 
& general sum of sets 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

984 
\end{constants} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

985 
\begin{ttbox}\makeatletter 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

986 
%\tdx{fst_def} fst p == @a. ? b. p = (a,b) 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

987 
%\tdx{snd_def} snd p == @b. ? a. p = (a,b) 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

988 
%\tdx{split_def} split c p == c (fst p) (snd p) 
3152  989 
\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

990 

2926  991 
\tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b') 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

992 
\tdx{Pair_inject} [ (a, b) = (a',b'); [ a=a'; b=b' ] ==> R ] ==> R 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

993 
\tdx{PairE} [ !!x y. p = (x,y) ==> Q ] ==> Q 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

994 

bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

995 
\tdx{fst_conv} fst (a,b) = a 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

996 
\tdx{snd_conv} snd (a,b) = b 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

997 
\tdx{surjective_pairing} p = (fst p,snd p) 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

998 

bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

999 
\tdx{split} split c (a,b) = c a b 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1000 
\tdx{expand_split} R(split c p) = (! x y. p = (x,y) > R(c x y)) 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1001 

3132
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

1002 
\tdx{SigmaI} [ a:A; b:B a ] ==> (a,b) : Sigma A B 
8e956415412f
Documents directory Induct; stylistic improvements
paulson
parents:
3045
diff
changeset

1003 
\tdx{SigmaE} [ c:Sigma A B; !!x y.[ x:A; y:B x; c=(x,y) ] ==> P ] ==> P 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1004 
\end{ttbox} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1005 
\caption{Type $\alpha\times\beta$}\label{holprod} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1006 
\end{figure} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1007 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1008 
Theory \thydx{Prod} (Fig.\ts\ref{holprod}) defines the product type 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1009 
$\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General 
3152  1010 
tuples are simulated by pairs nested to the right: 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1011 
\begin{center} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1012 
\begin{tabular}{cc} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1013 
\hline 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1014 
external & internal \\ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1015 
\hline 
3152  1016 
$\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n1} \times \tau@n)\dots)$ \\ 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1017 
\hline 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1018 
$(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n1},t@n)\dots)$ \\ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1019 
\hline 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1020 
\end{tabular} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1021 
\end{center} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1022 
In addition, it is possible to use tuples 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1023 
as patterns in abstractions: 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1024 
\begin{center} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1025 
{\tt\%($x$,$y$).$t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.$t$)} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1026 
\end{center} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1027 
Nested patterns are also supported. They are translated stepwise: 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1028 
{\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$ 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1029 
{\tt split(\%$x$.\%($y$,$z$).$t$)} $\leadsto$ \texttt{split(\%$x$.split(\%$y$ 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1030 
$z$.$t$))}. The reverse translation is performed upon printing. 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1031 
\begin{warn} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1032 
The translation between patterns and \texttt{split} is performed automatically 
1448
77379ae9ff0d
Stylistic changes to discussion of patternmatching
paulson
parents:
1429
diff
changeset

1033 
by the parser and printer. Thus the internal and external form of a term 
2926  1034 
may differ, which can affects proofs. For example the term {\tt 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1035 
(\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the 
2926  1036 
default simpset) to rewrite to {\tt(b,a)}. 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1037 
\end{warn} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1038 
In addition to explicit $\lambda$abstractions, patterns can be used in any 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1039 
variable binding construct which is internally described by a 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1040 
$\lambda$abstraction. Some important examples are 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1041 
\begin{description} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1042 
\item[Let:] \texttt{let {\it pattern} = $t$ in $u$} 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1043 
\item[Quantifiers:] \texttt{!~{\it pattern}:$A$.~$P$} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1044 
\item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1045 
\item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$} 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1046 
\item[Sets:] \texttt{{\ttlbrace}~{\it pattern}~.~$P$~{\ttrbrace}} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1047 
\end{description} 
1471  1048 

1049 
There is a simple tactic which supports reasoning about patterns: 

1050 
\begin{ttdescription} 

1051 
\item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all 

1052 
{\tt!!}quantified variables of product type by individual variables for 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1053 
each component. A simple example: 
1471  1054 
\begin{ttbox} 
1055 
{\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p} 

1056 
by(split_all_tac 1); 

1057 
{\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)} 

1058 
\end{ttbox} 

1059 
\end{ttdescription} 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1060 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1061 
Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1062 
which contains only a single element named {\tt()} with the property 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1063 
\begin{ttbox} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1064 
\tdx{unit_eq} u = () 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1065 
\end{ttbox} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1066 
\bigskip 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1067 

bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1068 
Theory \thydx{Sum} (Fig.~\ref{holsum}) defines the sum type $\alpha+\beta$ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1069 
which associates to the right and has a lower priority than $*$: $\tau@1 + 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1070 
\tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$. 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1071 

3152  1072 
The definition of products and sums in terms of existing types is not 
1073 
shown. The constructions are fairly standard and can be found in the 

1074 
respective theory files. 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1075 

bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1076 
\begin{figure} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1077 
\begin{constants} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1078 
\it symbol & \it metatype & & \it description \\ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1079 
\cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1080 
\cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1081 
\cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$ 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1082 
& & conditional 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1083 
\end{constants} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1084 
\begin{ttbox}\makeatletter 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1085 
%\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl x > z=f x) & 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1086 
% (!y. p=Inr y > z=g y)) 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1087 
% 
3152  1088 
\tdx{Inl_not_Inr} Inl a ~= Inr b 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1089 

bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1090 
\tdx{inj_Inl} inj Inl 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1091 
\tdx{inj_Inr} inj Inr 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1092 

1489  1093 
\tdx{sumE} [ !!x. P(Inl x); !!y. P(Inr y) ] ==> P s 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1094 

bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1095 
\tdx{sum_case_Inl} sum_case f g (Inl x) = f x 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1096 
\tdx{sum_case_Inr} sum_case f g (Inr x) = g x 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1097 

1489  1098 
\tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1099 
\tdx{expand_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) > R(f(x))) & 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1100 
(! y. s = Inr(y) > R(g(y)))) 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1101 
\end{ttbox} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1102 
\caption{Type $\alpha+\beta$}\label{holsum} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1103 
\end{figure} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1104 

bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1105 
\begin{figure} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1106 
\index{*"< symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1107 
\index{*"* symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1108 
\index{*div symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1109 
\index{*mod symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1110 
\index{*"+ symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1111 
\index{*" symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1112 
\begin{constants} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1113 
\it symbol & \it metatype & \it priority & \it description \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1114 
\cdx{0} & $nat$ & & zero \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1115 
\cdx{Suc} & $nat \To nat$ & & successor function\\ 
2926  1116 
% \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$ & & conditional\\ 
1117 
% \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$ 

1118 
% & & primitive recursor\\ 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1119 
\tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1120 
\tt div & $[nat,nat]\To nat$ & Left 70 & division\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1121 
\tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1122 
\tt + & $[nat,nat]\To nat$ & Left 65 & addition\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1123 
\tt  & $[nat,nat]\To nat$ & Left 65 & subtraction 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1124 
\end{constants} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1125 
\subcaption{Constants and infixes} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1126 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1127 
\begin{ttbox}\makeatother 
3045  1128 
\tdx{nat_induct} [ P 0; !!n. P n ==> P(Suc n) ] ==> P n 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1129 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1130 
\tdx{Suc_not_Zero} Suc m ~= 0 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1131 
\tdx{inj_Suc} inj Suc 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1132 
\tdx{n_not_Suc_n} n~=Suc n 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1133 
\subcaption{Basic properties} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1134 
\end{ttbox} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1135 
\caption{The type of natural numbers, \tydx{nat}} \label{holnat1} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1136 
\end{figure} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1137 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1138 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1139 
\begin{figure} 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1140 
\begin{ttbox}\makeatother 
2926  1141 
0+n = n 
1142 
(Suc m)+n = Suc(m+n) 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1143 

2926  1144 
m0 = m 
1145 
0n = n 

1146 
Suc(m)Suc(n) = mn 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1147 

2926  1148 
0*n = 0 
1149 
Suc(m)*n = n + m*n 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1150 

2926  1151 
\tdx{mod_less} m<n ==> m mod n = m 
1152 
\tdx{mod_geq} [ 0<n; ~m<n ] ==> m mod n = (mn) mod n 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1153 

2926  1154 
\tdx{div_less} m<n ==> m div n = 0 
1155 
\tdx{div_geq} [ 0<n; ~m<n ] ==> m div n = Suc((mn) div n) 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1156 
\end{ttbox} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1157 
\caption{Recursion equations for the arithmetic operators} \label{holnat2} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1158 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1159 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1160 
\subsection{The type of natural numbers, \textit{nat}} 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1161 
\index{nat@{\textit{nat}} type(} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1162 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1163 
The theory \thydx{NatDef} defines the natural numbers in a roundabout but 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1164 
traditional way. The axiom of infinity postulates a type~\tydx{ind} of 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1165 
individuals, which is nonempty and closed under an injective operation. The 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1166 
natural numbers are inductively generated by choosing an arbitrary individual 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1167 
for~0 and using the injective operation to take successors. This is a least 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1168 
fixedpoint construction. For details see the file \texttt{NatDef.thy}. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1169 

2926  1170 
Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the 
1171 
overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1172 
\cdx{min}, \cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1173 
\thydx{Nat} builds on \texttt{NatDef} and shows that {\tt<=} is a partial order, 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1174 
so \tydx{nat} is also an instance of class \cldx{order}. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1175 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1176 
Theory \thydx{Arith} develops arithmetic on the natural numbers. It defines 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1177 
addition, multiplication and subtraction. Theory \thydx{Divides} defines 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1178 
division, remainder and the ``divides'' relation. The numerous theorems 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1179 
proved include commutative, associative, distributive, identity and 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1180 
cancellation laws. See Figs.\ts\ref{holnat1} and~\ref{holnat2}. The 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1181 
recursion equations for the operators \texttt{+}, \texttt{} and \texttt{*} on 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1182 
\texttt{nat} are part of the default simpset. 
2926  1183 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1184 
Functions on \tydx{nat} can be defined by primitive or wellfounded recursion; 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1185 
see \S\ref{sec:HOL:recursive}. A simple example is addition. 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1186 
Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1187 
the standard convention. 
2926  1188 
\begin{ttbox} 
1189 
\sdx{primrec} "op +" nat 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1190 
" 0 + n = n" 
2926  1191 
"Suc m + n = Suc(m + n)" 
1192 
\end{ttbox} 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1193 
There is also a \sdx{case}construct 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1194 
of the form 
2926  1195 
\begin{ttbox} 
1196 
case \(e\) of 0 => \(a\)  Suc \(m\) => \(b\) 

1197 
\end{ttbox} 

1198 
Note that Isabelle insists on precisely this format; you may not even change 

1199 
the order of the two cases. 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1200 
Both \texttt{primrec} and \texttt{case} are realized by a recursion operator 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1201 
\cdx{nat_rec}, the details of which can be found in theory \texttt{NatDef}. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1202 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1203 
%The predecessor relation, \cdx{pred_nat}, is shown to be wellfounded. 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1204 
%Recursion along this relation resembles primitive recursion, but is 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1205 
%stronger because we are in higherorder logic; using primitive recursion to 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1206 
%define a higherorder function, we can easily Ackermann's function, which 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1207 
%is not primitive recursive \cite[page~104]{thompson91}. 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1208 
%The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the 
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1209 
%natural numbers are most easily expressed using recursion along~$<$. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1210 

3045  1211 
Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$ 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1212 
in subgoal~$i$ using theorem \texttt{nat_induct}. There is also the derived 
3152  1213 
theorem \tdx{less_induct}: 
2926  1214 
\begin{ttbox} 
1215 
[ !!n. [ ! m. m<n > P m ] ==> P n ] ==> P n 

1216 
\end{ttbox} 

1217 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1218 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1219 
Reasoning about arithmetic inequalities can be tedious. A minimal amount of 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1220 
automation is provided by the tactic \ttindex{trans_tac} of type \texttt{int > 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1221 
tactic} that deals with simple inequalities. Note that it only knows about 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1222 
{\tt 0}, \texttt{Suc}, {\tt<} and {\tt<=}. The following goals are all solved by 
2926  1223 
{\tt trans_tac 1}: 
1224 
\begin{ttbox} 

3152  1225 
{\out 1. \dots ==> m <= Suc(Suc m)} 
2926  1226 
{\out 1. [ \dots i <= j \dots Suc j <= k \dots ] ==> i < k} 
1227 
{\out 1. [ \dots Suc m <= n \dots ~ m < n \dots ] ==> \dots} 

1228 
\end{ttbox} 

1229 
For a complete description of the limitations of the tactic and how to avoid 

1230 
some of them, see the comments at the start of the file {\tt 

1231 
Provers/nat_transitive.ML}. 

1232 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1233 
If \texttt{trans_tac} fails you, try to find relevant arithmetic results in 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1234 
the library. The theory \texttt{NatDef} contains theorems about {\tt<} and 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1235 
{\tt<=}, the theory \texttt{Arith} contains theorems about \texttt{+}, 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1236 
\texttt{} and \texttt{*}, and theory \texttt{Divides} contains theorems about 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1237 
\texttt{div} and \texttt{mod}. Use the \texttt{find}functions to locate them 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1238 
(see the {\em Reference Manual\/}). 
2926  1239 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1240 
\begin{figure} 
1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1241 
\index{#@{\tt[]} symbol} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1242 
\index{#@{\tt\#} symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1243 
\index{"@@{\tt\at} symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1244 
\begin{constants} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1245 
\it symbol & \it metatype & \it priority & \it description \\ 
2926  1246 
\tt[] & $\alpha\,list$ & & empty list\\ 
1247 
\tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 & 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1248 
list constructor \\ 
2926  1249 
\cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\ 
1250 
\cdx{hd} & $\alpha\,list \To \alpha$ & & head \\ 

1251 
\cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\ 

3881  1252 
\cdx{last} & $\alpha\,list \To \alpha$ & & last element \\ 
1253 
\cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\ 

2926  1254 
\tt\at & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\ 
1255 
\cdx{map} & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$ 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1256 
& & apply to all\\ 
2926  1257 
\cdx{filter} & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$ 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1258 
& & filter functional\\ 
3487  1259 
\cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\ 
2926  1260 
\sdx{mem} & $[\alpha,\alpha\,list]\To bool$ & Left 55 & membership\\ 
1261 
\cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ & 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1262 
& iteration \\ 
2926  1263 
\cdx{concat} & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\ 
1264 
\cdx{rev} & $\alpha\,list \To \alpha\,list$ & & reverse \\ 

1265 
\cdx{length} & $\alpha\,list \To nat$ & & length \\ 

1266 
\cdx{nth} & $nat \To \alpha\,list \To \alpha$ & & indexing \\ 

1267 
\cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ && 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1268 
take or drop a prefix \\ 
2926  1269 
\cdx{takeWhile},\\ 
1270 
\cdx{dropWhile} & 

1271 
$(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ && 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1272 
take or drop a prefix 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1273 
\end{constants} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1274 
\subcaption{Constants and infixes} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1275 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1276 
\begin{center} \tt\frenchspacing 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1277 
\begin{tabular}{rrr} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1278 
\it external & \it internal & \it description \\{} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1279 
[$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1280 
\rm finite list \\{} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1281 
[$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1282 
\rm list comprehension 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1283 
\end{tabular} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1284 
\end{center} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1285 
\subcaption{Translations} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

1286 
\caption{The theory \thydx{List}} \label{hollist} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1287 
\end{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1288 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1289 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1290 
\begin{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1291 
\begin{ttbox}\makeatother 
2926  1292 
null [] = True 
1293 
null (x#xs) = False 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1294 

2926  1295 
hd (x#xs) = x 
1296 
tl (x#xs) = xs 

3881  1297 
tl [] = [] 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1298 

2926  1299 
[] @ ys = ys 
1300 
(x#xs) @ ys = x # xs @ ys 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1301 

2926  1302 
map f [] = [] 
1303 
map f (x#xs) = f x # map f xs 

1304 

1305 
filter P [] = [] 

1306 
filter P (x#xs) = (if P x then x#filter P xs else filter P xs) 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1307 

3487  1308 
set [] = \ttlbrace\ttrbrace 
1309 
set (x#xs) = insert x (set xs) 

2926  1310 

1311 
x mem [] = False 

1312 
x mem (y#ys) = (if y=x then True else x mem ys) 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1313 

2926  1314 
foldl f a [] = a 
1315 
foldl f a (x#xs) = foldl f (f a x) xs 

1316 

1317 
concat([]) = [] 

1318 
concat(x#xs) = x @ concat(xs) 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1319 

2926  1320 
rev([]) = [] 
1321 
rev(x#xs) = rev(xs) @ [x] 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1322 

2926  1323 
length([]) = 0 
1324 
length(x#xs) = Suc(length(xs)) 

1325 

1326 
nth 0 xs = hd xs 

1327 
nth (Suc n) xs = nth n (tl xs) 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1328 

2926  1329 
take n [] = [] 
1330 
take n (x#xs) = (case n of 0 => []  Suc(m) => x # take m xs) 

1331 

1332 
drop n [] = [] 

1333 
drop n (x#xs) = (case n of 0 => x#xs  Suc(m) => drop m xs) 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1334 

2926  1335 
takeWhile P [] = [] 
1336 
takeWhile P (x#xs) = (if P x then x#takeWhile P xs else []) 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1337 

2926  1338 
dropWhile P [] = [] 
1339 
dropWhile P (x#xs) = (if P x then dropWhile P xs else xs) 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1340 
\end{ttbox} 
2926  1341 
\caption{Recursions equations for list processing functions} 
1342 
\label{fig:HOL:listsimps} 

1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1343 
\end{figure} 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1344 
\index{nat@{\textit{nat}} type)} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1345 

dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1346 

3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1347 
\subsection{The type constructor for lists, \textit{list}} 
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1348 
\index{list@{\textit{list}} type(} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1349 

1422
bc628f4ef0cb
New version of type sections and many small changes.
nipkow
parents:
1389
diff
changeset

1350 
Figure~\ref{hollist} presents the theory \thydx{List}: the basic list 
3489
afa802078173
Added documentation for recdef, and tidied some other material
paulson
parents:
3487
diff
changeset

1351 
operations with their types and syntax. Type $\alpha \; list$ is 