CODEWITHSUNDEEP
isabelle
user1868607
user1868607

Reputation: 2600

How to apply standard to all subgoals in Isabelle?

To prove an equality "A = B" one can prove two inclusions "A ⊆ B" and "B ⊆ A". Now, I'm using the method "standard" to transform this goal into the goal "fix x in A and show x is in B". However, I don't know how to do this on all subgoals.

How can I do this in Isabelle?

Upvotes: 1

Views: 484

Answers (1)

user9716869 - supports Ukraine
user9716869 - supports Ukraine

Reputation: 1951

I decided to add peq's comment to my answer

if you import HOL-Eisbach.Eisbach you can use apply(all‹standard›)

If multiple goals emerge from a single goal as a result of an application of a method, then you can use semicolon ; (structural composition: see section 6.4 in Isar-ref) to apply the next method to all emerging subgoals, i.e.

lemma "(A::'a set) = B ∧ (C::'a set) = D"
  apply (intro conjI; standard; standard)
  oops

As a side remark, I do not believe that repeated application of standard is considered to be a very good style. For example, for your use case, normally, I use

lemma "(A::'a set) = B"
  apply(intro subset_antisym subsetI)
  oops

Hopefully, it should be sufficiently easy to see how you can also apply this method to multiple subgoals simultaneously.

Isabelle version: Isabelle2020

Upvotes: 1

Related Questions