src/HOL/Divides.thy
changeset 60930 dd8ab7252ba2
parent 60868 dd18c33c001e
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Divides.thy	Thu Aug 13 10:05:58 2015 +0200
     1.2 +++ b/src/HOL/Divides.thy	Thu Aug 13 15:22:11 2015 +0200
     1.3 @@ -2311,15 +2311,18 @@
     1.4      pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
     1.5      zmod_zmult2_eq zdiv_zmult2_eq)
     1.6  
     1.7 -definition adjust_div :: "int \<times> int \<Rightarrow> int"
     1.8 +context
     1.9 +begin
    1.10 +  
    1.11 +qualified definition adjust_div :: "int \<times> int \<Rightarrow> int"
    1.12  where
    1.13    "adjust_div qr = (let (q, r) = qr in q + of_bool (r \<noteq> 0))"
    1.14  
    1.15 -lemma adjust_div_eq [simp, code]:
    1.16 +qualified lemma adjust_div_eq [simp, code]:
    1.17    "adjust_div (q, r) = q + of_bool (r \<noteq> 0)"
    1.18    by (simp add: adjust_div_def)
    1.19  
    1.20 -definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
    1.21 +qualified definition adjust_mod :: "int \<Rightarrow> int \<Rightarrow> int"
    1.22  where
    1.23    [simp]: "adjust_mod l r = (if r = 0 then 0 else l - r)"
    1.24  
    1.25 @@ -2375,6 +2378,8 @@
    1.26    "1 mod - numeral n = - adjust_mod (numeral n) (snd (divmod Num.One n) :: int)"
    1.27    using numeral_mod_minus_numeral [of Num.One n] by simp
    1.28  
    1.29 +end
    1.30 +
    1.31  
    1.32  subsubsection \<open>Further properties\<close>
    1.33  
    1.34 @@ -2574,10 +2579,10 @@
    1.35          one_div_minus_numeral one_mod_minus_numeral
    1.36          numeral_div_numeral numeral_mod_numeral minus_numeral_div_numeral minus_numeral_mod_numeral
    1.37          numeral_div_minus_numeral numeral_mod_minus_numeral
    1.38 -        div_minus_minus mod_minus_minus adjust_div_eq of_bool_eq one_neq_zero
    1.39 +        div_minus_minus mod_minus_minus Divides.adjust_div_eq of_bool_eq one_neq_zero
    1.40          numeral_neq_zero neg_equal_0_iff_equal arith_simps arith_special divmod_trivial
    1.41          divmod_cancel divmod_steps divmod_step_eq fst_conv snd_conv numeral_One
    1.42 -        case_prod_beta rel_simps adjust_mod_def div_minus1_right mod_minus1_right
    1.43 +        case_prod_beta rel_simps Divides.adjust_mod_def div_minus1_right mod_minus1_right
    1.44          minus_minus numeral_times_numeral mult_zero_right mult_1_right}
    1.45          @ [@{lemma "0 = 0 \<longleftrightarrow> True" by simp}]);
    1.46        fun prepare_simpset ctxt = HOL_ss |> Simplifier.simpset_map ctxt
    1.47 @@ -2602,10 +2607,10 @@
    1.48      "k mod Int.Neg Num.One = 0"
    1.49      "Int.Pos m div Int.Pos n = (fst (divmod m n) :: int)"
    1.50      "Int.Pos m mod Int.Pos n = (snd (divmod m n) :: int)"
    1.51 -    "Int.Neg m div Int.Pos n = - (adjust_div (divmod m n) :: int)"
    1.52 -    "Int.Neg m mod Int.Pos n = adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
    1.53 -    "Int.Pos m div Int.Neg n = - (adjust_div (divmod m n) :: int)"
    1.54 -    "Int.Pos m mod Int.Neg n = - adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
    1.55 +    "Int.Neg m div Int.Pos n = - (Divides.adjust_div (divmod m n) :: int)"
    1.56 +    "Int.Neg m mod Int.Pos n = Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
    1.57 +    "Int.Pos m div Int.Neg n = - (Divides.adjust_div (divmod m n) :: int)"
    1.58 +    "Int.Pos m mod Int.Neg n = - Divides.adjust_mod (Int.Pos n) (snd (divmod m n) :: int)"
    1.59      "Int.Neg m div Int.Neg n = (fst (divmod m n) :: int)"
    1.60      "Int.Neg m mod Int.Neg n = - (snd (divmod m n) :: int)"
    1.61    by simp_all