Re: [Hol-info] Difficulties in proving the termination of a recursive function

You could make the definition with J as a list instead of a set. (Then you can define a set version in terms of that using SET_TO_LIST if you want.) Or you could do something like `FN p J = if FINITE J then case p of ... else ARB`. But that's probably more trouble than using a list. On 2 July

Re: [Hol-info] Difficulties in proving the termination of a recursive function

> because J is *NOT* assumed to be FINITE. On 1 July 2017 at 16:51, Chun Tian (binghe) wrote: > No ... my previous idea doesn't work. I got this goal unprovable: > > CARD (J DELETE a) < CARD J > > a ∈ J > > because J is assumed to be

Re: [Hol-info] Difficulties in proving the termination of a recursive function

No ... my previous idea doesn't work. I got this goal unprovable: CARD (J DELETE a) < CARD J a ∈ J because J is assumed to be FINITE. I think I still need to know how to put the cardinality bound into the relation for WF_REL_TAC ... Regards, Chun On 1

Re: [Hol-info] Difficulties in proving the termination of a recursive function

Hi again, I think it's possible to change the original definition to make the cardinality *decrease* instead: previous I use the set J as the set of constants that have already been processed, but I can also rethink it as the set of contants that *remains to be processed*: So now I have a

Re: [Hol-info] Difficulties in proving the termination of a recursive function

Hi Ramana, Thanks very much! Yes, actually I was seeking HOL's operator for building lexicographic relations but couldn't find it... For the cardinality of J, it will finally equal to the number of ``rec`` operators inside the input CCS term, and loosely speaking, ``CARD J`` should always

Re: [Hol-info] Difficulties in proving the termination of a recursive function

Hi Chun, Your relation that works looks like a lexicographic relation, which is something wf_rel_tac should be able to handle automatically. Could you try providing it using the LEX combinator, e.g., wf_rel_tac`inv_image ($< LEX $<) (\x y. (size(FST x), CARD(SND y)))` Actually, looking more

Re: [Hol-info] Difficulties in proving the termination of a recursive function

Hi Chun Tian, I'd have to look more closely at your desired function to be able to help. But, it's late and my eyes are giving out. If all you are after is to compute free names, maybe there is a better way. The following is what I would do for defining an operation calculating the free

[Hol-info] Difficulties in proving the termination of a recursive function

Hi, I have an inductive datatype called CCS and a recursive function FN trying to collect all free names of any CCS term into a set: val FN_def = Define ` (FN (nil :('a, 'b) CCS) (J: 'a set) = (EMPTY :'b Label set)) /\ ... (FN (rec x p) J = if (x IN J) then EMPTY else FN (CCS_Subst p (rec