Dynamic order statistic tree structures are a type of data structure that integrates the features of dynamic sets, order statistics, and search tree structures, supporting efficient data retrieval operations. These structures are widely used in fields like database systems, memory management, and file management. However, current research primarily focuses on structural invariants, such as balance, while neglecting discussions on functional correctness. Additionally, existing research methods mainly involve manual derivation or interactive mechanized verification for specific algorithms, lacking mature and reliable general verification patterns and having a low level of automation. To address this, an Isabelle-based functional modeling and automated verification framework for dynamic order statistic search tree structures was designed, establishing a verified general lemma library to reduce the time and cost of code verification for developers. Using this functional modeling framework, unbalanced binary search trees, balanced binary search trees (exemplified by red-black trees), and balanced multi-way search trees (exemplified by 2-3 trees) were selected as instantiated cases for demonstration. With the help of the automated verification framework, multiple instantiated cases can be automatically verified by simply using induction and calling the auto method once or the try command, providing a reference for automated verification of functional and structural correctness in complex data structure algorithms.