Note that Ramana's proof will only work if you first open lcsymtacs
Michael On 17/01/13 01:40, Ramana Kumar wrote: > 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] > <mailto:[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!
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ 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
