I use Ramana’s HOL mode for Vim, shortcut “hl”. That makes use of
HOL_Interactive.toggle_quietdec
For example, you can do
> HOL_Interactive.toggle_quietdec();
> open prim_recTheory pairTheory listTheory rich_listTheory;
> open ...
> HOL_Interactive.toggle_quietdec();
The advantage of the Vim
A starting point might be to use the function real_to_arbrat in binary_ieeeLib.
https://github.com/HOL-Theorem-Prover/HOL/tree/master/src/floating-point
For example, the following is one method to get a result:
fun arbrat_to_math_real x =
Real./ (Real.fromInt (Arbint.toInt (Arbrat.numerator
Your original goal seemed to be just an instance of
pred_setTheory.SUBSET_REFL
|- !s. s SUBSET s
Are you actually trying to prove:
!A. IMAGE FST (A CROSS A) SUBSET A
?
If so, you could have:
Q.prove(
`!A. IMAGE FST (A CROSS A) SUBSET A`,
simp [pred_setTheory.SUBSET_DEF]
\\ metis_tac
As an alternative workaround, you could edit the files in the
src/floating-point directory to remove the dependency on PackRealBig. For
example, you could try commenting out the lines
val floatToReal : term -> real
val wordToReal : term -> real
val realToFloat : real -> term
val
library) also support the generation of
witnesses for such theorems?
Thank you!
Regards,
Jiaqi
On Fri, Jun 27, 2014 at 6:23 PM, Anthony Fox ac...@cam.ac.uk wrote:
The tactic
ACCEPT_TAC
(blastLib.BBLAST_PROVE
``?r:word8. 100w ≤₊ r + 251w ∧ r + 251w ₊ 200w
I think it’s more likely that there was a problem with building minisat under
the latest Mac OS. To check that it is installed, try going to the directory
HOL/src/HolSat/sat_solvers/minisat
There should be a binary “minisat” there. Alternatively, to make sure it is
working properly, you can
-code/ (exited with code 1)
However, I do have compiler_demoScript.sml in
examples/machine-code/compiler/demo.
Thanks,
Jiaqi
On Sat, Apr 5, 2014 at 5:29 AM, Anthony Fox ac...@cam.ac.uk wrote:
I think it’s more likely that there was a problem with building minisat under
the latest Mac
How about
term_grammar.get_precedence (Parse.term_grammar())
?
On 10 Feb 2014, at 09:35, Ramana Kumar ramana.ku...@cl.cam.ac.uk wrote:
Is there a way to find the precedence/fixity information about a token in the
term grammar that is better than using Parse.term_grammar() and sifting
Hi Oliver,
Yes, the approach of the former ARMv7 model doesn’t translate naturally to the
new L3 setting. That is, it’s not possible to call co-processor “hook”
functions within the L3 specification itself.
I can think of two options:
1. If you want to model a specific co-processor then it’s
Rob,
On 29 Dec 2013, at 21:26, Rob Arthan r...@lemma-one.com wrote:
The code for HOL4 set abstractions says that the bound variables
of a set abstraction {t | p} are the intersection of the free variables
of t and p unless either side has no free vars, in which case the
bound variables
Just to add to Konrad’s e-mail.
There is a list “write operation in listTheory — it is defined as follows:
(∀e n. LUPDATE e n [] = []) ∧
(∀e x l. LUPDATE e 0 (x::l) = e::l) ∧
∀e n x l. LUPDATE e (SUC n) (x::l) = x::LUPDATE e n l
Other representation choices include:
- functions of type :
Hi Hamed,
Yes, the side-condition
n dimindex (:α)
is redundant. I’ve updated this theorem accordingly.
To get a theorem with no side-conditions we can introduce a MOD:
wordsTheory.n2w_DIV
| Q.SPEC `a MOD dimword(:'a)`
| SIMP_RULE (srw_ss()) [wordsTheory.n2w_mod]
| GEN_ALL
val it =
|-
Note quite sure how you got to 48 lines. I think only a single call to SRW_TAC
(or lcsymtacs.lrw) is needed.
val thm = Q.prove(
`TAKE (LENGTH bvs + 1)
(REVERSE bvs ++
h::
(blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) ++
DROP (LENGTH args0 + (LENGTH blvs +
Hi Hamed,
I’m assuming that your example comes from using the tool
arm_random_testingLib.arm_step_updates.
If you wish to manipulate these terms then you can do so using HOL4’s
collection of syntax functions (e.g. see Term, boolSyntax and wordsSyntax).
These libraries can be used to destruct
To reconstruct the datatype you can use EmitTeX.datatype_thm_to_string, which
is documented.
Anthony
On 22 Mar 2012, at 09:14, Michael Norrish wrote:
Unfortunately there isn't any documentation for emitLib. If you figure
anything out, patches fixing this situation would be gratefully
Hi,
This appears to be a bug in METIS_TAC. It should fail but it instead returns a
legitimate theorem - just one with inconsistent hypotheses. This appears to
relate to the fact that METIS_TAC is at heart a first-order prover, which
doesn't fit in with the types/theorems in wordsTheory. Joe
Hi,
I'm not entirely sure I understand what you're trying to define. If
you're just after the matrix that is matrix A with row i and column j
removed then you could define this as follows:
val dsyz_matrix = Define`
dszy_matrix (A:('n,'n) matrix) (i:num) (j:num) : ('n sub1,'n sub1)
Hi,
My guess for the correct definition is:
val det = Define`
det (A:('n ,'n) matrix) =
sigma (\p. (sign (dimindex(:'n)) p) *
(product (1n, dimindex(:'n))
(\(k:num). (A ' k ' (p (k:real))
{ (p:num - num) | permutes (dimindex(:'n)) p}`;
wordsLib.WORD_ARITH_EQ_ss doesn't do very much. It simply performs the
conversion
x = y |- x - y = 0w
but it does not simplify x - y. It is expected to be used in combination
with wordsLib.WORD_ARITH_ss, which is included in the stateful simpset srw_ss()
but not in std_ss.
The simpsets
One option is
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 p + 0x8w``
How should I proceed to prove it?
Lu
You could use
Globals.max_print_depth := 10;
(try: help max_print_depth).
You could also do
val _ = time defCNF.DEF_CNF_VECTOR_CONV ``my BIG input``;
which will perform the computation, giving you the time, but then throw away
the result.
Anthony.
On 11 Dec 2009, at 14:14, Khaza Anuarul
The second parameter is the word length. For example:
wordsSyntax.mk_word (Arbnum.fromInt 0xA, Arbnum.fromInt 32)
For convenience, there is also
wordsSyntax.mk_wordi (Arbnum.fromInt 0xA, 32)
and
wordsSyntax.mk_wordii (0xA, 32)
Be aware that Mosml integers are 31 bits wide. For example:
-
The theorem n2w_w2n
|- !w. n2w (w2n w) = w
cannot be applied in
``n2w (w2n w) = v``
when w and v do not have the same length, which is the case in your
goal.
For proving things about ``a @@ b``, I would recommend using the
latest HOL snapshot. I'm assuming that you're using the latest
T) F F
- EVAL ``(update (update not T T) F F) T```;
|- (update (update not T T) F F) T = T
Some examples of rewrites for sorting updates can be found in $HOLDIR/
examples/ARM/v4T/updateScript.sml. These are used in arm_evalLib.sml.
Anthony Fox.
On 16 Nov 2007, at 16:01, Bingham, Jesse D
24 matches
Mail list logo
