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



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
Description: This is a digitally signed message part



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