[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

[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?

[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?

[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 :

[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

[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

[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

[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

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

??: ""<ada.k...@qq.com>; "hol-info"<hol-info@lists.sourceforge.net>; : 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

[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

[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] 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