# HG changeset patch
# User paulson
# Date 965292750 -7200
# Node ID 0f3ee1f89ca87b71105244b1e750361adf27ce2f
# Parent  4d01dbf6ded7b4f48b7d68b0ee6289429c76f379
introduction of integer exponentiation

diff -r 4d01dbf6ded7 -r 0f3ee1f89ca8 src/HOL/Integ/IntArith.ML
--- 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";
+
diff -r 4d01dbf6ded7 -r 0f3ee1f89ca8 src/HOL/Integ/IntDiv.ML
--- 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);
diff -r 4d01dbf6ded7 -r 0f3ee1f89ca8 src/HOL/Integ/IntPower.ML
--- /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";
+
diff -r 4d01dbf6ded7 -r 0f3ee1f89ca8 src/HOL/Integ/IntPower.thy
--- /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
diff -r 4d01dbf6ded7 -r 0f3ee1f89ca8 src/HOL/Integ/NatBin.thy
--- 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