# [isabelle-dev] Problem with factorial-ring in combination with containers

Thiemann, Rene Rene.Thiemann at uibk.ac.at
Mon Oct 3 15:21:09 CEST 2016

```Dear all,

in the following theory, the export-code fails:

(Isabelle 957ba35d1338, AFP 618f04bf906f)

theory Problem
imports
"~~/src/HOL/Library/Polynomial_Factorial"
"\$AFP/thys/Containers/Set_Impl"
begin

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)"

end

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