Re: [Hol-info] The use of optionTheory for representing invisible actions in transition systems

Hi Michael, Thanks for your comments. Yes, I've realized that my sum type should be “beta + beta” after Konrad raised up sumTheory. I’ve seen how pred_setTheory disabled the pretty-printing of ``:’a set``, and I’m also trying to not introduce simple type abbreviations. On the other side,

Re: [Hol-info] [ExternalEmail] Re: Is ``:string ordinal`` uncountable or not?

Apologies for duplicated paragraphs below… Michael On 10/10/17, 09:27, "michael.norr...@data61.csiro.au" wrote: Strings have the same cardinality as numbers (there is a bijection between them established in string_numTheory), so string ordinal will be the

Re: [Hol-info] The use of optionTheory for representing invisible actions in transition systems

I think this is a case of “try it and see”. As per Konrad, it might be more natural to use sums, which is essentially what your original type was. But as both arguments were the same beta parameter, your sum was effectively beta + beta. Switching to a product beta * 2 is clearly equivalent.

Re: [Hol-info] Is ``:string ordinal`` uncountable or not?

Strings have the same cardinality as numbers (there is a bijection between them established in string_numTheory), so string ordinal will be the same type (up to isomorphism) as num ordinal. There’s no general way to know what the cardinality of a type is unless you have theorems to hand that

[Hol-info] Is ``:string ordinal`` uncountable or not?

Hi, In Michael Norrish and Brian Huffman's paper [1] about HOL’s ordinals, it’s said, “the distinct types ``:unit ordinal``, ``:bool ordinal``, and ``:num ordinal`` will all be isomorphic (they will all be copies of the countable ordinals).” “On the other hand, the type “:(num -> bool)

Re: [Hol-info] The use of optionTheory for representing invisible actions in transition systems

Hi Konrad, Thanks for your comments. I know a little about sum types but never go chances to use it. I’m going to keep my current Action type (based on optionTheory) and not touch the Label type. Regards, Chun Tian > Il giorno 09 ott 2017, alle ore 15:44, Konrad Slind

Re: [Hol-info] The use of optionTheory for representing invisible actions in transition systems

Hi Chun Tian, For your Label type the most appropriate primitive type would be sums (co-products). These are formalized in sumTheory, so you could look at that if you are interested. However, I think you might lose some clarity in your formalization by using them. Cheers, Konrad. On Mon, Oct

Re: [Hol-info] The use of optionTheory for representing invisible actions in transition systems

Hi again, For example, if I use pairTheory to represent my Label type, something like: val _ = type_abbrev ("Label", ``'b # bool``); val _ = overload_on ("name", ``\s. (s, T)``); val _ = overload_on ("coname", ``\s. (s, F)``); then retrieving the underlying names is simply the FST of the pair,

[Hol-info] The use of optionTheory for representing invisible actions in transition systems

Hi, I was having the following two Datatype definitions for representing "labels" and "actions" in transition systems like CCS/LTS: val _ = Datatype `Label = name 'b | coname 'b`; val _ = Datatype `Action = tau | label ('b Label)`; But yesterday, after my thesis work has been committed into