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
