(* Title: HOL/Complex/ex/BinEx.thy ID: $Id: BinEx.thy,v 1.4 2004/08/19 10:35:45 nipkow Exp $ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge *) header {* Binary arithmetic examples *} theory BinEx imports Complex_Main begin text {* Examples of performing binary arithmetic by simplification. This time we use the reals, though the representation is just of integers. *} subsection{*Real Arithmetic*} subsubsection {*Addition *} lemma "(1359::real) + -2468 = -1109" by simp lemma "(93746::real) + -46375 = 47371" by simp subsubsection {*Negation *} lemma "- (65745::real) = -65745" by simp lemma "- (-54321::real) = 54321" by simp subsubsection {*Multiplication *} lemma "(-84::real) * 51 = -4284" by simp lemma "(255::real) * 255 = 65025" by simp lemma "(1359::real) * -2468 = -3354012" by simp subsubsection {*Inequalities *} lemma "(89::real) * 10 ≠ 889" by simp lemma "(13::real) < 18 - 4" by simp lemma "(-345::real) < -242 + -100" by simp lemma "(13557456::real) < 18678654" by simp lemma "(999999::real) ≤ (1000001 + 1) - 2" by simp lemma "(1234567::real) ≤ 1234567" by simp subsubsection {*Powers *} lemma "2 ^ 15 = (32768::real)" by simp lemma "-3 ^ 7 = (-2187::real)" by simp lemma "13 ^ 7 = (62748517::real)" by simp lemma "3 ^ 15 = (14348907::real)" by simp lemma "-5 ^ 11 = (-48828125::real)" by simp subsubsection {*Tests *} lemma "(x + y = x) = (y = (0::real))" by arith lemma "(x + y = y) = (x = (0::real))" by arith lemma "(x + y = (0::real)) = (x = -y)" by arith lemma "(x + y = (0::real)) = (y = -x)" by arith lemma "((x + y) < (x + z)) = (y < (z::real))" by arith lemma "((x + z) < (y + z)) = (x < (y::real))" by arith lemma "(¬ x < y) = (y ≤ (x::real))" by arith lemma "¬ (x < y ∧ y < (x::real))" by arith lemma "(x::real) < y ==> ¬ y < x" by arith lemma "((x::real) ≠ y) = (x < y ∨ y < x)" by arith lemma "(¬ x ≤ y) = (y < (x::real))" by arith lemma "x ≤ y ∨ y ≤ (x::real)" by arith lemma "x ≤ y ∨ y < (x::real)" by arith lemma "x < y ∨ y ≤ (x::real)" by arith lemma "x ≤ (x::real)" by arith lemma "((x::real) ≤ y) = (x < y ∨ x = y)" by arith lemma "((x::real) ≤ y ∧ y ≤ x) = (x = y)" by arith lemma "¬(x < y ∧ y ≤ (x::real))" by arith lemma "¬(x ≤ y ∧ y < (x::real))" by arith lemma "(-x < (0::real)) = (0 < x)" by arith lemma "((0::real) < -x) = (x < 0)" by arith lemma "(-x ≤ (0::real)) = (0 ≤ x)" by arith lemma "((0::real) ≤ -x) = (x ≤ 0)" by arith lemma "(x::real) = y ∨ x < y ∨ y < x" by arith lemma "(x::real) = 0 ∨ 0 < x ∨ 0 < -x" by arith lemma "(0::real) ≤ x ∨ 0 ≤ -x" by arith lemma "((x::real) + y ≤ x + z) = (y ≤ z)" by arith lemma "((x::real) + z ≤ y + z) = (x ≤ y)" by arith lemma "(w::real) < x ∧ y < z ==> w + y < x + z" by arith lemma "(w::real) ≤ x ∧ y ≤ z ==> w + y ≤ x + z" by arith lemma "(0::real) ≤ x ∧ 0 ≤ y ==> 0 ≤ x + y" by arith lemma "(0::real) < x ∧ 0 < y ==> 0 < x + y" by arith lemma "(-x < y) = (0 < x + (y::real))" by arith lemma "(x < -y) = (x + y < (0::real))" by arith lemma "(y < x + -z) = (y + z < (x::real))" by arith lemma "(x + -y < z) = (x < z + (y::real))" by arith lemma "x ≤ y ==> x < y + (1::real)" by arith lemma "(x - y) + y = (x::real)" by arith lemma "y + (x - y) = (x::real)" by arith lemma "x - x = (0::real)" by arith lemma "(x - y = 0) = (x = (y::real))" by arith lemma "((0::real) ≤ x + x) = (0 ≤ x)" by arith lemma "(-x ≤ x) = ((0::real) ≤ x)" by arith lemma "(x ≤ -x) = (x ≤ (0::real))" by arith lemma "(-x = (0::real)) = (x = 0)" by arith lemma "-(x - y) = y - (x::real)" by arith lemma "((0::real) < x - y) = (y < x)" by arith lemma "((0::real) ≤ x - y) = (y ≤ x)" by arith lemma "(x + y) - x = (y::real)" by arith lemma "(-x = y) = (x = (-y::real))" by arith lemma "x < (y::real) ==> ¬(x = y)" by arith lemma "(x ≤ x + y) = ((0::real) ≤ y)" by arith lemma "(y ≤ x + y) = ((0::real) ≤ x)" by arith lemma "(x < x + y) = ((0::real) < y)" by arith lemma "(y < x + y) = ((0::real) < x)" by arith lemma "(x - y) - x = (-y::real)" by arith lemma "(x + y < z) = (x < z - (y::real))" by arith lemma "(x - y < z) = (x < z + (y::real))" by arith lemma "(x < y - z) = (x + z < (y::real))" by arith lemma "(x ≤ y - z) = (x + z ≤ (y::real))" by arith lemma "(x - y ≤ z) = (x ≤ z + (y::real))" by arith lemma "(-x < -y) = (y < (x::real))" by arith lemma "(-x ≤ -y) = (y ≤ (x::real))" by arith lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))" by arith lemma "(0::real) - x = -x" by arith lemma "x - (0::real) = x" by arith lemma "w ≤ x ∧ y < z ==> w + y < x + (z::real)" by arith lemma "w < x ∧ y ≤ z ==> w + y < x + (z::real)" by arith lemma "(0::real) ≤ x ∧ 0 < y ==> 0 < x + (y::real)" by arith lemma "(0::real) < x ∧ 0 ≤ y ==> 0 < x + y" by arith lemma "-x - y = -(x + (y::real))" by arith lemma "x - (-y) = x + (y::real)" by arith lemma "-x - -y = y - (x::real)" by arith lemma "(a - b) + (b - c) = a - (c::real)" by arith lemma "(x = y - z) = (x + z = (y::real))" by arith lemma "(x - y = z) = (x = z + (y::real))" by arith lemma "x - (x - y) = (y::real)" by arith lemma "x - (x + y) = -(y::real)" by arith lemma "x = y ==> x ≤ (y::real)" by arith lemma "(0::real) < x ==> ¬(x = 0)" by arith lemma "(x + y) * (x - y) = (x * x) - (y * y)" oops lemma "(-x = -y) = (x = (y::real))" by arith lemma "(-x < -y) = (y < (x::real))" by arith lemma "!!a::real. a ≤ b ==> c ≤ d ==> x + y < z ==> a + c ≤ b + d" by (tactic "fast_arith_tac 1") lemma "!!a::real. a < b ==> c < d ==> a - d ≤ b + (-c)" by (tactic "fast_arith_tac 1") lemma "!!a::real. a ≤ b ==> b + b ≤ c ==> a + a ≤ c" by (tactic "fast_arith_tac 1") lemma "!!a::real. a + b ≤ i + j ==> a ≤ b ==> i ≤ j ==> a + a ≤ j + j" by (tactic "fast_arith_tac 1") lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j" by (tactic "fast_arith_tac 1") lemma "!!a::real. a + b + c ≤ i + j + k ∧ a ≤ b ∧ b ≤ c ∧ i ≤ j ∧ j ≤ k --> a + a + a ≤ k + k + k" by arith lemma "!!a::real. a + b + c + d ≤ i + j + k + l ==> a ≤ b ==> b ≤ c ==> c ≤ d ==> i ≤ j ==> j ≤ k ==> k ≤ l ==> a ≤ l" by (tactic "fast_arith_tac 1") lemma "!!a::real. a + b + c + d ≤ i + j + k + l ==> a ≤ b ==> b ≤ c ==> c ≤ d ==> i ≤ j ==> j ≤ k ==> k ≤ l ==> a + a + a + a ≤ l + l + l + l" by (tactic "fast_arith_tac 1") lemma "!!a::real. a + b + c + d ≤ i + j + k + l ==> a ≤ b ==> b ≤ c ==> c ≤ d ==> i ≤ j ==> j ≤ k ==> k ≤ l ==> a + a + a + a + a ≤ l + l + l + l + i" by (tactic "fast_arith_tac 1") lemma "!!a::real. a + b + c + d ≤ i + j + k + l ==> a ≤ b ==> b ≤ c ==> c ≤ d ==> i ≤ j ==> j ≤ k ==> k ≤ l ==> a + a + a + a + a + a ≤ l + l + l + l + i + l" by (tactic "fast_arith_tac 1") subsection{*Complex Arithmetic*} lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii" by simp lemma "- (65745 + -47371*ii) = -65745 + 47371*ii" by simp text{*Multiplication requires distributive laws. Perhaps versions instantiated to literal constants should be added to the simpset.*} lemmas distrib = left_distrib right_distrib left_diff_distrib right_diff_distrib lemma "(1 + ii) * (1 - ii) = 2" by (simp add: distrib) lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii" by (simp add: distrib) lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii" by (simp add: distrib) text{*No inequalities or linear arithmetic: the complex numbers are unordered!*} text{*No powers (not supported yet)*} end
lemma
1359 + -2468 = -1109
lemma
93746 + -46375 = 47371
lemma
- 65745 = -65745
lemma
- -54321 = 54321
lemma
-84 * 51 = -4284
lemma
255 * 255 = 65025
lemma
1359 * -2468 = -3354012
lemma
89 * 10 ≠ 889
lemma
13 < 18 - 4
lemma
-345 < -242 + -100
lemma
13557456 < 18678654
lemma
999999 ≤ 1000001 + 1 - 2
lemma
1234567 ≤ 1234567
lemma
2 ^ 15 = 32768
lemma
-3 ^ 7 = -2187
lemma
13 ^ 7 = 62748517
lemma
3 ^ 15 = 14348907
lemma
-5 ^ 11 = -48828125
lemma
(x + y = x) = (y = 0)
lemma
(x + y = y) = (x = 0)
lemma
(x + y = 0) = (x = - y)
lemma
(x + y = 0) = (y = - x)
lemma
(x + y < x + z) = (y < z)
lemma
(x + z < y + z) = (x < y)
lemma
(¬ x < y) = (y ≤ x)
lemma
¬ (x < y ∧ y < x)
lemma
x < y ==> ¬ y < x
lemma
(x ≠ y) = (x < y ∨ y < x)
lemma
(¬ x ≤ y) = (y < x)
lemma
x ≤ y ∨ y ≤ x
lemma
x ≤ y ∨ y < x
lemma
x < y ∨ y ≤ x
lemma
x ≤ x
lemma
(x ≤ y) = (x < y ∨ x = y)
lemma
(x ≤ y ∧ y ≤ x) = (x = y)
lemma
¬ (x < y ∧ y ≤ x)
lemma
¬ (x ≤ y ∧ y < x)
lemma
(- x < 0) = (0 < x)
lemma
(0 < - x) = (x < 0)
lemma
(- x ≤ 0) = (0 ≤ x)
lemma
(0 ≤ - x) = (x ≤ 0)
lemma
x = y ∨ x < y ∨ y < x
lemma
x = 0 ∨ 0 < x ∨ 0 < - x
lemma
0 ≤ x ∨ 0 ≤ - x
lemma
(x + y ≤ x + z) = (y ≤ z)
lemma
(x + z ≤ y + z) = (x ≤ y)
lemma
w < x ∧ y < z ==> w + y < x + z
lemma
w ≤ x ∧ y ≤ z ==> w + y ≤ x + z
lemma
0 ≤ x ∧ 0 ≤ y ==> 0 ≤ x + y
lemma
0 < x ∧ 0 < y ==> 0 < x + y
lemma
(- x < y) = (0 < x + y)
lemma
(x < - y) = (x + y < 0)
lemma
(y < x + - z) = (y + z < x)
lemma
(x + - y < z) = (x < z + y)
lemma
x ≤ y ==> x < y + 1
lemma
x - y + y = x
lemma
y + (x - y) = x
lemma
x - x = 0
lemma
(x - y = 0) = (x = y)
lemma
(0 ≤ x + x) = (0 ≤ x)
lemma
(- x ≤ x) = (0 ≤ x)
lemma
(x ≤ - x) = (x ≤ 0)
lemma
(- x = 0) = (x = 0)
lemma
- (x - y) = y - x
lemma
(0 < x - y) = (y < x)
lemma
(0 ≤ x - y) = (y ≤ x)
lemma
x + y - x = y
lemma
(- x = y) = (x = - y)
lemma
x < y ==> x ≠ y
lemma
(x ≤ x + y) = (0 ≤ y)
lemma
(y ≤ x + y) = (0 ≤ x)
lemma
(x < x + y) = (0 < y)
lemma
(y < x + y) = (0 < x)
lemma
x - y - x = - y
lemma
(x + y < z) = (x < z - y)
lemma
(x - y < z) = (x < z + y)
lemma
(x < y - z) = (x + z < y)
lemma
(x ≤ y - z) = (x + z ≤ y)
lemma
(x - y ≤ z) = (x ≤ z + y)
lemma
(- x < - y) = (y < x)
lemma
(- x ≤ - y) = (y ≤ x)
lemma
a + b - (c + d) = a - c + (b - d)
lemma
0 - x = - x
lemma
x - 0 = x
lemma
w ≤ x ∧ y < z ==> w + y < x + z
lemma
w < x ∧ y ≤ z ==> w + y < x + z
lemma
0 ≤ x ∧ 0 < y ==> 0 < x + y
lemma
0 < x ∧ 0 ≤ y ==> 0 < x + y
lemma
- x - y = - (x + y)
lemma
x - - y = x + y
lemma
- x - - y = y - x
lemma
a - b + (b - c) = a - c
lemma
(x = y - z) = (x + z = y)
lemma
(x - y = z) = (x = z + y)
lemma
x - (x - y) = y
lemma
x - (x + y) = - y
lemma
x = y ==> x ≤ y
lemma
0 < x ==> x ≠ 0
lemma
(- x = - y) = (x = y)
lemma
(- x < - y) = (y < x)
lemma
[| a ≤ b; c ≤ d; x + y < z |] ==> a + c ≤ b + d
lemma
[| a < b; c < d |] ==> a - d ≤ b + - c
lemma
[| a ≤ b; b + b ≤ c |] ==> a + a ≤ c
lemma
[| a + b ≤ i + j; a ≤ b; i ≤ j |] ==> a + a ≤ j + j
lemma
[| a + b < i + j; a < b; i < j |] ==> a + a < j + j
lemma
a + b + c ≤ i + j + k ∧ a ≤ b ∧ b ≤ c ∧ i ≤ j ∧ j ≤ k --> a + a + a ≤ k + k + k
lemma
[| a + b + c + d ≤ i + j + k + l; a ≤ b; b ≤ c; c ≤ d; i ≤ j; j ≤ k; k ≤ l |] ==> a ≤ l
lemma
[| a + b + c + d ≤ i + j + k + l; a ≤ b; b ≤ c; c ≤ d; i ≤ j; j ≤ k; k ≤ l |] ==> a + a + a + a ≤ l + l + l + l
lemma
[| a + b + c + d ≤ i + j + k + l; a ≤ b; b ≤ c; c ≤ d; i ≤ j; j ≤ k; k ≤ l |] ==> a + a + a + a + a ≤ l + l + l + l + i
lemma
[| a + b + c + d ≤ i + j + k + l; a ≤ b; b ≤ c; c ≤ d; i ≤ j; j ≤ k; k ≤ l |] ==> a + a + a + a + a + a ≤ l + l + l + l + i + l
lemma
1359 + 93746 * \<i> - (2468 + 46375 * \<i>) = -1109 + 47371 * \<i>
lemma
- (65745 + -47371 * \<i>) = -65745 + 47371 * \<i>
lemmas distrib:
(a + b) * c = a * c + b * c
a * (b + c) = a * b + a * c
(a - b) * c = a * c - b * c
a * (b - c) = a * b - a * c
lemmas distrib:
(a + b) * c = a * c + b * c
a * (b + c) = a * b + a * c
(a - b) * c = a * c - b * c
a * (b - c) = a * b - a * c
lemma
(1 + \<i>) * (1 - \<i>) = 2
lemma
(1 + 2 * \<i>) * (1 + 3 * \<i>) = -5 + 5 * \<i>
lemma
-84 + 255 * \<i> + 51 * 255 * \<i> = -84 + 13260 * \<i>