src/HOL/Divides.thy
 changeset 60352 d46de31a50c4 parent 59833 ab828c2c5d67 child 60353 838025c6e278
1.1 --- a/src/HOL/Divides.thy	Mon Jun 01 18:59:21 2015 +0200
1.2 +++ b/src/HOL/Divides.thy	Mon Jun 01 18:59:21 2015 +0200
1.3 @@ -11,10 +11,15 @@
1.5  subsection {* Syntactic division operations *}
1.7 -class div = dvd +
1.8 -  fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "div" 70)
1.9 -    and mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "mod" 70)
1.10 -
1.11 +class div = dvd + divide +
1.12 +  fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "mod" 70)
1.13 +begin
1.14 +
1.15 +abbreviation div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "div" 70)
1.16 +where
1.17 +  "op div \<equiv> divide"
1.18 +
1.19 +end
1.21  subsection {* Abstract division in commutative semirings. *}
1.23 @@ -951,19 +956,26 @@
1.24    shows "divmod_nat m n = qr"
1.25    using assms by (auto intro: divmod_nat_rel_unique divmod_nat_rel_divmod_nat)
1.27 +instantiation nat :: "Divides.div"
1.28 +begin
1.29 +
1.30 +definition divide_nat where
1.31 +  div_nat_def: "divide m n = fst (divmod_nat m n)"
1.32 +
1.33 +definition mod_nat where
1.34 +  "m mod n = snd (divmod_nat m n)"
1.35 +
1.36 +instance ..
1.37 +
1.38 +end
1.39 +
1.40  instantiation nat :: semiring_div
1.41  begin
1.43 -definition div_nat where
1.44 -  "m div n = fst (divmod_nat m n)"
1.45 -
1.46  lemma fst_divmod_nat [simp]:
1.47    "fst (divmod_nat m n) = m div n"
1.50 -definition mod_nat where
1.51 -  "m mod n = snd (divmod_nat m n)"
1.52 -
1.53  lemma snd_divmod_nat [simp]:
1.54    "snd (divmod_nat m n) = m mod n"
1.56 @@ -1069,7 +1081,7 @@
1.57  ML {*
1.58  structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
1.59  (
1.60 -  val div_name = @{const_name div};
1.61 +  val div_name = @{const_name divide};
1.62    val mod_name = @{const_name mod};
1.63    val mk_binop = HOLogic.mk_binop;
1.64    val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
1.65 @@ -1184,18 +1196,23 @@
1.66    "(a+b) div (c::nat) = a div c + b div c + ((a mod c + b mod c) div c)"
1.67  by (blast intro: divmod_nat_rel_add1_eq [THEN div_nat_unique] divmod_nat_rel)
1.69 -lemma mod_lemma: "[| (0::nat) < c; r < b |] ==> b * (q mod c) + r < b * c"
1.70 -  apply (cut_tac m = q and n = c in mod_less_divisor)
1.71 -  apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
1.72 -  apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
1.74 -  done
1.75 -
1.76  lemma divmod_nat_rel_mult2_eq:
1.77 -  "divmod_nat_rel a b (q, r)
1.78 -   \<Longrightarrow> divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
1.80 -
1.81 +  assumes "divmod_nat_rel a b (q, r)"
1.82 +  shows "divmod_nat_rel a (b * c) (q div c, b *(q mod c) + r)"
1.83 +proof -
1.84 +  { assume "r < b" and "0 < c"
1.85 +    then have "b * (q mod c) + r < b * c"
1.86 +      apply (cut_tac m = q and n = c in mod_less_divisor)
1.87 +      apply (drule_tac [2] m = "q mod c" in less_imp_Suc_add, auto)
1.88 +      apply (erule_tac P = "%x. lhs < rhs x" for lhs rhs in ssubst)
1.90 +      done
1.91 +    then have "r + b * (q mod c) < b * c"
1.92 +      by (simp add: ac_simps)
1.93 +  } with assms show ?thesis
1.95 +qed
1.96 +
1.97  lemma div_mult2_eq: "a div (b * c) = (a div b) div (c::nat)"
1.98  by (force simp add: divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN div_nat_unique])
1.100 @@ -1583,8 +1600,16 @@
1.101    using odd_succ_div_two [of n] by simp
1.103  lemma odd_two_times_div_two_nat [simp]:
1.104 -  "odd n \<Longrightarrow> 2 * (n div 2) = n - (1 :: nat)"
1.105 -  using odd_two_times_div_two_succ [of n] by simp
1.106 +  assumes "odd n"
1.107 +  shows "2 * (n div 2) = n - (1 :: nat)"
1.108 +proof -
1.109 +  from assms have "2 * (n div 2) + 1 = n"
1.110 +    by (rule odd_two_times_div_two_succ)
1.111 +  then have "Suc (2 * (n div 2)) - 1 = n - 1"
1.112 +    by simp
1.113 +  then show ?thesis
1.114 +    by simp
1.115 +qed
1.117  lemma odd_Suc_minus_one [simp]:
1.118    "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
1.119 @@ -1669,24 +1694,24 @@
1.120  instantiation int :: Divides.div
1.121  begin
1.123 -definition div_int where
1.124 -  "a div b = fst (divmod_int a b)"
1.125 +definition divide_int where
1.126 +  div_int_def: "divide a b = fst (divmod_int a b)"
1.128 +definition mod_int where
1.129 +  "a mod b = snd (divmod_int a b)"
1.131 +instance ..
1.133 +end
1.135  lemma fst_divmod_int [simp]:
1.136    "fst (divmod_int a b) = a div b"
1.139 -definition mod_int where
1.140 -  "a mod b = snd (divmod_int a b)"
1.142  lemma snd_divmod_int [simp]:
1.143    "snd (divmod_int a b) = a mod b"