Re: [isabelle-dev] Remaining uses of defer_recdef?

[Makarius]

On Thu, 11 Jun 2015, Larry Paulson wrote:


We must go forward and not back.


Just to conclude the original question on this thread: 'defer_recdef' is 
unused, untested, unmaintained.  So it falls under the normal 
garbage-collection of source code.  I will remove it next week or so, 
unless there is another strong argument to keep it.


In contrast, the main 'recdef' is maintained a bit longer; of course 
without any plans to "localize" it.  Asymptotically, 'function' should 
take over its role, but there is presently no attempt to change the 
situation.



Makarius

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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

Absolutely, totally. We must go forward and not back.
Larry

> On 11 Jun 2015, at 13:27, Tobias Nipkow  wrote:
> 
> 
> On 11/06/2015 14:00, Makarius wrote:
>> Is that just a question of which side of the river has greener grass?
> 
> "Function" does a number of things very nicely, eg nested recursion and 
> partiality. That is worth taking on board.
> 
> Tobias
> 

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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Tobias Nipkow]

On 11/06/2015 14:00, Makarius wrote:

Is that just a question of which side of the river has greener grass?


"Function" does a number of things very nicely, eg nested recursion and 
partiality. That is worth taking on board.


Tobias



smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Makarius]

On Thu, 11 Jun 2015, Larry Paulson wrote:

It looks like there is more work to do here then. Clearly the old 
package is doing something clever and we need to figure out what. Sadly, 
it probably isn’t worth a third Ph.D. Larry



On 11 Jun 2015, at 06:58, Tobias Nipkow  wrote:

"Function" and "recdef" work very differently. "Function" first 
disambiguates the patterns, then it defines the graph of the function 
as an inductive definition. "Recdef" turns the definitions into a 
single recursion equation with case-expressions on the rhs.


Concerning the minimum number of equations: neither definition facility 
finds a minimum, it is too hard: Alexander Krauss. Pattern minimization 
problems over recursive data types. ICFP 2008.


What is funny about the situation of 'recdef' (Slind, HOL4) vs. 'function' 
(Krauss, Isabelle/HOL) is that the HOL4 workshop at CADE-2015 mentions 
that topic under Development Ideas, see also 
http://www.cl.cam.ac.uk/~rk436/hol15/


Is that just a question of which side of the river has greener grass?

There is some chance that I will attend the workshop, but I can't say much 
about that topic.



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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

It looks like there is more work to do here then. Clearly the old package is 
doing something clever and we need to figure out what. Sadly, it probably isn’t 
worth a third Ph.D.
Larry

> On 11 Jun 2015, at 06:58, Tobias Nipkow  wrote:
> 
> "Function" and "recdef" work very differently. "Function" first disambiguates 
> the patterns, then it defines the graph of the function as an inductive 
> definition. "Recdef" turns the definitions into a single recursion equation 
> with case-expressions on the rhs.
> 
> Concerning the minimum number of equations: neither definition facility finds 
> a minimum, it is too hard: Alexander Krauss. Pattern minimization problems 
> over recursive data types. ICFP 2008.
> 
> Tobias
> 
> On 10/06/2015 23:19, Larry Paulson wrote:
>> We need to figure out how recdef does it. The minimum number of equations is 
>> mathematically fixed, so recdef must be using conditional expressions or 
>> other tricks.
>> Larry
>> 
>>> On 9 Jun 2015, at 23:07, Gerwin Klein  wrote:
>>> 
>>> I can confirm that, at least that side is simple.
>>> 
>>> Tobias’ point about avoiding exponential blowup is important, though. Might 
>>> still be too early to retire recdef entirely if it is substantially better 
>>> for some kinds of definitions, esp if they are in use (I think the recdef 
>>> in Simpl is one of these).
>>> 
>>> Cheers,
>>> Gerwin
>>> 
 On 09.06.2015, at 11:27, Thomas Sewell  wrote:
 
 I've had a quick scan over the NICTA repositories. It doesn't look like
 there are any live original uses of recdef. There are recdefs in a copy
 of Simpl-AFP, and in some backups of historical papers.
 
 Short summary, NICTA doesn't have any stakes in recdef.
 
 Cheers,
   Thomas.
 
 On 08/06/15 06:13, Makarius wrote:
> On Sat, 6 Jun 2015, Gerwin Klein wrote:
> 
>> 
>>> On 06.06.2015, at 21:23, Makarius  wrote:
>>> 
>>> (2) 'defer_recdef' which is unused in the directly visible Isabelle
>>>  universe.  So it could be deleted today.
>>> 
>>> This mailing list thread is an opportunity to point out dark matter
>>> in the Isabelle universe, where 'defer_recdef' still occurs.
>>> Otherwise I will remove it soon, lets say within 1-2 weeks.
>> 
>> Unused in our part of the dark matter universe as well.
> 
> The thread has shifted over to actual 'recdef'. Are there remaining
> uses of 'recdef' in the NICTA dark matter?
> 
> So far I always thought the remaining uses in HOL-Decision_Procs are
> only a reminder that there are other important applications.
> 
> 
>   Makarius
>>> 
>>> 
>>> 
>>> 
>>> The information in this e-mail may be confidential and subject to legal 
>>> professional privilege and/or copyright. National ICT Australia Limited 
>>> accepts no liability for any damage caused by this email or its attachments.
>>> ___
>>> 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

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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Tobias Nipkow]

"Function" and "recdef" work very differently. "Function" first disambiguates 
the patterns, then it defines the graph of the function as an inductive 
definition. "Recdef" turns the definitions into a single recursion equation with 
case-expressions on the rhs.


Concerning the minimum number of equations: neither definition facility finds a 
minimum, it is too hard: Alexander Krauss. Pattern minimization problems over 
recursive data types. ICFP 2008.


Tobias

On 10/06/2015 23:19, Larry Paulson wrote:

We need to figure out how recdef does it. The minimum number of equations is 
mathematically fixed, so recdef must be using conditional expressions or other 
tricks.
Larry


On 9 Jun 2015, at 23:07, Gerwin Klein  wrote:

I can confirm that, at least that side is simple.

Tobias’ point about avoiding exponential blowup is important, though. Might 
still be too early to retire recdef entirely if it is substantially better for 
some kinds of definitions, esp if they are in use (I think the recdef in Simpl 
is one of these).

Cheers,
Gerwin


On 09.06.2015, at 11:27, Thomas Sewell  wrote:

I've had a quick scan over the NICTA repositories. It doesn't look like
there are any live original uses of recdef. There are recdefs in a copy
of Simpl-AFP, and in some backups of historical papers.

Short summary, NICTA doesn't have any stakes in recdef.

Cheers,
   Thomas.

On 08/06/15 06:13, Makarius wrote:

On Sat, 6 Jun 2015, Gerwin Klein wrote:




On 06.06.2015, at 21:23, Makarius  wrote:

(2) 'defer_recdef' which is unused in the directly visible Isabelle
  universe.  So it could be deleted today.

This mailing list thread is an opportunity to point out dark matter
in the Isabelle universe, where 'defer_recdef' still occurs.
Otherwise I will remove it soon, lets say within 1-2 weeks.


Unused in our part of the dark matter universe as well.


The thread has shifted over to actual 'recdef'. Are there remaining
uses of 'recdef' in the NICTA dark matter?

So far I always thought the remaining uses in HOL-Decision_Procs are
only a reminder that there are other important applications.


   Makarius





The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

We need to figure out how recdef does it. The minimum number of equations is 
mathematically fixed, so recdef must be using conditional expressions or other 
tricks.
Larry

> On 9 Jun 2015, at 23:07, Gerwin Klein  wrote:
> 
> I can confirm that, at least that side is simple.
> 
> Tobias’ point about avoiding exponential blowup is important, though. Might 
> still be too early to retire recdef entirely if it is substantially better 
> for some kinds of definitions, esp if they are in use (I think the recdef in 
> Simpl is one of these).
> 
> Cheers,
> Gerwin
> 
>> On 09.06.2015, at 11:27, Thomas Sewell  wrote:
>> 
>> I've had a quick scan over the NICTA repositories. It doesn't look like
>> there are any live original uses of recdef. There are recdefs in a copy
>> of Simpl-AFP, and in some backups of historical papers.
>> 
>> Short summary, NICTA doesn't have any stakes in recdef.
>> 
>> Cheers,
>>   Thomas.
>> 
>> On 08/06/15 06:13, Makarius wrote:
>>> On Sat, 6 Jun 2015, Gerwin Klein wrote:
>>> 
 
> On 06.06.2015, at 21:23, Makarius  wrote:
> 
> (2) 'defer_recdef' which is unused in the directly visible Isabelle
>  universe.  So it could be deleted today.
> 
> This mailing list thread is an opportunity to point out dark matter
> in the Isabelle universe, where 'defer_recdef' still occurs.
> Otherwise I will remove it soon, lets say within 1-2 weeks.
 
 Unused in our part of the dark matter universe as well.
>>> 
>>> The thread has shifted over to actual 'recdef'. Are there remaining
>>> uses of 'recdef' in the NICTA dark matter?
>>> 
>>> So far I always thought the remaining uses in HOL-Decision_Procs are
>>> only a reminder that there are other important applications.
>>> 
>>> 
>>>   Makarius
> 
> 
> 
> 
> The information in this e-mail may be confidential and subject to legal 
> professional privilege and/or copyright. National ICT Australia Limited 
> accepts no liability for any damage caused by this email or its attachments.
> ___
> 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] Remaining uses of defer_recdef?

[Gerwin Klein]

I can confirm that, at least that side is simple.

Tobias’ point about avoiding exponential blowup is important, though. Might 
still be too early to retire recdef entirely if it is substantially better for 
some kinds of definitions, esp if they are in use (I think the recdef in Simpl 
is one of these).

Cheers,
Gerwin

> On 09.06.2015, at 11:27, Thomas Sewell  wrote:
>
> I've had a quick scan over the NICTA repositories. It doesn't look like
> there are any live original uses of recdef. There are recdefs in a copy
> of Simpl-AFP, and in some backups of historical papers.
>
> Short summary, NICTA doesn't have any stakes in recdef.
>
> Cheers,
>Thomas.
>
> On 08/06/15 06:13, Makarius wrote:
>> On Sat, 6 Jun 2015, Gerwin Klein wrote:
>>
>>>
 On 06.06.2015, at 21:23, Makarius  wrote:

 (2) 'defer_recdef' which is unused in the directly visible Isabelle
   universe.  So it could be deleted today.

 This mailing list thread is an opportunity to point out dark matter
 in the Isabelle universe, where 'defer_recdef' still occurs.
 Otherwise I will remove it soon, lets say within 1-2 weeks.
>>>
>>> Unused in our part of the dark matter universe as well.
>>
>> The thread has shifted over to actual 'recdef'. Are there remaining
>> uses of 'recdef' in the NICTA dark matter?
>>
>> So far I always thought the remaining uses in HOL-Decision_Procs are
>> only a reminder that there are other important applications.
>>
>>
>>Makarius




The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Thomas Sewell]

I've had a quick scan over the NICTA repositories. It doesn't look like
there are any live original uses of recdef. There are recdefs in a copy
of Simpl-AFP, and in some backups of historical papers.

Short summary, NICTA doesn't have any stakes in recdef.

Cheers,
Thomas.

On 08/06/15 06:13, Makarius wrote:

On Sat, 6 Jun 2015, Gerwin Klein wrote:




On 06.06.2015, at 21:23, Makarius  wrote:

 (2) 'defer_recdef' which is unused in the directly visible Isabelle
   universe.  So it could be deleted today.

This mailing list thread is an opportunity to point out dark matter
in the Isabelle universe, where 'defer_recdef' still occurs.
Otherwise I will remove it soon, lets say within 1-2 weeks.


Unused in our part of the dark matter universe as well.


The thread has shifted over to actual 'recdef'. Are there remaining
uses of 'recdef' in the NICTA dark matter?

So far I always thought the remaining uses in HOL-Decision_Procs are
only a reminder that there are other important applications.


Makarius

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






The information in this e-mail may be confidential and subject to legal 
professional privilege and/or copyright. National ICT Australia Limited accepts 
no liability for any damage caused by this email or its attachments.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Tobias Nipkow]

A frequent use case is this: you have 5-10 interesting patterns where stuff 
happens and an otherwise pattern with a simple rhs. In that case you do want to 
write those 5-10 patterns explicitly and let the definition facility take care 
of the hundreds of patterns that the default case expands to. You don't really 
care that the induction has hundreds of cases because they are trivial. In 
contrast, rewriting such a definition to avoid the blowup is a pain in the 
backside and is not guaranteed to make proofs simpler.


Tobias

On 07/06/2015 21:46, Larry Paulson wrote:

I suggest looking for ways for users to avoid exponential blowup. Presumably 
this means avoiding deeply nested patterns in favour of conditional expressions 
in some cases. Such a formalisation might be easier to reason with too, who 
wants an induction rule with hundreds of cases?

But coming up with simple guidelines for users might be tricky.

Larry


On 7 Jun 2015, at 20:33, Florian Haftmann 
 wrote:

As far as I know, this is due to layered architecture of the function
package.  »recdef« does everything in one bunch and can hence optimize
for sequential pattern matching.  Each layer of »function« must feed its
result to its successor in a standardized form, and since there is no
overall concept of sequential pattern matching, it has to be compiled
away once and for all from the very beginning. (roughly spoken)

An optimization would require a modified architecture.


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Andreas Lochbihler]

On 06/06/15 17:11, Florian Haftmann wrote:

So are there any experience reports that the combinatorial explosion in
pattern matching in fun/function had to be worked around somehow?  Or do
we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?
I regularly have to work around this explosion problem. One example is in 
JinjaThreads/Common/BinOp.thy where I was not able to define the function binop as a 
whole, but I had to split it up into several definitions - fortunately, there was no 
recursion involved, so this was possible. There must also be a mailing list thread between 
Alexander Krauss and me on this topic, but I was not able to unearth it.


I have run into the same problem (with similar workarounds) a number of times. In case of 
a recursive function, I nowadays write


  "f x y z = (case x of ... => (case y of ... => | _ => ...) | _ => ...)"

and let simps_of_case split the equations by the pattern. In big cases, simps_of_case runs 
for a minute or two, but there is no hope to get these definitions through with the 
function. Of course, this does not work with overlapping patterns, but I rarely use them 
anyway. The main drawback here is that I do not get a suitable cases rule for the function 
definitions and the proofs accordingly look ugly (especially if I have nested patterns, 
i.e., nested case distinctions and lots of rename_tac+case_tac).


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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Makarius]

On Sat, 6 Jun 2015, Gerwin Klein wrote:




On 06.06.2015, at 21:23, Makarius  wrote:

 (2) 'defer_recdef' which is unused in the directly visible Isabelle
   universe.  So it could be deleted today.

This mailing list thread is an opportunity to point out dark matter in 
the Isabelle universe, where 'defer_recdef' still occurs.  Otherwise I 
will remove it soon, lets say within 1-2 weeks.


Unused in our part of the dark matter universe as well.


The thread has shifted over to actual 'recdef'. Are there remaining uses 
of 'recdef' in the NICTA dark matter?


So far I always thought the remaining uses in HOL-Decision_Procs are only 
a reminder that there are other important applications.



Makarius

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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

I suggest looking for ways for users to avoid exponential blowup. Presumably 
this means avoiding deeply nested patterns in favour of conditional expressions 
in some cases. Such a formalisation might be easier to reason with too, who 
wants an induction rule with hundreds of cases?

But coming up with simple guidelines for users might be tricky.

Larry

> On 7 Jun 2015, at 20:33, Florian Haftmann 
>  wrote:
> 
> As far as I know, this is due to layered architecture of the function
> package.  »recdef« does everything in one bunch and can hence optimize
> for sequential pattern matching.  Each layer of »function« must feed its
> result to its successor in a standardized form, and since there is no
> overall concept of sequential pattern matching, it has to be compiled
> away once and for all from the very beginning. (roughly spoken)
> 
> An optimization would require a modified architecture.

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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Florian Haftmann]

> I could not believe that recdef could not be replaced by fun, so here is
> the patch that removes usages of recdef from Decision_Procs. The proof
> rules that come out of the function package are fine (one just needs a
> few split_format (complete) attributes in a few places).

Let me emphasize this particular point.  When you give a specification
in Isabelle, there are two expectations:

a) The system is able to construct something which satisfies this
specification (the primitive definition)

AND

b) The system provides a mechanism to actually *reason* about resulting
properties in a (natural, intuitive, straight-forward) way (for
non-trivial specifications, typically an induction rule)

Practically, a) is of little (or at least reduced) value without b)

Hence, if there is evidence that working around function's pattern
explosion diminishes b), it is definitely a restriction and not just a
matter of taste how to construct and design specifications.

The question what can really be done to improve the situation, however,
is written on a different sheet.

Florian

P.S: Just a remark: in my personal view b) is even the dominant role of
advanced specification tools – the way how a specification is given
suggests how proofs can be conducted successfully.  Hence I still prefer
»primrec« if applicable since this makes it immediately clear that
proofs most likely will require induction on the corresponding datatype.

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Florian Haftmann]

> I could not believe that recdef could not be replaced by fun, so here is
> the patch that removes usages of recdef from Decision_Procs. The proof
> rules that come out of the function package are fine (one just needs a
> few split_format (complete) attributes in a few places).
> 
> I'm not sure if this is something for the repository though, since it
> has a factor of >2 impact on the build-time:
> 
> recdef: Finished HOL-Decision_Procs (0:03:53 elapsed time, 0:13:26 cpu
> time, factor 3.45)
> fun   : Finished HOL-Decision_Procs (0:08:24 elapsed time, 0:28:10 cpu
> time, factor 3.35)
> 
> On the other hand 8 minutes is still not much. The longest fun
> invocation (numadd in MIR) takes about 2 minutes, other are all below 20
> seconds.

A compromise could be to let just the 2 min recdef stand and migrate the
others…

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Florian Haftmann]

>> On 7 Jun 2015, at 07:38, Dmitriy Traytel > > wrote:
>>
>> I'm not sure if this is something for the repository though, since it
>> has a factor of >2 impact on the build-time:
> 
> Thanks for investigating. But how do we explain this?
> 
> Possibly “fun” insists on converting on creating unconditional patterns
> only, while “recdef” allows conditional equations. But one could easily
> insert conditions manually in order to simplify the set of patterns.

As far as I know, this is due to layered architecture of the function
package.  »recdef« does everything in one bunch and can hence optimize
for sequential pattern matching.  Each layer of »function« must feed its
result to its successor in a standardized form, and since there is no
overall concept of sequential pattern matching, it has to be compiled
away once and for all from the very beginning. (roughly spoken)

An optimization would require a modified architecture.

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Florian Haftmann]

>> So are there any experience reports that the combinatorial explosion in
>> pattern matching in fun/function had to be worked around somehow?  Or do
>> we have to conclude that the pattern complexity of the applications in
>> src/HOL/Decision_Procs is indeed domain-specific?
> I have some experience with the combinatorial explosion in fun. You
> don't need much: just take extended regular expressions (~10
> constructors) and define binary normalizing constructors (by some
> sequential pattern matching on both arguments). The AFP entry
> MSO_Regex_Equivalence is full of ~30 sec fun declarations.
> 
> While this is still on the edge of being bearable, try to add one more
> constructor... (I've seen examples where fun from 10 lines of
> specification produced something like 10^5 simp equations.) In a
> different formalization (AFP entry Formula_Derivatives) where I needed
> to have more then 10 constructors, I had to work around the function
> package by separating the datatype into two and defining the functions
> separately. (In the end, the separation had also positive effects, but
> still it felt like fighting the system when doing it.)

OK, the dragons are still there and not just a historic relic.

> Note that the domain is quite similar to Cooper---syntactic
> manipulations of expressions/formulas---but isn't it what we do quite
> often in Isabelle? Orthogonally, I have no idea, whether recdef would
> have helped me.

I would definitely not suggest to use recdef for any new application…
the open question is whether we have to think about a refinement or
extension of function.

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

> On 7 Jun 2015, at 07:38, Dmitriy Traytel  wrote:
> 
> I'm not sure if this is something for the repository though, since it has a 
> factor of >2 impact on the build-time:

Thanks for investigating. But how do we explain this?

Possibly “fun” insists on converting on creating unconditional patterns only, 
while “recdef” allows conditional equations. But one could easily insert 
conditions manually in order to simplify the set of patterns. There are 14 
instances of recdef in Cooper.thy. Do any of them stand out as extra slow?

Larry

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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Dmitriy Traytel]

Hi,

I could not believe that recdef could not be replaced by fun, so here is 
the patch that removes usages of recdef from Decision_Procs. The proof 
rules that come out of the function package are fine (one just needs a 
few split_format (complete) attributes in a few places).


I'm not sure if this is something for the repository though, since it 
has a factor of >2 impact on the build-time:


recdef: Finished HOL-Decision_Procs (0:03:53 elapsed time, 0:13:26 cpu 
time, factor 3.45)
fun   : Finished HOL-Decision_Procs (0:08:24 elapsed time, 0:28:10 cpu 
time, factor 3.35)


On the other hand 8 minutes is still not much. The longest fun 
invocation (numadd in MIR) takes about 2 minutes, other are all below 20 
seconds.


Dmitriy

On 07.06.2015 07:18, Amine Chaieb wrote:
I remember trying to convert Cooper's as well as other Decision proc's 
recdefs to fun, also with the help of Alex but gave up at some point.


I think the killer at the time was rather the induction principle and 
not the simp rules. The one derived by recdef really fits the 
definition and "spirit" of development. Also runtime at the time was 
not acceptable. I also remember havin the runtime problem with fun vs. 
primrec (so we left those there too).


  Context: Deep embedding of datatype + normal form on this data type 
+ set of recursive functions on syntax preserving normal form. The 
normal Form has conditions on nested patterns --> introduce new 
constructor for these common nested patterns in normal form.


We had combinatorial explosion due to the depth of the patterns (which 
is the main reason to introduce special constructors in the datatype, 
to reduce deep patterns).


The induction priciples with recdef really fitted, i.e. induct auto 
with spice did the job for lemmas you do not expect to spend time 
thinking as a software developer.


One could argue that one should introduce a new data type for 
normalized syntactic elements and perform such computations as needed. 
I dismissed this idea and did not explore it, since it comes with a 
high price. Perhaps there are better ways to do the formalization.


Amine.


On 06/06/2015 08:37 PM, Tobias Nipkow wrote:



On 06/06/2015 20:11, Larry Paulson wrote:
Pattern matching is a convenience, and can always be eliminated 
manually. Is there really no reasonable way to re-express the 
definitions in Cooper.thy?


You can always turn all patterns of the lhs into cases on the rhs and 
derive the individual equations as lemmas. You also need to derive an 
induction principle. I would rather keep recdef than do all that by 
hand.


Tobias


Larry

On 6 Jun 2015, at 16:11, Florian Haftmann 
 wrote:



The reason for the continued existence of recdef is that function can
cause a combinatorial explosion the way it compiles pattern 
matches. I
just tried Cooper.thy and changing one of the recdefs to function 
makes
Isabelle go blue (purple) in the face until one gives up. Hardware 
alone

will not solve that one.

Now one could argue that since we need recdef, we should also keep 
the
special variant defer_recdef, but if nobody speaks up for it, we 
don't

have a proof that we really need it and it should go.


At the time of their writing the recdef examples in (nowadays)
src/HOL/Decision_Procs were the power applications of their times.

Since then power applications have grown bigger and bigger and
fun/function have been used widespread.  It seems strange to me 
that no

application since then had never hit the same concrete wall again.

So are there any experience reports that the combinatorial 
explosion in
pattern matching in fun/function had to be worked around somehow?  
Or do

we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?

Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de 



___
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


# HG changeset patch
# User traytel
# Date 1433658664 -7200
#  So Jun 07 08:31:04 2015 +0200
# Node ID 03ef7232e0f060ed68756b902bd55ec9a51ed9b7
# Parent  392402362c3e01d9556b59674ce2d4f38903bd0b
get rid of recdef from Decision_Procs

diff -r 392402362c3e -r 03ef7232e0f0 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Fr Jun 05 09:15:37 2015 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	So Jun 07 08:31:04 2015 +0200
@@ -6,7 +6,6 @@
 imports
   Complex_Main
   "~~/src/HOL/Library/Code_Target_Numeral"
-  "

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Amine Chaieb]

I remember trying to convert Cooper's as well as other Decision proc's 
recdefs to fun, also with the help of Alex but gave up at some point.


I think the killer at the time was rather the induction principle and 
not the simp rules. The one derived by recdef really fits the definition 
and "spirit" of development. Also runtime at the time was not 
acceptable. I also remember havin the runtime problem with fun vs. 
primrec (so we left those there too).


  Context: Deep embedding of datatype + normal form on this data type + 
set of recursive functions on syntax preserving normal form. The normal 
Form has conditions on nested patterns --> introduce new constructor for 
these common nested patterns in normal form.


We had combinatorial explosion due to the depth of the patterns (which 
is the main reason to introduce special constructors in the datatype, to 
reduce deep patterns).


The induction priciples with recdef really fitted, i.e. induct auto with 
spice did the job for lemmas you do not expect to spend time thinking as 
a software developer.


One could argue that one should introduce a new data type for normalized 
syntactic elements and perform such computations as needed. I dismissed 
this idea and did not explore it, since it comes with a high price. 
Perhaps there are better ways to do the formalization.


Amine.


On 06/06/2015 08:37 PM, Tobias Nipkow wrote:



On 06/06/2015 20:11, Larry Paulson wrote:
Pattern matching is a convenience, and can always be eliminated 
manually. Is there really no reasonable way to re-express the 
definitions in Cooper.thy?


You can always turn all patterns of the lhs into cases on the rhs and 
derive the individual equations as lemmas. You also need to derive an 
induction principle. I would rather keep recdef than do all that by hand.


Tobias


Larry

On 6 Jun 2015, at 16:11, Florian Haftmann 
 wrote:



The reason for the continued existence of recdef is that function can
cause a combinatorial explosion the way it compiles pattern matches. I
just tried Cooper.thy and changing one of the recdefs to function 
makes
Isabelle go blue (purple) in the face until one gives up. Hardware 
alone

will not solve that one.

Now one could argue that since we need recdef, we should also keep the
special variant defer_recdef, but if nobody speaks up for it, we don't
have a proof that we really need it and it should go.


At the time of their writing the recdef examples in (nowadays)
src/HOL/Decision_Procs were the power applications of their times.

Since then power applications have grown bigger and bigger and
fun/function have been used widespread.  It seems strange to me that no
application since then had never hit the same concrete wall again.

So are there any experience reports that the combinatorial explosion in
pattern matching in fun/function had to be worked around somehow?  
Or do

we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?

Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de 



___
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] Remaining uses of defer_recdef?

[Dmitriy Traytel]

Hi Florian,

On 06.06.2015 17:11, Florian Haftmann wrote:

The reason for the continued existence of recdef is that function can
cause a combinatorial explosion the way it compiles pattern matches. I
just tried Cooper.thy and changing one of the recdefs to function makes
Isabelle go blue (purple) in the face until one gives up. Hardware alone
will not solve that one.

Now one could argue that since we need recdef, we should also keep the
special variant defer_recdef, but if nobody speaks up for it, we don't
have a proof that we really need it and it should go.

At the time of their writing the recdef examples in (nowadays)
src/HOL/Decision_Procs were the power applications of their times.

Since then power applications have grown bigger and bigger and
fun/function have been used widespread.  It seems strange to me that no
application since then had never hit the same concrete wall again.

So are there any experience reports that the combinatorial explosion in
pattern matching in fun/function had to be worked around somehow?  Or do
we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?
I have some experience with the combinatorial explosion in fun. You 
don't need much: just take extended regular expressions (~10 
constructors) and define binary normalizing constructors (by some 
sequential pattern matching on both arguments). The AFP entry 
MSO_Regex_Equivalence is full of ~30 sec fun declarations.


While this is still on the edge of being bearable, try to add one more 
constructor... (I've seen examples where fun from 10 lines of 
specification produced something like 10^5 simp equations.) In a 
different formalization (AFP entry Formula_Derivatives) where I needed 
to have more then 10 constructors, I had to work around the function 
package by separating the datatype into two and defining the functions 
separately. (In the end, the separation had also positive effects, but 
still it felt like fighting the system when doing it.)


Note that the domain is quite similar to Cooper---syntactic 
manipulations of expressions/formulas---but isn't it what we do quite 
often in Isabelle? Orthogonally, I have no idea, whether recdef would 
have helped me.


Dmitriy

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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

> On 6 Jun 2015, at 19:37, Tobias Nipkow  wrote:
> 
> You can always turn all patterns of the lhs into cases on the rhs and derive 
> the individual equations as lemmas. You also need to derive an induction 
> principle. I would rather keep recdef than do all that by hand.

Are we talking about this definition?

recdef prep "measure fmsize"
  "prep (E T) = T"
  "prep (E F) = F"
  "prep (E (Or p q)) = Or (prep (E p)) (prep (E q))"
  "prep (E (Imp p q)) = Or (prep (E (NOT p))) (prep (E q))"
  "prep (E (Iff p q)) = Or (prep (E (And p q))) (prep (E (And (NOT p) (NOT 
q"
  "prep (E (NOT (And p q))) = Or (prep (E (NOT p))) (prep (E(NOT q)))"
  "prep (E (NOT (Imp p q))) = prep (E (And p (NOT q)))"
  "prep (E (NOT (Iff p q))) = Or (prep (E (And p (NOT q (prep (E(And (NOT 
p) q)))"
  "prep (E p) = E (prep p)"
  "prep (A (And p q)) = And (prep (A p)) (prep (A q))"
  "prep (A p) = prep (NOT (E (NOT p)))"
  "prep (NOT (NOT p)) = prep p"
  "prep (NOT (And p q)) = Or (prep (NOT p)) (prep (NOT q))"
  "prep (NOT (A p)) = prep (E (NOT p))"
  "prep (NOT (Or p q)) = And (prep (NOT p)) (prep (NOT q))"
  "prep (NOT (Imp p q)) = And (prep p) (prep (NOT q))"
  "prep (NOT (Iff p q)) = Or (prep (And p (NOT q))) (prep (And (NOT p) q))"
  "prep (NOT p) = NOT (prep p)"
  "prep (Or p q) = Or (prep p) (prep q)"
  "prep (And p q) = And (prep p) (prep q)"
  "prep (Imp p q) = prep (Or (NOT p) q)"
  "prep (Iff p q) = Or (prep (And p q)) (prep (And (NOT p) (NOT q)))"
  "prep p = p"
  (hints simp add: fmsize_pos)

So what is recdef doing right that fun is doing wrong?

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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Tobias Nipkow]

On 06/06/2015 20:11, Larry Paulson wrote:

Pattern matching is a convenience, and can always be eliminated manually. Is 
there really no reasonable way to re-express the definitions in Cooper.thy?


You can always turn all patterns of the lhs into cases on the rhs and derive the 
individual equations as lemmas. You also need to derive an induction principle. 
I would rather keep recdef than do all that by hand.


Tobias


Larry


On 6 Jun 2015, at 16:11, Florian Haftmann 
 wrote:


The reason for the continued existence of recdef is that function can
cause a combinatorial explosion the way it compiles pattern matches. I
just tried Cooper.thy and changing one of the recdefs to function makes
Isabelle go blue (purple) in the face until one gives up. Hardware alone
will not solve that one.

Now one could argue that since we need recdef, we should also keep the
special variant defer_recdef, but if nobody speaks up for it, we don't
have a proof that we really need it and it should go.


At the time of their writing the recdef examples in (nowadays)
src/HOL/Decision_Procs were the power applications of their times.

Since then power applications have grown bigger and bigger and
fun/function have been used widespread.  It seems strange to me that no
application since then had never hit the same concrete wall again.

So are there any experience reports that the combinatorial explosion in
pattern matching in fun/function had to be worked around somehow?  Or do
we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?

Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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






smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

Pattern matching is a convenience, and can always be eliminated manually. Is 
there really no reasonable way to re-express the definitions in Cooper.thy?
Larry

> On 6 Jun 2015, at 16:11, Florian Haftmann 
>  wrote:
> 
>> The reason for the continued existence of recdef is that function can
>> cause a combinatorial explosion the way it compiles pattern matches. I
>> just tried Cooper.thy and changing one of the recdefs to function makes
>> Isabelle go blue (purple) in the face until one gives up. Hardware alone
>> will not solve that one.
>> 
>> Now one could argue that since we need recdef, we should also keep the
>> special variant defer_recdef, but if nobody speaks up for it, we don't
>> have a proof that we really need it and it should go.
> 
> At the time of their writing the recdef examples in (nowadays)
> src/HOL/Decision_Procs were the power applications of their times.
> 
> Since then power applications have grown bigger and bigger and
> fun/function have been used widespread.  It seems strange to me that no
> application since then had never hit the same concrete wall again.
> 
> So are there any experience reports that the combinatorial explosion in
> pattern matching in fun/function had to be worked around somehow?  Or do
> we have to conclude that the pattern complexity of the applications in
> src/HOL/Decision_Procs is indeed domain-specific?
> 
>   Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
> 
> ___
> 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] Remaining uses of defer_recdef?

[Florian Haftmann]

> The reason for the continued existence of recdef is that function can
> cause a combinatorial explosion the way it compiles pattern matches. I
> just tried Cooper.thy and changing one of the recdefs to function makes
> Isabelle go blue (purple) in the face until one gives up. Hardware alone
> will not solve that one.
> 
> Now one could argue that since we need recdef, we should also keep the
> special variant defer_recdef, but if nobody speaks up for it, we don't
> have a proof that we really need it and it should go.

At the time of their writing the recdef examples in (nowadays)
src/HOL/Decision_Procs were the power applications of their times.

Since then power applications have grown bigger and bigger and
fun/function have been used widespread.  It seems strange to me that no
application since then had never hit the same concrete wall again.

So are there any experience reports that the combinatorial explosion in
pattern matching in fun/function had to be worked around somehow?  Or do
we have to conclude that the pattern complexity of the applications in
src/HOL/Decision_Procs is indeed domain-specific?

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Tobias Nipkow]

The reason for the continued existence of recdef is that function can cause a 
combinatorial explosion the way it compiles pattern matches. I just tried 
Cooper.thy and changing one of the recdefs to function makes Isabelle go blue 
(purple) in the face until one gives up. Hardware alone will not solve that one.


Now one could argue that since we need recdef, we should also keep the special 
variant defer_recdef, but if nobody speaks up for it, we don't have a proof that 
we really need it and it should go.


Tobias

On 06/06/2015 13:23, Makarius wrote:

On Sat, 6 Jun 2015, Larry Paulson wrote:


I’d be happy to see the complete phasing out of TFL. It’s had its day. It was
always a tricky thing to maintain. I’m amazed that it still works despite all
of the many fundamental changes to system APIs.


There are actually two remaining parts of TFL:

   (1) 'recdef' which is still used in Isabelle + AFP applications, but
 very rarely and some effort could be made to get rid of it.

   (2) 'defer_recdef' which is unused in the directly visible Isabelle
 universe.  So it could be deleted today.

This mailing list thread is an opportunity to point out dark matter in the
Isabelle universe, where 'defer_recdef' still occurs.  Otherwise I will remove
it soon, lets say within 1-2 weeks.


Apart from that we should also work on (1) eventually.  It has become a ritual
to ask about the purpose of old 'recdef', and it usually leads to the result as
"still needed" for odd reasons that I then forget immediately.  So I have
developed a reluctance to ask again.


 Makarius


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





smime.p7s
Description: S/MIME Cryptographic Signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Makarius]

On Sat, 6 Jun 2015, Larry Paulson wrote:

I’d be happy to see the complete phasing out of TFL. It’s had its day. 
It was always a tricky thing to maintain. I’m amazed that it still works 
despite all of the many fundamental changes to system APIs.


There are actually two remaining parts of TFL:

  (1) 'recdef' which is still used in Isabelle + AFP applications, but
very rarely and some effort could be made to get rid of it.

  (2) 'defer_recdef' which is unused in the directly visible Isabelle
universe.  So it could be deleted today.

This mailing list thread is an opportunity to point out dark matter in the 
Isabelle universe, where 'defer_recdef' still occurs.  Otherwise I will 
remove it soon, lets say within 1-2 weeks.



Apart from that we should also work on (1) eventually.  It has become a 
ritual to ask about the purpose of old 'recdef', and it usually leads to 
the result as "still needed" for odd reasons that I then forget 
immediately.  So I have developed a reluctance to ask again.



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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

I’d be happy to see the complete phasing out of TFL. It’s had its day. It was 
always a tricky thing to maintain. I’m amazed that it still works despite all 
of the many fundamental changes to system APIs.

Larry

> On 5 Jun 2015, at 21:42, Florian Haftmann 
>  wrote:
> 
>> Cleaning up some obscure corners of the system, I've come across the old
>> defer_recdef command.
>> 
>> Are there any remaining uses of this historical relic?  I don't see any
>> in the main Isabelle repository + AFP.
> 
> Some years ago the idea was to let recdef stand as long as there are
> examples in the distribution.  The consequence would be to dismantle
> unused parts altogether.
> 
> Further suggestios?
> 
>   Florian

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

Re: [isabelle-dev] Remaining uses of defer_recdef?

[Florian Haftmann]

> Cleaning up some obscure corners of the system, I've come across the old
> defer_recdef command.
> 
> Are there any remaining uses of this historical relic?  I don't see any
> in the main Isabelle repository + AFP.

Some years ago the idea was to let recdef stand as long as there are
examples in the distribution.  The consequence would be to dismantle
unused parts altogether.

Further suggestios?

Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



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