[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.