我如何证明具有具有示意图变量的假设的界变量的子目标？

Question

我是伊莎贝尔菜鸟。我有一个sublocale，它给我带有绑定变量的子目标。子目标是我在其他某些地区内拥有的假设的确切副本。当我实例化它们时，它们只能使用自由变量来完成。我如何解决这个问题？

这里给出的是我的子目标

 1. ⋀n. plus n zero = n
 2. ⋀n m. plus n (suc m) = suc (plus n m)
 3. ⋀n. times n zero = zero
 4. ⋀n m. times n (suc m) = plus (times n m) n
 5. ⋀x. (zero = zero ∨ (∃m. suc m = zero)) ∧
         (x = zero ∨ (∃m. suc m = x) ⟶
          suc x = zero ∨ (∃m. suc m = suc x)) ⟶
         (∀x. x = zero ∨ (∃m. suc m = x))

，我需要使用

locale th2 = th1 +
  fixes 
    plus :: "'a ⇒ 'a ⇒ 'a"
  assumes
     arith_1: "plus n zero = n"
    and plus_suc: "plus n (suc m) = suc ( plus n m)"

对假设的任何引用的任何假设中的一个（仅几个），最终具有示意性变量，我只能用自由变量替换它们。我该如何处理这个问题？ 任何帮助都非常感谢

Answer 1

您的环境定义并不意味着您认为它的作用。

在您的定义中：

  assumes
     arith_1: "plus n zero = n"
    and plus_suc: "plus n (suc m) = suc ( plus n m)"

表示n和m已固定在整个语言环境中。您真正想要的是：

  assumes
     arith_1: "⋀n. plus n zero = n"
    and plus_suc: "⋀n m. plus n (suc m) = suc ( plus n m)"

起初这似乎有些奇怪，因为它与定理的行为相同，但不是最自然的行为。