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)
------------------------------------------------------------------------------
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
