Isabelle 中的模式匹配存在目标

Question

想知道有没有办法写出下面的模式匹配：

have "∃ q1 q2 q3 q4.
        b0^2 - a1^2 = 
            q1*(-1 + a0^2 + b0^2 - t^2 * a0^2 * b0^2) +
            q2*(-1 + a1^2 + b1^2 - t^2 * a1^2 * b1^2) +
            q3*(a0 * b0 - a1 * b1) +
            q4*(a1 * b0 + a0 * b1)"   
    (is "∃ q1 q2 q3 q4. ?a = ?b")

目前我的模式匹配失败，我担心这在一般情况下可能无法实现...

Answer 1

如果这样写，?a和?b是bool类型的常量，即它们不能依赖于q1到q4 .由于在您的情况下，语句取决于它们，因此模式匹配失败。

你必须写成

(is "∃ q1 q2 q3 q4. ?a q1 q2 q3 q4 = ?b q1 q2 q3 q4")

然后就可以了。

否则，?a 会是什么，用在存在量词之外？它将引用未绑定到任何地方的变量 q1 到 q4。

Isabelle 中的模式匹配存在目标

Pattern matching existential goal in Isabelle

isabelle