# HG changeset patch
# User paulson
# Date 990448554 -7200
# Node ID fbca0f74bcefc304e6df04d6bb93803ef61cc47f
# Parent  f6eebbbed44938def41bfcb2eb198b8f51f408e6
Division examples

diff -r f6eebbbed449 -r fbca0f74bcef src/ZF/ex/BinEx.ML
--- a/src/ZF/ex/BinEx.ML	Mon May 21 12:51:15 2001 +0200
+++ b/src/ZF/ex/BinEx.ML	Mon May 21 14:35:54 2001 +0200
@@ -6,7 +6,7 @@
 Examples of performing binary arithmetic by simplification
 *)
 
-context Bin.thy;
+context Main.thy;
 
 (*All runtimes below are on a 300MHz Pentium*)
 
@@ -55,7 +55,7 @@
 
 (** Comparisons **)
 
-Goal "(#89) $* #10 ~= #889";  
+Goal "(#89) $* #10 \\<noteq> #889";  
 by (Simp_tac 1); 
 result();
 
@@ -78,3 +78,45 @@
 Goal "(#1234567) $<= #1234567";  
 by (Simp_tac 1); 
 result();
+
+
+(*** Quotient and remainder!! [they could be faster] ***)
+
+Goal "#23 zdiv #3 = #7";
+by (Simp_tac 1); 
+result();
+
+Goal "#23 zmod #3 = #2";
+by (Simp_tac 1); 
+result();
+
+(** negative dividend **)
+
+Goal "#-23 zdiv #3 = #-8";
+by (Simp_tac 1); 
+result();
+
+Goal "#-23 zmod #3 = #1";
+by (Simp_tac 1); 
+result();
+
+(** negative divisor **)
+
+Goal "#23 zdiv #-3 = #-8";
+by (Simp_tac 1); 
+result();
+
+Goal "#23 zmod #-3 = #-1";
+by (Simp_tac 1); 
+result();
+
+(** Negative dividend and divisor **)
+
+Goal "#-23 zdiv #-3 = #7";
+by (Simp_tac 1); 
+result();
+
+Goal "#-23 zmod #-3 = #-2";
+by (Simp_tac 1); 
+result();
+