Kevin Kappelmann (Jul 21 2022 at 13:17): 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
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
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: Apr 17 2024 at 20:15 UTC