Stream: Beginner Questions

Topic: Applying cases for nested patterns without subgoal

Maximilian Vollath (Jan 10 2025 at 13:16):

When a function is defined over pattern matching its argument, I often have to apply cases in a proof.
But when the definition additionally does pattern matching over the components, can I just apply cases over both patterns at once?

For example:
fun my_fun where "my_fun (a, MyType x y) = ..."
To prove a property of my_fun c I often do

apply (cases  c)
subgoal for _ b
apply (cases b)
by simp

Can I just simplify this into one line?

Maximilian Schäffeler (Jan 10 2025 at 13:23):

Like this? by (cases rule: my_fun.cases[of c]) simp

Maximilian Vollath (Jan 10 2025 at 18:06):

Yes exactly like that, thanks!

Last updated: Feb 01 2025 at 20:19 UTC