Re: [Hol-info] How to define term-like multi-recursive structures?

2017-10-30 Thread Chun Tian
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 ->

Re: [Hol-info] How to define term-like multi-recursive structures?

2017-10-29 Thread Michael.Norrish
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

Re: [Hol-info] How to define term-like multi-recursive structures?

2017-10-27 Thread Chun Tian
> 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

Re: [Hol-info] How to define term-like multi-recursive structures?

2017-10-26 Thread Michael.Norrish
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

Re: [Hol-info] How to define term-like multi-recursive structures?

2017-10-26 Thread Chun Tian (binghe)
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> >

Re: [Hol-info] How to define term-like multi-recursive structures?

2017-10-26 Thread Chun Tian (binghe)
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

Re: [Hol-info] How to define term-like multi-recursive structures?

2017-10-25 Thread Michael.Norrish
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