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.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.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.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
```