[Hol-info] A question about the definition of the function in HOL4

Hi,guys I am working with HOL4. I defined a function in HOL4,like following - fun ccdd a b c d = if ((a = b) /\ (c = d)) then true else false; It responded that: ! Toplevel input: ! fun ccdd a b c d = if ((a = b) /\ (c = d)) then true else false; !

[Hol-info] A question about the theorem in HOL4?

Hi,guys I am working with HOL4. FST is in pairTheory, its definition is [FST] Theorem |- ∀x y. FST (x,y) = x But, When I use it like following: val n = FST (1,2); It responses:! Toplevel input: ! val n = FST (1,2); ! ^^^ ! Type clash

[Hol-info] How to show the function body in ML?

Hi,guys I am working with HOL4. I finded a function "find" in ML Structure list,and I wanted to see the function body of "find". I printed : - find; > > val it = fn : string -> ((string * string) * (thm * class)) list The result only shows the types of the function. Its

[Hol-info] Is there a function that can produce random number in HOL4?

Hi,guys I am working with HOL4. Now, I need a function that can produce random number. For example, supposing that function rand can create a random number, then x=rand ()/LENGTH, where x is a number between 1 and LENGTH. Does anyone know this? Thanks!-

[Hol-info] What is the advantage of HOL4?

Hi,guys I am working with HOL4. Recently, I read some papers, knowing that there are some other theorem provers, like PVS,COQ. They are similar in many aspects. For example, the logic used by them is Higher order logic. I am wondering What is the advantage of HOL4? Thanks!---

[Hol-info] A question about rewrite in HOL4

Hi,guys I am working with HOL4. This is the subgoal > val it = TAKE h' (CX (INSERT h t) p q) ++ DROP h' (CX (INSERT h t) q p) = TAKE h (CX l p q) ++ DROP h (CX l q p) 0. !p' q'. (LENGTH p' = LENGTH q') ==>

[Hol-info] A question about specialization in HOL4

Hi,guys I am working with HOL4. This is the subgoal > val it = CX (INSERT h (CAN l)) p q = CX (h::l) p q 0. !p q n. (LENGTH p = LENGTH q) ==> (CX (CAN l) p q = CX l p q) 1. LENGTH p = LENGTH q : p

[Hol-info] A question about rewrite in HOL4

Hi,guys I am working with HOL4. > val it = TAKE n (TAKE n (CX l p q) ++ DROP n (CX l q p)) ++ DROP n (TAKE n (CX l q p) ++ DROP n (CX l p q)) = CX l p q 0. p IN d 1. q IN d 2. LENGTH p = LENGTH q 3. LENGTH

[Hol-info] A question about adding an assumption with "by"

Hi,guys I am working with HOL4. I am going to prove g`!p q. (LENGTH p = LENGTH q) ==> !l m n . TAKE n (TAKE m (CX l p q) ++ DROP m (CX l q p)) ++ DROP n (TAKE m (CX l q p) ++ DROP m (CX l p q)) = TAKE m (TAKE

[Hol-info] A question about a proof with TAKE and DROP?

Hi,guys I am working with HOL4. I am going to prove g`!p q. (LENGTH p = LENGTH q) ==> !l m n . TAKE n (TAKE m (CX l p q) ++ DROP m (CX l q p)) ++ DROP n (TAKE m (CX l q p) ++ DROP m (CX l p q)) = TAKE m (TAKE

[Hol-info] a question about rewrite in HOL4

Hi,guys I am working with HOL4. I am going to prove g`!p q n l. ( (LENGTH p = LENGTH q) /\ (LENGTH p <= n)) ==> (LENGTH (cx l p q) <=n ) `; Where the definition of cx is val cx_def = Define` (cx [] p q = p) ?? (cx (x::xs) p q = TAKE x (cx xs p q) ++ DROP x

[Hol-info] How to transform list format from "(cx l q p)" to "l"

Hey,guys I am learning to use HOL4. Here are some questions about my proving: g`!p q:bool list l:num list. (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) = LENGTH p) `; e (Induct_on `l`); e (RW_TAC list_ss [cx_defn]); - e (RW_TAC list_ss [cx_defn]); OK.. 1 subgoal: > val it =

[Hol-info] [SPAM] some questions about the use of THEN and THENL in HOL4

Hey guys, I am learning to use HOL4. In listTheory , I found that: val DROP_0 = store_thm( "DROP_0", ``DROP 0 l = l``, Induct_on `l` THEN SRW_TAC [] []); I was wondering that after "Induct_on `l`", there should be two subgoals. But the following was "THEN SRW_TAC [] []", I thought it sho

[Hol-info] [SPAM] some questions about the proving process in HOL4

Hey guys, I am learning to use HOL4. There is a function named "TAKE" in HOL4, which can get the first n elements in a list. When I was proving one property of TAKE, I find an interesting thing. As follows: - g`!p:bool list n:num. (LENGTH p = 0) ==> (TAKE 0 p = p) `; - e (REPEAT STRIP_TAC);

[Hol-info] How to specify the data type in a recursive definition in HOL4

Hey guys, I am learning to use HOL4. I defined a function named "first" in HOL4. This function can get the first n elements in a list. As follows: - val first_def = Define`(first [] n = [] ) /\ (first p 0 = [] ) /\ (first p n = HD p :: first (TL

[Hol-info] some questions about the use of HD and TL in listTheory

Hey guys, I am learning to use HOL4. I defined a function named "first" in HOL4. This function can get the first n elements in a list. As follows: - val first_def = Define`(first [] n = [] ) /\ (first (p::pl) 0 = [] ) /\ (first (p::pl) n = HD (p:

[Hol-info] ?????? About the use of symbol | in HOL4

quot;; : Re: [Hol-info] About the use of symbol | in HOL4 Hi Ada, In the first case you're trying to define a function in the HOL logic. In the second case you're defining a SML function Jeremy On 29/11/15 22:15, Ada wrote: > Hey guys, > > I am learning to use

[Hol-info] About the use of symbol | in HOL4

Hey guys, I am learning to use HOL. I find an interesting thing about the use of symbol | in HOL4. I defined an function named fir, as follows: - val fir_def = Define` (fir [] n = [] ) | (fir p 0 = [])`; But failed , it responsed that: Don't expect to find a | in this position after

[Hol-info] How to transform the proof form

Hey guys, I am learning to use HOL. Here is some code. load "abs_tools"; open abs_tools; val _ = type_abbrev ("num_field", ``:complex -> bool``); (* --

[Hol-info] request for One Paper

Hey guys, I am learning Formal Verification. I am reading some papers about COQ and HOL. Now I need a paper,as follows but I can't find it. *Could anyone help me find it,and send it to me? Thanks! --Wish. 0FEC4736@46A59B65.ECB45356 Description: Binary data --

[Hol-info] about METIS_TAC

Hey guys, I am learning to use HOL. When I use METIS_TAC, I don't know the system's response. For example: what I input are: -open arithmeticTheory; -val divides_def = Define `divides a b = ?x. b = a * x`; -set_fixity "divid