I agree that the second conjuncts of each are probably annoying. I'd keep just the first conjuncts and think about adding
0 < n ==> TAKE n (x::xs) = x::TAKE (n - 1) xs as well as the analogous one for DROP. There is as yet no way to remove specific theorems, but there should be (and there's a github issue, that you made: https://github.com/HOL-Theorem-Prover/HOL/issues/313). If the theorems are declared [simp] inside listTheory, then you can remove them, as well as a lot else, by removing the fragment called "list". Michael > On 27 Jun 2016, at 15:28, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote: > > Hi hol-info, > > I want to ask whether anyone thinks these are good automatic rewrites in > listTheory? > > |- (∀n. TAKE n [] = []) ∧ > ∀n x xs. TAKE n (x::xs) = if n = 0 then [] else x::TAKE (n − 1) xs > |- (∀n. DROP n [] = []) ∧ > ∀n x xs. DROP n (x::xs) = if n = 0 then x::xs else DROP (n − 1) xs > > I find them annoying because they introduce a conditional, which then causes > subgoal splits when rewriting (with rw or srw_tac). While they are sometimes > good rewrites, I don't think they should be _automatic_, as they currently > are. > > Shall we remove them from srw_ss? > > On another note, is there a way to remove things from srw_ss after they have > been added? I see only how to do that for named fragments (which I don't > think the above rewrites are in one of). > > Ramana > ------------------------------------------------------------------------------ > Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San > Francisco, CA to explore cutting-edge tech and listen to tech luminaries > present their vision of the future. This family event has something for > everyone, including kids. Get more information and register today. > http://sdm.link/attshape_______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ------------------------------------------------------------------------------ Attend Shape: An AT&T Tech Expo July 15-16. Meet us at AT&T Park in San Francisco, CA to explore cutting-edge tech and listen to tech luminaries present their vision of the future. This family event has something for everyone, including kids. Get more information and register today. http://sdm.link/attshape _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
