[isabelle-dev] cs. 3911cf09899a

[Lukas Bulwahn]

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.

> 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.
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.

But what you are suggesting is that anything related to some concept 
must be in that
specific theory.
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.

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

>> +subsection {* An executable card operator on finite types *}
>> +
>> +lemma
>> +  [code]: "card R = length (filter R enum)"
>> +by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV
> Collect_def)
>
> Our current efforts for having 'a set as type constrcutor will turn this
> superfluous if not hindering.
>
I was aware of this aspect when writing this lemma.
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?


Lukas