Search code examples
isabelle

Merging 2 subgoals with common unknown variable in Isabelle proof


Im currently trying to prove a lemma in Isabelle and I'm left with 2 subgoals, which both have the same unknown variable ?Q11. Is it possible to merge the two subgoals into one by "transitivity"? That is by replacing ?Q11 in the second subgoal by the set in which ?Q11 is contained in the first subgoal.

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}}

The goal I would like to obtain would be something like

 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}}}}}

which is proven directly by simp.

Thanks.


Solution

  • You can

    apply (rule order.refl)
    

    which solves the first goal using reflexivity of the subset relation. This instatiates ?Q11 accordingly.

    Of course this does not really "merge subgoals", but it achieves the desired effect.