Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unbound schematic variable: ?thesis

Email Gateway (Aug 07 2020 at 07:35):

From: Christopher Hoskin <christopher.hoskin@gmail.com>
When trying to conclude the following lemma, I am getting "Unbound
schematic variable: ?thesis" in the line " from dir_D uDuS show
?thesis". What has gone wrong, and how should I conclude the result?

Thanks

Christopher

theory Scratch
imports "HOL-Lattice.CompleteLattice"
begin

definition directed :: "'a::complete_lattice set ⇒ bool"
where "directed D ≡ (D≠{})∧(∀a∈D. ∀b∈D. ∃c∈D. a⊑c ∧ b⊑c)"

lemma
assumes "S≠{}"
assumes D_def: "D={⨆F | F. F ⊆ S ∧ finite F}"
shows "directed D" and "⨆D=⨆S"
proof -
have "D≠{}"
using D_def by blast
{ fix a b assume a_def: "a∈D" and b_def: "b∈D"
obtain F1 where "a=⨆F1" and "F1⊆S" and "finite F1"
using D_def ‹a ∈ D› by blast
obtain F2 where "b=⨆F2" and "F2⊆S" and "finite F2"
using D_def ‹b ∈ D› by blast
define c where "c=⨆(F1∪F2)"
have "c∈D"
using D_def ‹F1 ⊆ S› ‹F2 ⊆ S› ‹finite F1› ‹finite F2› c_def by blast
have "a ⊑ c ∧ b⊑c"
by (simp add: Join_subset_mono ‹a = ⨆F1› ‹b = ⨆F2› c_def)
then have "∃c∈D. a⊑c ∧ b⊑c"
using ‹c ∈ D› by blast
}
from this have dir_D: "directed D"
by (simp add: ‹D ≠ {}› directed_def)
have "⨆D⊑⨆S"
by (smt D_def Join_least Join_subset_mono mem_Collect_eq)
{ fix a assume "a∈S"
have "a=⨆{a}∧finite {a}"
by (simp add: Join_singleton)
from this have "a∈D"
using D_def ‹a ∈ S› by blast
from this have "S⊆D"
by (smt D_def Join_singleton finite.intros(1) finite_insert
insert_is_Un mem_Collect_eq mk_disjoint_insert subsetI sup_ge1)
}
from this have "⨆S⊑⨆D"
by (meson Join_least Join_subset_mono)
from this have uDuS: "⨆D=⨆S"
by (simp add: ‹⨆D ⊑ ⨆S› leq_antisym)
from dir_D uDuS show ?thesis
qed

end

Email Gateway (Aug 07 2020 at 07:43):

From: Manuel Eberl <eberlm@in.tum.de>
?thesis is only set when you when you state a single goal. Here, you
have two goals, so there is no ?thesis.

Just change that one line towards the very end to

from this show uDuS: "⨆D=⨆S"
by (simp add: ‹⨆D ⊑ ⨆S› leq_antisym)

i.e. "show" the goal by explicitly writing it down.

You can, in principle, also introduce your own abbreviations in the
lemma statement, e.g.

lemma
assumes "S≠{}"
assumes D_def: "D={⨆F | F. F ⊆ S ∧ finite F}"
shows "directed D" (is ?thesis1)
and "⨆D=⨆S" (is ?thesis2)

but since the goals are so short, it is not really worth it.

Personally, I would say that writing ?thesis/?case should only be used
when the goal is too unwieldy to write directly. But that is just a
matter of taste.

Cheers,

Manuel

Email Gateway (Aug 07 2020 at 17:13):

From: Christopher Hoskin <christopher.hoskin@gmail.com>
Dear Manuel,

Thank you very much for the explanation!

Christopher

Email Gateway (Aug 08 2020 at 10:10):

From: isabelle-users@florianmaerkl.de
Hi Christopher,

that's because you have multiple goals in your lemma:

shows "directed D" and "⨆D=⨆S"

Instead of using ?thesis you can type them out manually:

from dir_D uDuS show "directed D" "⨆D=⨆S" by auto

Florian

Last updated: Jan 04 2025 at 20:18 UTC