Re: [isabelle-dev] Problem with factorial-ring in combination with containers
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 finite_UNIV for the types on which they want to execute big operators. But most users do not import Card_UNIV, so they are not affected. Using a copy of "finite" is also possible and maybe even a good idea. The existing constant "finite" is an important concept in many theorems. Using a copy "finite_code" in the code equations separates code generation from logical reasoning, which is often a good thing. However, if we then implement the existing constant "finite" using the equation "finite = finite_code" then we have not gained much and introduced some amount of duplication. And if we stick to the existing setup for "finite" with "finite (set xs) = True" "finite (List.coset ys) = Code.abort ... ..." then we run into the very same pattern-match problems that René reported. If we delete all code equations for "finite", then this renders quickcheck a little bit less useful, because it can no longer work on theorems involving finiteness. But I am not sure how much quickcheck can do in practice for theorems involving "finite". Andreas On 03/10/16 22:51, Manuel Eberl wrote: 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 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
Re: [isabelle-dev] Problem with factorial-ring in combination with containers
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 >> 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
Re: [isabelle-dev] Problem with factorial-ring in combination with containers
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 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
Re: [isabelle-dev] Problem with factorial-ring in combination with containers
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 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 ⇒
Re: [isabelle-dev] Problem with factorial-ring in combination with containers
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
Re: [isabelle-dev] Problem with factorial-ring in combination with containers
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] Problem with factorial-ring in combination with containers
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
