HOL 定理证明器：添加到现有理论答案

【问题标题】：HOL Theorem Prover: Adding to existing theoryHOL 定理证明器：添加到现有理论
【发布时间】：2018-05-15 18:40:37
【问题描述】：

我正在尝试将一个定理添加到现有理论中。我要添加的定理是：

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

我的第一步是证明这个定理；但是，当我尝试设定目标时，我收到了几条错误消息：

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

【问题讨论】：

标签： hol

【解决方案1】：

我觉得应该是这样的

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

和

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

【讨论】：

谢谢！我能够设定目标；但是，我无法证明这一点。 PROVE_TAC 不起作用，ASM_REWRITE_TAC 也不起作用。想法？
你需要做一个归纳。列表的归纳原则很可能在声明列表时自动生成。恐怕我在 HOL 从来没有走那么远。尝试运行DB.find_in "induct" (DB.find "list");。只是浏览一下教程，看来你最好试试e (Induct_on `l1`);。
我忘了补充，我尝试的第一步是 e(Induct_on l1) 工作正常，但我仍然无法完成证明。
对于基本情况，您需要将APP [] l2重写为l2，然后将LENGTH []重写为0，然后将0 + LENGTH l2重写为LENGTH l2。
对于step案例，需要将LENGTH (APP (h::l1) l2)改写为LENGTH (h::(APP l1 l2))，再改写为1 + LENGTH (APP l1 l2)。并且还将LENGTH (h::l1) 重写为1 + LENGTH l1，然后将(1 + LENGTH l1) + (LENGTH l2) 重写为1 + (LENGTH l1 + LENGTH l2)。然后在应用归纳假设之前将1 + x = 1 + y 重写为x = y。我想 HOL 有策略自动完成大部分这些步骤。