Hi list, is there a good reason for not using Ocaml modules in HOL Light?
This would yield a better name management, and shorter and more readable proofs. For instance, instead of having: # REAL_ADD_SYM;; val it : thm = |- !x y. x + y = y + x # REAL_ADD_LID;; val it : thm = |- !x. &0 + x = x # REAL_ADD_ASSOC;; val it : thm = |- !x y z. x + y + z = (x + y) + z # ... We could have: module Real : sig val ( ADD_SYM ) : thm val ( ADD_LID ) : thm val ( ADD_ASSOC ) : thm ... end And similarly: module Complex : sig val ( ADD_SYM ) : thm val ( ADD_LID ) : thm val ( ADD_ASSOC ) : thm ... end Then, if in a context where real numbers are prominent, one could just open the Real module, but still access Complex theorems by using the dot notation. Going further, we could even use the local opening (http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc77) or aliasing (http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc74) of modules. But both seem incompatible with the current camlp5 extension used by HOL Light. -- Vincent Aravantinos Postdoctoral Fellow, Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
