Suppose that we have defined a type of finite multisets as in the documentation
for define_quotient_type, based on the equivalence relation multisame on
lists. First we prove that the equivalence relation multisame is indeed
reflexive and transitive:
# let MULTISAME_REFL,MULTISAME_TRANS = (CONJ_PAIR o prove)
(`(!l:(A)list. multisame l l) /\
(!l1 l2 l3:(A)list.
multisame l1 l2 /\ multisame l2 l3 ==> multisame l1 l3)`,
REWRITE_TAC[multisame] THEN MESON_TAC[]);;
We would like to define the multiplicity of an element in a multiset. First we
define this notion on the representing type of lists:
# let listmult = new_definition
`listmult a l = LENGTH (FILTER (\x:A. x = a) l)`;;
and prove that it is welldefined. Note that the second argument is
the only one we want to lift to the quotient type, so that's the only one for
which we use the relation multisame. For the first argument and the result we
only use equality:
# let LISTMULT_WELLDEF = prove
(`!a a':A l l'.
a = a' /\ multisame l l' ==> listmult a l = listmult a' l'`,
SIMP_TAC[listmult; multisame]);;
Now we can lift it to a multiplicity function on the quotient type:
# let multiplicity,multiplicity_th =
lift_function multiset_rep (MULTISAME_REFL,MULTISAME_TRANS)
"multiplicity" LISTMULT_WELLDEF;;
val multiplicity : thm =
|- multiplicity a l = (@u. ?l. listmult a l = u /\ list_of_multiset l l)
val multiplicity_th : thm =
|- listmult a l = multiplicity a (multiset_of_list (multisame l))
Another example is the `union' of multisets, which we can consider as the
lifting of the APPEND operation on lists, which we show is welldefined:
# let APPEND_WELLDEF = prove
(`!l l' m m' :A list.
multisame l l' /\ multisame m m'
==> multisame (APPEND l m) (APPEND l' m')`,
SIMP_TAC[multisame; FILTER_APPEND]);;
and lift as follows:
# let munion,munion_th =
lift_function multiset_rep (MULTISAME_REFL,MULTISAME_TRANS)
"munion" APPEND_WELLDEF;;
val munion : thm =
|- munion l m =
multiset_of_list
(\u. ?l m.
multisame (APPEND l m) u /\
list_of_multiset l l /\
list_of_multiset m m)
val munion_th : thm =
|- multiset_of_list (multisame (APPEND l m)) =
munion (multiset_of_list (multisame l)) (multiset_of_list (multisame m))
For continuation of this example, showing how to lift theorems from the
representing functions to the functions on the quotient type, see the
documentation entry for lift_theorem.