有关联的，并且可交换操作

解方程考虑伊莎贝尔像这样的目标（而不用担心ccProd和ccFromList）：有关联的，并且可交换操作

ccProd {x} (set xs) ⊔ (ccProd {x} (set ys) ⊔ (ccFromList xs ⊔ (ccFromList ys ⊔ ccProd (set xs) (set ys)))) = 
ccProd {x} (set xs) ⊔ (ccFromList xs ⊔ (ccFromList ys ⊔ (ccProd {x} (set ys) ⊔ ccProd (set xs) (set ys))))

这是真的，因为⊔是联想和交换。我通常的做法是使用

apply (metis join_assoc join_comm)

它可以工作，但已经花了很长时间才能完成。

同样，我有这样

ccProd {x} (set xs) ⊔ (ccProd {x} (set ys) ⊔ (ccFromList xs ⊔ (ccFromList ys ⊔ ccProd (set xs) (set ys)))) = 
ccFromList xs ⊔ (ccProd {x} (set ys) ⊔ (ccFromList ys ⊔ (ccProd (set xs) {x} ⊔ ccProd (set xs) (set ys))))

，我还需要办理的ccProd可交换的一个实例的目标。再次

apply (metis join_assoc join_comm ccProd_comm)

做的工作，但需要更长的时间。

有更好的方法来解决涉及交换和关联算子的方程吗？

也许战术也不simpproc，鉴于定理join_assoc join_comm，就解决了第一个目标，降低第二目标

ccProd {x} (set xs) = ccProd (set xs) {x}

来源

2014-12-03 Joachim Breitner

推理高达关联性和可交换的伊莎贝尔，则通常用简化器，并下令改写。在你的例子中，你为简化器提供了关联性规则（从左到右），交换性规则和左交换性规则。细节在Isabelle/HOL教程中进行了解释（第9.1节，置换重写规则）。

然后，简化器会将方程的两边重新排列成一个正态形式，由Isabelle中的隐式项序确定。因此，你在双方都会得到平等的条件，这些条件表现为反身性是平等的。除非您的运营商也满足取消法律，否则这种方法不会将第二个示例减少到不同的部分。如果幸运的话，简化器将这两个术语在相同的位置旋转。你可以使用一堆形式为a = b ==> a ⊔ c = b ⊔ c的引入规则。但是，这是相当脆弱的。如果您重命名变量，则订单可能会发生变化，从而打破证明。然而，ccProd似乎也是可交换的，所以只需将简写法的交换律加入即可。然后，它将首先正常化这些子项并解决所有问题。

来源

2014-12-03 13:07:49

嗯。考虑到交换性规则等问题，我一直认为简化器会循环。所以将'join_comm'标记为'[simp]'实际上是安全的？看起来好像很棒！ – 2014-12-03 14:02:41

将'join_comm'添加到simpset是安全的，因为它本身不会导致循环。就个人而言，我更喜欢在simpset中不使用AC规则。这样，简化器就不会混合这些术语，这使得在子目标未解决时更易于理解。 – 2014-12-03 15:20:05

另外一个好点;在添加它们之后，我现在要修复一些证据...... – 2014-12-03 15:53:36

如果您有一个ab_semigroup_mult或ab_semigroup_add的实例，那么比simpset经常加上ac_simps常常会有诀窍。

例如，如果我通过更换您的上述目标以下（因为我得到一个语法错误与⊔）：

lemma 
    fixes ccProd :: "_ ⇒ _ ⇒ 'a::ab_semigroup_add" 
    shows "ccProd {x} (set xs) + (ccProd {x} (set ys) + (ccFromList xs + (ccFromList ys + ccProd (set xs) (set ys)))) = 
    ccProd {x} (set xs) + (ccFromList xs + (ccFromList ys + (ccProd {x} (set ys) + ccProd (set xs) (set ys))))"

然后by (simp add: ac_simps)成功。

更新：还有相应区域abel_semigroup那又是“注册” ac_simps。所以，你的第二个引理可以大致如下

interpretation abel_semigroup ccProd 
sorry

这就是你展示ccProd是AC（除了已经确定的ab_semigroup_add上述实例）工作。

lemma 
    "ccProd {x} (set xs) + (ccProd {x} (set ys) + (ccFromList xs + (ccFromList ys + ccProd (set xs) (set ys)))) = 
    ccFromList xs + (ccProd {x} (set ys) + (ccFromList ys + (ccProd (set xs) {x} + ccProd (set xs) (set ys))))" 
by (simp add: ac_simps)

来源

2014-12-03 13:08:10 chris

有关联的，并且可交换操作

回答

相关问题