1.1 --- a/src/HOL/Divides.thy	Thu May 30 10:21:28 2002 +0200
     1.2 +++ b/src/HOL/Divides.thy	Fri May 31 07:53:37 2002 +0200
     1.3 @@ -50,6 +50,80 @@
     1.4  done
     1.5  
     1.6  lemma split_div:
     1.7 + "P(n div k :: nat) =
     1.8 + ((k = 0 \<longrightarrow> P 0) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P i)))"
     1.9 + (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
    1.10 +proof
    1.11 +  assume P: ?P
    1.12 +  show ?Q
    1.13 +  proof (cases)
    1.14 +    assume "k = 0"
    1.15 +    with P show ?Q by(simp add:DIVISION_BY_ZERO_DIV)
    1.16 +  next
    1.17 +    assume not0: "k \<noteq> 0"
    1.18 +    thus ?Q
    1.19 +    proof (simp, intro allI impI)
    1.20 +      fix i j
    1.21 +      assume n: "n = k*i + j" and j: "j < k"
    1.22 +      show "P i"
    1.23 +      proof (cases)
    1.24 +	assume "i = 0"
    1.25 +	with n j P show "P i" by simp
    1.26 +      next
    1.27 +	assume "i \<noteq> 0"
    1.28 +	with not0 n j P show "P i" by(simp add:add_ac)
    1.29 +      qed
    1.30 +    qed
    1.31 +  qed
    1.32 +next
    1.33 +  assume Q: ?Q
    1.34 +  show ?P
    1.35 +  proof (cases)
    1.36 +    assume "k = 0"
    1.37 +    with Q show ?P by(simp add:DIVISION_BY_ZERO_DIV)
    1.38 +  next
    1.39 +    assume not0: "k \<noteq> 0"
    1.40 +    with Q have R: ?R by simp
    1.41 +    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
    1.42 +    show ?P by(simp add:mod_div_equality2)
    1.43 +  qed
    1.44 +qed
    1.45 +
    1.46 +lemma split_mod:
    1.47 + "P(n mod k :: nat) =
    1.48 + ((k = 0 \<longrightarrow> P n) \<and> (k \<noteq> 0 \<longrightarrow> (!i. !j<k. n = k*i + j \<longrightarrow> P j)))"
    1.49 + (is "?P = ?Q" is "_ = (_ \<and> (_ \<longrightarrow> ?R))")
    1.50 +proof
    1.51 +  assume P: ?P
    1.52 +  show ?Q
    1.53 +  proof (cases)
    1.54 +    assume "k = 0"
    1.55 +    with P show ?Q by(simp add:DIVISION_BY_ZERO_MOD)
    1.56 +  next
    1.57 +    assume not0: "k \<noteq> 0"
    1.58 +    thus ?Q
    1.59 +    proof (simp, intro allI impI)
    1.60 +      fix i j
    1.61 +      assume "n = k*i + j" "j < k"
    1.62 +      thus "P j" using not0 P by(simp add:add_ac mult_ac)
    1.63 +    qed
    1.64 +  qed
    1.65 +next
    1.66 +  assume Q: ?Q
    1.67 +  show ?P
    1.68 +  proof (cases)
    1.69 +    assume "k = 0"
    1.70 +    with Q show ?P by(simp add:DIVISION_BY_ZERO_MOD)
    1.71 +  next
    1.72 +    assume not0: "k \<noteq> 0"
    1.73 +    with Q have R: ?R by simp
    1.74 +    from not0 R[THEN spec,of "n div k",THEN spec, of "n mod k"]
    1.75 +    show ?P by(simp add:mod_div_equality2)
    1.76 +  qed
    1.77 +qed
    1.78 +
    1.79 +(*
    1.80 +lemma split_div:
    1.81  assumes m: "m \<noteq> 0"
    1.82  shows "P(n div m :: nat) = (!i. !j<m. n = m*i + j \<longrightarrow> P i)"
    1.83         (is "?P = ?Q")
    1.84 @@ -91,5 +165,5 @@
    1.85    from m Q[THEN spec,of "n div m",THEN spec, of "n mod m"]
    1.86    show ?P by(simp add:mod_div_equality2)
    1.87  qed
    1.88 -
    1.89 +*)
    1.90  end

     2.1 --- a/src/HOL/Integ/NatBin.thy	Thu May 30 10:21:28 2002 +0200
     2.2 +++ b/src/HOL/Integ/NatBin.thy	Fri May 31 07:53:37 2002 +0200
     2.3 @@ -22,9 +22,9 @@
     2.4  use "nat_bin.ML"
     2.5  setup nat_bin_arith_setup
     2.6  
     2.7 -(* Enable arith to deal with div 2 and mod 2: *)
     2.8 -declare split_div[of 2, simplified,arith_split]
     2.9 -declare split_mod[of 2, simplified,arith_split]
    2.10 +(* Enable arith to deal with div/mod k where k is a numeral: *)
    2.11 +declare split_div[of _ _ "number_of k", standard, arith_split]
    2.12 +declare split_mod[of _ _ "number_of k", standard, arith_split]
    2.13  
    2.14  lemma nat_number_of_Pls: "number_of Pls = (0::nat)"
    2.15    by (simp add: number_of_Pls nat_number_of_def)