[Hol-info] How can I generate a proof article file from running the NAME.ml file in HOL-Light?

hi, How can i running the NAME.ml file in HOl-Light? How can I generate a proof article file from running the NAME.ml file in HOL-Light? -- The Planet: dedicated and managed hosting, cloud storage, colocation Stay onlin

[Hol-info] How can I use the tool of reader read the proof article file in HOL4?

Hi， I have been generated a proof article file from a HOL Light theory file. But I found that the opentheory can’t use the large .ml file to generate the proof articles,for example vector.ml.When I run the command “opentheory compile”,the screen appeard the erroe of “out of memory”.Can you tell

[Hol-info] How can I use the tool of reader read the proof article file in HOL4?

Hi， I have been generated a proof article file from a HOL Light theory file. But I found that the opentheory can’t use the large .ml file to generate the proof articles,for example vector.ml.When I run the command “opentheory compile”,the screen appeard the erroe of “out of memory”.Can you tell

[Hol-info] the different between with type and datatype in HOL4

Hi everyone， Who know the different between with type and datatype in HOL4? I wanted to define a new type for matrix in HOL4, but I might be confusing type with datatype. I didn’t know how to start to define the type of matrix. Who can help me ? Thank you very much. I’m looking for your r

Re: [Hol-info] the different between with type and datatype in HOL4

Dear Konrad and Anthony, Thank you very much! With your help, I defined vectors and matrix so that I can start my work on proving some matrix theorems now. I guess some more questions will be encoutered. Maybe I need more advice and help and I appreciate previously. Best Wishes, Amy ---

[Hol-info] I could not find the solution to prove the sub goal。

Hi everyone, I have to prove a goal in HOL4: g`!(A:('a , 'b) matrix) (B:('c , 'a) matrix) (C:('d , 'c) matrix). A ** (B ** C) = (A ** B) ** C`; After having applied SRW_TAC as following, I could not find the solution to prove the subgoal: e(SRW_TAC [fcpLib.FCP_ss] [matrix_prod]); 1 subgoa

[Hol-info] I want to define inverted sequence in HOL4

hi, everyone I want to define inverted sequence in HOL4. How can I define arrangement or full permutation in HOL4? Who can give me some hints on permutation? Thank you very much! I’m looking for your reply. Best wishes Amy---

[Hol-info] How can I correct the type?

Hi everyone, I have to define the determinant definition in HOL4 and I define it as following: val det = Define ` det (A:('n ,'n) matrix) = sigma ( (sign (dimindex(:'n)) p) * ( prod_iter ( (1:num), dimindex(:'n) ) (\(k:num). (A %% k %% (p (k) ) ) ):real ) ) { (p:num -> num) | permutes

[Hol-info] Who knows the means of “ITSET” and “SUM_IMAGE”?

Hi everyone, Who knows the means of “ITSET” and “SUM_IMAGE” (they were in the pred_setTheory)? val ITSET_def = let open TotalDefn in tDefine "ITSET" `ITSET (s:'a->bool) (b:'b) = if FINITE s then if s={} then b else ITSET (REST s) (f (CHOICE s) b)

[Hol-info] How can I correct the definition about the submatrix?

hi everyone, I want to define a submatrix Mij is formed by throwing away row i and column j : The initial matrix of order n, this splitting gives n smaller matrix of order n-1. I define the definition of submatrix as follow: val dsyz_matrix = Define`dszy_matrix (A:('n,'n) matrix) (r:n