[Hol-info] polyml thread support

Hey, Can I use the thread support in PolyML to do this task? and how? I'd like to run a ML function, which runs a HOL proof, for a certain amount of time, say 20 seconds, and if the function hasn't terminated by this time limit, I want to kill that thread and run the same function again with a dif

[Hol-info] convert HOL formula to latex

Hi, I'd like to put some HOL theorems in a paper that is written in latex. Is there an easy way to format HOL formulas nicely in latex? Thanks. Lu -- ___ hol-info mailing list

[Hol-info] Tex Package for \HOLTokenEquiv

Hi, I'm using EmitTeX to convert a HOL theorem into a TeX string, the function print_theorem_as_tex generates a token: \HOLTokenEquiv. Which package should I add in order for Tex to recognize this command except holtexbasic and holtex? Where to get it? Thanks. Lu

[Hol-info] convert an SML int variable into a word32 term?

Hey, Suppose there is a variable in SML: val v = 0xA How can I get a term which has the value of "v" in word32? I found mk_word in wordsSyntax, but I have no idea what the second parameter should be (I guess the first might be v)? Thanks. Lu --

[Hol-info] Compress HOL message for match_term

Hi, When I use match_term with some types unspecified, HOL always generates a message similar to the following: <> Is there a way to depress the message so that I don't have to see a long list of messages. Specifying the types is not a good option since the matched terms have multiple types a

[Hol-info] efficient way to prove concrete sets disjoint?

Hi, I'd like to prove two sets disjoint. Currently, I use DISJOINT_DEF,INTER_DEF,EXTENSION to rewrite the goal first, then Cases_on each bound, and finally use WORD_DECIDE_TAC. This approach works, but it takes a long time. For example, it takes over 40s to prove the following theorem: DI

[Hol-info] specify an out-of-order universally quantified variables?

Hi, I have a theorem of the form: !x1 x2 ... x(i-1) xi x(i+1) ... xn. t and I'd like to instantiate xi to another term, say y, without touching other universally quantified variables, namely, I want to rewrite it to: !x1 x2 ... x(i-1) x(i+1) ... xn. t[y/xi] Is there a handy operation for this

[Hol-info] subset relation in set match

Hi, I've a question on proving set subset relation, and apply MATCH to set. Here's a goal: ?la ins. ins IN c /\ INS_SPEC lq ins la 0. !lq. lq IN BIGUNION {run_to i lp c | i < k} ==> ?la ins. ins IN c /\ INS_SPEC lq ins la 1. i <

[Hol-info] solved - subset relation in set match

I've solved the problem by using GSPECIFICATION and other arithmetic simps. Thanks. Lu Hi, I've a question on proving set subset relation, and apply MATCH to set. Here's a goal: ?la ins. ins IN c /\ INS_SPEC lq ins la 0. !lq. lq IN BIGU

[Hol-info] pair matching problem in Hol_reln

Hi, I'm having a problem in matching pairs when using inductive relation for proof. It can be demonstrated by the following example. Suppose I define a relation: val (PEQ_rules, PEQ_ind, PEW_cases) = Hol_reln ` (!l1:num a1:num l2:num a2:num. (l1 = l2) ==> PEQ (l1,a1) (l2,a2))` val [PEQ_INS]

[Hol-info] move quantifiers to the very front?

Hi, Is there a theorem that I can move (existential) quantifiers to the very front of an assumption? For example, goal p ==> ?x y. (?u v. q u v \/ m u v) /\ t x y I'd like to get something like: goal p ==> (q u v \/ m u v) /\ t x y Thanks a lot. Lu -

[Hol-info] word inequality tac?

Hi, I have an inequality proof: ``(p:bool[32]) + 0x4w <> p + 0x8w`` How should I proceed to prove it? Lu -- Return on Information: Google Enterprise Search pays you back Get the facts. http://p.sf.net/sfu/google-dev2d

Re: [Hol-info] word inequality tac?

? Lu > simpLib.SIMP_PROVE (srw_ss()++wordsLib.WORD_ARITH_EQ_ss) [] > ``(p:bool[32]) + 0x4w <> p + 0x8w``; > > Anthony. > > On 12 Dec 2009, at 00:21, Lu Zhao wrote: > >> Hi, >> >> I have an inequality proof: >> >> ``(p:bool[32]) + 0x4w

[Hol-info] make polyml display integer in hex format

Hi, Is there a way to make polyml display an integer in its hex format? For example, > 0x12; val it = 18 : int I want to have 0x12 echoed back instead of 18. Thanks. Lu -- This SF.Net email is sponsored by the Verizo

[Hol-info] How to remove a same function in a goal

Hi, I have a goal looks like the following `f x = f y` I want to reduce it to `x = y` How can I do this, if it's doable? Thanks. Lu -- Download Intel® Parallel Studio Eval Try the new software tools for yourself. Spe

[Hol-info] Prove a simple word expression

Hi, How can I proceed to prove this seemingly very simple expression? I'm not familiar with word proofs. ``(0x3w && (x :bool[32]) + 0x4w = 0x0w) <=> (0x3w && x = 0x0w)`` or more general, ``(0x3w && (x :bool[32]) + y * 0x4w = 0x0w) <=> (0x3w && x = 0x0w)`` Any suggestion is appreciated. Thank

[Hol-info] Programming goal stack?

Hi, I have a situation where I don't know what the best solution is. I have a goal of the form x ==> y, and after an initial rewrite on x and after REPEAT STRIP_TAC, I have a list of subgoals. Here's the problem. 1) According to different situations, the length of the list of subgoals varies;

Re: [Hol-info] Programming goal stack?

small theorems. Thank you anyway. Lu liy_...@encs.concordia.ca wrote: > Please give more details on your goal. > > Good Luck, > Liya > > Quoting Lu Zhao : > >> Hi, >> >> I have a situation where I don't know what the best solution is. >> >

[Hol-info] a better way to simplify an UPDATE function

Hi, I have an UPDATE function simplified as: ((a =+ x) ((b =+ y) ((a =+ z) f))) or some other format, where updating on the same element is separated by updating on other elements: ((a =+ x) ((b =+ y) ... ((a =+ z) f) ...)) I wan to remove the redundant inner updates, but when I use UPDATE_E

[Hol-info] proof automation using sml structure

Hi, Although this is not an SML list, I come across this problem when using HOL, and I think there are many SML exports here, so I just ask this question. I wrote an SML functor to facilitate some proof automation. I have several proof cases. For each case, I create a structure from the funct

Re: [Hol-info] proof automation using sml structure

FYI, I'm using PolyML 5.4. Lu Zhao wrote: > Hi, > > Although this is not an SML list, I come across this problem when using > HOL, and I think there are many SML exports here, so I just ask this > question. > > I wrote an SML functor to facilitate some proof aut

[Hol-info] Defining a relation using Hol_reln?

Hi, I'm having the following error when I attempt to define a relation with Hol_reln: Exception raised at IndDefLib.Hol_reln: at IndDefLib.Hol_mono_reln: at IndDefRules.derive_strong_induction: at Thm.EQ_MP: The failure of "derive_strong_induction" happens for a situation like the following. I

[Hol-info] how to remove a defined constant?

Hi, I have a situation like this that makes removing a defined term desirable. I first define a function: val FOO_def = Define `FOO bsp ksp = ...` and later its parameter val bsp_def = Define `bsp = ...` I define bsp_def, because the right hand side of bsp definition is very long for which I

Re: [Hol-info] proof automation using sml structure

Michael Norrish wrote: > On 14/02/11 04:38, Lu Zhao wrote: > >> I wrote an SML functor to facilitate some proof automation. I have >> several proof cases. For each case, I create a structure from the >> functor and use the structure to prove the case. This seems fine un

Re: [Hol-info] proof automation using sml structure

l result = C.compute(); Some people may not like the idea of using references in functional programming, but it gives a nicer interface in this case. Cheers! Lu Lu Zhao wrote: > Michael Norrish wrote: >> On 14/02/11 04:38, Lu Zhao wrote: >> >>> I wrote an SML functor to f

[Hol-info] useful HOL statistics to show the amount of proof work?

Hi, First, please forgive me if this question is too silly. I had this question when I talked to a colleague, who has no idea about theorem proving at all, about the amount of proof work that can be involved in solving a problem. How to evaluate the amount of proof work that HOL does? What are

Re: [Hol-info] useful HOL statistics to show the amount of proof work?

> I would like to know how we can collect these information, I mean the > run time, gctime, and primitive inference steps and so on, especially in I found out in Count.sml that there are other utilities available, too. For example, you can use the following to start counting: val meter = Count.m

[Hol-info] creating a set with a customized order function?

Hi, I have a set whose elements are pairs, and I want to use a comparison function on the first element of the pair in the set operation. For example, val e1 = ``(0x1w:word32, 4:num)``; val e2 = ``(0x1w:word32, 8:num)``; val s1 = mk_insert(e2, mk_insert(e1,``{}:(word32#num) set``)) when I use S

Re: [Hol-info] creating a set with a customized order function?

On 04/13/2011 05:54 PM, Michael Norrish wrote: > On 14/04/11 08:35, Lu Zhao wrote: >> when I use SIMP_CONV (std_ss++PRED_SET_ss) [] s1, I want to get >> something like: > >> {(0x1w,8); (0x1w,4)} = {(0x1w,x)} > >> where x is either 8 or 4, since I don't care

[Hol-info] migrate to new version: temp_add_user_printer

Hi, I have a pretty printer function added by using temp_add_user_printer. It looks like the following: -- fun pp_lins Gs sys (ppsFun:ppstream_funs) gravs d pps t : unit = let val (label, code) = (dest_pair) t val ins = code

Re: [Hol-info] useful HOL statistics to show the amount of proof work?

/07/2011 11:29 AM, Lu Zhao wrote: > I found out in Count.sml that there are other utilities available, too. > For example, you can use the following to start counting: > > val meter = Count.mk_meter(); > > and use > > Count.report(Count.read meter); > > to see the statist