Search code examples
hol

HOL Theorem Prover: Adding to existing theory

I am trying to add a theorem to an existing Theory. The theorem that I am trying to add is: 

!l1 l2.LENGTH (APP l1 l2) = LENGTH l1 + l2

My first step is to prove the theorem; however, when I try to set the goal, I am getting several error messages: 

set_goal( [],``! (l1:'a list) (l2:'a list).LENGTH (APP l1 l2) = LENGTH l1 + l2``)`
Solution

  • I think that should be

    ∀l1 l2. LENGTH (APP l1 l2) = LENGTH l1 + LENGTH l2

    and

    set_goal([], ``! (l1:'a list) (l2:'a list).LENGTH (APP l1 l2) = LENGTH l1 + LENGTH l2``)