[isabelle-dev] cs. 3911cf09899a

[Florian Haftmann]

> On 10/03/2011 04:59 PM, Florian Haftmann wrote:
>>> +text {* Definitions could be moved to Transitive_Closure if they are
>> of more general use. *}
>>
>> is there any striking reason *not* to do so in the first place?  At a
>> first glimpse I can't see anything which relates to Enum.thy in those
>> theorems.
>>
> Well, the definition is made because it is not possible to define
> recursive functions
> inlined in other definitions in Isabelle.
> Otherwise, I could have avoided it at all.

I do not doubt the necessity or purpose of the definition, which has
nothing recursive.  I just remark that it could have gone to
Transitive_Closure in the first place.

>> In my opinion it is high time to abandone the tradition of such comment
>> jokes in the HOL theories: if theorems are there, they *will* be used,
>> or at least it is not at our judgment for whom they are useful.  So it
>> is best to have the theorems where they belong to, unless bootstrap
>> reasons dictate something else.
> 
> The theorems are useful for my development, but I can't judge if they
> are useful
> in general.

Indeed.  Nobody can in first instance.

> More specifically, adding this definition correctly would also require
> to prove many
> more basic lemmas, such as introduction and elimination rules.
> In this way, I am following a long tradition of tool developers,
> defining constants for
> their "internal" purposes, which we hope are not picked up by users.
> You can find these traditions in almost every tool in the HOL image.

That's very fine.  But also those »internal« constants ought to reside
in appropriate places, e.g. internal_split in Product_Type.thy, nat_aux
in Int.thy, dummy_term and valapp in Code_Evaluation.

If a constant is supposed to be »internal«, it's good practice to hide
it in the namespace.

There have also been examples of operations which started as being
considered »internal« but later one it has been discovered that users
have defined their own variant of it.  AFAIR, Sum_Type.Projl was such a
thing.

Such a thing like ntrancl seems general enough that also users could
benefit from it and therefore I would not view it as internal, but this
is in the first place my personal opinion.  If such things are buried
somewhere users will start to define their own private copy which leads
to duplication.

The lack of fundamental proof rules is no obstacle in the first place:
experiences shows that if a definition is useful, theorems start to
agglomerate soon.

> But what you are suggesting is that anything related to some concept
> must be in that
> specific theory.

The »must« is too strict.  But I argue that if I have a bin labeled
»chocolate« and one labeled »cookies«, it is straightforward to put the
chocolate in the first bin and the cookies in the latter if nothing
speaks against it.

> But there are obvious counterexamples, such as More_List, and different
> Util Theories
> that contain specific definitions and lemmas, sofar only used in those
> developments.

More_List and More_Set are things which I have on my todo list and hope
to be able to tackle after the 'a set issue.  But also these theories
have already made a step from »specific« to »general«: they came into
being by factoring out generic stuff from specific applications.

It's not clear to me to which »Util« theories you are referring to;  the
unintegrated auxiliary theories in various AFP session surely are a
problematic issue, but involve different issues of meta-organization
than the distribution.

> If you have strong feelings about this being at the wrong place, you can
> move it.

I have no »feelings«, just an educated guess that sometimes somebody
*will* move it, either by necessity or by psychological strain.  In an
amortized view, you do not save any work by leaving it as it is.

> If it hinders the efforts, it might actually be because the predicate
> and set distinction has consequences,
> we have overlooked sofar.
> 
> The definition of card(inality) is clearly related to sets.
> 
> But will there also exist a definition of the cardinality of a predicate?
> For lemmas about the tranclp predicate, one needs the number of values
> for which a relation is true (the cardinality).
> 
> So, what's the opinion on this?

Just inline the cardinality for predicates into the main theorem.  There
is no need for a separate definition.

I guess the following AFP problem results from that fundamental change:
http://isabelle.in.tum.de/reports/Isabelle/report/11aa8e74cf064dc9bb9c10f72882a9d0

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20111003/b00acd52/attachment.sig>