Re: [isabelle-dev] Problem with factorial-ring in combination with containers

[Manuel Eberl]

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] Jenkins maintenance

[Manuel Eberl]

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
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Problem with factorial-ring in combination with containers

[Andreas Lochbihler]

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] Jenkins maintenance

[Lawrence Paulson]

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 to use) would be ideal.
Larry

> On 3 Oct 2016, at 16:12, Manuel Eberl  wrote:
> 
> I for one think that a big improvement would be a system where no one
> pushes to the repository directly: every push goes to a testing server,
> and if the test is successful, the changes can then automatically be
> merged into the repository without an additional test. This avoids the
> current duplication of tests where one first pushes to the testboard,
> waits for everything to run through, and then pushes to the repository
> where everything is tested again.

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Jenkins maintenance

[Manuel Eberl]

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 this
happen, and that's what Lars did – much of it, as I gather, in his free
time. I'm sure Lars does not object to others adapting this
infrastructure, and he has in fact already implemented a number of
suggestions for improvements.

>From what I have picked up, the new testing infrastructure we have now
is also a lot more adaptable and maintainable than anything we had
before. The words ‘industry standard’ may seem meaningless to you,
Makarius, but it cannot be denied that if /everyone/ does testing in a
certain way these days, then that is at least some evidence that it
might be a good idea to consider. Relying on the vague idea that things
never break because people never make mistakes does not seem like a
sensible approach to me – and once you accept that things /can/ break
because people /do/ make mistakes, prompt notification of /what/ broke
and /why/ is important.

No one is saying that the current state of affairs is optimal. I can
think of a number of possible improvements myself and have privately
communicated them to Lars, who seemed quite grateful for the feedback.

I for one think that a big improvement would be a system where no one
pushes to the repository directly: every push goes to a testing server,
and if the test is successful, the changes can then automatically be
merged into the repository without an additional test. This avoids the
current duplication of tests where one first pushes to the testboard,
waits for everything to run through, and then pushes to the repository
where everything is tested again. It would also be an effective
safeguard against breaking the repository (and possibly even the AFP),
which /does/ happen quite frequently. (cf. the current situation where
things have been broken for days) Another improvement I can think of is
that it would be good to have a little more control over testing:
aborting tests when they are not necessary anymore, testing only the
repository (and not the AFP) etc. All of this we can talk about and find
a solution in time.

It is important here to stress that none of us is working /against/
another – we all want the best possible infrastructure to do our work,
and I for one do not like the path this discussion has been taking. The
reality of it all is that our testing infrastructure was in shambles for
quite some time. Then Lars came along and put in a lot of effort to get
things up and running again. The main response on this mailing list were
vague insinuations that he does not understand how to do tests, or does
not care about doing it properly, which could hardly be farther removed
from the truth.

This email is getting a bit longer than I had planned, so let me
summarise my points once more for additional clarity:
– The current testing infrastructure is good, but not perfect, and we
should work together to make it better.
– The testboard, while also not perfect, has already become an
invaluable tool in my work on both Isabelle and the AFP.
– The tone of the discussion on this mailing list could occasionally do
with a little less passive-aggressiveness and fewer underhanded
insinuations.
– Lars deserves enormous gratitude from all of us for the work he put
into this so far. Of course, this does not mean that his decisions must
not be criticised, but when you work on something (mostly) alone in your
free time and the only public response you get is complaints, that's not
exactly uplifting.


Cheers and a happy Unification Day to all of you,

Manuel
___
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

[Manuel Eberl]

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

[Andreas Lochbihler]

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

[Manuel Eberl]

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

[Thiemann, Rene]

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] The HOL Light library

[Lawrence Paulson]

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 the next 
release.

Larry

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev