Isabelle：变量 x 仅出现在右侧

如何解决Isabelle：变量 x 仅出现在右侧

inductive S :: "alpha list ⇒ bool" where
 empty : "S []" | 
 step1 : "S w ⟹ S (a # w @ [b])" |
 step2 : "⟦S w1; S w2⟧ ⟹ S (w1 @ w2)"

inductive T :: "alpha list ⇒ bool" where
 empty : "T []" |
 step : "⟦T w1; T w2⟧ ⟹ T (w1 @ [a] @ w2 @ [b])"

fun balanced :: "nat ⇒ alpha list ⇒ bool" where
"balanced 0 w = S w"  |
"balanced (Suc 0) w = S (a # w)" |
"(balanced n w = S (a # m @ w)) ⟹ (balanced (Suc n) w = S (a # a # m @ w))"

我正在尝试编写一个函数 balanced 以便 balanced n w 为真，当且仅当 S (an @ w) 其中包含 n 相同 alphalist 的列表。对于函数 "(balanced n w = S (a # m @ w)) ⟹ (balanced (Suc n) w = S (a # a # m @ w))" 的第三个方程，即使左侧有 m，我也会收到错误“变量“m”仅出现在右侧：”。 我能想到的唯一解决方案是用另一种方式编写函数，但暂时想不出如何。

解决方法

就目前而言，您的定义没有多大意义。您试图从 m 的结果中找出 balanced n w，即使返回的类型是 bool。您无法将其转换为传递给 S 的特定参数，就像您无法将肉剁成一只会走路的鸡一样。

如果你真的想说“如果有一些 m 满足这个，那么使用那个 m”，那么你需要一个显式的存在量词，然后使用 SOME 运算符将见证作为实际表达式。不过，我不建议这样做。

我相信您实际上想说的是balanced n w = S (replicate n a @ w)。这个定义没有问题被接受（如果我没记错 replicate 的参数顺序），但是对于证明这两个语法等价的潜​​在问题，这个定义对你没有帮助。

在这个证明中引入 balanced 中间概念的要点是你不必直接将一个派生树映射到另一个派生树。您实际上想要的是一个函数，它从左到右递归地处理输入 w，并且根本不引用 S 或 T。换句话说，您需要一个算法来决定语法是否与输入匹配。 balanced n w = S (replicate n a @ w) 那么用归纳法证明它是一件好事。

由于这是一个练习（来自 prog-prove 和/或具体语义，如果有人在家中遵循），我现在不会只向您展示递归定义，但如果您坚持尝试，请告诉我让它工作。