Theory Polynomial_Interpolation.Improved_Code_Equations
section ‹Improved Code Equations›
text ‹This theory contains improved code equations for certain algorithms.›
theory Improved_Code_Equations
imports
"HOL-Computational_Algebra.Polynomial"
"HOL-Library.Code_Target_Nat"
begin
subsection ‹@{const divmod_integer}.›
text ‹We improve @{thm divmod_integer_code} by deleting @{const sgn}-expressions.›
text ‹We guard the application of divmod-abs' with the condition @{term "x ≥ 0 ∧ y ≥ 0"},
so that application can be ensured on non-negative values. Hence, one can drop "abs" in
target language setup.›
definition divmod_abs' where
"x ≥ 0 ⟹ y ≥ 0 ⟹ divmod_abs' x y = Code_Numeral.divmod_abs x y"
lemma divmod_integer_code''[code]: "divmod_integer k l =
(if k = 0 then (0, 0)
else if l > 0 then
(if k > 0 then divmod_abs' k l
else case divmod_abs' (- k) l of (r, s) ⇒
if s = 0 then (- r, 0) else (- r - 1, l - s))
else if l = 0 then (0, k)
else apsnd uminus
(if k < 0 then divmod_abs' (-k) (-l)
else case divmod_abs' k (-l) of (r, s) ⇒
if s = 0 then (- r, 0) else (- r - 1, - l - s)))"
unfolding divmod_integer_code
by (cases "l = 0"; cases "l < 0"; cases "l > 0"; auto split: prod.splits simp: divmod_abs'_def divmod_abs_def)
code_printing
constant divmod_abs' ⇀
(SML) "IntInf.divMod/ ( _,/ _ )"
and (Eval) "Integer.div'_mod/ ( _ )/ ( _ )"
and (OCaml) "Z.div'_rem"
and (Haskell) "divMod/ ( _ )/ ( _ )"
and (Scala) "!((k: BigInt) => (l: BigInt) => l == 0 match { case true => (BigInt(0), k) case false => (k '/% l) })"
subsection ‹@{const Euclidean_Rings.divmod_nat}.›
text ‹We implement @{const Euclidean_Rings.divmod_nat} via @{const divmod_integer}
instead of invoking both division and modulo separately,
and we further simplify the case-analysis which is
performed in @{thm divmod_integer_code''}.›
lemma divmod_nat_code'[code]: "Euclidean_Rings.divmod_nat m n = (
let k = integer_of_nat m; l = integer_of_nat n
in map_prod nat_of_integer nat_of_integer
(if k = 0 then (0, 0)
else if l = 0 then (0,k) else
divmod_abs' k l))"
using divmod_nat_code [of m n]
by (simp add: divmod_abs'_def integer_of_nat_eq_of_nat Let_def)
subsection ‹@{const binomial}›
lemma binomial_code[code]:
"n choose k = (if k ≤ n then fact n div (fact k * fact (n - k)) else 0)"
using binomial_eq_0[of n k] binomial_altdef_nat[of k n] by simp
end