1% appendix.tex %
2% Principal lemmas %
3
4% ----------------------------------------------------------------------------
5
6\section{Principal lemmas}
7\label{PrincipalLemmas}
8
9Binomial coefficients, \verb@CHOOSE@:
10\begin{session}
11\begin{verbatim}
12CHOOSE_LESS = |- !n k. n < k ==> (CHOOSE n k = 0)
13
14CHOOSE_SAME = |- !n. CHOOSE n n = 1
15\end{verbatim}
16\end{session}
17
18Algebraic laws:
19\begin{session}
20\begin{verbatim}
21RIGHT_CANCELLATION =
22|- !plus. Group plus ==> (!a b c. (plus b a = plus c a) ==> (b = c))
23
24RING_0 =
25|- !plus times.
26    RING(plus,times) ==>
27    (!a. times(Id plus)a = Id plus) /\ (!a. times a(Id plus) = Id plus)
28\end{verbatim}
29\end{session}
30
31\newpage
32Scalar powers:
33\begin{session}
34\begin{verbatim}
35POWER_1 = |- !plus. MONOID plus ==> (POWER plus 1 a = a)
36
37POWER_DISTRIB =
38|- !plus times.
39    RING(plus,times) ==>
40    (!a b n. times a(POWER plus n b) = POWER plus n(times a b))
41
42POWER_ADD =
43|- !plus.
44    MONOID plus ==>
45    (!m n a. POWER plus(m + n)a = plus(POWER plus m a)(POWER plus n a))
46\end{verbatim}
47\end{session}
48
49Reduction of lists:
50\begin{session}
51\begin{verbatim}
52REDUCE_APPEND =
53|- !plus.
54    MONOID plus ==>
55    (!as bs.
56      REDUCE plus(APPEND as bs) = plus(REDUCE plus as)(REDUCE plus bs))
57
58REDUCE_MAP_MULT =
59|- !plus times.
60    RING(plus,times) ==>
61    (!a bs. REDUCE plus(MAP(times a)bs) = times a(REDUCE plus bs))
62
63REDUCE_MAP =
64|- !plus.
65    MONOID plus /\ COMMUTATIVE plus ==>
66    (!f g as.
67      REDUCE plus(MAP(\k. plus(f k)(g k))as) =
68      plus(REDUCE plus(MAP f as))(REDUCE plus(MAP g as)))
69\end{verbatim}
70\end{session}
71
72Subranges of the natural numbers:
73\begin{session}
74\begin{verbatim}
75RANGE_TOP = |- !n m. RANGE m(SUC n) = APPEND(RANGE m n)[m + n]
76
77RANGE_SHIFT = |- !n m. RANGE(SUC m)n = MAP SUC(RANGE m n)
78\end{verbatim}
79\end{session}
80
81\newpage
82$\Sigma$-notation:
83\begin{session}
84\begin{verbatim}
85SIGMA_ID = |- !plus m f. SIGMA(plus,m,0)f = Id plus
86
87SIGMA_LEFT_SPLIT =
88|- !plus m n f. SIGMA(plus,m,SUC n)f = plus(f m)(SIGMA(plus,SUC m,n)f)
89
90SIGMA_RIGHT_SPLIT =
91|- !plus.
92    MONOID plus ==>
93    (!m n f. SIGMA(plus,m,SUC n)f = plus(SIGMA(plus,m,n)f)(f(m + n)))
94
95SIGMA_SHIFT =
96|- !plus m n f. SIGMA(plus,SUC m,n)f = SIGMA(plus,m,n)(f o SUC)
97
98SIGMA_MULT_COMM =
99|- !plus times.
100    RING(plus,times) ==>
101    (!m n a f.
102      times a(SIGMA(plus,m,n)f) = SIGMA(plus,m,n)((times a) o f))
103
104SIGMA_PLUS_COMM =
105|- !plus.
106    MONOID plus /\ COMMUTATIVE plus ==>
107    (!f g m n.
108      plus(SIGMA(plus,m,n)f)(SIGMA(plus,m,n)g) =
109      SIGMA(plus,m,n)(\k. plus(f k)(g k)))
110
111SIGMA_EXT =
112|- !plus.
113    MONOID plus ==>
114    (!f g m n.
115      (!k. k < n ==> (f(m + k) = g(m + k))) ==>
116      (SIGMA(plus,m,n)f = SIGMA(plus,m,n)g))
117\end{verbatim}
118\end{session}
119
120Terms from the Binomial Theorem:
121\begin{session}
122\begin{verbatim}
123BINTERM_0 =
124|- !plus times.
125    RING(plus,times) ==>
126    (!a b n. BINTERM plus times a b n 0 = POWER times n a)
127
128BINTERM_n =
129|- !plus times.
130    RING(plus,times) ==>
131    (!a b n. BINTERM plus times a b n n = POWER times n b)
132\end{verbatim}
133\end{session}
134