Search code examples
isabelle

Pattern matching existential goal in Isabelle

I was wondering if there is a way to write the following pattern matching:

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")

Currently I'm getting a pattern matching fail, I have the concern that this may not be possible in general...

Solution

  • If you write it like this, ?a and ?b are constants of type bool, i.e. they must not depend on q1 to q4. Since, in your case, the statement depends on them, the pattern matching fails.

    You have to write it as 

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

    and then it works.

    Otherwise, what would ?a be, used outside the existential quantifier? It would refer to variables q1 to q4 that are not bound anywhere.