Search code examples
isabelle

Breaking conjunctions of the form &&& into subgoals in Isabelle


If I write in Isar something like:

have "(x ↔ z) ∙ R = (xa ↔ z) ∙ S" 
     "(x ↔ z) ∙ T = (xa ↔ z) ∙ Ta" 
     "(x ↔ z) ∙ q = (xa ↔ z) ∙ t" 

I will get a subgoal:

(x ↔ z) ∙ R = (xa ↔ z) ∙ S &&&
(x ↔ z) ∙ T = (xa ↔ z) ∙ Ta &&&
(x ↔ z) ∙ q = (xa ↔ z) ∙ t

How do I split this &&& into three subgoals?


Solution

  • One usually only encounters such subgoals when one states a lemma with more than one statement, and this is nothing to worry about. It is virtually impossible for this to cause any problems during everyday use – you can just ignore it.

    To elaborate: When you write something like lemma P1 P2, you do indeed see P1 &&& P2 as a proof obligation. However, do not be alarmed by that: if you run any proof method, this meta-conjunction is immediately split and you have the two separate subgoals P1 and P2 even before that method sees the goal. So just pretend it's two separate subgoals from the beginning.

    (With enough criminal energy, it is probably possible to avoid this automatic splitting, but only if you define your own proof methods.)