Isabelle中的归纳定义是否为有限生成？

For anyone working with inductive definitions, Peter Aczel's seminal paper is a must-reference. Here's a core takeaway about how rules are formalized:

In inductive definitions, a rule is defined as a binary pair (X, x). Here, X is referred to as the premise set, and x is the conclusion. This rule is commonly notated as X → x.

A critical point to note: this formal definition doesn't restrict the premise set X to be finite. However, from hands-on experience with verification tasks, I've found that we only ever deal with finite premise sets in practice. A perfect example is the reflexive transitive closure—this construct relies on finite premises to be feasible for real-world verification and computation.

内容的提问来源于stack exchange，提问作者Gergely