## Stream: Beginner Questions

### Topic: cases and schematic variables

#### Kevin Kappelmann (Jul 21 2022 at 13:17):

I am quite confused about the `cases` method. I want to specify some `case_names` for a lemma and then apply it to a goal using `cases`. However, `cases` either complains and does not apply the theorem or does not correctly assign the `?cases` schematic variables (I think). Any ideas if this an error on my side or the fault of `cases`?

``````theory Scratch
imports Main
begin

consts P :: "'a ⇒ bool"
consts Q :: "'a ⇒ bool"
consts R :: "'a ⇒ 'a ⇒ bool"

lemma my_cases [case_names a b]:
assumes "P x"
and "Q y"
shows "R x y"
sorry

lemma "R t1 t2"
proof (cases rule: my_cases)
(*the proof state correctly shows
1. P t1
2. Q t2
*)
(*the output panel suggests the following outline:*)
case a
then show ?thesis sorry (*Failed to refine any pending goal*)
next
case b
then show ?thesis sorry
oops

lemma "R t1 t2"
proof (cases t1 rule: my_cases)
print_cases
(*Prints the following (note the schematic variable ?y)
a:
let "?case" = "P t1"
b:
let "?case" = "Q ?y"
*)
case a
then show ?case sorry (*this works*)
next
case b
then show ?case sorry (*Unbound schematic variable: ?case*)
oops

lemma "R t1 t2"
proof (cases t1 t2 rule: my_cases) (*Rule has fewer variables than instantiations given*)
oops

end
``````

#### Fabian Huch (Jul 21 2022 at 13:24):

For your last example, directly instantiating the theorem works:

``````proof (cases rule: my_cases[of t1 t2])
case a
then show ?case sorry
next
case b
then show ?case sorry
qed
``````

No idea why it won't accept the two instantiations directly, though.

#### Mathias Fleury (Jul 21 2022 at 13:24):

It also works with

``````proof (induction rule: my_cases)
case a
then show ?case sorry
next
case b
then show ?case sorry
qed
``````

#### Mathias Fleury (Jul 21 2022 at 13:25):

My guess is that cases is only meant to add assumption, not to change the goal

#### Manuel Eberl (Jul 26 2022 at 12:29):

Yup. If it changes the goal, it's an induction rule. Compare e.g. something like `linorder_wlog`.

Last updated: Dec 07 2023 at 20:16 UTC