*To*: Joachim Breitner <mail at joachim-breitner.de>*Subject*: Re: [isabelle] adm and fixrec’s induct rules*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 8 Sep 2010 06:39:56 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1283936780.2414.3.camel@kirk>*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> <1283936780.2414.3.camel@kirk>*Sender*: huffman.brian.c at gmail.com

On Wed, Sep 8, 2010 at 2:06 AM, Joachim Breitner <mail at joachim-breitner.de> wrote: > 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? Sorry, I guess what I said was a bit misleading. There is no "foo_rec" constant. I only meant "foo_rec" to stand for the functional (a possibly large lambda term) of which "foo" is the least fixed-point. Maybe a more explicit example will my suggestion more clear. domain 'a llist = LNil | LCons (lazy 'a) (lazy "'a llist") fixrec repeat :: "'a -> 'a llist" where "repeat$a = LCons$a$(repeat$a)" These lemmas are generated by fixrec: repeat_def: "repeat == fix$(LAM r a. LCons$a$(r$a))" repeat.unfold: "repeat = (LAM a. LCons$a$(repeat$a))" repeat.simps: "repeat$a = LCons$a$(repeat$a)" repeat.induct: "adm P ==> P \<bottom> ==> (!!x. P x ==> P (LAM a. LCons$a$(x$a))) ==> P repeat" And I would suggest that you also define repeat_chain :: "nat => 'a -> 'a llist" "repeat_chain n == iterate n$(LAM r a. LCons$a$(r$a))$\<bottom>" and prove the lemmas "repeat_chain (Suc n) = (LAM a. LCons$a$(repeat_chain n$a))" "adm P ==> (!!n. P (repeat_chain n)) ==> P repeat" - Brian

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

**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

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

- Previous by Date: Re: [isabelle] problem with class and sulocale declarations
- Next by Date: Re: [isabelle] adm and fixrec’s induct rules
- 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