# [isabelle] Case names qualified by locale

Hi,
I like how I can use a named case for coinduction, where P is a
coinductive predicate:
lemma "P n"
proof (coinduction rule: P.coinduct)
case P show ?case sorry
qed
This works fine.
However, suppose P is inside a locale L. Sometimes I need coinduction
over L.P:
lemma "L.P n"
proof (coinduction rule: L.P.coinduct)
case P show ?case sorry
qed
Although the coinduction works, "case P" doesn't work because the case
name is not available. My workaround so far was to explicitly use
fix/assume/show. I would prefer to have "case P" and ?case because the
formulas in coinduction proofs are often very long.
I tried to find out from the HOL source code where the case names are
defined, but couldn't find anything.
Is there a way to use a named case with the fully qualified coinduction
rule?
I have attached a minimal example exhibiting the problem.
A follow-up question is, is there a way to use a named case when the
coinduction rule is L.P.coinduct[OF something] instead of only
L.P.coinduct (which often seems useful when using L.P.coinduct instead
of P.coinduct)?
Thanks,
Christoph

theory Test imports Main begin
locale L begin
coinductive P where "P 0"
lemma "P n" proof (coinduction rule: P.coinduct)
case P show ?case sorry (* case P and ?case are recognized *)
qed
end
lemma "L.P n" proof (coinduction rule: L.P.coinduct)
case P show ?case sorry (* Undefined case: "P", Unbound schematic variable: ?case *)
qed
end

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