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 <konrad.sl...@gmail.com>
> ha scritto:
>
> 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
>
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
