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