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 9, 2017 at 8:07 AM, Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:
> 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, and
> relabeling operation is inverting the SND of pairs. Is this idea
> recommended? (although I see no benefits other than shorter generated
> theory files)
>
> Regards,
>
> Chun Tian
>
>
>
> On 9 October 2017 at 13:58, Chun Tian (binghe) <binghe.l...@gmail.com>
> wrote:
>
>> 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 HOL's example
>> directory, I suddenly realized: isn't the "Action" type a perfect case to
>> use HOL's optionTheory? that is, using NONE as tau (invisible action), and
>> SOME for all others:
>>
>> val _ = type_abbrev ("Action", ``:'b Label option``);
>> val _ = overload_on ("tau", ``NONE :'b Action``); (* NONE is invisible
>> (tau) *)
>> val _ = overload_on ("label", ``\(l :'b Label). SOME l``);
>>
>> optionTheory provided already the induction, nchotomy, one_one, ...
>> theorems, so all I need to do is to use INST_TYPE to convert them into
>> theorems for my fake "Action" type, e. g.
>>
>> (* Define structural induction on actions
>> |- ∀P. P tau ∧ (∀L. P (label L)) ⇒ ∀A. P A
>> *)
>> val Action_induction = save_thm (
>> "Action_induction", INST_TYPE [``:'a`` |-> ``:'b Label``]
>> option_induction);
>>
>> So I've made the changes, and it works amazingly well. Isn't this too
>> perfect?
>>
>> P. S. Is there any existing "simple" type in HOL such that I can prevent
>> using Datatype for defining the "Label" type?
>>
>> Regards,
>>
>> Chun Tian
>> 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
