# How to write a low-level proof in Isar?

I would like to formalize

                              [q /\ r]
------- conjunct1
[p]             q
------ disjI1  -------- disjI2
p \/ (q /\ r)  p \/ q          p \/ q
-------------------------------------- disjE
p \/ q


where the rule names correspond to Isabelle lemmas.

I came up with the following, trying to follow the basic rules of natural deduction:

Theory Example

imports Main

begin

lemma p_imp_porq: assumes p shows "p ∨ q"
proof -
show ?thesis using assms by (rule disjI1[of p q])
qed

lemma qandr_imp_q: assumes "q ∧ r" shows q
proof -
show ?thesis using assms by (rule conjunct1[of q r])
qed

lemma q_imp_porq: assumes q shows "p ∨ q"
proof -
show ?thesis using assms by (rule disjI2[of q p])
qed

lemma qandr_imp_porq: assumes "q ∧ r" shows "p ∨ q"
proof -
have q using assms by (rule qandr_imp_q)
from this show ?thesis by (rule q_imp_porq)
qed

lemma por_qandr_imp_porq: assumes "p ∨ (q ∧ r)" shows "p ∨ q"
proof -
show ?thesis using assms apply (rule disjE[of p "q ∧ r" "p∨q"])
subgoal by (rule p_imp_porq)
subgoal by (rule qandr_imp_porq)
done
qed

end


Now, I would like to write the last one in proper Isar structured proof but I don't know how. Could you give an advice?

One way to accomplish this, somewhat in the lines of what you did, is the following:

lemma por_qandr_imp_porq: assumes "p ∨ (q ∧ r)" shows "p ∨ q"
proof -
note assms
moreover
have "p ⟹ p ∨ q"
by (rule p_imp_porq)
moreover
have "q ∧ r ⟹ p ∨ q"
by (rule qandr_imp_porq)
ultimately
show ?thesis
by (rule disjE)
qed


This illustrates the use of moreover...ultimately, which accumulates facts for later use. Perhaps the reason that makes this particular proof more difficult is that you have to either write it in this way or instantiate the lemmas with the particular values, as you did or as in the following snippet:

lemma por_qandr_imp_porq': assumes "p ∨ (q ∧ r)" shows "p ∨ q"
proof -
note assms
moreover
note p_imp_porq[of p q]
moreover
note qandr_imp_porq[of q r p]
ultimately
show ?thesis
by (rule disjE)
qed


A third way, albeit longer, exemplifies the use of consider:

lemma por_qandr_imp_porq'': assumes "p ∨ (q ∧ r)" shows "p ∨ q"
proof -
from assms
consider (p) "p" | (qr) "q ∧ r" by (rule disjE)
then show ?thesis
proof (cases)
case p
then show ?thesis by (rule p_imp_porq)
next
case qr
then show ?thesis by (rule qandr_imp_porq)
qed
qed


EDIT: I'm sorry to bump the question but after second read, some observations could be done to the OP code to get it more Isar-ish.

In first place, using a proof...qed block for the first three lemmas is redundant, since a terminal proof can handle them. And actually, instantiations aren't needed either:

lemma p_imp_porq: assumes p shows "p ∨ q"
using assms by (rule disjI1)


In the 4th lemma, then can be used in place of from this. Now, as personal preference, I keep these connectors in a separate line together with quoted local facts (in the case of from or with) and another separate line citing previously proved lemmas with using and the proof methods. So, my preferred format for this lemma would be

lemma qandr_imp_porq: assumes ‹q ∧ r› shows ‹p ∨ q›
proof -
from ‹q ∧ r›
have q
by (rule qandr_imp_q)
then
show ‹p ∨ q›
by (rule q_imp_porq)
qed


The use of the ‹...› quotes allows to use explicit reference, which results in a more explicit proof text. In this lemma you quoted two rules. Actually, the whole proof could be organized in a single lemma, respecting your low-level approach:

lemma por_qandr_imp_porq: assumes "p ∨ (q ∧ r)" shows "p ∨ q"
proof -
from assms
consider (p) "p" | (qr) "q ∧ r"
by (rule disjE)
then
show ‹p ∨ q›
proof (cases)
case p
then
show ‹p ∨ q› by (rule disjI1)
next
case qr
then
have ‹q› by (rule conjunct1)
then
show ‹p ∨ q› by (rule disjI2)
qed
qed

• It is a pity that we do not have syntax highlighting for Isabelle yet! Commented Mar 16, 2023 at 21:10