Re: [isabelle] adm and fixrec’s induct rules



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.