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, my previous type abbreviation for Action has little problems: defining ``:’b Action`` as ``:‘b Label option`` won’t cause any confusion, and constants like NONE and SOME still have usual display:
> ``NONE``;
val it =
“(NONE :α option)”:
term
> ``tau``; (* this is actually a NONE *)
val it =
“(τ :α Action)”:
term
If I had ``’b Label`` abbreviated as ``:’b + ‘b``, then ``’b Action`` becomes
``:(’b + ‘b) option``, it seems a disaster again. So my current experience
is, when creating type abbreviations, I should either create complex
combination of primitive types, or simple sum or prod types based on new types
(i.e. defined by Datatype or type bijections, etc).
Regards,
Chun Tian
> Il giorno 10 ott 2017, alle ore 00:32, <michael.norr...@data61.csiro.au>
> <michael.norr...@data61.csiro.au> ha scritto:
>
> 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.
>
> One issue with the type abbreviation approach is that you will find the
> pretty-printer describing bool # bool as a bool Label. (You can turn this
> off though, just as the set abbreviation is turned off for printing in the
> pred_set theory.)
>
> Michael
>
> From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
> Date: Tuesday, 10 October 2017 at 00:09
> To: hol-info <hol-info@lists.sourceforge.net>
> Subject: 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, 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
