New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Submit Partitions.thy, RelationProperties.thy and their dependencies to the AFP #36

Open

clange opened this issue Sep 10, 2013 · 1 comment

Assignees

Labels

community isabelle

Member

clange commented Sep 10, 2013

Submission guidelines

probably best as separate entries:

Partitions
RelationProperties (mainly: injective functions)
Common dependencies

ghost assigned clange

Contributor

caminati commented Oct 1, 2013

As a byproduct of further auction theory theorems in d.thy, now there is much more stuff in c.thy regarding relations. For example:

quotientation by equivalence relations.
kernel of a function as a partition of its domain.
compatibility (when does quotientation preserve runiq?).
passing from a partition to its equivalence relation (e.g., in case 2 we get the equivalence relation of all the preimages of the same elements).

clange mentioned this issue

Announce verified algorithm for “all injective functions of a set” to Isabelle community #42

Open

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment