[isabelle] Wellsortedness error in code equation Gcd_nat_inst.Lcm_nat



When generalizing the following function from

  definition primitive :: "int poly ⇒ int × int poly"

to

   definition primitive :: "'a::{ring_div,Gcd} poly ⇒ 'a × 'a poly"
   where
     "primitive p = (
       let d = Gcd (set (coeffs p))
       in (d, (*sdiv d*) p))"

this is accepted by the system (with "sdiv d" as well).

However evaluation works differently: While the "int" version works as expected, the version generalized above reports an error (the same with and without "sdiv d"):

   value "primitive [:2::int, 4, 6, 8:] = (2, [:1, 2, 3, 4:])"

   Wellsortedness error
   (in code equation Gcd_nat_inst.Lcm_nat ?m ≡
                     if finite ?m
                     then Finite_Set.fold gcd_nat_inst.lcm_nat
                       one_nat_inst.one_nat ?m
                     else zero_nat_inst.zero_nat):
   Type nat not of sort finite
   No type arity nat :: finite

Is there somebody who immediately knows a way out (and thus helps me to avoid delving into unexplored depths of Isabelle) ?

If not, any hint is appreciated!

Many thanks in advance,
Walther

Attachment: Two_Sorts.thy
Description: application/extension-thy



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.