[isabelle-dev] Problem with factorial-ring in combination with containers
Rene.Thiemann at uibk.ac.at
Mon Oct 3 15:21:09 CEST 2016
in the following theory, the export-code fails:
(Isabelle 957ba35d1338, AFP 618f04bf906f)
definition foo :: "'a :: factorial_semiring_gcd ⇒ 'a ⇒ 'a" where
"foo x y = gcd y x"
definition bar :: "int ⇒ int" where
"bar x = foo x (x - 1)"
export_code bar in Haskell
The problem arises from two issues:
- factorial_semiring_gcd requires code for
Gcd :: “Set ‘a => ‘a”, not only for the binary “gcd :: ‘a => ‘a => ‘a”!
- the code-equation for Gcd is Gcd_eucl_set: "Gcd_eucl (set xs) = foldl gcd_eucl 0 xs”
where “set” is only a constructor if one does not load the container-library.
It would be nice, if one can either alter factorial_semiring_gcd so that it does not
require “Gcd” anymore, or if the code-equation is modified in a way that permits
co-existence with containers. (Of course, similarly for Lcm).
With best regards,
Akihisa, Sebastiaan, and René
PS: We currently solve the problem by disabling Gcd and Lcm as follows:
lemma [code]: "(Gcd_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Gcd on sets'') (λ _. Gcd_eucl)" by simp
lemma [code]: "(Lcm_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Lcm on sets'') (λ _. Lcm_eucl)" by simp
More information about the isabelle-dev