CODEWITHSUNDEEP
isabelle
user1868607
user1868607

Reputation: 2610

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...

Upvotes: 1

Views: 144

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8298

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.

Upvotes: 3

Related Questions