Email Gateway (Aug 18 2022 at 13:42): Email Gateway (Aug 18 2022 at 13:42):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
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... *}".
In case no one has already proven this lemma, and someone is interested
in a proof, here is one.
Regards,
Peter
RBT_add.thy
Email Gateway (Aug 18 2022 at 13:42):From: Alexander Krauss <krauss@in.tum.de>
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
Last updated: May 03 2024 at 08:18 UTC