Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Case names qualified by locale

Email Gateway (Aug 22 2022 at 11:18):

From: Christoph Dittmann <f-isabellelist@yozora.eu>
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
Test.thy

Email Gateway (Aug 22 2022 at 11:22):

From: Lars Noschinski <noschinl@in.tum.de>
I don't know why the case names are lost here, but you should be able to
use the names by using

L.P.coinduct[case_names P Q R]

or maybe

L.P.coinduct[consumes 1, case_names P Q R]

as a workaround.

-- Lars

Email Gateway (Aug 22 2022 at 11:22):

From: Christoph Dittmann <f-isabellelist@yozora.eu>
Thanks, this works great. I didn't know you could use [case_names] there.

Christoph

Email Gateway (Aug 22 2022 at 11:25):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

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

I don't know why the case names are lost here

The case names are not »lost«. L.P is a opaque foundational constant,
and the corresponding declarations are applied only in resulting
contexts, i. e. in the context of the locale itself or due to
interpretation.

You might consider wrapping up you matter in something like

context
begin

interpretation prefix!: L … <proof>

lemma …
proof (coinduction rule: prefix.P.coinduct)
case P …
qed

end

which will give you the full declarations from L inside a certain block.

Hope this helps.
Florian

but you should be able to

use the names by using

L.P.coinduct[case_names P Q R]

or maybe

L.P.coinduct[consumes 1, case_names P Q R]

as a workaround.

-- Lars

signature.asc

Last updated: May 01 2024 at 20:18 UTC