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
This, too, is an industry standard. Of course, I am not the expert, but
I'm pretty sure this is achievable with the system we have – if there is
a consensus that this is what we want, that is.
Manuel
___
isabelle-dev mailing list
isabelle-...@in.tum.de
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’d be happy with this, if it’s achievable.
I’ve only tried the testboard once or twice; I find it too easy to do the wrong
thing when you have a choice of targets to push to, and I have a powerful
machine so I prefer to test there. But a mechanism of the sort you describe
(provided it’s easy
I have decided to add my own opinions to this debate. My knowledge of
the old testing system is limited, but I hope my perspective will still
hold some interest.
First of all, a usable testing infrastructure does not grow overnight by
itself. Someone has to put in a lot of time and effort to make
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
I’ve just added a lot more advanced material from HOL Light. There isn't much
about this in the NEWS file; unfortunately there is no headline result to
mention or even a dominant theme. Nor can we say that the entire library has
been ported. But I still think it’s a significant development for
10 matches
Mail list logo
