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



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





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