Mizar-style single step reasoning in Isabelle proofs · General

Suppose I want to prove the commutativity of set union: A ∪ (B ∪ C) = (A ∪ B) ∪ C holds.

theory Scratch imports Main
begin


lemma commutative_union : "A ∪ (B ∪ C) = (A ∪ B) ∪ C"
  apply (simp add: semigroup.assoc sup.semigroup_axioms)
  oops

lemma commutative_union : "A ∪ (B ∪ C) = (A ∪ B) ∪ C"
  apply(subgoal_tac "A ∪ (B ∪ C) ⊆ (A ∪ B) ∪ C")
  apply(subgoal_tac "(A ∪ B) ∪ C ⊆ A ∪ (B ∪ C)")
    apply blast
   apply(subgoal_tac "∀a. a ∈ A ∪ (B ∪ C) = (a ∈ A ∨ a ∈ (B ∪ C))")
  apply(subgoal_tac "∀a.  (a ∈ A ∨ a ∈ (B ∪ C)) = (a ∈ A ∨ a ∈ B ∨ a ∈ C)")
  apply(subgoal_tac "∀a.  (a ∈ A ∨ a ∈ B ∨ a ∈ C) = ((a ∈ A ∨ a ∈ B) ∨ a ∈ C) ")
      apply(subgoal_tac "∀a. ((a ∈ A ∨ a ∈ B) ∨ a ∈ C) = (a ∈ (A ∪ B) ∨ a ∈ C)")
  apply(subgoal_tac "∀a. (a ∈ (A ∪ B) ∨ a ∈ C) = (a ∈ (A ∪ B) ∪ C)")
        apply blast+
  done

end

The first proof is kind of cheating, as it uses facts about set unions from the library.
The second proof tries to detail out the proof, however is a bit clumsy and definitely not idiomatic.
I was wondering if there is an elegant and idiomatic way to write this proof, such that each step does one rewriting,
without any verbose script lines like apply blast, just like the single-step proofs in Mizar? (Sebastian very kindly showed how this can be done in Mizar but I forgot where to get that Mizar snippet for the same proposition now, would be nice if someone can point me to that Mizar snippet proving
A ∪ (B ∪ C) = (A ∪ B) ∪ C.)

Wolfgang Jeltsch (Oct 25 2023 at 18:30):

Isar is Isabelle’s Mizar-style proof language. Have you looked at the prog-prove tutorial, which is mentioned as the first document on the documentation page of the Isabelle website? An introduction to Isar is provided there towards the end.

Chengsong Tan (Oct 25 2023 at 19:02):

I did look at that a while ago, and my experience was not very pleasant last time Isarfying real-world proofs. I remember being stuck in the middle of an Isar proof for a complicated lemma that involved many steps.

I was just wondering if there's a simple construct that allows you to do one rewriting at a time. Something that manipulates the proof state one step further and nothing else (just like elimination rules do).
I will give it a second careful read, but a quick skim seem to suggest that from this seem to be the best available construct?

Wolfgang Jeltsch (Oct 25 2023 at 21:48):

When it comes to proof methods, you may want to have a look at unfold and subst. Also the Isar construct unfolding could be useful.

Sad that your experience with Isar was negative. In my opinion it’s one of the greatest features of Isabelle.

Note that Isar not only gives you readable proofs, but it also generally makes proving easier, because you state intermediate propositions that you want to show, which also helps to guide automated provers.

Wolfgang Jeltsch (Oct 25 2023 at 21:50):

If you could say more concretely where you get stuck with Isar, people might be able to help you overcome the difficulties that you experience. As I said, Isar is a great feature in my opinion, and I suspect that you’ve merely approached it in an unfortunate way.

Stream: General

Topic: Mizar-style single step reasoning in Isabelle proofs

Chengsong Tan (Oct 25 2023 at 17:41):

Wolfgang Jeltsch (Oct 25 2023 at 18:30):

Chengsong Tan (Oct 25 2023 at 19:02):

Wolfgang Jeltsch (Oct 25 2023 at 21:48):

Wolfgang Jeltsch (Oct 25 2023 at 21:50):