Re: [isabelle] Multiset elements
there's also a "copy" of Multiset (called Multiset_Extension) in the AFP
entry Well-Quasi-Orders. The point here was to have the multiset
extension of an arbitrary order (given as predicate of type "'a => 'a =>
bool") over a fixed carrier set (not a full type).
This theory is not polished at all, but maybe it contains something
useful. At some point I'll have to clean this up ...
On 08/22/2014 12:26 PM, Jasmin Christian Blanchette wrote:
Am 21.08.2014 um 13:24 schrieb René Thiemann <rene.thiemann at uibk.ac.at>:
if you're going to work on the Multiset-theory, I suggest to add the following four lemmas which might be of general interest:
Thanks. I have just added them to my repository and pushed them to the testboard.
The IsaFoR project seems to have much more to offer in terms of multiset support. If you have other contributions or ideas, please let us know.
Incidentally, the refactoring Dmitriy and I (and Florian) have in mind will probably not happen in the immediate future. We're using multisets in a formalization that we would like to submit to the AFP, so we'd like it to work with both Isabelle2014 and the repository version (as much as possible). Once it's published, we'll start playing with the "Multiset" theory.
Incidentally, our formalization happens to be not too remote from IsaFoR thematically -- our multisets are clauses or collections of clauses in a formalized theorem prover. We'll probably need to talk. ;)
This archive was generated by a fusion of
Pipermail (Mailman edition) and