author  clasohm 
Thu, 29 Jun 1995 12:28:27 +0200  
changeset 1163  c080ff36d24e 
parent 1162  7be0684950a3 
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 

8 
Church's original paper~\cite{church40}. Andrews's book~\cite{andrews86} is a 

9 
full description of higherorder logic. Experience with the {\sc hol} system 

10 
has demonstrated that higherorder logic is useful for hardware verification; 

11 
beyond this, it is widely applicable in many areas of mathematics. It is 

12 
weaker than {\ZF} set theory but for most applications this does not matter. 

13 
If you prefer {\ML} to Lisp, you will probably prefer \HOL\ to~{\ZF}. 

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

14 

1162  15 
The syntax of Isabelle's \HOL\ has recently been changed to look more like the 
16 
traditional syntax of higherorder logic. Function application is now 

17 
curried. To apply the function~$f$ to the arguments~$a$ and~$b$ in \HOL, you 

18 
must write $f\,a\,b$. Note that $f(a,b)$ means ``$f$ applied to the pair 

19 
$(a,b)$'' in \HOL. We write ordered pairs as $(a,b)$, not $\langle 

20 
a,b\rangle$ as in {\ZF} and earlier versions of \HOL. Early releases of 

21 
Isabelle included still another version of~\HOL, with explicit type inference 

22 
rules~\cite{paulsonCOLOG}. This version no longer exists, but \thydx{ZF} 

23 
supports a similar style of reasoning. 

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

24 

1162  25 
\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

26 
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

27 
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

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

29 
and application. There is no `apply' operator: function applications are 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

30 
written as simply~$f~a$ rather than $f{\tt`}a$. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

31 

1162  32 
These identifications allow Isabelle to support \HOL\ particularly nicely, 
33 
but they also mean that \HOL\ requires more sophistication from the user 

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

34 
 in particular, an understanding of Isabelle's type system. Beginners 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

35 
should work with {\tt show_types} set to {\tt true}. Gain experience by 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

36 
working in firstorder logic before attempting to use higherorder logic. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

37 
This chapter assumes familiarity with~{\FOL{}}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

38 

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

39 

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

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

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

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

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

44 
\cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

45 
\cdx{not} & $bool\To bool$ & negation ($\neg$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

47 
\cdx{False} & $bool$ & absurdity ($\bot$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

48 
\cdx{If} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

49 
\cdx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

50 
\cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

54 

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

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

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

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

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

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

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

61 
\tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha::term$ & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

62 
Hilbert description ($\epsilon$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

63 
{\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha::term\To bool)\To bool$ & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

64 
universal quantifier ($\forall$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

66 
existential quantifier ($\exists$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

67 
{\tt?!} or {\tt EX!} & \cdx{Ex1} & $(\alpha::term\To bool)\To bool$ & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

68 
unique existence ($\exists!$) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

72 

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

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

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

75 
\index{&@{\tt\&} symbol} 
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{*"""> symbol} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

79 
\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

80 
\sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

81 
Right 50 & composition ($\circ$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

82 
\tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

83 
\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

84 
\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

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

86 
\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

87 
\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

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

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

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

91 
\subcaption{Infixes} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

92 
\caption{Syntax of {\tt 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$} \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

102 
&  & "\at~" id~id^* " . " formula \\ 
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 
&  & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

106 
\multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\[2ex] 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

110 
&  & term " < " 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 
&  & "\ttilde\ " formula \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

113 
&  & formula " \& " 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 
&  & "!~~~" id~id^* " . " formula 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

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

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

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

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

124 
\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

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

126 

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 
\section{Syntax} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

129 
The type class of higherorder terms is called~\cldx{term}. Type variables 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

130 
range over this class by default. The equality symbol and quantifiers are 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

131 
polymorphic over class {\tt term}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

132 

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

133 
Class \cldx{ord} consists of all ordered types; the relations $<$ and 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

134 
$\leq$ are polymorphic over this class, as are the functions 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

135 
\cdx{mono}, \cdx{min} and \cdx{max}. Three other 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

136 
type classes  \cldx{plus}, \cldx{minus} and \cldx{times}  permit 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

137 
overloading of the operators {\tt+}, {\tt} and {\tt*}. In particular, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

138 
{\tt} is overloaded for set difference and subtraction. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

142 

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

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

144 
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

145 
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

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

147 

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

148 
\begin{warn} 
1162  149 
\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

150 
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

151 
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

152 
$\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

153 
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

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

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

156 

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

157 
\subsection{Types}\label{holtypes} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

158 
The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

159 
formulae are terms. The builtin type~\tydx{fun}, which constructs function 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

160 
types, is overloaded with arity {\tt(term,term)term}. Thus, $\sigma\To\tau$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

161 
belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

163 

1162  164 
Types in \HOL\ must be nonempty; otherwise the quantifier rules would be 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

165 
unsound. I have commented on this elsewhere~\cite[\S7]{paulsonCOLOG}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

166 

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

167 
\index{type definitions} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

168 
Gordon's {\sc hol} system supports {\bf type definitions}. A type is 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

169 
defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

170 
bool$, and a theorem of the form $\exists x::\sigma.P~x$. Thus~$P$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

171 
specifies a nonempty subset of~$\sigma$, and the new type denotes this 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

172 
subset. New function constants are generated to establish an isomorphism 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

173 
between the new type and the subset. If type~$\sigma$ involves type 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

174 
variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

175 
a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

176 
type. Melham~\cite{melham89} discusses type definitions at length, with 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

178 

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

179 
Isabelle does not support type definitions at present. Instead, they are 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

180 
mimicked by explicit definitions of isomorphism functions. The definitions 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

181 
should be supported by theorems of the form $\exists x::\sigma.P~x$, but 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

182 
Isabelle cannot enforce this. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

183 

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

184 

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

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

186 
Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$ 
1162  187 
satisfying~$P[a]$, if such exists. Since all terms in \HOL\ denote 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

188 
something, a description is always meaningful, but we do not know its value 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

189 
unless $P[x]$ defines it uniquely. We may write descriptions as 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

190 
\cdx{Eps}($P$) or use the syntax 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

191 
\hbox{\tt \at $x$.$P[x]$}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

192 

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

193 
Existential quantification is defined by 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

194 
\[ \exists x.P~x \;\equiv\; P(\epsilon x.P~x). \] 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

195 
The unique existence quantifier, $\exists!x.P[x]$, is defined in terms 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

196 
of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

197 
quantifications. For instance, $\exists!x y.P~x~y$ abbreviates 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

198 
$\exists!x. \exists!y.P~x~y$; note that this does not mean that there 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

199 
exists a unique pair $(x,y)$ satisfying~$P~x~y$. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

200 

1162  201 
\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} 
202 
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

203 
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

204 
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

205 
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

206 
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

207 
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

208 
\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

209 
true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

211 

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

212 
All these binders have priority 10. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

213 

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

214 

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

215 
\subsection{The \sdx{let} and \sdx{case} constructions} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

217 
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

218 
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

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

220 

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

222 
\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"" \dots ""~c@n~"=>"~e@n\] 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

223 
as a uniform means of expressing {\tt case} constructs. Therefore {\tt 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

224 
case} and \sdx{of} are reserved words. However, so far this is mere 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

225 
syntax and has no logical meaning. By declaring translations, you can 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

226 
cause instances of the {\tt case} construct to denote applications of 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

227 
particular case operators. The patterns supplied for $c@1$,~\ldots,~$c@n$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

228 
distinguish among the different case operators. For an example, see the 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

229 
case construct for lists on page~\pageref{hollist} below. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

230 

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

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

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

233 
\tdx{refl} t = (t::'a) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

234 
\tdx{subst} [ s=t; P s ] ==> P(t::'a) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

235 
\tdx{ext} (!!x::'a. (f x::'b) = g x) ==> (\%x.f x) = (\%x.g x) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

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

240 
\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

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

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

243 
\end{figure} 
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 

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

246 
\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

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

248 
\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

249 
\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

250 
\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

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

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

253 
\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

254 
\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

255 
\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

256 

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

257 
\tdx{Inv_def} Inv == (\%(f::'a=>'b) y. @x. f x=y) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

258 
\tdx{o_def} op o == (\%(f::'b=>'c) g (x::'a). f(g x)) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

259 
\tdx{if_def} If P x y == (\%P x y.@z::'a.(P=True > z=x) & (P=False > z=y)) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

260 
\tdx{Let_def} Let s f == f s 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

264 

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

265 

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

266 
\section{Rules of inference} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

267 
Figure~\ref{holrules} shows the inference rules of~\HOL{}, with 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

268 
their~{\ML} names. Some of the rules deserve additional comments: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

270 
\item[\tdx{ext}] expresses extensionality of functions. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

271 
\item[\tdx{iff}] asserts that logically equivalent formulae are 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

273 
\item[\tdx{selectI}] gives the defining property of the Hilbert 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

274 
$\epsilon$operator. It is a form of the Axiom of Choice. The derived rule 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

275 
\tdx{select_equality} (see below) is often easier to use. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

276 
\item[\tdx{True_or_False}] makes the logic classical.\footnote{In 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

277 
fact, the $\epsilon$operator already makes the logic classical, as 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

278 
shown by Diaconescu; see Paulson~\cite{paulsonCOLOG} for details.} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

280 

1162  281 
\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

282 
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

283 
(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

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

285 
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

286 
higherorder logic may equate formulae and even functions over formulae. 
1162  287 
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

288 
metaequality~({\tt==}) for definitions. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

289 

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

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

291 
mentions the type variable~{\tt'a}. This allows you to instantiate 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

292 
type variables explicitly by calling {\tt res_inst_tac}. By default, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

293 
explicit type variables have class \cldx{term}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

294 

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

295 
Include type constraints whenever you state a polymorphic goal. Type 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

296 
inference may otherwise make the goal more polymorphic than you intended, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

297 
with confusing results. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

298 

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

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

300 
If resolution fails for no obvious reason, try setting 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

301 
\ttindex{show_types} to {\tt true}, causing Isabelle to display types of 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

302 
terms. Possibly set \ttindex{show_sorts} to {\tt true} as well, causing 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

303 
Isabelle to display sorts. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

304 

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

305 
\index{unification!incompleteness of} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

306 
Where function types are involved, Isabelle's unification code does not 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

307 
guarantee to find instantiations for type variables automatically. Be 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

308 
prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac}, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

309 
possibly instantiating type variables. Setting 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

310 
\ttindex{Unify.trace_types} to {\tt true} causes Isabelle to report 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

311 
omitted search paths during unification.\index{tracing!of unification} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

313 

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

314 

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

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

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

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

318 
\tdx{trans} [ r=s; s=t ] ==> r=t 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

319 
\tdx{ssubst} [ t=s; P s ] ==> P(t::'a) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

320 
\tdx{box_equals} [ a=b; a=c; b=d ] ==> c=d 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

321 
\tdx{arg_cong} x=y ==> f x=f y 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

322 
\tdx{fun_cong} f=g ==> f x=g x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

324 

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

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

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

327 

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

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

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

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

331 
\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

332 

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

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

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

335 
\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

336 

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

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

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

339 
\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

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

341 

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

342 
\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

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

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

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

346 

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

347 
\tdx{eqTrueI} P ==> P=True 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

348 
\tdx{eqTrueE} P=True ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

350 

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

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

352 
\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

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

354 

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 
\begin{figure} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

358 
\tdx{allI} (!!x::'a. P x) ==> !x. P x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

359 
\tdx{spec} !x::'a.P x ==> P x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

360 
\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

361 
\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

362 

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

363 
\tdx{exI} P x ==> ? x::'a.P x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

365 

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

366 
\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

367 
\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

368 
] ==> R 
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{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

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

372 

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

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

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

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

376 

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

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

378 
\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

379 
\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

380 
\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

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

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

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

384 

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

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

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

387 
\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

388 
\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

389 
\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

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

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

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

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

394 

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

395 

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

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

397 
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

398 
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

399 
conjunctions, implications, and universal quantifiers. 
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 
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

402 
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

403 
simplifying both sides of an equation. 
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 

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

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

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

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

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

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

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

412 
\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

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

414 
\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

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

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

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

418 
\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

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

420 
\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

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

422 
\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

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

424 
\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

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

426 
\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

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

428 
\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

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

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

431 
& bounded quantifiers \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

434 
\cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

435 
& injective/surjective \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

437 
& injective over subset 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

441 

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

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

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

444 
\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

445 
\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

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

447 
\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

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

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

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

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

452 

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

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

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

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

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

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

458 
\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

459 
\tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

462 
& Left 70 & intersection ($\inter$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

464 
& Left 65 & union ($\union$) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

468 
& Left 50 & subset ($\subseteq$) 
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{Infixes} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

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

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

474 

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

475 

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

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

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

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

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

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

481 
$a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm nonmembership\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

482 
\{$a@1$, $\ldots$\} & insert $a@1$ $\ldots$ \{\} & \rm finite set \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

483 
\{$x$.$P[x]$\} & Collect($\lambda x.P[x]$) & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

485 
\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

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

487 
\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

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

489 
\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

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

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

492 
\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

493 
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

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

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

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

497 

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

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

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

500 
term & = & \hbox{other terms\ldots} \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

502 
&  & "\{ " term\; ("," term)^* " \}" \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

503 
&  & "\{ " id " . " formula " \}" \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

521 
\subcaption{Full Grammar} 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

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

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

524 

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

525 

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

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

527 
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

528 
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

529 
{\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

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

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

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

533 
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

534 
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

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

536 
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

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

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

539 
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

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

541 
\end{itemize} 
1162  542 
Finite unions and intersections have the same behaviour in \HOL\ as they 
543 
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

544 
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

545 

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

546 

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

547 
\subsection{Syntax of set theory}\index{*set type} 
1162  548 
\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

549 
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

550 
clarity and to avoid complications involving function types in unification. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

551 
Since Isabelle does not support type definitions (as mentioned in 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

552 
\S\ref{holtypes}), the isomorphisms between the two types are declared 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

553 
explicitly. Here they are natural: {\tt Collect} maps $\alpha\To bool$ to 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

554 
$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

555 
argument order). 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

556 

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

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

558 
translations. Figure~\ref{holsetsyntax2} presents the grammar of the new 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

559 
constructs. Infix operators include union and intersection ($A\union B$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

560 
and $A\inter B$), the subset and membership relations, and the image 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

561 
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

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

563 

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

564 
The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

565 
obvious manner using~{\tt insert} and~$\{\}$: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

567 
\{a@1, \ldots, a@n\} & \equiv & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

568 
{\tt insert}~a@1~({\tt insert}\ldots({\tt insert}~a@n~\{\})\ldots) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

570 

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

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

572 
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

573 
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

574 
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

575 
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

576 

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

577 
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

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

579 
\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

580 
\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

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

582 
The constants~\cdx{Ball} and~\cdx{Bex} are defined 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

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

587 
\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

588 
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

589 
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

590 
\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

591 

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

592 
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

593 
$\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

594 
\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

595 
\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

596 

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

597 
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

598 
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

599 
\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

600 
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

601 

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

602 
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

603 
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

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

605 

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

606 

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

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

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

609 
\tdx{mem_Collect_eq} (a : \{x.P x\}) = P a 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

610 
\tdx{Collect_mem_eq} \{x.x:A\} = A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

611 

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

612 
\tdx{empty_def} \{\} == \{x.False\} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

613 
\tdx{insert_def} insert a B == \{x.x=a\} Un B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

614 
\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

615 
\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

616 
\tdx{subset_def} A <= B == ! x:A. x:B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

618 
\tdx{Int_def} A Int B == \{x.x:A & x:B\} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

619 
\tdx{set_diff_def} A  B == \{x.x:A & x~:B\} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

620 
\tdx{Compl_def} Compl A == \{x. ~ x:A\} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

621 
\tdx{INTER_def} INTER A B == \{y. ! x:A. y: B x\} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

622 
\tdx{UNION_def} UNION A B == \{y. ? x:A. y: B x\} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

623 
\tdx{INTER1_def} INTER1 B == INTER \{x.True\} B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

624 
\tdx{UNION1_def} UNION1 B == UNION \{x.True\} B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

625 
\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

626 
\tdx{Union_def} Union S == (UN x:S. x) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

628 
\tdx{image_def} f``A == \{y. ? x:A. y=f x\} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

629 
\tdx{range_def} range f == \{y. ? x. y=f x\} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

630 
\tdx{mono_def} mono f == !A B. A <= B > f A <= f B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

631 
\tdx{inj_def} inj f == ! x y. f x=f y > x=y 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

632 
\tdx{surj_def} surj f == ! y. ? x. y=f x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

633 
\tdx{inj_onto_def} inj_onto f A == !x:A. !y:A. f x=f y > x=y 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

637 

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

638 

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

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

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

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

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

643 
\tdx{CollectE} [ a : \{x.P x\}; P a ==> W ] ==> W 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

644 

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

645 
\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

646 
\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

647 
\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

648 

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

649 
\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

650 
\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

651 
\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

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

653 

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

654 
\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

655 
\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

656 
\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

657 

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

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

659 
\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

660 

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

661 
\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

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

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

664 
\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

665 

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

666 
\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

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

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

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

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

671 
\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

672 
\end{figure} 
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 

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

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

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

677 
\tdx{emptyE} a : \{\} ==> P 
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{insertI1} a : insert a B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

680 
\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

681 
\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

682 

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

683 
\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

684 
\tdx{ComplD} [ c : Compl A ] ==> ~ c:A 
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{UnI1} c:A ==> c : A Un B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

687 
\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

688 
\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

689 
\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

690 

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

691 
\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

692 
\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

693 
\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

694 
\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

695 

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

696 
\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

697 
\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

698 

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

699 
\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

700 
\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

701 
\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

702 

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

703 
\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

704 
\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

705 

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

706 
\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

707 
\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

708 
\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

709 

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

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

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

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

713 
\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

714 
\end{figure} 
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 

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

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

718 
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

719 
axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

721 
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

722 

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

723 
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

724 
quantifiers, unions, intersections, complements and the subset relation. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

725 
They also include straightforward properties of functions: image~({\tt``}) and 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

726 
{\tt range}, and predicates concerning monotonicity, injectiveness and 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

728 

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

729 
The predicate \cdx{inj_onto} is used for simulating type definitions. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

730 
The statement ${\tt inj_onto}~f~A$ asserts that $f$ is injective on the 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

731 
set~$A$, which specifies a subset of its domain type. In a type 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

732 
definition, $f$ is the abstraction function and $A$ is the set of valid 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

733 
representations; we should not expect $f$ to be injective outside of~$A$. 
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 
\begin{figure} \underscoreon 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

737 
\tdx{Inv_f_f} inj f ==> Inv f (f x) = x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

738 
\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

739 

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

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

741 
% [ 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

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

743 
\tdx{imageI} [ x:A ] ==> f x : f``A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

744 
\tdx{imageE} [ b : f``A; !!x.[ b=f x; x:A ] ==> P ] ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

745 

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

746 
\tdx{rangeI} f x : range f 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

747 
\tdx{rangeE} [ b : range f; !!x.[ b=f x ] ==> P ] ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

748 

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

749 
\tdx{monoI} [ !!A B. A <= B ==> f A <= f B ] ==> mono f 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

751 

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

752 
\tdx{injI} [ !! x y. f x = f y ==> x=y ] ==> inj f 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

753 
\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

754 
\tdx{injD} [ inj f; f x = f y ] ==> x=y 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

755 

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

756 
\tdx{inj_ontoI} (!!x y. [ f x=f y; x:A; y:A ] ==> x=y) ==> inj_onto f A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

757 
\tdx{inj_ontoD} [ inj_onto f A; f x=f y; x:A; y:A ] ==> x=y 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

758 

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

759 
\tdx{inj_onto_inverseI} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

760 
(!!x. x:A ==> g(f x) = x) ==> inj_onto f A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

761 
\tdx{inj_onto_contraD} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

762 
[ inj_onto f A; x~=y; x:A; y:A ] ==> ~ f x=f y 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

766 

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

767 

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

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

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

770 
\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

771 
\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

772 

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

773 
\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

774 
\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

775 

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

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

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

778 
\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

779 

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

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

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

782 
\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

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

784 
\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

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

786 

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

787 

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

788 
\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

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

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

791 
\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

792 
\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

793 
\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

794 

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

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

796 
\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

797 
\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

798 
\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

799 

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

800 
\tdx{Compl_disjoint} A Int (Compl A) = \{x.False\} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

801 
\tdx{Compl_partition} A Un (Compl A) = \{x.True\} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

803 
\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

804 
\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

805 

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

806 
\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

807 
\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

808 
\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

809 

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

810 
\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

811 
\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

812 
\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

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

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

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

816 

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

817 

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

818 
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

819 
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

820 
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

821 
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

822 
\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

823 
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

824 
\tdx{equalityCE} supports classical reasoning about extensionality, 
1162  825 
after the fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

827 

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

828 
Figure~\ref{holfun} presents derived inference rules involving functions. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

829 
They also include rules for \cdx{Inv}, which is defined in theory~{\tt 
1162  830 
HOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

831 
inverse of~$f$. They also include natural deduction rules for the image 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

832 
and range operators, and for the predicates {\tt inj} and {\tt inj_onto}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

833 
Reasoning about function composition (the operator~\sdx{o}) and the 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

834 
predicate~\cdx{surj} is done simply by expanding the definitions. See 
1162  835 
the file {\tt HOL/fun.ML} for a complete listing of the derived rules. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

836 

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

837 
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

838 
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

839 
bounds. Reasoning directly about subsets often yields clearer proofs than 
1162  840 
reasoning about the membership relation. See the file {\tt HOL/subset.ML}. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

841 

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

842 
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

843 
include commutative, associative and distributive laws involving unions, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

844 
intersections and complements. The proofs are mostly trivial, using the 
1162  845 
classical reasoner; see file {\tt HOL/equalities.ML}. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

846 

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

847 

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

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

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

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

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

852 
& & ordered pairs $(a,b)$ \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

853 
\cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

854 
\cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

855 
\cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

856 
& & generalized projection\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

857 
\cdx{Sigma} & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

858 
$[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

859 
& general sum of sets 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

862 
\tdx{fst_def} fst p == @a. ? b. p = (a,b) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

863 
\tdx{snd_def} snd p == @b. ? a. p = (a,b) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

864 
\tdx{split_def} split c p == c (fst p) (snd p) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

865 
\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. \{(x,y)\} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

866 

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

867 

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

868 
\tdx{Pair_inject} [ (a, b) = (a',b'); [ a=a'; b=b' ] ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

869 
\tdx{fst_conv} fst (a,b) = a 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

870 
\tdx{snd_conv} snd (a,b) = b 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

871 
\tdx{split} split c (a,b) = c a b 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

872 

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

873 
\tdx{surjective_pairing} p = (fst p,snd p) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

874 

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

875 
\tdx{SigmaI} [ a:A; b:B a ] ==> (a,b) : Sigma A B 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

876 

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

877 
\tdx{SigmaE} [ c: Sigma A B; 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

878 
!!x y.[ x:A; y:B x; c=(x,y) ] ==> P ] ==> P 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

880 
\caption{Type $\alpha\times\beta$}\label{holprod} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

882 

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

883 

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

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

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

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

887 
\cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

888 
\cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

889 
\cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

893 
\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl x > z=f x) & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

894 
(!y. p=Inr y > z=g y)) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

895 

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

896 
\tdx{Inl_not_Inr} ~ Inl a=Inr b 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

897 

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

898 
\tdx{inj_Inl} inj Inl 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

899 
\tdx{inj_Inr} inj Inr 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

900 

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

901 
\tdx{sumE} [ !!x::'a. P(Inl x); !!y::'b. P(Inr y) ] ==> P s 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

902 

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

903 
\tdx{sum_case_Inl} sum_case f g (Inl x) = f x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

904 
\tdx{sum_case_Inr} sum_case f g (Inr x) = g x 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

905 

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

906 
\tdx{surjective_sum} sum_case (\%x::'a. f(Inl x)) (\%y::'b. f(Inr y)) s = f s 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

908 
\caption{Type $\alpha+\beta$}\label{holsum} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

910 

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

911 

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

912 
\section{Generic packages and classical reasoning} 
1162  913 
\HOL\ instantiates most of Isabelle's generic packages; 
914 
see {\tt HOL/ROOT.ML} for details. 

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

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

916 
\item 
1162  917 
Because it includes a general substitution rule, \HOL\ instantiates the 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

918 
tactic {\tt hyp_subst_tac}, which substitutes for an equality 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

919 
throughout a subgoal and its hypotheses. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

921 
It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

922 
simplification set for higherorder logic. Equality~($=$), which also 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

923 
expresses logical equivalence, may be used for rewriting. See the file 
1162  924 
{\tt HOL/simpdata.ML} for a complete listing of the simplification 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

927 
It instantiates the classical reasoner, as described below. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

928 
\end{itemize} 
1162  929 
\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

930 
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

931 
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

932 

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

933 
The classical reasoner is set up as the structure 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

934 
{\tt Classical}. This structure is open, so {\ML} identifiers such 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

935 
as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

936 
\HOL\ defines the following classical rule sets: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

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

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

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

943 
\item[\ttindexbold{prop_cs}] contains the propositional rules, namely 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

944 
those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

945 
along with the rule~{\tt refl}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

946 

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

947 
\item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

948 
{\tt allI} and~{\tt exE} and the unsafe rules {\tt allE} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

949 
and~{\tt exI}, as well as rules for unique existence. Search using 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

950 
this classical set is incomplete: quantified formulae are used at most 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

952 

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

953 
\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

954 
quantifiers, subsets, comprehensions, unions and intersections, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

955 
complements, finite sets, images and ranges. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

958 
See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

959 
{Chap.\ts\ref{chap:classical}} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

960 
for more discussion of classical proof methods. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

961 

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

962 

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

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

964 
The basic higherorder logic is augmented with a tremendous amount of 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

965 
material, including support for recursive function and type definitions. A 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

966 
detailed discussion appears elsewhere~\cite{paulsoncoind}. The simpler 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

967 
definitions are the same as those used by the {\sc hol} system, but my 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

968 
treatment of recursive types differs from Melham's~\cite{melham89}. The 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

969 
present section describes product, sum, natural number and list types. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

970 

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

971 
\subsection{Product and sum types}\index{*"* type}\index{*"+ type} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

972 
Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

973 
the ordered pair syntax {\tt($a$,$b$)}. Theory \thydx{Sum} defines the 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

974 
sum type $\alpha+\beta$. These use fairly standard constructions; see 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

975 
Figs.\ts\ref{holprod} and~\ref{holsum}. Because Isabelle does not 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

976 
support abstract type definitions, the isomorphisms between these types and 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

977 
their representations are made explicitly. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

978 

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

979 
Most of the definitions are suppressed, but observe that the projections 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

980 
and conditionals are defined as descriptions. Their properties are easily 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

981 
proved using \tdx{select_equality}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

982 

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

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

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

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

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

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

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

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

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

991 
\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

992 
\cdx{0} & $nat$ & & zero \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

993 
\cdx{Suc} & $nat \To nat$ & & successor function\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

997 
& & primitive recursor\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

998 
\cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

999 
\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

1000 
\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

1001 
\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

1002 
\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

1003 
\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

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

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

1006 

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

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

1008 
\tdx{nat_case_def} nat_case == (\%a f n. @z. (n=0 > z=a) & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1009 
(!x. n=Suc x > z=f x)) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1010 
\tdx{pred_nat_def} pred_nat == \{p. ? n. p = (n, Suc n)\} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1011 
\tdx{less_def} m<n == (m,n):pred_nat^+ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1012 
\tdx{nat_rec_def} nat_rec n c d == 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1013 
wfrec pred_nat n (nat_case (\%g.c) (\%m g. d m (g m))) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1014 

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

1015 
\tdx{add_def} m+n == nat_rec m n (\%u v. Suc v) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1016 
\tdx{diff_def} mn == nat_rec n m (\%u v. nat_rec v 0 (\%x y.x)) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1017 
\tdx{mult_def} m*n == nat_rec m 0 (\%u v. n + v) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1018 
\tdx{mod_def} m mod n == wfrec (trancl pred_nat) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1019 
m (\%j f. if j<n then j else f jn)) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1020 
\tdx{quo_def} m div n == wfrec (trancl pred_nat), 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1021 
m (\%j f. if j<n then 0 else Suc(f jn)) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1024 
\caption{Defining {\tt nat}, the type of natural numbers} \label{holnat1} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1026 

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

1027 

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

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

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

1030 
\tdx{nat_induct} [ P 0; !!k. [ P k ] ==> P(Suc k) ] ==> P n 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1031 

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

1032 
\tdx{Suc_not_Zero} Suc m ~= 0 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1033 
\tdx{inj_Suc} inj Suc 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1034 
\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

1035 
\subcaption{Basic properties} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1036 

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

1037 
\tdx{pred_natI} (n, Suc n) : pred_nat 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1038 
\tdx{pred_natE} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1039 
[ p : pred_nat; !!x n. [ p = (n, Suc n) ] ==> R ] ==> R 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1040 

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

1041 
\tdx{nat_case_0} nat_case a f 0 = a 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1042 
\tdx{nat_case_Suc} nat_case a f (Suc k) = f k 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1043 

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

1044 
\tdx{wf_pred_nat} wf pred_nat 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1045 
\tdx{nat_rec_0} nat_rec 0 c h = c 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1046 
\tdx{nat_rec_Suc} nat_rec (Suc n) c h = h n (nat_rec n c h) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1047 
\subcaption{Case analysis and primitive recursion} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1048 

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

1049 
\tdx{less_trans} [ i<j; j<k ] ==> i<k 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1050 
\tdx{lessI} n < Suc n 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1051 
\tdx{zero_less_Suc} 0 < Suc n 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1052 

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

1053 
\tdx{less_not_sym} n<m > ~ m<n 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1054 
\tdx{less_not_refl} ~ n<n 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1055 
\tdx{not_less0} ~ n<0 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1056 

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

1057 
\tdx{Suc_less_eq} (Suc m < Suc n) = (m<n) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1058 
\tdx{less_induct} [ !!n. [ ! m. m<n > P m ] ==> P n ] ==> P n 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1059 

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

1060 
\tdx{less_linear} m<n  m=n  n<m 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1061 
\subcaption{The lessthan relation} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

1065 

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

1066 

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

1067 
\subsection{The type of natural numbers, {\tt nat}} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1068 
The theory \thydx{Nat} defines the natural numbers in a roundabout but 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1069 
traditional way. The axiom of infinity postulates an type~\tydx{ind} of 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1070 
individuals, which is nonempty and closed under an injective operation. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1071 
The natural numbers are inductively generated by choosing an arbitrary 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1072 
individual for~0 and using the injective operation to take successors. As 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1073 
usual, the isomorphisms between~\tydx{nat} and its representation are made 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1075 

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

1076 
The definition makes use of a least fixed point operator \cdx{lfp}, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1077 
defined using the KnasterTarski theorem. This is used to define the 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1078 
operator \cdx{trancl}, for taking the transitive closure of a relation. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1079 
Primitive recursion makes use of \cdx{wfrec}, an operator for recursion 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1080 
along arbitrary wellfounded relations. The corresponding theories are 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1081 
called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@. Elsewhere I have described 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1082 
similar constructions in the context of set theory~\cite{paulsonsetII}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1083 

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

1084 
Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1085 
overloads $<$ and $\leq$ on the natural numbers. As of this writing, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1086 
Isabelle provides no means of verifying that such overloading is sensible; 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1087 
there is no means of specifying the operators' properties and verifying 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1088 
that instances of the operators satisfy those properties. To be safe, the 
1162  1089 
\HOL\ theory includes no polymorphic axioms asserting general properties of 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1090 
$<$ and~$\leq$. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1091 

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

1092 
Theory \thydx{Arith} develops arithmetic on the natural numbers. It 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1093 
defines addition, multiplication, subtraction, division, and remainder. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1094 
Many of their properties are proved: commutative, associative and 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1095 
distributive laws, identity and cancellation laws, etc. The most 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1096 
interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1097 
Division and remainder are defined by repeated subtraction, which requires 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

1098 
wellfounded rather than primitive recursion. See Figs.\ts\ref{holnat1} 
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

1099 
and~\ref{holnat2}. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1100 

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

1101 
The predecessor relation, \cdx{pred_nat}, is shown to be wellfounded. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1102 
Recursion along this relation resembles primitive recursion, but is 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1103 
stronger because we are in higherorder logic; using primitive recursion to 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1104 
define a higherorder function, we can easily Ackermann's function, which 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1105 
is not primitive recursive \cite[page~104]{thompson91}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1106 
The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1107 
natural numbers are most easily expressed using recursion along~$<$. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1108 

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

1109 
The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1110 
variable~$n$ in subgoal~$i$. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1111 

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

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

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

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

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

1116 
\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

1117 
\cdx{Nil} & $\alpha list$ & & empty list\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1118 
\tt \# & $[\alpha,\alpha list]\To \alpha list$ & Right 65 & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1119 
list constructor \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1120 
\cdx{null} & $\alpha list \To bool$ & & emptiness test\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1121 
\cdx{hd} & $\alpha list \To \alpha$ & & head \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1122 
\cdx{tl} & $\alpha list \To \alpha list$ & & tail \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1123 
\cdx{ttl} & $\alpha list \To \alpha list$ & & total tail \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1124 
\tt\at & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1125 
\sdx{mem} & $[\alpha,\alpha list]\To bool$ & Left 55 & membership\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1126 
\cdx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1127 
& & mapping functional\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1128 
\cdx{filter} & $(\alpha \To bool) \To (\alpha list \To \alpha list)$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1129 
& & filter functional\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1130 
\cdx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1131 
& & forall functional\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1132 
\cdx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1133 
\beta]\To\beta] \To \beta$ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1136 
\subcaption{Constants and infixes} 
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 
\begin{center} \tt\frenchspacing 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1141 
\sdx{[]} & Nil & \rm empty list \\{} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1142 
[$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

1143 
\rm finite list \\{} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1144 
[$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

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

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

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

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

1149 

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

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

1151 
\tdx{list_induct} [ P []; !!x xs. [ P xs ] ==> P x#xs) ] ==> P l 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1152 

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

1153 
\tdx{Cons_not_Nil} (x # xs) ~= [] 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1154 
\tdx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1155 
\subcaption{Induction and freeness} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1157 
\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

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

1159 

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

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

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

1162 
\tdx{list_rec_Nil} list_rec [] c h = c 
1162  1163 
\tdx{list_rec_Cons} list_rec (a#l) c h = h a l (list_rec l c h) 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1164 

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

1165 
\tdx{list_case_Nil} list_case c h [] = c 
1162  1166 
\tdx{list_case_Cons} list_case c h (x#xs) = h x xs 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1167 

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

1168 
\tdx{map_Nil} map f [] = [] 
1162  1169 
\tdx{map_Cons} map f (x#xs) = f x # map f xs 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1170 

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

1171 
\tdx{null_Nil} null [] = True 
1162  1172 
\tdx{null_Cons} null (x#xs) = False 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1173 

1162  1174 
\tdx{hd_Cons} hd (x#xs) = x 
1175 
\tdx{tl_Cons} tl (x#xs) = xs 

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

1176 

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

1177 
\tdx{ttl_Nil} ttl [] = [] 
1162  1178 
\tdx{ttl_Cons} ttl (x#xs) = xs 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1179 

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

1180 
\tdx{append_Nil} [] @ ys = ys 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1181 
\tdx{append_Cons} (x#xs) \at ys = x # xs \at ys 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1182 

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

1183 
\tdx{mem_Nil} x mem [] = False 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

1184 
\tdx{mem_Cons} 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

1185 

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

1186 
\tdx{filter_Nil} filter P [] = [] 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

1187 
\tdx{filter_Cons} 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

1188 

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

1189 
\tdx{list_all_Nil} list_all P [] = True 
1162  1190 
\tdx{list_all_Cons} list_all P (x#xs) = (P x & list_all P xs) 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1192 
\caption{Rewrite rules for lists} \label{hollistsimps} 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1194 

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

1195 

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

1196 
\subsection{The type constructor for lists, {\tt list}} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1197 
\index{*list type} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1198 

1162  1199 
\HOL's definition of lists is an example of an experimental method for 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

1200 
handling recursive data types. Figure~\ref{hollist} presents the theory 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1201 
\thydx{List}: the basic list operations with their types and properties. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1202 

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

1203 
The \sdx{case} construct is defined by the following translation: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1206 
\begin{array}{r@{\;}l@{}l} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1207 
"case " e " of" & "[]" & " => " a\\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1208 
"" & x"\#"xs & " => " b 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1211 
"list_case"~a~(\lambda x\;xs.b)~e 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1213 
The theory includes \cdx{list_rec}, a primitive recursion operator 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1214 
for lists. It is derived from wellfounded recursion, a general principle 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1215 
that can express arbitrary total recursive functions. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1216 

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

1217 
The simpset \ttindex{list_ss} contains, along with additional useful lemmas, 
1163
c080ff36d24e
changed 'chol' labels to 'hol'; added a few parentheses
clasohm
parents:
1162
diff
changeset

1218 
the basic rewrite rules that appear in Fig.\ts\ref{hollistsimps}. 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1219 

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

1220 
The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1221 
variable~$xs$ in subgoal~$i$. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1222 

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

1223 

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

1224 
\section{Datatype declarations} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1225 
\index{*datatype(} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1226 

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

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

1228 

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

1229 
It is often necessary to extend a theory with \MLlike datatypes. This 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1230 
extension consists of the new type, declarations of its constructors and 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1231 
rules that describe the new type. The theory definition section {\tt 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1232 
datatype} represents a compact way of doing this. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1233 

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

1234 

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

1235 
\subsection{Foundations} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1236 

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

1237 
A datatype declaration has the following general structure: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1238 
\[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1239 
C_1~\tau_{11}~\dots~\tau_{1k_1} ~\mid~ \dots ~\mid~ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1240 
C_m~\tau_{m1}~\dots~\tau_{mk_m} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1242 
where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1243 
$\tau_{ij}$ are one of the following: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1245 
\item type variables $\alpha_1,\dots,\alpha_n$, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1246 
\item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1247 
type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1248 
\{\alpha_1,\dots,\alpha_n\}$, 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1249 
\item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1250 
makes it a recursive type. To ensure that the new type is not empty at 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1251 
least one constructor must consist of only nonrecursive type 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1254 
If you would like one of the $\tau_{ij}$ to be a complex type expression 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1255 
$\tau$ you need to declare a new type synonym $syn = \tau$ first and use 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1256 
$syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1257 
recursive type itself, thus ruling out problematic cases like \[ \mbox{\tt 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1258 
datatype}~ t ~=~ C(t \To t) \] together with unproblematic ones like \[ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1259 
\mbox{\tt datatype}~ t ~=~ C(t~list). \] 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1260 

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

1261 
The constructors are automatically defined as functions of their respective 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1263 
\[ C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \] 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1264 
These functions have certain {\em freeness} properties: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1266 
\item[\tt distinct] They are distinct: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1267 
\[ C_i~x_1~\dots~x_{k_i} \neq C_j~y_1~\dots~y_{k_j} \qquad 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1268 
\mbox{for all}~ i \neq j. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1270 
\item[\tt inject] They are injective: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1271 
\[ (C_j~x_1~\dots~x_{k_j} = C_j~y_1~\dots~y_{k_j}) = 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1272 
(x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j}) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1275 
Because the number of inequalities is quadratic in the number of 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1276 
constructors, a different method is used if their number exceeds 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1277 
a certain value, currently 4. In that case every constructor is mapped to a 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

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

1281 
\mbox{\it t\_ord}(C_1~x_1~\dots~x_{k_1}) & = & 0 \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1283 
\mbox{\it t\_ord}(C_m x_1~\dots~x_{k_m}) & = & m1 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1286 
and distinctness of constructors is expressed by: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1288 
\mbox{\it t\_ord}~x \neq \mbox{\it t\_ord}~y \Imp x \neq y. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1290 
In addition a structural induction axiom {\tt induct} is provided: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1292 
\infer{P x} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1294 
\Forall x_1\dots x_{k_1}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1295 
\List{P~x_{r_{11}}; \dots; P~x_{r_{1l_1}}} & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1296 
\Imp & P(C_1~x_1~\dots~x_{k_1}) \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1298 
\Forall x_1\dots x_{k_m}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1299 
\List{P~x_{r_{m1}}; \dots; P~x_{r_{ml_m}}} & 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1300 
\Imp & P(C_m~x_1~\dots~x_{k_m}) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1303 
where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1304 
= (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1305 
all arguments of the recursive type. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1306 

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

1307 
The type also comes with an \MLlike \sdx{case}construct: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1310 
\mbox{\tt case}~e~\mbox{\tt of} & C_1~x_{11}~\dots~x_{1k_1} & \To & e_1 \\ 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1312 
\mid & C_m~x_{m1}~\dots~x_{mk_m} & \To & e_m 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1315 
In contrast to \ML, {\em all} constructors must be present, their order is 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1316 
fixed, and nested patterns are not supported. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1317 

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

1318 

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

1319 
\subsection{Defining datatypes} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1320 

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

1321 
A datatype is defined in a theory definition file using the keyword {\tt 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1322 
datatype}. The definition following {\tt datatype} must conform to the 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1323 
syntax of {\em typedecl} specified in Fig.~\ref{datatypegrammar} and must 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1324 
obey the rules in the previous section. As a result the theory is extended 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1325 
with the new type, the constructors, and the theorems listed in the previous 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1327 

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

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

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

1330 
typedecl : typevarlist id '=' (cons + '') 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1332 
cons : (id  string) ( ()  '(' (typ + ',') ')' ) ( ()  mixfix ) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1334 
typ : typevarlist id 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1337 
typevarlist : ()  tid  '(' (tid + ',') ')' 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1340 
\caption{Syntax of datatype declarations} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1341 
\label{datatypegrammar} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1343 

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

1344 
Reading the theory file produces a structure which, in addition to the usual 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1345 
components, contains a structure named $t$ for each datatype $t$ defined in 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1346 
the file.\footnote{Otherwise multiple datatypes in the same theory file would 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1347 
lead to name clashes.} Each structure $t$ contains the following elements: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1349 
val distinct : thm list 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1350 
val inject : thm list 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1351 
val induct : thm 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1352 
val cases : thm list 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1353 
val simps : thm list 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1354 
val induct_tac : string > int > tactic 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1356 
{\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1357 
above. For convenience {\tt distinct} contains inequalities in both 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1360 
If there are five or more constructors, the {\em t\_ord} scheme is used for 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1361 
{\tt distinct}. In this case the theory {\tt Arith} must be contained 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1362 
in the current theory, if necessary by including it explicitly. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1364 
The reduction rules of the {\tt case}construct are in {\tt cases}. All 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1365 
theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1366 
{\tt simps} for use with the simplifier. The tactic {\verb$induct_tac$~{\em 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1367 
var i}\/} applies structural induction over variable {\em var} to 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1368 
subgoal {\em i}. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1369 

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

1370 

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

1371 
\subsection{Examples} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1372 

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

1373 
\subsubsection{The datatype $\alpha~list$} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1374 

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

1375 
We want to define the type $\alpha~list$.\footnote{Of course there is a list 
1162  1376 
type in HOL already. This is only an example.} To do this we have to build 
1377 
a new theory that contains the type definition. We start from {\tt HOL}. 

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

1378 
\begin{ttbox} 
1162  1379 
MyList = HOL + 
1113
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1380 
datatype 'a list = Nil  Cons 'a ('a list) 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

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

1383 
After loading the theory (\verb$use_thy "MyList"$), we can prove 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1384 
$Cons~x~xs\neq xs$. First we build a suitable simpset for the simplifier: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1386 
val mylist_ss = HOL_ss addsimps MyList.list.simps; 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1387 
goal MyList.thy "!x. Cons x xs ~= xs"; 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1388 
{\out Level 0} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1389 
{\out ! x. Cons x xs ~= xs} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1390 
{\out 1. ! x. Cons x xs ~= xs} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1392 
This can be proved by the structural induction tactic: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1394 
by (MyList.list.induct_tac "xs" 1); 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1395 
{\out Level 1} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1396 
{\out ! x. Cons x xs ~= xs} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1397 
{\out 1. ! x. Cons x Nil ~= Nil} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1398 
{\out 2. !!a list.} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1399 
{\out ! x. Cons x list ~= list ==>} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1400 
{\out ! x. Cons x (Cons a list) ~= Cons a list} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1402 
The first subgoal can be proved with the simplifier and the distinctness 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1403 
axioms which are part of \verb$mylist_ss$. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1405 
by (simp_tac mylist_ss 1); 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1406 
{\out Level 2} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1407 
{\out ! x. Cons x xs ~= xs} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1408 
{\out 1. !!a list.} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1409 
{\out ! x. Cons x list ~= list ==>} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1410 
{\out ! x. Cons x (Cons a list) ~= Cons a list} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1412 
Using the freeness axioms we can quickly prove the remaining goal. 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1414 
by (asm_simp_tac mylist_ss 1); 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1415 
{\out Level 3} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1416 
{\out ! x. Cons x xs ~= xs} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1417 
{\out No subgoals!} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1419 
Because both subgoals were proved by almost the same tactic we could have 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1420 
done that in one step using 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1422 
by (ALLGOALS (asm_simp_tac mylist_ss)); 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

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

1424 

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

1425 

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

1426 
\subsubsection{The datatype $\alpha~list$ with mixfix syntax} 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1427 

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

1428 
In this example we define the type $\alpha~list$ again but this time we want 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1429 
to write {\tt []} instead of {\tt Nil} and we want to use the infix operator 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1430 
\verb# instead of {\tt Cons}. To do this we simply add mixfix annotations 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1431 
after the constructor declarations as follows: 
dd7284573601
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm
parents:
diff
changeset

1432 
\begin{ttbox} 
1162  1433 
MyList = HOL + 
1113 