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

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.

It also works with

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

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

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