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

[Thiemann, Rene]

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)" 
  
export_code bar in Haskell 
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