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) ==> (LENGTH (cx l p q) = LENGTH p)`,
Induct \\ simp[cx_def,LENGTH_TAKE_EQ]);
val th = Q.prove(
`!p q n l.
(LENGTH p = LENGTH q) /\ (LENGTH p <= n) ==>
LENGTH (cx l p q) <= n `,
simp[cx_length]);
On 5 March 2016 at 01:06, Ada <ada.k...@qq.com> wrote:
> 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 (cx xs q p))`
>
> I had proved " !l p q . (LENGTH p = LENGTH q) ==> (LENGTH (cx l p q) =
> LENGTH p)", named "cx_length"
> so I used,
> e (RW_TAC list_ss [cx_length]);
> But it can't work, does anyone know the reason?
>
> Thanks!
>
>
> ------------------------------------------------------------------------------
> Site24x7 APM Insight: Get Deep Visibility into Application Performance
> APM + Mobile APM + RUM: Monitor 3 App instances at just $35/Month
> Monitor end-to-end web transactions and take corrective actions now
> Troubleshoot faster and improve end-user experience. Signup Now!
> http://pubads.g.doubleclick.net/gampad/clk?id=272487151&iu=/4140
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
