paulson@5545: (*  Title:      HOL/ex/BinEx.thy
paulson@5545:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@5545:     Copyright   1998  University of Cambridge
paulson@5545: *)
paulson@5545: 
wenzelm@58889: section {* Binary arithmetic examples *}
wenzelm@11024: 
haftmann@28952: theory BinEx
haftmann@28952: imports Complex_Main
haftmann@28952: begin
wenzelm@11024: 
paulson@14113: subsection {* Regression Testing for Cancellation Simprocs *}
paulson@14113: 
paulson@14113: lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "2*u = (u::int)"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "(i + j + 12 + (k::int)) - 15 = y"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "(i + j + 12 + (k::int)) - 5 = y"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "y - b < (b::int)"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "y - (3*b + c) < (b::int) - 2*c"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "(2*x - (u*v) + y) - v*3*u = (w::int)"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "(i + j + 12 + (k::int)) = u + 15 + y"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "(i + j*2 + 12 + (k::int)) = j + 5 + y"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "a + -(b+c) + b = (d::int)"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "a + -(b+c) - b = (d::int)"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: (*negative numerals*)
paulson@14113: lemma "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "(i + j + -3 + (k::int)) < u + 5 + y"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "(i + j + 3 + (k::int)) < u + -6 + y"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "(i + j + -12 + (k::int)) - 15 = y"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "(i + j + 12 + (k::int)) - -15 = y"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14113: lemma "(i + j + -12 + (k::int)) - -15 = y"
paulson@14113: apply simp  oops
paulson@14113: 
paulson@14124: lemma "- (2*i) + 3  + (2*i + 4) = (0::int)"
paulson@14124: apply simp  oops
paulson@14124: 
paulson@14124: 
paulson@14113: 
paulson@14113: subsection {* Arithmetic Method Tests *}
paulson@14113: 
paulson@14113: 
paulson@14113: lemma "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"
paulson@14113: by arith
paulson@14113: 
paulson@14113: lemma "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"
paulson@14113: by arith
paulson@14113: 
paulson@14113: lemma "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d"
paulson@14113: by arith
paulson@14113: 
paulson@14113: lemma "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"
paulson@14113: by arith
paulson@14113: 
paulson@14113: lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"
paulson@14113: by arith
paulson@14113: 
haftmann@58410: lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - (- 1) < j+j - 3"
paulson@14113: by arith
paulson@14113: 
paulson@14113: lemma "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"
paulson@14113: by arith
paulson@14113: 
paulson@14113: lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
paulson@14113:       ==> a <= l"
paulson@14113: by arith
paulson@14113: 
paulson@14113: lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
paulson@14113:       ==> a+a+a+a <= l+l+l+l"
paulson@14113: by arith
paulson@14113: 
paulson@14113: lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
paulson@14113:       ==> a+a+a+a+a <= l+l+l+l+i"
paulson@14113: by arith
paulson@14113: 
paulson@14113: lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
paulson@14113:       ==> a+a+a+a+a+a <= l+l+l+l+i+l"
paulson@14113: by arith
paulson@14113: 
paulson@14113: lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
paulson@14113:       ==> 6*a <= 5*l+i"
paulson@14113: by arith
paulson@14113: 
paulson@14113: 
paulson@14113: 
wenzelm@11024: subsection {* The Integers *}
wenzelm@11024: 
wenzelm@11024: text {* Addition *}
wenzelm@11024: 
wenzelm@11704: lemma "(13::int) + 19 = 32"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(1234::int) + 5678 = 6912"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(1359::int) + -2468 = -1109"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(93746::int) + -46375 = 47371"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11024: 
wenzelm@11024: text {* \medskip Negation *}
wenzelm@11024: 
wenzelm@11704: lemma "- (65745::int) = -65745"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "- (-54321::int) = 54321"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11024: 
wenzelm@11024: text {* \medskip Multiplication *}
wenzelm@11024: 
wenzelm@11704: lemma "(13::int) * 19 = 247"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(-84::int) * 51 = -4284"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(255::int) * 255 = 65025"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(1359::int) * -2468 = -3354012"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(89::int) * 10 \<noteq> 889"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(13::int) < 18 - 4"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(-345::int) < -242 + -100"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(13557456::int) < 18678654"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "(999999::int) \<le> (1000001 + 1) - 2"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(1234567::int) \<le> 1234567"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@15965: text{*No integer overflow!*}
paulson@15965: lemma "1234567 * (1234567::int) < 1234567*1234567*1234567"
paulson@15965:   by simp
paulson@15965: 
wenzelm@11024: 
wenzelm@11024: text {* \medskip Quotient and Remainder *}
wenzelm@11024: 
wenzelm@11704: lemma "(10::int) div 3 = 3"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "(10::int) mod 3 = 1"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11024: text {* A negative divisor *}
wenzelm@11024: 
wenzelm@11704: lemma "(10::int) div -3 = -4"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(10::int) mod -3 = -2"
wenzelm@11024:   by simp
paulson@5545: 
wenzelm@11024: text {*
wenzelm@11024:   A negative dividend\footnote{The definition agrees with mathematical
paulson@15965:   convention and with ML, but not with the hardware of most computers}
wenzelm@11024: *}
wenzelm@11024: 
wenzelm@11704: lemma "(-10::int) div 3 = -4"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(-10::int) mod 3 = 2"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11024: text {* A negative dividend \emph{and} divisor *}
wenzelm@11024: 
wenzelm@11704: lemma "(-10::int) div -3 = 3"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(-10::int) mod -3 = -1"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11024: text {* A few bigger examples *}
wenzelm@11024: 
paulson@11868: lemma "(8452::int) mod 3 = 1"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(59485::int) div 434 = 137"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(1000006::int) mod 10 = 6"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11024: 
wenzelm@11024: text {* \medskip Division by shifting *}
wenzelm@11024: 
wenzelm@11704: lemma "10000000 div 2 = (5000000::int)"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "10000001 mod 2 = (1::int)"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "10000055 div 32 = (312501::int)"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "10000055 mod 32 = (23::int)"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "100094 div 144 = (695::int)"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "100094 mod 144 = (14::int)"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11024: 
paulson@12613: text {* \medskip Powers *}
paulson@12613: 
paulson@12613: lemma "2 ^ 10 = (1024::int)"
paulson@12613:   by simp
paulson@12613: 
haftmann@58410: lemma "(- 3) ^ 7 = (-2187::int)"
paulson@12613:   by simp
paulson@12613: 
paulson@12613: lemma "13 ^ 7 = (62748517::int)"
paulson@12613:   by simp
paulson@12613: 
paulson@12613: lemma "3 ^ 15 = (14348907::int)"
paulson@12613:   by simp
paulson@12613: 
haftmann@58410: lemma "(- 5) ^ 11 = (-48828125::int)"
paulson@12613:   by simp
paulson@12613: 
paulson@12613: 
wenzelm@11024: subsection {* The Natural Numbers *}
wenzelm@11024: 
wenzelm@11024: text {* Successor *}
wenzelm@11024: 
wenzelm@11704: lemma "Suc 99999 = 100000"
huffman@45615:   by simp
wenzelm@11024: 
wenzelm@11024: 
wenzelm@11024: text {* \medskip Addition *}
wenzelm@11024: 
wenzelm@11704: lemma "(13::nat) + 19 = 32"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(1234::nat) + 5678 = 6912"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(973646::nat) + 6475 = 980121"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11024: 
wenzelm@11024: text {* \medskip Subtraction *}
wenzelm@11024: 
wenzelm@11704: lemma "(32::nat) - 14 = 18"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "(14::nat) - 15 = 0"
wenzelm@11024:   by simp
paulson@5545: 
paulson@11868: lemma "(14::nat) - 1576644 = 0"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(48273776::nat) - 3873737 = 44400039"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11024: 
wenzelm@11024: text {* \medskip Multiplication *}
wenzelm@11024: 
wenzelm@11704: lemma "(12::nat) * 11 = 132"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(647::nat) * 3643 = 2357021"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11024: 
wenzelm@11024: text {* \medskip Quotient and Remainder *}
wenzelm@11024: 
wenzelm@11704: lemma "(10::nat) div 3 = 3"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "(10::nat) mod 3 = 1"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(10000::nat) div 9 = 1111"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "(10000::nat) mod 9 = 1"
wenzelm@11024:   by simp
wenzelm@11024: 
wenzelm@11704: lemma "(10000::nat) div 16 = 625"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "(10000::nat) mod 16 = 0"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@5545: 
paulson@12613: text {* \medskip Powers *}
paulson@12613: 
paulson@12613: lemma "2 ^ 12 = (4096::nat)"
paulson@12613:   by simp
paulson@12613: 
paulson@12613: lemma "3 ^ 10 = (59049::nat)"
paulson@12613:   by simp
paulson@12613: 
paulson@12613: lemma "12 ^ 7 = (35831808::nat)"
paulson@12613:   by simp
paulson@12613: 
paulson@12613: lemma "3 ^ 14 = (4782969::nat)"
paulson@12613:   by simp
paulson@12613: 
paulson@12613: lemma "5 ^ 11 = (48828125::nat)"
paulson@12613:   by simp
paulson@12613: 
paulson@12613: 
wenzelm@11024: text {* \medskip Testing the cancellation of complementary terms *}
wenzelm@11024: 
paulson@11868: lemma "y + (x + -x) = (0::int) + y"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "y + (-x + (- y + x)) = (0::int)"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "-x + (y + (- y + x)) = (0::int)"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "x + (x + (- x + (- x + (- y + - z)))) = (0::int) - y - z"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "x + x - x - x - y - z = (0::int) - y - z"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "x + y + z - (x + z) = y - (0::int)"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "x + (y + (y + (y + (-x + -x)))) = (0::int) + y - x + y + y"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "x + (y + (y + (y + (-y + -x)))) = y + (0::int) + y"
wenzelm@11024:   by simp
wenzelm@11024: 
paulson@11868: lemma "x + y - x + z - x - y - z + x < (1::int)"
wenzelm@11024:   by simp
wenzelm@11024: 
haftmann@28952: 
haftmann@28952: subsection{*Real Arithmetic*}
haftmann@28952: 
haftmann@28952: subsubsection {*Addition *}
haftmann@28952: 
haftmann@28952: lemma "(1359::real) + -2468 = -1109"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: lemma "(93746::real) + -46375 = 47371"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: 
haftmann@28952: subsubsection {*Negation *}
haftmann@28952: 
haftmann@28952: lemma "- (65745::real) = -65745"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: lemma "- (-54321::real) = 54321"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: 
haftmann@28952: subsubsection {*Multiplication *}
haftmann@28952: 
haftmann@28952: lemma "(-84::real) * 51 = -4284"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: lemma "(255::real) * 255 = 65025"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: lemma "(1359::real) * -2468 = -3354012"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: 
haftmann@28952: subsubsection {*Inequalities *}
haftmann@28952: 
haftmann@28952: lemma "(89::real) * 10 \<noteq> 889"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: lemma "(13::real) < 18 - 4"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: lemma "(-345::real) < -242 + -100"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: lemma "(13557456::real) < 18678654"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: lemma "(999999::real) \<le> (1000001 + 1) - 2"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: lemma "(1234567::real) \<le> 1234567"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: 
haftmann@28952: subsubsection {*Powers *}
haftmann@28952: 
haftmann@28952: lemma "2 ^ 15 = (32768::real)"
haftmann@28952: by simp
haftmann@28952: 
haftmann@58410: lemma "(- 3) ^ 7 = (-2187::real)"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: lemma "13 ^ 7 = (62748517::real)"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: lemma "3 ^ 15 = (14348907::real)"
haftmann@28952: by simp
haftmann@28952: 
haftmann@58410: lemma "(- 5) ^ 11 = (-48828125::real)"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: 
haftmann@28952: subsubsection {*Tests *}
haftmann@28952: 
haftmann@28952: lemma "(x + y = x) = (y = (0::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x + y = y) = (x = (0::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x + y = (0::real)) = (x = -y)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x + y = (0::real)) = (y = -x)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "((x + y) < (x + z)) = (y < (z::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "((x + z) < (y + z)) = (x < (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(\<not> x < y) = (y \<le> (x::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "\<not> (x < y \<and> y < (x::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x::real) < y ==> \<not> y < x"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(\<not> x \<le> y) = (y < (x::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "x \<le> y \<or> y \<le> (x::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "x \<le> y \<or> y < (x::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "x < y \<or> y \<le> (x::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "x \<le> (x::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "((x::real) \<le> y) = (x < y \<or> x = y)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "\<not>(x < y \<and> y \<le> (x::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "\<not>(x \<le> y \<and> y < (x::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(-x < (0::real)) = (0 < x)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "((0::real) < -x) = (x < 0)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(-x \<le> (0::real)) = (0 \<le> x)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "((0::real) \<le> -x) = (x \<le> 0)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x::real) = y \<or> x < y \<or> y < x"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(0::real) \<le> x \<or> 0 \<le> -x"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "((x::real) + y \<le> x + z) = (y \<le> z)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "((x::real) + z \<le> y + z) = (x \<le> y)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(w::real) < x \<and> y < z ==> w + y < x + z"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(0::real) < x \<and> 0 < y ==> 0 < x + y"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(-x < y) = (0 < x + (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x < -y) = (x + y < (0::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(y < x + -z) = (y + z < (x::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x + -y < z) = (x < z + (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "x \<le> y ==> x < y + (1::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x - y) + y = (x::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "y + (x - y) = (x::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "x - x = (0::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x - y = 0) = (x = (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "((0::real) \<le> x + x) = (0 \<le> x)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(-x \<le> x) = ((0::real) \<le> x)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x \<le> -x) = (x \<le> (0::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(-x = (0::real)) = (x = 0)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "-(x - y) = y - (x::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "((0::real) < x - y) = (y < x)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "((0::real) \<le> x - y) = (y \<le> x)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x + y) - x = (y::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(-x = y) = (x = (-y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "x < (y::real) ==> \<not>(x = y)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x \<le> x + y) = ((0::real) \<le> y)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(y \<le> x + y) = ((0::real) \<le> x)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x < x + y) = ((0::real) < y)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(y < x + y) = ((0::real) < x)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x - y) - x = (-y::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x + y < z) = (x < z - (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x - y < z) = (x < z + (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x < y - z) = (x + z < (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x \<le> y - z) = (x + z \<le> (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x - y \<le> z) = (x \<le> z + (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(-x < -y) = (y < (x::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(-x \<le> -y) = (y \<le> (x::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(0::real) - x = -x"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "x - (0::real) = x"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(0::real) < x \<and> 0 \<le> y ==> 0 < x + y"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "-x - y = -(x + (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "x - (-y) = x + (y::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "-x - -y = y - (x::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(a - b) + (b - c) = a - (c::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x = y - z) = (x + z = (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x - y = z) = (x = z + (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "x - (x - y) = (y::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "x - (x + y) = -(y::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "x = y ==> x \<le> (y::real)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(0::real) < x ==> \<not>(x = 0)"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(x + y) * (x - y) = (x * x) - (y * y)"
haftmann@28952:   oops
haftmann@28952: 
haftmann@28952: lemma "(-x = -y) = (x = (y::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "(-x < -y) = (y < (x::real))"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
haftmann@31066: by linarith
haftmann@28952: 
haftmann@28952: lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
haftmann@31066: by linarith
haftmann@28952: 
haftmann@28952: lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
haftmann@31066: by linarith
haftmann@28952: 
haftmann@28952: lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"
haftmann@31066: by linarith
haftmann@28952: 
haftmann@28952: lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
haftmann@31066: by linarith
haftmann@28952: 
haftmann@28952: lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k"
haftmann@28952: by arith
haftmann@28952: 
haftmann@28952: lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
haftmann@28952:     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
haftmann@31066: by linarith
haftmann@28952: 
haftmann@28952: lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
haftmann@28952:     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
haftmann@31066: by linarith
haftmann@28952: 
haftmann@28952: lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
haftmann@28952:     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
haftmann@31066: by linarith
haftmann@28952: 
haftmann@28952: lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
haftmann@28952:     ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l"
haftmann@31066: by linarith
haftmann@28952: 
haftmann@28952: 
haftmann@28952: subsection{*Complex Arithmetic*}
haftmann@28952: 
haftmann@28952: lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: lemma "- (65745 + -47371*ii) = -65745 + 47371*ii"
haftmann@28952: by simp
haftmann@28952: 
haftmann@28952: text{*Multiplication requires distributive laws.  Perhaps versions instantiated
haftmann@28952: to literal constants should be added to the simpset.*}
haftmann@28952: 
haftmann@28952: lemma "(1 + ii) * (1 - ii) = 2"
haftmann@28952: by (simp add: ring_distribs)
haftmann@28952: 
haftmann@28952: lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii"
haftmann@28952: by (simp add: ring_distribs)
haftmann@28952: 
haftmann@28952: lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"
haftmann@28952: by (simp add: ring_distribs)
haftmann@28952: 
haftmann@28952: text{*No inequalities or linear arithmetic: the complex numbers are unordered!*}
haftmann@28952: 
haftmann@28952: text{*No powers (not supported yet)*}
haftmann@28952: 
paulson@5545: end