src/HOL/Code_Numeral.thy
changeset 53069 d165213e3924
parent 52435 6646bb548c6b
child 54489 03ff4d1e6784
     1.1 --- a/src/HOL/Code_Numeral.thy	Sun Aug 18 15:29:50 2013 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Sun Aug 18 15:29:50 2013 +0200
     1.3 @@ -223,6 +223,21 @@
     1.4    "of_nat (nat_of_integer k) = max 0 k"
     1.5    by transfer auto
     1.6  
     1.7 +instance integer :: semiring_numeral_div
     1.8 +  by intro_classes (transfer,
     1.9 +    fact semiring_numeral_div_class.diff_invert_add1
    1.10 +    semiring_numeral_div_class.le_add_diff_inverse2
    1.11 +    semiring_numeral_div_class.mult_div_cancel
    1.12 +    semiring_numeral_div_class.div_less
    1.13 +    semiring_numeral_div_class.mod_less
    1.14 +    semiring_numeral_div_class.div_positive
    1.15 +    semiring_numeral_div_class.mod_less_eq_dividend
    1.16 +    semiring_numeral_div_class.pos_mod_bound
    1.17 +    semiring_numeral_div_class.pos_mod_sign
    1.18 +    semiring_numeral_div_class.mod_mult2_eq
    1.19 +    semiring_numeral_div_class.div_mult2_eq
    1.20 +    semiring_numeral_div_class.discrete)+
    1.21 +
    1.22  
    1.23  subsection {* Code theorems for target language integers *}
    1.24  
    1.25 @@ -347,24 +362,15 @@
    1.26    "snd (divmod_abs k l) = \<bar>k\<bar> mod \<bar>l\<bar>"
    1.27    by (simp add: divmod_abs_def)
    1.28  
    1.29 -lemma divmod_abs_terminate_code [code]:
    1.30 -  "divmod_abs (Neg k) (Neg l) = divmod_abs (Pos k) (Pos l)"
    1.31 -  "divmod_abs (Neg k) (Pos l) = divmod_abs (Pos k) (Pos l)"
    1.32 -  "divmod_abs (Pos k) (Neg l) = divmod_abs (Pos k) (Pos l)"
    1.33 +lemma divmod_abs_code [code]:
    1.34 +  "divmod_abs (Pos k) (Pos l) = divmod k l"
    1.35 +  "divmod_abs (Neg k) (Neg l) = divmod k l"
    1.36 +  "divmod_abs (Neg k) (Pos l) = divmod k l"
    1.37 +  "divmod_abs (Pos k) (Neg l) = divmod k l"
    1.38    "divmod_abs j 0 = (0, \<bar>j\<bar>)"
    1.39    "divmod_abs 0 j = (0, 0)"
    1.40    by (simp_all add: prod_eq_iff)
    1.41  
    1.42 -lemma divmod_abs_rec_code [code]:
    1.43 -  "divmod_abs (Pos k) (Pos l) =
    1.44 -    (let j = sub k l in
    1.45 -       if j < 0 then (0, Pos k)
    1.46 -       else let (q, r) = divmod_abs j (Pos l) in (q + 1, r))"
    1.47 -  apply (simp add: prod_eq_iff Let_def prod_case_beta)
    1.48 -  apply transfer
    1.49 -  apply (simp add: sub_non_negative sub_negative div_pos_pos_trivial mod_pos_pos_trivial div_pos_geq mod_pos_geq)
    1.50 -  done
    1.51 -
    1.52  lemma divmod_integer_code [code]:
    1.53    "divmod_integer k l =
    1.54      (if k = 0 then (0, 0) else if l = 0 then (0, k) else