发表机构
University of Cambridge; École Normale Supérieure; University of California, Berkeley（剑桥大学; 巴黎高等师范学院; 加州大学伯克利分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文面向初学者介绍 Isabelle/HOL 元编程，通过多元多项式次数上界自动估计的 poly_degree 命令示例，展示实现与验证过程，并提供自包含教程。
AI 中文摘要
本文为初学者介绍了 Isabelle/HOL 中的元编程，基于一个处理多元多项式的运行示例展开。该示例源于我们对通用丢番图对的形式化。我们描述了 poly_degree 命令的实现，该命令计算多元多项式总次数的上界并自动证明其正确性。完整的元程序处理多种特殊情况，但为便于阐述，此处我们展示一个简化版本。我们描述了开发过程和设计决策；我们的目标是为希望开始学习元编程的数学家提供一个简短且自包含的 Isabelle/ML 教程。
英文摘要
This article offers an introduction to metaprogramming in Isabelle/HOL for beginners, based on a running example for working with multivariate polynomials. The example is motivated by our formalisation of universal Diophantine pairs. We describe the implementation of the poly_degree command, which computes upper bounds on the total degrees of multivariate polynomials and automatically proves their correctness. The complete metaprogram handles a variety of special cases but herein we present a simplified version for the sake of exposition. We describe our development process and design decisions; our goal is to offer a small and self-contained tutorial on Isabelle/ML, for mathematicians who want to get started with metaprogramming.
