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