Re: [Hol-info] a question about rewrite in HOL4

> On 5 Mar 2016, at 09:01, Ramana Kumar wrote: > > I think RW_TAC doesn't handle conditional rewrites very well. Try using rw or > simp instead. > RW_TAC handles conditional rewrites in exactly the same way as simp and rw. If I try RW_TAC list_ss [cx_length] with

[Hol-info] CFP: Graphical Models for Security (GraMSec'16)

* GraMSec'16 The Third International Workshop on Graphical Models for Security Co-located with CSF 2016 Lisbon, Portugal - June 27, 2016 http://gramsec.uni.lu/ *

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

Thank you for your reply! My version of HOL4 is HOL-4 [Kananaskis 10 (stdknl, built Mon Nov 10 14:27:30 2014)], where Moscow ML version 2.01 (January 2004). Then from https://hol-theorem-prover.org/#get, I installed PolyML5.6-32bit, and pointed ""bin/build". Then I got HOL-4 [Kananaskis 10

Re: [Hol-info] a question about rewrite in HOL4

I think RW_TAC doesn't handle conditional rewrites very well. Try using rw or simp instead. This worked for me: open listTheory val cx_def = Define` (cx [] p q = p) ∧ (cx (x::xs) p q = TAKE x (cx xs p q) ++ DROP x (cx xs q p))` val cx_length = Q.prove( `!l p q . (LENGTH p = LENGTH q)

[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] [VeryComp 2016] - 1st Call for Paper

[Apologies for multiple postings] == FIRST CALL FOR PAPERS == 1st International Workshop on Formal to Practical Software Verification and Composition (VeryComp 2016) Co-located event of STAF 2016 (http://staf2016.conf.tuwien.ac.at/) Wien, Austria - July 4th 2016 Web site: