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
