Hi,
thanks for your further comments. But now I feel maybe it’s worth to attack
the more difficult problem instead: porting the BNF_datatype [1] to HOL4. Once
this is done, not only I can use finite maps directly in the datatype
definition, but also I could easily have infinite sums (:num ->
You would have to define every function in terms of “fix” and then come up with
a clause for the new constant using “Fix” as well (or prove a new “axiom” for
the type). You would also need to prove new induction and cases theorems. But
yes, this “cheap approach” might be doable.
Michael
On
> Il giorno 27 ott 2017, alle ore 17:35, Chun Tian ha
> scritto:
>
> Thanks for your comments.
>
> If I quotient [1] the original CCS datatype into another one, I could expect
> to have the a “fix” constructor with a finite map, right?
>
> On the the other side, what
chael.norr...@data61.csiro.au>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] How to define term-like multi-recursive structures?
Hi again,
I'm surprised that, ``('a, 'b) alist`` (or ``('a # 'b) list``) is supported by
datatype package. So I'm going to have the
haviours in time. Perhaps one
>> approach would be to define the syntax as a co-datatype, allowing the
>> syntax itself to be infinite. This'd be a bit weird though…
>>
>> Michael
>>
>> From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
>
t weird though…
>
> Michael
>
> From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
> Date: Thursday, 26 October 2017 at 00:05
> To: hol-info <hol-info@lists.sourceforge.net>
> Subject: [Hol-info] How to define term-like multi-recursive str
fine the syntax as a co-datatype, allowing the syntax itself to be
infinite. This'd be a bit weird though…
Michael
From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
Date: Thursday, 26 October 2017 at 00:05
To: hol-info <hol-info@lists.sourceforge.net>
Subject: [Hol-info] How t