Thanks! The secret sauce seems to be EL_APPEND2, and possibly whatever is
in lrw. (And I should use LIST_EQ_REWRITE more often too.)
This should make a lot of my subgoal proofs much shorter :)
On Wed, Feb 27, 2013 at 7:02 PM, Anthony Fox <ac...@cam.ac.uk> wrote:
> 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 <ramana.ku...@cl.cam.ac.uk> 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
> > hol-info@lists.sourceforge.net
> > 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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
