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 cases where finiteness wasn't obvious (e.g. complement), but I abandoned that idea for some reason. Still, at the moment, I think that might be the best solution. Any thoughts? Manuel On 03/10/16 17:37, Andreas Lochbihler wrote: > 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 Code.abort (Gcd A))" > > Note that this does *not* pull in finite_UNIV. We could implement the > finiteness test by > > "finite (set xs) = True" > "finite (List.coset ys) = Code.abort (STR ''Finiteness test on > Complement'') ..." > > If one imports HOL/Library/Card_UNIV or Containers, then one has to > provide instances for finite_UNIV and a bunch of other type classes > anyways. That's the price of using more complicated libraries. > > AFAICS, it does not really matter whether the iteration combinator takes > an additional argument, because they can be expressed in terms of each > other: > > fold_default dflt f A x = (if finite A then dflst A else > Finite_Set.fold f A x) > Finite_Set.fold f A x = fold_default (%A. THE ... A ...) f A x > > The advantage of fold_default with a default value is that the > finiteness test remains inside the implementation library B whereas with > Finite_Set.fold, the finiteness test must be done whenever one wants to > use the combinator. So this might be an argument in favour of fold_default. > > Andreas > > On 03/10/16 16:27, Manuel Eberl wrote: >> 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 it is quite simply defined that way, but for Gcd/Lcm >> it is not. >> >> So the alternative would be something like "Gcd A = (if finite A then >> <combinator magic> else Code.abort …)". This does not work well either, >> because it requires being able to decide "finite A", which typically >> introduces the unwanted typeclass requirement "finite_UNIV". >> >> My suggestion would be a combinator that, in order to implement a >> function f :: 'a set => 'a, takes as arguments both a fold operation of >> type "'a cfc" /and/ the function f itself. >> >> It then performs the fold on any "finite by construction" set (e.g. sets >> represented by the "set" constructor) and returns "Code.abort … (f A)" >> for anything else (e.g. a set represented by the "coset" constructor). >> >> I planned on implementing this at some point, but I've quite a bit of >> other stuff to do and I wanted to discuss it first, so I never really >> got around to doing it. >> >> Cheers, >> >> Manuel >> >> >> On 03/10/16 16:15, Andreas Lochbihler wrote: >>> 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 yet. They >>> should work all kinds of big operators (setsum, setprod, Gcd, etc) and >>> could be added to the HOL library. >>> >>> Of course, some special case tricks no longer work if go for a generic >>> iteration operation. For example, one could prove "Gcd (List.coset xs) = >>> 1" for natural numbers and declare a code equation. Such things would no >>> longer be possible, but I am not sure whether they are done at all at >>> the moment. >>> >>> Manuel's suggestion of code_abort is a bit cleaner than René's use >>> Code.abort, because Code.abort does not work with normalisation by >>> evaluation whereas code_abort does. >>> >>> Best, >>> Andreas >>> >>> >>> On 03/10/16 15:29, Manuel Eberl wrote: >>>> 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 the operations from A depend >>>> on the implementation that is chosen for sets. A cannot give code >>>> equations for every possible implementation of sets, while B cannot >>>> possibly import every theory that has operations involving sets and >>>> give >>>> code equations for it. >>>> >>>> The best possible solution would be to imitate the way it is currently >>>> done for setsum, setprod, etc: Define a sufficiently general combinator >>>> that iterates over the set and give the code equations in A in terms of >>>> this combinator. Then B only has to reimplement this generic >>>> combinator. >>>> >>>> That would be the cleanest solution, but I'm not sure how such a >>>> combinator would look like. The folding operation would probably >>>> have to >>>> satisfy some associativity/commutativity laws and have that information >>>> available at the type level (similar to the cfc type in Containers). >>>> >>>> >>>> By the way, my current workaround for this problem is to declare all >>>> problematic constants as "code_abort". >>>> >>>> >>>> Cheers, >>>> >>>> Manuel >>>> >>>> >>>> On 03/10/16 15:21, Thiemann, Rene wrote: >>>>> 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 >>>>> _______________________________________________ >>>>> isabelle-dev mailing list >>>>> isabelle-...@in.tum.de >>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >>>>> >>>>> >>>>> >>>> _______________________________________________ >>>> isabelle-dev mailing list >>>> isabelle-...@in.tum.de >>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >>>> >>>> >>>> _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev