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

Question

我目前正在尝试证明 Isabelle 中的一个引理，我剩下 2 个子目标，它们都有相同的未知变量 ?Q11。 "transitivity" 是否可以将两个子目标合并为一个？即用第一个子目标中包含?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 生效。

当然这并不是真的"merge subgoals"，但是达到了预期的效果

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

Merging 2 subgoals with common unknown variable in Isabelle proof

isabelle