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<mailto: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
