scratch

theory Scratch
imports Main
begin

theorem ex1:
  assumes pq: "¬P ∨ Q"
  shows "P ⟶ Q"
proof -
  have imppq: "P ⟹ Q"
  proof -
    assume p: "P"
    have qq: "Q ⟹ Q"
    proof -
      assume "Q" then show "Q" by this
    qed
    have npq: "¬P ⟹ Q"
    proof -
      assume np: "¬P"
      have nnq: "¬¬Q"
    proof -
      have nqfal: "¬Q ⟹ False"
      proof -
        assume nq: "¬Q"
        from np and p show "False" by (rule notE)
      qed
       from nqfal show "¬¬Q" by (rule notI)
    qed
     from nnq show "Q" by (rule notnotD)
   qed
    from pq and qq and npq show "Q" by (rule disjE)
  qed
   from imppq show "P ⟶ Q" by (rule impI)
qed

end