Email Gateway (Aug 18 2022 at 15:53): 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: Nov 21 2024 at 12:39 UTC