Re: [isabelle] recdef problem



Christian,

I wanted to define following function (which gives the set of positions of a term---where a position is a possibly empty list of natural numbers):

 consts pos :: "('v,'f)term => nat list set"
  recdef pos "measure (% t. size t)"
   "pos (Var v) = {[]}"
   "pos (Fun f ts) =
    {[]} Un {(i#p) | i p. i : {0..<length ts} & p : pos (ts!i)}"

which is not possible automatically because of the unsolved goal:

 \<forall> :001 ts. size (ts ! :001) < Suc (term_list_size ts)

now my questions:
1) what does :001 mean (I just assumed its the index variable i from my definition).

It's an internal variable produced by the simplifier. I am not sure why
you get to see this strange name, but reading it as "i" is probably just
right.

2) why is the information i : {0..<length ts} lost, which would make the unsolved goal equivalent to:

You are missing a congruence rule here. Congruence rules are needed for recdef
to know at which values the recursive call actually occurs. In your example, the
following congruence rule for conjunction helps:

lemma conj_cong[recdef_cong]:
  "[| A = A'; A' ==> B = B' |] ==> A & B = A' & B' "
by blast

In the second premise, you see the hypothesis A'. This gives you the extra hypothesis for the termination proof.

You can see congruence rules as if they express something about evaluation
order, which is not otherwise defined, since we're just doing logic. By giving
this congruence rule to recdef you state (and have proved) that the second part of the conjunction only relevant if the first part is satisfied. In the tutorial (end of 9.2.2) this is only mentioned briefly, but the example given there works out-of-the-box, because the map_cong rule is there already (and conj_cong should
probably also be). In general you need a suitable congruence rule for every
higher-order combinator you use in the definition.

You can see the preconfigured congruence rules by issuing

ML "RecdefPackage.print_recdefs (the_context ())"

By looking at some of them you will quickly learn how to make your own ones if
you need them.

3) is it possible to do a termination proof for a recdef definition fully by hand in order to make sure, that i : {0..<length ts} is used?

Yes you can, by a largely unkown feature:

Issue your recdef definition using the "permissive" keyword:

recdef (permissive) pos ....

Then the defintion goes through, but the unproven termination conditions end up as premises of the pos.simps rules:

thm pos.simps

Then you can set up a manual proof by

recdef_tc abc: pos

and when you have finished the proof, the lemmas will be stored as "abc". You
will still have to remove the premises manually from pos.simps though.

The above information is for Isabelle 2005. In the developer snapshot you would
instead use the new "function" package. There, handling termination proofs is
easier and can be done manually, but the issue with congruence rules remains.

Hope this helps...

Alex





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