# HG changeset patch # User wenzelm # Date 1001609052 -7200 # Node ID 6ef2535fff9393b486f533b8f7c6fb9df817317c # Parent 3ccea743e5e71053e9a39c3c6e0dc120852673b9 new-style theory; diff -r 3ccea743e5e7 -r 6ef2535fff93 src/HOL/Real/ex/BinEx.ML --- a/src/HOL/Real/ex/BinEx.ML Thu Sep 27 18:43:40 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,353 +0,0 @@ -(* Title: HOL/Real/ex/BinEx.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1999 University of Cambridge - -Examples of performing binary arithmetic by simplification -This time we use the reals, though the representation is just of integers. -*) - -(*** Addition ***) - -Goal "(#1359::real) + #-2468 = #-1109"; -by (Simp_tac 1); -qed ""; - -Goal "(#93746::real) + #-46375 = #47371"; -by (Simp_tac 1); -qed ""; - -(*** Negation ***) - -Goal "- (#65745::real) = #-65745"; -by (Simp_tac 1); -qed ""; - -Goal "- (#-54321::real) = #54321"; -by (Simp_tac 1); -qed ""; - - -(*** Multiplication ***) - -Goal "(#-84::real) * #51 = #-4284"; -by (Simp_tac 1); -qed ""; - -Goal "(#255::real) * #255 = #65025"; -by (Simp_tac 1); -qed ""; - -Goal "(#1359::real) * #-2468 = #-3354012"; -by (Simp_tac 1); -qed ""; - -(*** Inequalities ***) - -Goal "(#89::real) * #10 ~= #889"; -by (Simp_tac 1); -qed ""; - -Goal "(#13::real) < #18 - #4"; -by (Simp_tac 1); -qed ""; - -Goal "(#-345::real) < #-242 + #-100"; -by (Simp_tac 1); -qed ""; - -Goal "(#13557456::real) < #18678654"; -by (Simp_tac 1); -qed ""; - -Goal "(#999999::real) <= (#1000001 + #1)-#2"; -by (Simp_tac 1); -qed ""; - -Goal "(#1234567::real) <= #1234567"; -by (Simp_tac 1); -qed ""; - -(** Tests **) -Goal "(x + y = x) = (y = (#0::real))"; -by(arith_tac 1); - -Goal "(x + y = y) = (x = (#0::real))"; -by(arith_tac 1); - -Goal "(x + y = (#0::real)) = (x = -y)"; -by(arith_tac 1); - -Goal "(x + y = (#0::real)) = (y = -x)"; -by(arith_tac 1); - -Goal "((x + y) < (x + z)) = (y < (z::real))"; -by(arith_tac 1); - -Goal "((x + z) < (y + z)) = (x < (y::real))"; -by(arith_tac 1); - -Goal "(~ x < y) = (y <= (x::real))"; -by(arith_tac 1); - -Goal "~(x < y & y < (x::real))"; -by(arith_tac 1); - -Goal "(x::real) < y ==> ~ y < x"; -by(arith_tac 1); - -Goal "((x::real) ~= y) = (x < y | y < x)"; -by(arith_tac 1); - -Goal "(~ x <= y) = (y < (x::real))"; -by(arith_tac 1); - -Goal "x <= y | y <= (x::real)"; -by(arith_tac 1); - -Goal "x <= y | y < (x::real)"; -by(arith_tac 1); - -Goal "x < y | y <= (x::real)"; -by(arith_tac 1); - -Goal "x <= (x::real)"; -by(arith_tac 1); - -Goal "((x::real) <= y) = (x < y | x = y)"; -by(arith_tac 1); - -Goal "((x::real) <= y & y <= x) = (x = y)"; -by(arith_tac 1); - -Goal "~(x < y & y <= (x::real))"; -by(arith_tac 1); - -Goal "~(x <= y & y < (x::real))"; -by(arith_tac 1); - -Goal "(-x < (#0::real)) = (#0 < x)"; -by(arith_tac 1); - -Goal "((#0::real) < -x) = (x < #0)"; -by(arith_tac 1); - -Goal "(-x <= (#0::real)) = (#0 <= x)"; -by(arith_tac 1); - -Goal "((#0::real) <= -x) = (x <= #0)"; -by(arith_tac 1); - -Goal "(x::real) = y | x < y | y < x"; -by(arith_tac 1); - -Goal "(x::real) = #0 | #0 < x | #0 < -x"; -by(arith_tac 1); - -Goal "(#0::real) <= x | #0 <= -x"; -by(arith_tac 1); - -Goal "((x::real) + y <= x + z) = (y <= z)"; -by(arith_tac 1); - -Goal "((x::real) + z <= y + z) = (x <= y)"; -by(arith_tac 1); - -Goal "(w::real) < x & y < z ==> w + y < x + z"; -by(arith_tac 1); - -Goal "(w::real) <= x & y <= z ==> w + y <= x + z"; -by(arith_tac 1); - -Goal "(#0::real) <= x & #0 <= y ==> #0 <= x + y"; -by(arith_tac 1); - -Goal "(#0::real) < x & #0 < y ==> #0 < x + y"; -by(arith_tac 1); - -Goal "(-x < y) = (#0 < x + (y::real))"; -by(arith_tac 1); - -Goal "(x < -y) = (x + y < (#0::real))"; -by(arith_tac 1); - -Goal "(y < x + -z) = (y + z < (x::real))"; -by(arith_tac 1); - -Goal "(x + -y < z) = (x < z + (y::real))"; -by(arith_tac 1); - -Goal "x <= y ==> x < y + (#1::real)"; -by(arith_tac 1); - -Goal "(x - y) + y = (x::real)"; -by(arith_tac 1); - -Goal "y + (x - y) = (x::real)"; -by(arith_tac 1); - -Goal "x - x = (#0::real)"; -by(arith_tac 1); - -Goal "(x - y = #0) = (x = (y::real))"; -by(arith_tac 1); - -Goal "((#0::real) <= x + x) = (#0 <= x)"; -by(arith_tac 1); - -Goal "(-x <= x) = ((#0::real) <= x)"; -by(arith_tac 1); - -Goal "(x <= -x) = (x <= (#0::real))"; -by(arith_tac 1); - -Goal "(-x = (#0::real)) = (x = #0)"; -by(arith_tac 1); - -Goal "-(x - y) = y - (x::real)"; -by(arith_tac 1); - -Goal "((#0::real) < x - y) = (y < x)"; -by(arith_tac 1); - -Goal "((#0::real) <= x - y) = (y <= x)"; -by(arith_tac 1); - -Goal "(x + y) - x = (y::real)"; -by(arith_tac 1); - -Goal "(-x = y) = (x = (-y::real))"; -by(arith_tac 1); - -Goal "x < (y::real) ==> ~(x = y)"; -by(arith_tac 1); - -Goal "(x <= x + y) = ((#0::real) <= y)"; -by(arith_tac 1); - -Goal "(y <= x + y) = ((#0::real) <= x)"; -by(arith_tac 1); - -Goal "(x < x + y) = ((#0::real) < y)"; -by(arith_tac 1); - -Goal "(y < x + y) = ((#0::real) < x)"; -by(arith_tac 1); - -Goal "(x - y) - x = (-y::real)"; -by(arith_tac 1); - -Goal "(x + y < z) = (x < z - (y::real))"; -by(arith_tac 1); - -Goal "(x - y < z) = (x < z + (y::real))"; -by(arith_tac 1); - -Goal "(x < y - z) = (x + z < (y::real))"; -by(arith_tac 1); - -Goal "(x <= y - z) = (x + z <= (y::real))"; -by(arith_tac 1); - -Goal "(x - y <= z) = (x <= z + (y::real))"; -by(arith_tac 1); - -Goal "(-x < -y) = (y < (x::real))"; -by(arith_tac 1); - -Goal "(-x <= -y) = (y <= (x::real))"; -by(arith_tac 1); - -Goal "(a + b) - (c + d) = (a - c) + (b - (d::real))"; -by(arith_tac 1); - -Goal "(#0::real) - x = -x"; -by(arith_tac 1); - -Goal "x - (#0::real) = x"; -by(arith_tac 1); - -Goal "w <= x & y < z ==> w + y < x + (z::real)"; -by(arith_tac 1); - -Goal "w < x & y <= z ==> w + y < x + (z::real)"; -by(arith_tac 1); - -Goal "(#0::real) <= x & #0 < y ==> #0 < x + (y::real)"; -by(arith_tac 1); - -Goal "(#0::real) < x & #0 <= y ==> #0 < x + y"; -by(arith_tac 1); - -Goal "-x - y = -(x + (y::real))"; -by(arith_tac 1); - -Goal "x - (-y) = x + (y::real)"; -by(arith_tac 1); - -Goal "-x - -y = y - (x::real)"; -by(arith_tac 1); - -Goal "(a - b) + (b - c) = a - (c::real)"; -by(arith_tac 1); - -Goal "(x = y - z) = (x + z = (y::real))"; -by(arith_tac 1); - -Goal "(x - y = z) = (x = z + (y::real))"; -by(arith_tac 1); - -Goal "x - (x - y) = (y::real)"; -by(arith_tac 1); - -Goal "x - (x + y) = -(y::real)"; -by(arith_tac 1); - -Goal "x = y ==> x <= (y::real)"; -by(arith_tac 1); - -Goal "(#0::real) < x ==> ~(x = #0)"; -by(arith_tac 1); - -Goal "(x + y) * (x - y) = (x * x) - (y * y)"; - -Goal "(-x = -y) = (x = (y::real))"; -by(arith_tac 1); - -Goal "(-x < -y) = (y < (x::real))"; -by(arith_tac 1); - -Goal "!!a::real. [| a <= b; c <= d; x+y a+c <= b+d"; -by (fast_arith_tac 1); - -Goal "!!a::real. [| a < b; c < d |] ==> a-d <= b+(-c)"; -by (fast_arith_tac 1); - -Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c"; -by (fast_arith_tac 1); - -Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"; -by (fast_arith_tac 1); - -Goal "!!a::real. [| a+b < i+j; a a+a < j+j"; -by (fast_arith_tac 1); - -Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; -by (arith_tac 1); - -Goal "!!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 (fast_arith_tac 1); - -Goal "!!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 (fast_arith_tac 1); - -Goal "!!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 (fast_arith_tac 1); - -Goal "!!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 (fast_arith_tac 1); - diff -r 3ccea743e5e7 -r 6ef2535fff93 src/HOL/Real/ex/BinEx.thy --- a/src/HOL/Real/ex/BinEx.thy Thu Sep 27 18:43:40 2001 +0200 +++ b/src/HOL/Real/ex/BinEx.thy Thu Sep 27 18:44:12 2001 +0200 @@ -1,2 +1,352 @@ +(* Title: HOL/Real/ex/BinEx.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1999 University of Cambridge +*) -BinEx = Real +header {* Binary arithmetic examples *} + +theory BinEx = Real: + +text {* + Examples of performing binary arithmetic by simplification This time + we use the reals, though the representation is just of integers. +*} + +text {* \medskip Addition *} + +lemma "(#1359::real) + #-2468 = #-1109" + by simp + +lemma "(#93746::real) + #-46375 = #47371" + by simp + + +text {* \medskip Negation *} + +lemma "- (#65745::real) = #-65745" + by simp + +lemma "- (#-54321::real) = #54321" + by simp + + +text {* \medskip Multiplication *} + +lemma "(#-84::real) * #51 = #-4284" + by simp + +lemma "(#255::real) * #255 = #65025" + by simp + +lemma "(#1359::real) * #-2468 = #-3354012" + by simp + + +text {* \medskip 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 + + +text {* \medskip 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") + +end