在 Isabelle 证明中合并 2 个具有共同未知变量的子目标

Question

我目前正试图在 Isabelle 中证明一个引理，剩下 2 个子目标，它们都具有相同的未知变量 ?Q11。 是否可以通过“传递性”将两个子目标合并为一个？ 也就是说，将第二个子目标中的 ?Q11 替换为第一个子目标中包含 ?Q11 的集合。

goal (2 subgoals):
 1. ⋀s. ?Q11 s ⊆ {s. s⦇msg_sender := address_this s, address_this := add2 s⦈ ∈ {s. s⦇g := 2⦈ ∈ {t. g t = 2}}}
 2. {s. g s = 0} ⊆ {s. s⦇msg_sender := address_this s, address_this := add1 s⦈ ∈ {sa. sa⦇g := 1⦈ ∈ ?Q11 s}}

我想达到的目标是

 1. {s. g s = 0} ⊆ {s. s⦇msg_sender := address_this s, address_this := add1 s⦈ ∈ {sa. sa⦇g := 1⦈ ∈ {s. s⦇msg_sender := address_this s, address_this := add2 s⦈ ∈ {s. s⦇g := 2⦈ ∈ {t. g t = 2}}}}}

由 simp 直接证明。

谢谢。

Answer 1

你可以

apply (rule order.refl)

使用子集关系的自反性解决了第一个目标。这相应地使 ?Q11 成立。

当然这并没有真正“合并子目标”，但它达到了预期的效果。