Hi Liya, | Could I use the related theorem of HOL Light in HOL? Actually, I need | use List or Vector in HOL now. However, I don't know how to use a list | or vector in HOL, although I know a rich source of theorems on Vector | can be find in HOL Light. Since I have to use some other important | theorems in HOL, Could you give me some information?
You could either transfer the theories at the "object code" level, i.e. copying the primitive inferences, or at the "source code" level by adapting the HOL Light tactic scripts. The latter is more elegant and might give you the chance to improve or modify things as you go, but it would probably be a significant expenditure of effort since the higher-level rules and tactics are a bit different in the two systems. So if you just want to get something going quickly, the "object code" method may be more efficient. Indeed, it's not difficult in principle to import proofs via copying the primitive inferences. (Though it can get a bit trickier if things are defined differently in the two systems.) For example, HOL Light already has a library written by Steven Obua to record the primitive inferences used in proofs while HOL Light runs, so they can be imported by another system (see the "Proofrecording/" subdirectory). Steven's original setup was mainly intended for import into Isabelle/HOL but it could be exploited by other systems. Chantal Keller has recently adapted it to import HOL Light proofs into Coq. There are also two other more ambitious setups under development for transferring low-level proofs between HOL systems in several directions, one due to Mark Adams and the other to Joe Hurd. Either of these is probably usable to do what you want, or could be made so without too much more work. John. ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
