Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Coinduction and induction

Email Gateway (Aug 18 2022 at 12:08):

From: li yongjian <lyj238@gmail.com>
hi:
I may ask a stupid question, here I want to know the meanings of the
saying " Coinduction and induction are a parir of duals". Does this
means that if we define
a set S inductively, then we can define (-S) coinductively?

For example, in the Auth lib, we define
the function parts inductively as follows:
consts parts :: "msg set => msg set"
inductive "parts H"
intros
Inj [intro]: "X \<in> H ==> X \<in> parts H"
Fst: "{|X,Y|} \<in> parts H ==> X \<in> parts H"
Snd: "{|X,Y|} \<in> parts H ==> Y \<in> parts H"
Body: "Crypt K X \<in> parts H ==> X \<in> parts H"

So there should be a coinductive defintion for a function
not_parts such that not_parts H= - (parts H)?
But I have not find how to give a coinductive definition for
not_parts ?

Who can give such a defintion of not_parts ?
or I have sth wrong with the meaning of the dualilty between induction
and coinduction.

regards!

Email Gateway (Aug 18 2022 at 12:31):

From: Tjark Weber <webertj@in.tum.de>
Li,

if f is a monotone function (on a Boolean algebra, say), then

-(lfp f) = gfp g,

where g(x) := -f(-x).

Best,
Tjark

Last updated: May 03 2024 at 08:18 UTC