*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] adm and fixrec’s induct rules*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Wed, 08 Sep 2010 11:06:20 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTimQaNKR1sR_zhPv+Ye3d9w6C+Fce2eQ-P5wfaZu@mail.gmail.com>*References*: <1283436852.29045.36.camel@kirk> <1283437959.29045.42.camel@kirk> <AANLkTiks9_nW7znhWgdRByPCfy8_n+7jx3045JV87z3K@mail.gmail.com> <1283543423.2794.18.camel@kirk> <AANLkTimm0y6Krcbes=ZtHme8XF2pLge2jvK8HrScmGw7@mail.gmail.com> <1283588404.2560.7.camel@kirk> <AANLkTimMJsff_xuoxyvh=TyXBVAOhnKy3rVzJ1jRSTru@mail.gmail.com> <1283890295.3857.25.camel@kirk> <AANLkTimQaNKR1sR_zhPv+Ye3d9w6C+Fce2eQ-P5wfaZu@mail.gmail.com>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

Dear Brian, Am Dienstag, den 07.09.2010, 16:30 -0700 schrieb Brian Huffman: > So here's what I'd *like* fixrec to do: In addition to defining "foo > == fix$(LAM f. foo_rec f)", also define another nat-indexed sequence > of approximations to foo: "foo_chain n == iterate n$(LAM f. foo_rec > f)$\<bottom>". Then it could generate an unfolding rule: > > "foo_chain (Suc n) = foo_rec (foo_chain n)" > > and a strong induction rule: > > "adm P ==> (!!n. P (foo_chain n)) ==> P foo" > > I think such a rule would allow you to prove separate lemmas about > foo_chain, and re-use them inside later inductions. This way you could > avoid having to do those big simultaneous inductions you complained > about. Even without automation from fixrec, it might be worthwhile to > define the extra constant and prove the extra rules manually. I’d like to try that, but here, the symbol "foo_rec" is not known. And looking at src/HOLCF/Tools/fixrec.ML (without understanding much), I can not find a string ending in "rec" anywhere. The _def theorems generated by fixrec seem to contain the equations of my functions directly. Are you sure that the _rec symbol is actually generated? Thanks, Joachim -- Joachim Breitner e-Mail: mail at joachim-breitner.de Homepage: http://www.joachim-breitner.de ICQ#: 74513189 Jabber-ID: nomeata at joachim-breitner.de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] adm and fixrec’s induct rules***From:*Brian Huffman

**References**:**[isabelle] fixrec’s demand for continuity proofs***From:*Joachim Breitner

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Joachim Breitner

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Brian Huffman

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Joachim Breitner

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Brian Huffman

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Joachim Breitner

**Re: [isabelle] fixrec’s demand for continuity proofs***From:*Brian Huffman

**[isabelle] adm and fixrec’s induct rules***From:*Joachim Breitner

**Re: [isabelle] adm and fixrec’s induct rules***From:*Brian Huffman

- Previous by Date: Re: [isabelle] problem with class and sulocale declarations
- Next by Date: Re: [isabelle] problem with class and sulocale declarations
- Previous by Thread: Re: [isabelle] adm and fixrec’s induct rules
- Next by Thread: Re: [isabelle] adm and fixrec’s induct rules
- Cl-isabelle-users September 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list