[isabelle] union-find based unification

Dear all,

is anybody aware of an Isabelle/HOL (or even better Imperative_HOL) formalization of a union-find data structure for which also code can be generated? I found


which mentions union-find trees in the introduction, but by skimming over the theory names nothing immediately jumped at me ;)

The reason I ask is for an efficient (code generatable) formalization, using union-find, of a first-order unification algorithm. Anybody aware that this was already done?



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