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 2017 at 00:52, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> > because J is *NOT* assumed to be FINITE.
>
> On 1 July 2017 at 16:51, Chun Tian (binghe) <binghe.l...@gmail.com> 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 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 July 2017 at 16:28, Chun Tian (binghe) <binghe.l...@gmail.com>
>> wrote:
>>
>>> 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 definition like this:
>>>
>>> val FN_defn = Hol_defn "FN" `
>>> (FN (nil :('a, 'b) CCS) (J: 'a set) = (EMPTY :'b Label set)) /\
>>> (FN (prefix (label l) p) J = l INSERT (FN p J)) /\
>>> (FN (prefix tau p) J = FN p J) /\
>>> (FN (sum p q) J = (FN p J) UNION (FN q J)) /\
>>> (FN (par p q) J = (FN p J) UNION (FN q J)) /\
>>> (FN (restr L p) J = (FN p J) DIFF (L UNION (IMAGE COMPL_LAB L))) /\
>>> (FN (relab p rf) J = IMAGE (REP_Relabeling rf) (FN p J)) /\
>>> (FN (var x) J = EMPTY) /\
>>> (FN (rec x p) J = if (x IN J) then
>>> FN (CCS_Subst p (rec x p) x) (J DELETE x)
>>> else EMPTY) `;
>>>
>>> and by following your way, using: WF_REL_TAC `inv_image ($< LEX $<) (\x.
>>> (size (FST x), CARD (SND x)))`, and then I have the following sub-goal
>>> which looks perfect: (and no need to prove the well-foundness any more)
>>>
>>> Current goal:
>>>
>>> size (CCS_Subst p (rec x p) x) < size (rec x p) ∨
>>> (size (CCS_Subst p (rec x p) x) = size (rec x p)) ∧
>>> CARD (J DELETE x) < CARD J
>>> ------------------------------------
>>> x ∈ J
>>>
>>> To actually use this definition, I need to set the initial J set as the
>>> set of all constants in the CCS term, but that's irrelevant to the above FN
>>> definition. So I would say my initial problem has completely resolved.
>>>
>>> Thank you again!!!
>>>
>>> Regards,
>>>
>>> Chun Tian
>>>
>>>
>>> On 1 July 2017 at 12:55, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:
>>>
>>>> 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 closely, I see that you want the cardinality of
>>>> J to _increase_. This is not obviously well-founded: can you explain what
>>>> the upper limit of the cardinality of J is, and incorporate this into the
>>>> relation?
>>>>
>>>> Cheers,
>>>> Ramana
>>>>
>>>> On 1 July 2017 at 19:51, Konrad Slind <konrad.sl...@gmail.com> wrote:
>>>>
>>>>> 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 variables
>>>>> in the lambda calculus, and the same idea should I hope also work for
>>>>> CCS. The main benefit is that
>>>>> you don't have a call to another function (substitution) in the
>>>>> recursive call. And termination
>>>>> is trivial.
>>>>> ------------------------------------------------------------
>>>>> ---------------------------------------
>>>>> load "stringLib";
>>>>>
>>>>> Datatype `term = Var string | App term term | Abs string term`;
>>>>>
>>>>> val FV_def =
>>>>> Define
>>>>> `(FV (Var s) scope = if s IN scope then {} else {s}) /\
>>>>> (FV (App t1 t2) scope = FV t1 scope UNION FV t2 scope) /\
>>>>> (FV (Abs v t) scope = FV t (v INSERT scope))`;
>>>>>
>>>>>
>>>>> On Sat, Jul 1, 2017 at 4:14 AM, Chun Tian (binghe) <
>>>>> binghe.l...@gmail.com> wrote:
>>>>>
>>>>>> 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 x p) x)
>>>>>> (x INSERT J))`;
>>>>>>
>>>>>> val free_names = new_definition ("free_names",
>>>>>> ``free_names p = FN(p, EMPTY)``);
>>>>>>
>>>>>> The only reason that HOL can’t prove the termination is because of
>>>>>> the last branch in above definition involving another recursive function
>>>>>> CCS_Subst: in some cases the term ``(CCS_Subst p (rec x p) x)`` may
>>>>>> return
>>>>>> ``(rec x p)``, and as a result, the size of the first parameter of FN
>>>>>> doesn’t decrease!
>>>>>>
>>>>>> But this is why I have the second parameter J of FN: whenever
>>>>>> calculating the value of ``FN (rec x p) J``, it first check if x is in
>>>>>> the
>>>>>> set J, and the recursive call happens only if it’s not in, and then x is
>>>>>> inserted into J to prevent further recursive invocation of FN at deeper
>>>>>> levels. So I believe above definition is well-defined and must always
>>>>>> terminate. In another words, for all other branches, the size of CCS
>>>>>> term
>>>>>> must decrease in recursive calls, and in the last branch, the cardinality
>>>>>> of the set J will increase.
>>>>>>
>>>>>> I firstly tried to use WF_REL_TAC with a measure, but I could NOT
>>>>>> find a good measure with both parameters considered. For example, if I
>>>>>> use
>>>>>> “the size of CCS term MINUS the cardinality of the set J”, which seems
>>>>>> always decrease in each recursive calls, i.e. WF_REL_TAC `measure (\x.
>>>>>> (size o FST) x - (CARD o SND) x)`, this is actually not a measure,
>>>>>> because it may also take negative values, thus not WF at all.
>>>>>>
>>>>>> Now if I try to use Defn.tgoal to find the tacticals which helps HOL
>>>>>> to prove the termination, I got the following initial goal:
>>>>>>
>>>>>> Initial goal:
>>>>>>
>>>>>> ∃R.
>>>>>> WF R ∧
>>>>>> (∀p J x.
>>>>>> x ∉ J ⇒ R (CCS_Subst p (rec x p) x,x INSERT J) (rec x p,J)) ∧
>>>>>> (∀q J p. R (p,J) (p || q,J)) ∧ (∀p J q. R (q,J) (p || q,J)) ∧
>>>>>> (∀q J p. R (p,J) (p + q,J)) ∧ (∀p J q. R (q,J) (p + q,J)) ∧
>>>>>> (∀l J p. R (p,J) (label l..p,J)) ∧
>>>>>> (∀rf J p. R (p,J) (relab p rf,J)) ∧ (∀J p. R (p,J) (τ..p,J)) ∧
>>>>>> ∀L J p. R (p,J) (ν L p,J)
>>>>>>
>>>>>> So the goal is nothing but to supply a relation such that, the
>>>>>> parameter pairs in each recursive call must be strictly “smaller”. But
>>>>>> if
>>>>>> I supply such a relation:
>>>>>>
>>>>>> Q.EXISTS_TAC `\x y. (size (FST x) < size (FST y)) \/
>>>>>> ((size (FST x) = size (FST y)) /\ (CARD (SND x) > CARD (SND
>>>>>> y)))`
>>>>>>
>>>>>> which seems precisely captured my understanding on the termination
>>>>>> condition. But the funny thing is, I can prove all the sub-goals except
>>>>>> for
>>>>>> the well-foundness (that is, WF R), which is automatically handled in the
>>>>>> WF_REL_TAC approach.
>>>>>>
>>>>>> Can anyone suggest me some ideas or possible paths to resolve this
>>>>>> issue? or possible ways to prove the WF of arbitrary relations? Since all
>>>>>> the related defintions are long and omitted, I’m not expecting any
>>>>>> ready-to-use scripts.
>>>>>>
>>>>>> Regards,
>>>>>>
>>>>>> Chun Tian
>>>>>>
>>>>>> --
>>>>>> Chun Tian (binghe)
>>>>>> University of Bologna (Italy)
>>>>>>
>>>>>>
>>>>>> ------------------------------------------------------------
>>>>>> ------------------
>>>>>> Check out the vibrant tech community on one of the world's most
>>>>>> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>>>>>> _______________________________________________
>>>>>> hol-info mailing list
>>>>>> hol-info@lists.sourceforge.net
>>>>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>>>>
>>>>>>
>>>>>
>>>>> ------------------------------------------------------------
>>>>> ------------------
>>>>> Check out the vibrant tech community on one of the world's most
>>>>> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>>>>> _______________________________________________
>>>>> hol-info mailing list
>>>>> hol-info@lists.sourceforge.net
>>>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>>>>
>>>>>
>>>>
>>>
>>>
>>> --
>>> Chun Tian (binghe)
>>> University of Bologna (Italy)
>>>
>>>
>>
>>
>> --
>> Chun Tian (binghe)
>> University of Bologna (Italy)
>>
>>
>
>
> --
> Chun Tian (binghe)
> University of Bologna (Italy)
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
