--- a/src/HOL/Integ/IntArith.ML Thu Aug 03 10:46:01 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML Thu Aug 03 10:52:30 2000 +0200
@@ -67,3 +67,53 @@
simpset() addsimps [int_0_less_mult_iff,
linorder_not_less RS sym]));
qed "zmult_le_0_iff";
+
+
+(*** Products and 1, by T. M. Rasmussen ***)
+
+Goal "(m = m*(n::int)) = (n = #1 | m = #0)";
+by Auto_tac;
+by (stac (zmult_cancel1 RS sym) 1);
+by Auto_tac;
+qed "zmult_eq_self_iff";
+
+Goal "[| #1 < m; #1 < n |] ==> #1 < m*(n::int)";
+by (res_inst_tac [("z2.0","#1*n")] zless_trans 1);
+by (rtac zmult_zless_mono1 2);
+by (ALLGOALS Asm_simp_tac);
+qed "zless_1_zmult";
+
+Goal "[| #0 < n; n ~= #1 |] ==> #1 < (n::int)";
+by (arith_tac 1);
+val lemma = result();
+
+Goal "#0 < (m::int) ==> (m * n = #1) = (m = #1 & n = #1)";
+by Auto_tac;
+by (case_tac "m=#1" 1);
+by (case_tac "n=#1" 2);
+by (case_tac "m=#1" 4);
+by (case_tac "n=#1" 5);
+by Auto_tac;
+by distinct_subgoals_tac;
+by (subgoal_tac "#1<m*n" 1);
+by (Asm_full_simp_tac 1);
+by (rtac zless_1_zmult 1);
+by (ALLGOALS (rtac lemma));
+by Auto_tac;
+by (subgoal_tac "#0<m*n" 1);
+by (Asm_simp_tac 2);
+by (dtac (int_0_less_mult_iff RS iffD1) 1);
+by Auto_tac;
+qed "pos_zmult_eq_1_iff";
+
+Goal "(m*n = (#1::int)) = ((m = #1 & n = #1) | (m = #-1 & n = #-1))";
+by (case_tac "#0<m" 1);
+by (asm_simp_tac (simpset() addsimps [pos_zmult_eq_1_iff]) 1);
+by (case_tac "m=#0" 1);
+by (Asm_simp_tac 1);
+by (subgoal_tac "#0 < -m" 1);
+by (arith_tac 2);
+by (dres_inst_tac [("n","-n")] pos_zmult_eq_1_iff 1);
+by Auto_tac;
+qed "zmult_eq_1_iff";
+
--- a/src/HOL/Integ/IntDiv.ML Thu Aug 03 10:46:01 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML Thu Aug 03 10:52:30 2000 +0200
@@ -567,6 +567,18 @@
by (blast_tac (claset() addIs [quorem_div_mod RS lemma RS quorem_mod]) 1);
qed "zmod_zmult1_eq";
+Goal "(a*b) mod (c::int) = ((a mod c) * b) mod c";
+by (rtac trans 1);
+by (res_inst_tac [("s","b*a mod c")] trans 1);
+by (rtac zmod_zmult1_eq 2);
+by (ALLGOALS (simp_tac (simpset() addsimps [zmult_commute])));
+qed "zmod_zmult1_eq'";
+
+Goal "(a*b) mod (c::int) = ((a mod c) * (b mod c)) mod c";
+by (rtac (zmod_zmult1_eq' RS trans) 1);
+by (rtac zmod_zmult1_eq 1);
+qed "zmod_zmult_distrib";
+
Goal "b ~= (#0::int) ==> (a*b) div b = a";
by (asm_simp_tac (simpset() addsimps [zdiv_zmult1_eq]) 1);
qed "zdiv_zmult_self1";
@@ -615,7 +627,6 @@
MRS lemma RS quorem_mod]) 1);
qed "zmod_zadd1_eq";
-
Goal "(a mod b) div b = (#0::int)";
by (zdiv_undefined_case_tac "b = #0" 1);
by (auto_tac (claset(),
@@ -634,6 +645,20 @@
qed "mod_mod_trivial";
Addsimps [mod_mod_trivial];
+Goal "(a+b) mod (c::int) = ((a mod c) + b) mod c";
+by (rtac (trans RS sym) 1);
+by (rtac zmod_zadd1_eq 1);
+by (Simp_tac 1);
+by (rtac (zmod_zadd1_eq RS sym) 1);
+qed "zmod_zadd_left_eq";
+
+Goal "(a+b) mod (c::int) = (a + (b mod c)) mod c";
+by (rtac (trans RS sym) 1);
+by (rtac zmod_zadd1_eq 1);
+by (Simp_tac 1);
+by (rtac (zmod_zadd1_eq RS sym) 1);
+qed "zmod_zadd_right_eq";
+
Goal "a ~= (#0::int) ==> (a+b) div a = b div a + #1";
by (asm_simp_tac (simpset() addsimps [zdiv_zadd1_eq]) 1);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/IntPower.ML Thu Aug 03 10:52:30 2000 +0200
@@ -0,0 +1,41 @@
+(* Title: IntPower.thy
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+
+Integer powers
+*)
+
+
+Goal "((x::int) mod m)^y mod m = x^y mod m";
+by (induct_tac "y" 1);
+by Auto_tac;
+by (rtac (zmod_zmult1_eq RS trans) 1);
+by (Asm_simp_tac 1);
+by (rtac (zmod_zmult_distrib RS sym) 1);
+qed "zpower_zmod";
+
+Goal "#1^y = (#1::int)";
+by (induct_tac "y" 1);
+by Auto_tac;
+qed "zpower_1";
+Addsimps [zpower_1];
+
+Goal "(x*z)^y = ((x^y)*(z^y)::int)";
+by (induct_tac "y" 1);
+by Auto_tac;
+qed "zpower_zmult_distrib";
+
+Goal "x^(y+z) = ((x^y)*(x^z)::int)";
+by (induct_tac "y" 1);
+by Auto_tac;
+qed "zpower_zadd_distrib";
+
+Goal "(x^y)^z = (x^(y*z)::int)";
+by (induct_tac "y" 1);
+by Auto_tac;
+by (stac zpower_zmult_distrib 1);
+by (stac zpower_zadd_distrib 1);
+by (Asm_simp_tac 1);
+qed "zpower_zpower";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/IntPower.thy Thu Aug 03 10:52:30 2000 +0200
@@ -0,0 +1,18 @@
+(* Title: IntPower.thy
+ ID: $Id$
+ Author: Thomas M. Rasmussen
+ Copyright 2000 University of Cambridge
+
+Integer powers
+*)
+
+IntPower = IntDiv +
+
+instance
+ int :: {power}
+
+primrec
+ power_0 "p ^ 0 = #1"
+ power_Suc "p ^ (Suc n) = (p::int) * (p ^ n)"
+
+end
--- a/src/HOL/Integ/NatBin.thy Thu Aug 03 10:46:01 2000 +0200
+++ b/src/HOL/Integ/NatBin.thy Thu Aug 03 10:52:30 2000 +0200
@@ -8,7 +8,7 @@
This case is simply reduced to that for the non-negative integers
*)
-NatBin = IntDiv +
+NatBin = IntPower +
instance
nat :: number