By the way, your listAdd function is almost equal to ``list$MAP2 complex_add``, and if you used that, you could use rich_listTheory.LENGTH_MAP2.
To prove your goal, just use induction on l1, cases on l2, and rewrite with listAdd_def. e(Induct >> rw[listAdd_def] >> Cases_on`l2` >> fs[listAdd_def]); On Wed, Jan 16, 2013 at 8:49 AM, Yuntao Peng <[email protected]>wrote: > I am a beginner of HOL4 > The function of complex list add is define as follow. > val listAdd_def = Define `(listAdd [] (l2:complex list) = []) /\ > (listAdd ((h1::t1):complex list) [] =[]) /\ > (listAdd ((h1::t1):complex list) (l2:complex > list) = (h1 + HD l2)::(listAdd t1 (TL l2)))`; > Now there is a goals I want to prove > The first one is > g `!l1:complex list l2:complex list. (LENGTH l1 = LENGTH l2) ==> (LENGTH > (listAdd l1 l2) = LENGTH l1)`; > Thanks to the listTheory is base on real, so I can not use its theorem. > > Thanks! > > > ------------------------------------------------------------------------------ > Master Java SE, Java EE, Eclipse, Spring, Hibernate, JavaScript, jQuery > and much more. Keep your Java skills current with LearnJavaNow - > 200+ hours of step-by-step video tutorials by Java experts. > SALE $49.99 this month only -- learn more at: > http://p.sf.net/sfu/learnmore_122612 > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > >
------------------------------------------------------------------------------ Master Java SE, Java EE, Eclipse, Spring, Hibernate, JavaScript, jQuery and much more. Keep your Java skills current with LearnJavaNow - 200+ hours of step-by-step video tutorials by Java experts. SALE $49.99 this month only -- learn more at: http://p.sf.net/sfu/learnmore_122612
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
