Yesterday I wanted to change the definition of my datatype to support
summing over a set of values of the same type:
val _ = Datatype `CCS = nil
| var 'a
| prefix ('b Action) CCS
| summ (CCS set) (num set)`;
if so, then the original binary "sum" will become the new summ operator
over a two-element set. Later I may even change "num set" into ('a ordinal
-> bool).
But HOL doesn't allow me to do so, strangely saying "can't find definition
for nested type: fun"
Exception raised at Datatype.Hol_datatype:
at ind_types.define_type:
at ind_types.define_type_nested:
Can't find definition for nested type: fun
Exception-
HOL_ERR
{message =
"at ind_types.define_type:\nat ind_types.define_type_nested:\nCan't
find definition for nested type: fun",
origin_function = "Hol_datatype", origin_structure = "Datatype"}
raised
What's the problem here? How can I correctly define such a datatype?
Regards,
Chun
On 3 July 2017 at 13:22, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> Hi,
>
> Currently I have the following Datatype "(‘a, ‘b) CCS" which supports
> binary “sum” operation:
>
> val _ = Datatype `CCS = nil
> | var 'a
> | prefix ('b Action) CCS
> | sum CCS CCS
> ...`;
>
> I also have a recursive function for calculating the “sum” of this
> datatype stored in a function: f(0) + f(1) + f(2) + … + f(n)
>
> val CCS_SIGMA_def = Define `
> (CCS_SIGMA (f :num -> ('a, 'b) CCS) 0 = f 0) /\
> (CCS_SIGMA f (SUC n) = sum (CCS_SIGMA f n) (f (SUC n))) `;
>
> val _ = overload_on ("SIGMA", ``CCS_SIGMA``);
>
> I don’t like above CCS_SIGMA_def, maybe later I’ll switch to another
> definition more like the SUM_IMAGE defined in HOL’s pred_setTheory:
>
> val SUM_IMAGE_DEF = new_definition(
> "SUM_IMAGE_DEF",
> ``SUM_IMAGE f s = ITSET (\e acc. f e + acc) s 0``);
>
> which takes a set of numbers as the second parameter, looks more flexible.
> But it seems that all related theorems have to assume the finiteness of the
> set parameter.
>
> My questions are:
>
> 1. is it possible to define a special SUM_IMAGE for my CCS datatype, and
> it also supports (countable) infinite sums: ``SUM_IMAGE p (UNIV: num)``
> valid and meaningful?
>
> 2. if this is impossible, what’s the necessary modification to the
> original datatype definition?
>
> 3. what’s the necessary modification to support sums over limit ordinals
> (using HOL’s ordinalTheory in examples)? that is, for L a limit ordinal, I
> need to construct a sum of all ordinals M smaller than L: SUM f(M), for all
> M < L
>
> 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
