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
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
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
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
--
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
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
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
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 <
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
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]
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
-
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
?
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
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
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
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
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;
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.
>>
>
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
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
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
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
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
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
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
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
> 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
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
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
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
/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
31 matches
Mail list logo