# [isabelle] case_names and consumes

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

theory Test imports Main begin
consts precond1 :: bool
consts precond2 :: bool
consts case1 :: bool
consts case2 :: bool
lemma case_rule[consumes 2, case_names case1 case2]:
assumes "precond1"
assumes "precond2"
assumes "case1 \<Longrightarrow> Q"
assumes "case2 \<Longrightarrow> Q"
shows "Q"
sorry
lemma
assumes "precond1" and "precond2"
shows Q
using assms proof (cases rule: case_rule)
print_cases
oops
lemma
assumes "precond1"
shows Q
using assms proof (cases rule: case_rule)
print_cases
oops
end

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