# [isabelle] Coinduction and induction

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!
On Tue, Jul 1, 2008 at 7:29 AM, Jeremy Dawson <jeremy at rsise.anu.edu.au> wrote:
> Richard Warburton wrote:
>>
>> I was wondering if someone knew of any good examples of papers using
>> coinduction within Isabelle/HOL? If there were available theory
>> files relating to such papers it would also be most helpful.
>>
>> regards,
>>
>> Richard Warburton
>>
>>
>
> Richard,
>
> My paper in TPHOLs last year has an example of the use of coinduction:
>
> Jeremy E. Dawson, Formalising Generalised Substitutions
> <file:///home/web/jeremy/public_html/pubs/fgc/fgs/> In 20th International
> Conference on Theorem Proving in Higher Order Logics Kaiserslautern,
> September 2007 (TPHOLs 2007), LNCS 4732, 54-69
>
> Link at http://users.rsise.anu.edu.au/~jeremy/
>
> The use of coinduction was a significant improvement on the way I'd done the
> same thing previously, so I give it a fair amount of detail
>
> Jeremy
>
>

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