Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] obtains forgets consumes and case_names in loc...


view this post on Zulip Email Gateway (Aug 18 2022 at 15:53):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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


Last updated: Mar 28 2024 at 20:16 UTC