Coalgebras: prove Rutten's Theorem 7.3

coalgebra: Prove Rutten's theorems 7.1 and 7.2

Make resolve_then try harder to keep assumptions "in order"

In particular, when resolving p1 ... pn ==> qj against q1 ... qm ==> r
the result will be

p1 ... pn q1 ... q{j-1} q{j+1}...q{m} ==> r

modulo the fact that unification may cause assumptions to become the
same (duplicates are eliminated), either as each other, or as an
existing hypothesis. This makes the proposed irule (goal_assum o
resolve_then Any mp_tac) behave a bit more like MATCH_MP_TAC, rather
than as currently.

Fix Unicode violation in previous

coalgAxioms: prove the interesting case of the first iso theorem

Extract simple Set-category theory from coalgAxioms into separate thy

This is very simple stuff indeed, but it doesn't depend on any axioms
and may be independently useful.

Prove that pushouts in Set are unique up to isomorphism

Inasmuch as this is possible to prove at all, given the poverties of
HOL types.

Add a little lemma about pushouts in Set

Fix Unicode violations

Prove some basic category theory results (over Set) in coalgAxioms

This is in service of getting some of Rutten's results more
abstractly. Not sure if it's really worth it though.

Prove a chunk of Rutten's Theorem 7.1 (First Isomorphism theorem)

More co-algebra mechanisation, mostly done with Rutten §6

Fix Unicode violation in src/

More progress on mechanising Rutten

Start of some abstract mechanisation of coalgebra theory