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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
