[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

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 mailing list