Предопределенные функции для двоичных деревьев в Isabelle

Question

Существуют ли какие-либо предопределенные функции для бинарных деревьев в Изабель? Например, чтобы перейти к левой стороне двоичного дерева?

Answer 1

С Isabelle2014 существует небольшая теория для двоичных деревьев в ~~/src/HOL/Library/Tree. Если этот тип соответствует вашей цели, вы можете использовать его и функции, определенные на нем. Например, существуют селекторные функции left и right, которые возвращают левое и правое поддерево дерева.

Если вам нужно определить свой собственный тип данных, вы можете использовать синтаксис селектора datatype_new для определения селекторов по своему усмотрению.