Hi Manuel,
My point with "finite" was that for the current default setup, you don't need any type
class instantiations (see the code equations below). Only if someone imports Card_UNIV
from HOL/Library (e.g., for FinFun or for Containers), he or she has to do the
instantiations for
Hm, that sounds reasonable.
However, I am not sure whether using "finite" is really such a good
idea; it will lead to people having to instantiate "finite_UNIV" for all
kinds of things all the time.
I think I once considered a similar solution using a copy of "finite"
that does Code.abort in
Hi Manuel,
Indeed, generic iteration over a set is only well-defined if the set is finite. For an
infinite set, the generic iteration combinator returns an unspecified value, not 0 or 1.
In fact, I had imagined a code equation like you described, namely
"Gcd A = (if finite A then ... else
I'm afraid it's not quite as easy as that. You cannot use the existing
combinators for comp_fun_commute for Gcd. For infinite sets, these
combinators return the neutral element (i.e. "0" for Gcd and "1" for
Lcm), but not every infinite set has Gcd 0 or Lcm 1. For setsum/setprod,
this works because
Hi René and Manuel,
Indeed, for sets, expressing the code equations in terms of a generic iteration operation
on sets would do the job for most of the cases. The comp_fun_commute and comp_fun_idem
types in Containers precisely do this, but they have not been integrated in the HOL
library
This is a problem that I have given quite some thought in the past. The
problem is the following: You have a theory A providing certain
operations on sets (in this case: Gcd) and a theory B providing
implementations for sets (in this case: Containers).
The problem is that the code equations for
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
