*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: [isabelle] adm and fixrec’s induct rules*From*: Joachim Breitner <mail at joachim-breitner.de>*Date*: Tue, 07 Sep 2010 22:11:35 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTimMJsff_xuoxyvh=TyXBVAOhnKy3rVzJ1jRSTru@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>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

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: assumes "cont (λx. f x)" shows "adm (λx. single_valued (f x))" using assms unfolding single_valued_def by (intro adm_lemmas adm_not_mem cont2cont adm_subst[of f]) _________________________________________________________ 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. 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. Thanks for your support, 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

- Previous by Date: [isabelle] Congruence rule for Let
- Next by Date: Re: [isabelle] adm and fixrec’s induct rules
- Previous by Thread: Re: [isabelle] fixrec’s demand for continuity proofs
- 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