Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] König's Lemma?

view this post on Zulip Email Gateway (Aug 18 2022 at 15:50):

From: Lars Noschinski <noschinl@in.tum.de>
Hi everyone,

does there exists a formalization of König's Lemma in Isabelle/HOL?
Grepping the standard library and the AFP did not get me any matches.

-- Lars

view this post on Zulip Email Gateway (Aug 18 2022 at 15:51):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Lars,

does there exists a formalization of König's Lemma in Isabelle/HOL?
I have a formalisation of König's lemma where paths are modelled as
coinductive lists. I have now added it to Coinductive in the AFP
development branch as an example application.

Andreas

Last updated: Apr 25 2024 at 12:23 UTC