On 16/01/13 19:49, Yuntao Peng wrote:
> Now there is a goals I want to prove [...]
> Thanks to the listTheory is base on real, so I can not use its theorem.
I’m not sure what you mean by this last sentence. Certainly, the theory of
lists (listTheory) is not tied to real numbers at all.
Also, as
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, ju
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]);
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
