# 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<z |] ==> 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<b; i<j |] ==> 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 \<noteq> #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) \<le> (#1000001 + #1)-#2"
+  by simp
+
+lemma "(#1234567::real) \<le> #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 "(\<not> x < y) = (y \<le> (x::real))"
+  by arith
+
+lemma "\<not> (x < y \<and> y < (x::real))"
+  by arith
+
+lemma "(x::real) < y ==> \<not> y < x"
+  by arith
+
+lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)"
+  by arith
+
+lemma "(\<not> x \<le> y) = (y < (x::real))"
+  by arith
+
+lemma "x \<le> y \<or> y \<le> (x::real)"
+  by arith
+
+lemma "x \<le> y \<or> y < (x::real)"
+  by arith
+
+lemma "x < y \<or> y \<le> (x::real)"
+  by arith
+
+lemma "x \<le> (x::real)"
+  by arith
+
+lemma "((x::real) \<le> y) = (x < y \<or> x = y)"
+  by arith
+
+lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)"
+  by arith
+
+lemma "\<not>(x < y \<and> y \<le> (x::real))"
+  by arith
+
+lemma "\<not>(x \<le> y \<and> y < (x::real))"
+  by arith
+
+lemma "(-x < (#0::real)) = (#0 < x)"
+  by arith
+
+lemma "((#0::real) < -x) = (x < #0)"
+  by arith
+
+lemma "(-x \<le> (#0::real)) = (#0 \<le> x)"
+  by arith
+
+lemma "((#0::real) \<le> -x) = (x \<le> #0)"
+  by arith
+
+lemma "(x::real) = y \<or> x < y \<or> y < x"
+  by arith
+
+lemma "(x::real) = #0 \<or> #0 < x \<or> #0 < -x"
+  by arith
+
+lemma "(#0::real) \<le> x \<or> #0 \<le> -x"
+  by arith
+
+lemma "((x::real) + y \<le> x + z) = (y \<le> z)"
+  by arith
+
+lemma "((x::real) + z \<le> y + z) = (x \<le> y)"
+  by arith
+
+lemma "(w::real) < x \<and> y < z ==> w + y < x + z"
+  by arith
+
+lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z"
+  by arith
+
+lemma "(#0::real) \<le> x \<and> #0 \<le> y ==> #0 \<le> x + y"
+  by arith
+
+lemma "(#0::real) < x \<and> #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 \<le> 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) \<le> x + x) = (#0 \<le> x)"
+  by arith
+
+lemma "(-x \<le> x) = ((#0::real) \<le> x)"
+  by arith
+
+lemma "(x \<le> -x) = (x \<le> (#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) \<le> x - y) = (y \<le> x)"
+  by arith
+
+lemma "(x + y) - x = (y::real)"
+  by arith
+
+lemma "(-x = y) = (x = (-y::real))"
+  by arith
+
+lemma "x < (y::real) ==> \<not>(x = y)"
+  by arith
+
+lemma "(x \<le> x + y) = ((#0::real) \<le> y)"
+  by arith
+
+lemma "(y \<le> x + y) = ((#0::real) \<le> 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 \<le> y - z) = (x + z \<le> (y::real))"
+  by arith
+
+lemma "(x - y \<le> z) = (x \<le> z + (y::real))"
+  by arith
+
+lemma "(-x < -y) = (y < (x::real))"
+  by arith
+
+lemma "(-x \<le> -y) = (y \<le> (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 \<le> x \<and> y < z ==> w + y < x + (z::real)"
+  by arith
+
+lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)"
+  by arith
+
+lemma "(#0::real) \<le> x \<and> #0 < y ==> #0 < x + (y::real)"
+  by arith
+
+lemma "(#0::real) < x \<and> #0 \<le> 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 \<le> (y::real)"
+  by arith
+
+lemma "(#0::real) < x ==> \<not>(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 \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> 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 \<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"
+  by arith
+
+lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
+    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
+    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
+    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
+    ==> 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"
+  by (tactic "fast_arith_tac 1")
+
+end