# 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 \ P 0) \ (k \ 0 \ (!i. !j P i)))" + (is "?P = ?Q" is "_ = (_ \ (_ \ ?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 \ 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 \ 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 \ 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 \ P n) \ (k \ 0 \ (!i. !j P j)))" + (is "?P = ?Q" is "_ = (_ \ (_ \ ?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 \ 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 \ 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 \ 0" shows "P(n div m :: nat) = (!i. !j 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)