author nipkow Fri, 31 May 2002 07:53:37 +0200 changeset 13189 81ed5c6de890 parent 13188 596776f878f8 child 13190 172f65d0c3d1
Now arith can deal with div/mod arbitrary nat numerals.
 src/HOL/Divides.thy file | annotate | diff | comparison | revisions src/HOL/Integ/NatBin.thy file | annotate | diff | comparison | revisions
```--- 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"
+      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"]
+  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"
+    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"]
+  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"]
qed
-
+*)
end```
```--- 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)"