Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] case_names and consumes


view this post on Zulip Email Gateway (Aug 18 2022 at 16:10):

From: Lars Noschinski <noschinl@in.tum.de>
Hello everyone,

i've got a case rule which has the following form:

lemma case_rule[consumes 2, case_names case1 case2]:
assumes "precond1"
assumes "precond2"
assumes "case1 ==> Q"
assumes "case2 ==> Q"
shows "Q"
sorry

The first two assumptions are preconditions, so I'd like to have these
two consumed by cases.

This works fine, if I'm really supplying two facts to the cases method:

lemma
assumes "precond1" and "precond2"
shows Q
using assms proof (cases rule: case_rule)
print_cases
(* cases:

* case1:
* let "?case" = "?Q"
* assume "case1"
* case2:
* let "?case" = "?Q"
* assume "case2"
*)
oops

but if I supply only one fact, cases consumes this fact without
complaining, but after that, the case names are wrong (in Isabelle
2009-2), because three goals instead of two remain:

lemma
assumes "precond1"
shows Q
using assms proof (cases rule: case_rule)
print_cases
(* cases:

* case1:
* let "?case" = "precond2"
* case2:
* let "?case" = "?Q"
* assume "case1"
*)
oops

This seems wrong to me as the isar reference manual specifies that the
case names apply to the suffix of the list of premises (which works fine
if I don't specify consumes).

Independent from that, I wonder why print_cases pretends that there is
a ?case-binding which does not exist in reality, i.e.

case case1 then show ?case ...

fails because ?case is not bound. For a case distinction theorem like
the above (but without consumes-declaration) such a binding would seem
quite useful to me.

-- Lars
test.thy


Last updated: Mar 29 2024 at 08:18 UTC