Email Gateway (Aug 19 2022 at 17:29): Email Gateway (Aug 19 2022 at 17:29):From: "Eugene W. Stark" <stark@cs.stonybrook.edu>
It seems like with almost anything I try to do with locales,
I run up against behavior that I have no way to comprehend from
the documentation that comes with the Isabelle2014 system.
Here is my latest example (below and also attached).
The interpretation of partial_order inside the sup_semilattice
locale context block succeeds, but an attempt to declare
sup_semilattice as a sublocale of partial_order fails.
Even though the "locale tutorial" says that the final sublocale
proof will take place in the context of the sup_semilattice locale,
apparently the connection between the parameter sup of that
locale and the derived notion le is not retained.
What is also strange is that the identifier le is not completely free:
if I enter a dummy lemma like have "le = le" and CTRL-mouse
over the "le", it shows not a completely generic type but actually
the type inherited from the sup_semilattice locale.
Can anyone explain how I should understand this? Thanks.
- Gene Stark
theory Strange
imports Main
begin
locale partial_order =
fixes le :: "'a ⇒ 'a ⇒ bool"
assumes le_refl: "le x x"
and le_antisym: "le x y ∧ le y x ⟶ x = y"
and le_trans: "le x y ∧ le y z ⟶ le x z"
locale sup_semilattice =
fixes I :: 'a and sup :: "'a ⇒ 'a ⇒ 'a"
assumes sup_unit_left: "sup I x = x"
and sup_unit_right: "sup x I = x"
and sup_commute: "sup x y = sup y x"
and sup_assoc: "sup x (sup y z) = sup (sup x y) z"
and sup_idem: "sup x x = x"
begin
definition le where "le x y = (sup x y = y)"
lemma le_refl: "le x x" using le_def sup_idem by blast
lemma le_antisym: "⟦ le x y; le y x ⟧ ⟹ x = y" using le_def sup_commute by auto
lemma le_trans: "⟦ le x y; le y z ⟧ ⟹ le x z" using le_def sup_assoc by metis
lemma le_po: "partial_order le"
proof
fix x y z
show "le x x" using le_refl by auto
show "le x y ∧ le y x ⟶ x = y" using le_antisym by auto
show "le x y ∧ le y z ⟶ le x z" using le_trans by blast
qed
interpretation partial_order le using le_po by auto
end
sublocale sup_semilattice ⊆ partial_order
proof
fix x y z
show "le x x" using le_refl by auto (* Fails! Nitpick gives a counterexample. *)
show "le x y ∧ le y x ⟶ x = y" using le_antisym by auto
show "le x y ∧ le y z ⟶ le x z" using le_trans by blast
qed
end
Strange.thy
Email Gateway (Aug 19 2022 at 17:31):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Gene,
Can anyone explain how I should understand this? Thanks.
there is actually nothing strange here:
sublocale sup_semilattice ⊆ partial_order
Note that on the right on side of »⊆« there is a locale expression, not
a locale name. To establish the desired correspondence, you have to
give an explicit instantiation for the parameter(s) of partial_order:
sublocale sup_semilattice ⊆ partial_order le
Otherwise just default names for fresh variables are instantiated.
Hope this helps,
Florian
signature.asc
Last updated: Apr 24 2024 at 12:33 UTC