Proving implications · Beginner Questions

I'm feeling particularly daft today. I need to prove a theorem of the form P ==> Q ==> R. I assumed that a way to do this would be to assume P /\ Q and then show R:

lemma s:
  shows "P ⟹ Q ⟹ R"
proof -
  assume "P ∧ Q"
  show R
end

This leads to the dreaded "Local statement fails to refine any pending goal". An alternative form:

lemma s:
  shows "P ⟹ Q ⟹ R"
proof -
  assume "P" and " Q"
  show R
end

Can someone explain this to me? I'd swear that I've done things like this before, but apparently not.

Kevin Kappelmann (Feb 13 2026 at 19:04):

With assume you can get your hands on a premise of a goal. In your example, P and Q are premises of your goal.

P \land Q

is not a premise of your goal.

If you insist on using

P \land Q

, you can use presume and later show that

P \land Q

is implied by the premises of your goal. I discharge that obligation implicitly below by using auto after the final qed:

lemma "P ⟹ Q ⟹ R"
proof -
  presume "P ∧ Q"
  show R sorry
qed auto

John Hughes (Feb 13 2026 at 19:27):

OK...that makes some sense. I'm not sure what it was that I was remembering, but that clears it up. But it brings up another puzzling thing -- what ?thesis refers to. Programming and Proving says this:

"The unknown ?thesis is implicitly matched against any goal stated by lemma or show. Here is a typical example: ..."

but in the midst of a rather messy proof, I have the following example of something that's confusing me:

      show "Q ∈ Points ⟹  Q ⊲ chain_begin (x # xs) ⟹ is_chain (x # xs)
         ⟹ is_chain c ⟹ xs ≠ [] ⟹ realization (x # xs) Q ⊲ chain_end (x # xs)" for Q
      proof -
        show ?thesis

I would have expected ?thesis to be the thing written in the show just above, but instead it turns out to be realization (x # xs) Q ⊲ chain_end (x # xs), which I cannot prove, because that's only true if the five things before it are all true.

[The actual proof has some steps between the proof and the show ?thesis, but I wanted a minimal example of the phenomenon.]

Kevin Kappelmann (Feb 13 2026 at 19:36):

John Hughes (Feb 13 2026 at 19:43):

So P&P was oversimplifying, I guess. Is there a way to access the assumptions of the innermost pending claim? Without that, it seems hard for me to prove anything.

Kevin Kappelmann (Feb 13 2026 at 19:50):

You can use meta implication + assume, as you already did above, or you can use a for clause for the premises, which you can then refer to by using that, by giving an explicit name, or by literal quotation:

notepad
begin
  fix A B C
  have "A ⟹ B ⟹ C"
  proof -
    assume A B
    then show C sorry
  qed
next
  fix A B C
  have C if A and myprem: B
  proof -
    thm that (*hover here*)
    thm myprem (*hover here*)
    thm ‹A› (*hover here*)
    from that show C sorry
  qed
end

John Hughes (Feb 13 2026 at 20:04):

Ah. I see. In the first half, I could also write then show ?thesis I find, which makes sense now.

Stream: Beginner Questions