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

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

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

Dear Manuel,

Thank you very much for the explanation!

Christopher

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: Sep 28 2021 at 19:14 UTC