Re: [isabelle] Lemma: Library/RBT.map-of-alist-of



Hi Peter,

in the current distribution, the lemma "Library/RBT.map-of-alist-of" is
not shown, but marked with an "oops".
The whole development of folding an RB-tree is marked with "text {* The
following is still incomplete... *}".

Indeed it is. We don't really have big experience in using that theory, so there may be more missing lemmas...

In case no one has already proven this lemma, and someone is interested
in a proof, here is one.

Cool, thanks! I added them, including the other rules (Still need to do some testing before making them [simp])

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.