Hi, I think, it is even simpler:
SIMP_TAC list_ss [rich_listTheory.DROP_APPEND2] Best Thomas On Wed, 2013-02-27 at 22:10 +0000, Ramana Kumar wrote: > 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 <[email protected]> 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 > <[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 ------------------------------------------------------------------------------ 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
