Splitting a variable of product/tuple/pair type into its members in apply style

Question

let's assume we are working with a pair of type ('a × 'a) and define a fun with pattern matching for it.

fun test :: "('a × 'a) ⇒ 'a ⇒ bool" where "test (a,b) c = True"

If I now have a variable a_b of type ('a × 'a), how can I replace it into its pair representation (a,b) in an apply style proof. For example, what is the best way to show the following lemma? How can I replace test a_b c with test (a,b) c?

lemma "test a_b c = True"

Does this also apply to pairs in the assumptions?

lemma "¬ test a_b c ⟹ flying_pigs"

Answer 1

How about using cases/case_tac on a_b?