Stream: General

Topic: Command show ?thesis does not work

Gergely Buday (Feb 05 2026 at 14:24):

I have a goal in the middle of a large proof (sorry I cannot copy it here or come up with a minimal non-working example). When I copy the goal into a show statement, I get

Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:

I get the same when I use

show ?thesis

What can cause this? I have a fix and an assume statement in the beginning of the proof, and the original goal starts with

∀b∈{xs. set xs ⊆ B ∧ distinct xs} .

terru (Feb 05 2026 at 14:33):

what is your assume? If you assume things which are not in the goal (& I don't see your original goal having any assumptions), then Isabelle will accept the assumption (it will even accept assume False), but then give you this error when trying to use show, as what you are showing is not a refinement of the goal you actually wanted to prove (but instead <your assumption> ==> <your actual goal>)

Gergely Buday (Feb 05 2026 at 14:36):

I changed it to

  have ba:
    "(∀b. b∈{xs. set xs ⊆ B ∧ distinct xs} ⟶ conclusion        "
        proof -
          fix b
          assume b_assumption: "b ∈ {xs. set xs ⊆ B ∧ distinct xs}"

but I still get the same error message

Gergely Buday (Feb 05 2026 at 14:38):

This happens also when I have

∀b∈{xs. set xs ⊆ B ∧ distinct xs} . conclusion

terru (Feb 05 2026 at 14:48):

the proof - will not change anything (the - means "do not do anything to the goal"). If you delete the -, a default proof method will be applied; for your second case that should transform ∀b∈{xs. set xs ⊆ B ∧ distinct xs} . conclusion to ⋀b. b∈{xs. set xs ⊆ B ∧ distinct xs} ⟹ conclusion, at which point you can use assume

(note that assume only works with the meta-level ⟹, not the object-level ⟶, so sometimes you first have to convert one to the other)

Gergely Buday (Feb 05 2026 at 15:08):

OK I go down to the simplest example I can come up:

lemma "⋀a. P a ⟹ Q a"
proof -
  fix a
  assume "P a"
  show ?thesis

where I get

Type unification failed: Clash of types "_ ⇒ _" and "bool"

Type error in application: incompatible operand type

Operator:  Trueprop :: bool ⇒ prop
Operand:   ?thesis :: 'a ⇒ bool

Why I get this?

Maximilian Schäffeler (Feb 05 2026 at 18:39):

While do not know how exactly ?thesis is constructed in general, you can inspect it using term ?thesis in the proof and you will obtain the result "Q" :: "'a ⇒ bool".
So when you write show ?thesis you are trying to initiate a "proof of a function", but Isabelle expects a proof of a proposition.

Balazs Toth (Feb 05 2026 at 22:05):

I'm also not a 100% sure how ?thesis gets constructed, but here different ways of how your example works:

lemma "⋀a. P a ⟹ Q a"
proof -
  fix a
  assume "P a"
  show "?thesis a"
    sorry
qed

lemma "⋀a. P a ⟹ Q a"
proof -
  fix a
  assume "P a"
  show "Q a"
    sorry
qed

lemma
  assumes "P a"
  shows "Q a"
  using assms
proof -
  fix a
  assume "P a"
  show ?thesis
    sorry
qed

lemma
  assumes "P a"
  shows "Q a"
proof -
  fix a
  show ?thesis
    using assms
    sorry
qed

Last updated: Feb 06 2026 at 20:37 UTC