*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*: Tue, 7 Sep 2010 16:30:06 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1283890295.3857.25.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>*Sender*: huffman.brian.c at gmail.com

On Tue, Sep 7, 2010 at 1:11 PM, Joachim Breitner <mail at joachim-breitner.de> wrote: > Dear Brian, > > I have been working some more with HOLCF (although my supervisers warned > me that I might run into difficulties or make life harder for me...), > and I have some suggestions and some questions. I hope you don’t mind me > accosting them to you, and remember that these really are only > suggestions, not requests :-) > > First I noticed that I tend to have a lot of admissibility statements to > proof. With the lemmas provided in Adm.thy, this is usually not a big > problem. I wonder if it would be sensible to take a similar approach > than taken with cont2cont: I.e. have a ruleset adm2adm that I can amend, > so that I can just use "apply (intros adm2adm)" without listing all my > custon adm rules, and be done in most cases. Or possibly "apply (intros > adm2adm cont2cont)", if some rules involve continuity claims, such as > this one I wrote: > _________________________________________________________ > lemma adm_single_valued: [...] Hi Joachim, You can easily create your own named rulesets using the Named_Thms ML functor, like this: ML {* structure Adm2Adm = Named_Thms ( val name = "adm2adm" val description = "admissibility intro rule" ) *} setup Adm2Adm.setup This defines a dynamic theorem list called "adm2adm", as well as an attribute called "adm2adm" that will add a theorem to the list. You can then populate the ruleset with pre-existing rules from Adm.thy using a declare statement: declare <names of adm rules> [adm2adm] > My next question is about pattern matching in fixrec equations. At the > moment, fixrec only supports very few constructors in patterns, and the > Discr constructor is not supported. Therefore, I have only one equation > with a large case expression then, which makes the .induct rule > relatively unpleasant to work with (compared with, e.g., the function > package). I’d be glad if I could use the Discr constructor in patterns, > and I’d be even more pleased if arbitrary patterns can be used inside > the Discr constructor. You can extend fixrec by associating match combinators with new constructors, using the Fixrec.add_matchers ML command. To see how to do this, look at my latest update to List_Cpo.thy, where I set up Nil and Cons to work with fixrec: http://isabelle.in.tum.de/repos/isabelle/rev/3989b2b44dba Unfortunately this won't work for all constructors -- fixrec has some hard-wired assumptions about the kinds of constructors it will work with. For one, it assumes that the arguments to the constructor will all have types in class cpo. This means that the "Discr" and "Def" constructors won't work, because their argument types are generally not cpos. I'd like to relax this restriction, but doing so would require rewriting fixrec's pattern-match compiler, which I don't really have time to do right now -- I need to finish my dissertation first! > And finaly, I’d like to have some advice. I tried to proof a statement > "P f" about the function f defined by fixrec, using f.induct. I noticed > that it would be easier if I know "Q f", so I proved that (again using > f.induct). Turning back to the proof of "P f", I found out that the > lemma "Q f" is useless, as in the inductive proof of "P f" I am not > working with f, but rather an approximation. > > I worked around it by proving P and Q simultaneously in one induction, > but the proof is becoming illegibly convoluted. > > Is there maybe a cleaner and more idiomatic way of handing such a case? > I’m afraid that if I continue this way, in the end all statements of my > projects will be proven in one huge induct rule. And Isabelle is already > moving slowly inside the induct proof. I'm afraid that with the foo.induct rules currently produced by fixrec, you're probably stuck doing the simultaneous inductions. Fortunately it is possible to create a stronger induction rule, but unfortunately fixrec does not generate such a rule for you. (It's on my long list of things to do after I finish my degree :) Here's how fixrec currently generates its induction rules: When you define a recursive constant "foo :: 'a", fixrec builds a functional "foo_rec :: 'a => 'a", and defines foo as its least fixed-point: "foo == fix$(LAM f. foo_rec f)". Then fixrec uses the "fix_ind" lemma to generate an induction rule for foo: lemma fix_ind: assumes "adm P" and "P \<bottom>" and "!!x. P x ==> P (F$x)" shows "P (fix$F)" The problem is that fix_ind is weaker than it could be. Here is a stronger form of induction for least fixed-points that could be used instead: lemma assumes "adm P" and "!!n. P (iterate n$F$\<bottom>)" shows "P (fix$F)" 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. > Thanks for your support, > Joachim Thanks for your interest in HOLCF! Hope this helps, - 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

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