Note quite sure how you got to 48 lines. I think only a single call to SRW_TAC
(or lcsymtacs.lrw) is needed.
val thm = Q.prove(
`TAKE (LENGTH bvs + 1)
(REVERSE bvs ++
h::
(blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) ++
DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4)))
(REVERSE bvs ++
h::
(blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) =
TAKE (LENGTH bvs + 1)
(REVERSE bvs ++
h::
(blvs ++ [benv; x] ++ REVERSE args0 ++ [cl0] ++ st)) ++ st`,
lrw [listTheory.LIST_EQ_REWRITE, rich_listTheory.EL_DROP,
rich_listTheory.EL_APPEND2, rich_listTheory.EL_CONS,
arithmeticTheory.PRE_SUB1]
)
Anthony
On 27 Feb 2013, at 17:58, Ramana Kumar <[email protected]> wrote:
> I just wrote a fairly manual 48-line proof of the following.
> Is there some decision procedure, simpset, or tactic I could use to automate
> it that I'm not aware of?
> The theorems in srw_ss() seem not to play very well together on this kind of
> stuff.
>
> TAKE (LENGTH bvs + 1)
> (REVERSE bvs ++
> Block 3 [CodePtr a; bve]::
> (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++
> DROP (LENGTH args0 + (LENGTH blvs + (LENGTH bvs + 4)))
> (REVERSE bvs ++
> Block 3 [CodePtr a; bve]::
> (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) =
> TAKE (LENGTH bvs + 1)
> (REVERSE bvs ++
> Block 3 [CodePtr a; bve]::
> (blvs ++ [benv; CodePtr ret] ++ REVERSE args0 ++ [cl0] ++ st)) ++
> st
>
> ------------------------------------------------------------------------------
> Everyone hates slow websites. So do we.
> Make your web apps faster with AppDynamics
> Download AppDynamics Lite for free today:
> http://p.sf.net/sfu/appdyn_d2d_feb_______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_feb
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
