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
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 +
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
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 +, 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
