*To*: Christian Sternagel <christian.sternagel at uibk.ac.at>*Subject*: Re: [isabelle] recdef problem*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Thu, 22 Feb 2007 18:39:41 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20070221132123.GA3967@pc6197-c703.uibk.ac.at>*References*: <20070221132123.GA3967@pc6197-c703.uibk.ac.at>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.3)

Christian,

I wanted to define following function (which gives the set ofpositions of a term---where a position is a possibly empty list ofnatural 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 frommy 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 makethe unsolved goal equivalent to:

You are missing a congruence rule here. Congruence rules are needed for recdef

following congruence rule for conjunction helps: lemma conj_cong[recdef_cong]: "[| A = A'; A' ==> B = B' |] ==> A & B = A' & B' " by blast

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

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 definitionfully 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 ....

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.

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

**References**:**[isabelle] recdef problem***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] isatool make for document preparation
- Next by Date: Re: [isabelle] isatool make for document preparation
- Previous by Thread: [isabelle] recdef problem
- Next by Thread: [isabelle] post-doc position in Paris
- Cl-isabelle-users February 2007 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