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