Stream: Beginner Questions

Topic: cases and schematic variables


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mathias Fleury (Jul 21 2022 at 13:25):

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

view this post on Zulip 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: Feb 27 2024 at 08:17 UTC