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
