# HG changeset patch
# User nipkow
# Date 1022824417 -7200
# Node ID 81ed5c6de8902e05f6dd7d38368947d757d92722
# Parent  596776f878f83f10b1f42a96cdfbf55ed667a20c
Now arith can deal with div/mod arbitrary nat numerals.

diff -r 596776f878f8 -r 81ed5c6de890 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Thu May 30 10:21:28 2002 +0200
+++ b/src/HOL/Divides.thy	Fri May 31 07:53:37 2002 +0200
@@ -50,6 +50,80 @@
 done
 
 lemma split_div:
+ "P(n div k :: nat) =
+ ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
+ (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
+proof
+  assume P: ?P
+  show ?Q
+  proof (cases)
+    assume "k = 0"
+    with P show ?Q by(simp add:DIVISION_BY_ZERO_DIV)
+  next
+    assume not0: "k \<noteq> 0"
+    thus ?Q
+    proof (simp, intro allI impI)
+      fix i j
+      assume n: "n = k*i + j" and j: "j < k"
+      show "P i"
+      proof (cases)
+	assume "i = 0"
+	with n j P show "P i" by simp
+      next
+	assume "i \<noteq> 0"
+	with not0 n j P show "P i" by(simp add:add_ac)
+      qed
+    qed
+  qed
+next
+  assume Q: ?Q
+  show ?P
+  proof (cases)
+    assume "k = 0"
+    with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV)
+  next
+    assume not0: "k \<noteq> 0"
+    with Q have R: ?R by simp
+    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
+    show ?P by(simp add:mod_div_equality2)
+  qed
+qed
+
+lemma split_mod:
+ "P(n mod k :: nat) =
+ ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
+ (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
+proof
+  assume P: ?P
+  show ?Q
+  proof (cases)
+    assume "k = 0"
+    with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD)
+  next
+    assume not0: "k \<noteq> 0"
+    thus ?Q
+    proof (simp, intro allI impI)
+      fix i j
+      assume "n = k*i + j" "j < k"
+      thus "P j" using not0 P by(simp add:add_ac mult_ac)
+    qed
+  qed
+next
+  assume Q: ?Q
+  show ?P
+  proof (cases)
+    assume "k = 0"
+    with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD)
+  next
+    assume not0: "k \<noteq> 0"
+    with Q have R: ?R by simp
+    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
+    show ?P by(simp add:mod_div_equality2)
+  qed
+qed
+
+(*
+lemma split_div:
 assumes m: "m \<noteq> 0"
 shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"
        (is "?P = ?Q")
@@ -91,5 +165,5 @@
   from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
   show ?P by(simp add:mod_div_equality2)
 qed
-
+*)
 end
diff -r 596776f878f8 -r 81ed5c6de890 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Thu May 30 10:21:28 2002 +0200
+++ b/src/HOL/Integ/NatBin.thy	Fri May 31 07:53:37 2002 +0200
@@ -22,9 +22,9 @@
 use "nat_bin.ML"
 setup nat_bin_arith_setup
 
-(* Enable arith to deal with div 2 and mod 2: *)
-declare split_div[of 2, simplified,arith_split]
-declare split_mod[of 2, simplified,arith_split]
+(* Enable arith to deal with div/mod k where k is a numeral: *)
+declare split_div[of _ _ "number_of k", standard, arith_split]
+declare split_mod[of _ _ "number_of k", standard, arith_split]
 
 lemma nat_number_of_Pls: "number_of Pls = (0::nat)"
   by (simp add: number_of_Pls nat_number_of_def)