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.4  
     1.5  subsection {* Syntactic division operations *}
     1.6  
     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.20  
    1.21  subsection {* Abstract division in commutative semirings. *}
    1.22  
    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.26  
    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.42  
    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.48    by (simp add: div_nat_def)
    1.49  
    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.55    by (simp add: mod_nat_def)
    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.68  
    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.73 -  apply (simp add: add_mult_distrib2)
    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.79 -by (auto simp add: mult.commute mult.left_commute divmod_nat_rel_def add_mult_distrib2 [symmetric] mod_lemma)
    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.89 +      apply (simp add: add_mult_distrib2)
    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.94 +    by (auto simp add: divmod_nat_rel_def algebra_simps add_mult_distrib2 [symmetric])
    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.99  
   1.100 @@ -1583,8 +1600,16 @@
   1.101    using odd_succ_div_two [of n] by simp
   1.102  
   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.116  
   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.122  
   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.127 +
   1.128 +definition mod_int where
   1.129 +  "a mod b = snd (divmod_int a b)"
   1.130 +
   1.131 +instance ..
   1.132 +
   1.133 +end
   1.134  
   1.135  lemma fst_divmod_int [simp]:
   1.136    "fst (divmod_int a b) = a div b"
   1.137    by (simp add: div_int_def)
   1.138  
   1.139 -definition mod_int where
   1.140 -  "a mod b = snd (divmod_int a b)"
   1.141 -
   1.142  lemma snd_divmod_int [simp]:
   1.143    "snd (divmod_int a b) = a mod b"
   1.144    by (simp add: mod_int_def)
   1.145  
   1.146 -instance ..
   1.147 -
   1.148 -end
   1.149 -
   1.150  lemma divmod_int_mod_div:
   1.151    "divmod_int p q = (p div q, p mod q)"
   1.152    by (simp add: prod_eq_iff)
   1.153 @@ -1909,7 +1934,7 @@
   1.154  ML {*
   1.155  structure Cancel_Div_Mod_Int = Cancel_Div_Mod
   1.156  (
   1.157 -  val div_name = @{const_name div};
   1.158 +  val div_name = @{const_name Rings.divide};
   1.159    val mod_name = @{const_name mod};
   1.160    val mk_binop = HOLogic.mk_binop;
   1.161    val mk_sum = Arith_Data.mk_sum HOLogic.intT;