> 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 the repository version of HOL,
*
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/
*
Graphic
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 (std
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)
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
[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: verycomp2016.disim.
