1
$\begingroup$

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?

$\endgroup$

1 Answer 1

2
$\begingroup$

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
$\endgroup$
1
  • 1
    $\begingroup$ It is a pity that we do not have syntax highlighting for Isabelle yet! $\endgroup$ Commented Mar 16, 2023 at 21:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.