有限集上递归函数pcart的终止性证明及定义优化问询

用户提供的简化版理论代码如下：

theory Simplified
  imports Main "HOL-Library.FSet"
begin

inductive_set Fin where
  emptyI: "{} ∈ Fin" | 
  insertI: "A ∈ Fin ⟹ insert a A ∈ Fin"

lemma Fin_is_finite: "x ∈ Fin ⟹ finite x"
  using Fin.inducts by auto

lemma finite_is_Fin: "finite x ⟹ x ∈ Fin"
  by (metis Fin.simps Finp_Fin_eq finite_ne_induct)

definition ext :: "nat set ⇒ nat set set" where 
  "ext X = {{x}| x. x ∈ X}"

function pcart :: "nat set fset ⇒ nat set set" where 
  "pcart {||} = {}" | 
  "pcart (finsert a A) = ext a ∪ pcart A ∪ {{x}∪y| x y. x ∈ a ∧ y ∈ pcart A}"
  apply blast
  apply blast
  apply blast

当前卡在最后一个终止性子目标的证明：

⋀a A aa Aa.
       finsert a A = finsert aa Aa ⟹
       ext a ∪ pcart_sumC A ∪ {{x} ∪ y |x y. x ∈ a ∧ y ∈ pcart_sumC A} =
       ext aa ∪ pcart_sumC Aa ∪ {{x} ∪ y |x y. x ∈ aa ∧ y ∈ pcart_sumC Aa}

问题解答 #

1. 是否有更简便的方式定义该递归函数以证明其终止性？

有两种更高效的方案：

• 用primrec替代function：fset的递归结构天然适配原始递归，primrec会自动处理终止性证明，无需手动验证等式一致性。定义示例：

  primrec pcart :: "nat set fset ⇒ nat set set" where
    "pcart {||} = {}" |
    "pcart (finsert a A) = ext a ∪ pcart A ∪ {{x} ∪ y | x y. x ∈ a ∧ y ∈ pcart A}"
  

  它依赖fset的有限性和递归结构，自动生成终止性所需的证明义务，无需额外操作。
• 显式指定终止度量：若坚持用function，可以基于fsize（fset的大小）定义终止关系，直接完成证明：

  function pcart :: "nat set fset ⇒ nat set set" where 
    "pcart {||} = {}" | 
    "pcart (finsert a A) = ext a ∪ pcart A ∪ {{x}∪y| x y. x ∈ a ∧ y ∈ pcart A}"
  by (termination, relation "measure fsize", auto)
  

  利用finsert会使集合大小严格递增的性质，auto可自动完成终止性验证。

2. 若坚持当前版本，如何证明终止性？

当前卡住的是等式一致性证明：需证明finsert构造的等价fset对应的函数值相等。核心思路是拆分finsert a A = finsert aa Aa的两种情况：

1. 情况1：元素相同且子集相等：a = aa且A = Aa，直接由等式自反性得证。
2. 情况2：元素已存在于子集中：比如a ∈ A，此时finsert a A = A，可转化为更小的fset（A - {||a||}），结合递归定义的归纳假设展开等式两边，利用集合运算性质证明相等。

具体证明步骤示例：

apply (case_tac "a = aa")
 apply (simp add: fset_eq_iff)
apply (case_tac "a ∈ A")
 apply (simp add: finsert_eq_finsert_iff fset_eq_iff, metis pcart.psimps(2) finite_is_Fin Fin_is_finite)
apply (case_tac "aa ∈ Aa")
 apply (simp add: finsert_eq_finsert_iff fset_eq_iff, metis pcart.psimps(2) finite_is_Fin Fin_is_finite)

3. 如何证明pcart {||} = {}？

跳过终止证明后无法证此引理，是因为function定义的函数在未完成终止性/一致性证明前，其等式规则（如pcart.psimps）并未完全生效。解决方法：

• 若用primrec定义，基础情况的等式直接作为定义的一部分，可直接调用pcart.simps(1)，无需额外证明。
• 若用function完成完整证明，pcart.psimps(1)会自动可用，证明只需引用定义：

  lemma pcart_empty: "pcart {||} = {}"
    by (simp add: pcart.psimps(1))
  

内容的提问来源于stack exchange，提问作者Alicia M.