[isabelle] obtains forgets consumes and case_names in locales



Hi all,

I stumbled across the following odd behaviour of obtains in locales:
Normally, theorems stated with obtains carry appropriate case_names and consumes declaration, e.g. the following works as expected.

lemma test:
  assumes "n = n"
  obtains (first_case) "n = 0"
  | (second_case) n' where "n = Suc n'"
by(cases n) auto

lemma assumes "n = n" shows P
using assms
proof(cases rule: test)
  case first_case
next
  case (second_case n')
oops

When I do not provide names for the obtains-cases in the lemma, test is still declared with a "consumes 1" and case_names 1 2.

However, when I put lemma test into a locale that fixes at least one parameter, these declarations change:

locale A =
  fixes a :: "'a"
begin

lemma test:
  assumes "n = n"
  obtains (first_case) "n = 0"
  | (second_case) n' where "n = Suc n'"
by(cases n) auto

Lemma test now carries the consumes 0 declaration and case_names 1 2 3, independent of whether the names for obtains-cases are given - which is at least unexpected. Is this a bug or am I better not to rely on obtains producing proper consumes and case_names declarations in general?

Regards,
Andreas






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.