Stream: Beginner Questions

Topic: Multiple instances of the same locale in one theorem

Yiming Xu (Oct 07 2024 at 03:15):

I believe it would be good if I can use multiple instances of the same locale. For example, what should people do if we have the locale of partial orders, and have a theorem talking about, say, an isomorphism, between two partial orders? How do people invoke the relevant fact about locales in such case?
More concretely, I have a locale for "models"

locale model =
  fixes
    W :: ‹'w set› and
    Rd :: ‹('r ⇒ 'w list ⇒ bool)› and
    V :: ‹ ('p ⇒ 'w ⇒ bool)›
  assumes
    Rd_on_W: ‹⋀wl m. Rd m wl ⟹ list_all (λw. w ∈ W) wl› and
begin
...
end

Then a tuple (W,Rd,V) is a model. But I may want to prove something like:

bmor f τ (W0,Rd0,V0) (W,Rd,V) under the assumptions that both W0,R0,V0 and W,Rd,V are models. Is there any pretty way of doing that? Or do we just write it as assumptions? (I do not quite want to.)

Mathias Fleury (Oct 07 2024 at 05:00):

interprete

Mathias Fleury (Oct 07 2024 at 05:04):

You can locally prove that something is a locale:

locale model =
  fixes
    W :: ‹'w set› and
    Rd :: ‹('r ⇒ 'w list ⇒ bool)› and
    V :: ‹ ('p ⇒ 'w ⇒ bool)›
  assumes
    Rd_on_W: ‹⋀wl m. Rd m wl ⟹ list_all (λw. w ∈ W) wl›
begin
lemma T: ‹True ∨ P W›
  by auto
end

lemma
  fixes
    W :: ‹'w set› and
    Rd :: ‹('r ⇒ 'w list ⇒ bool)› and
    V :: ‹ ('p ⇒ 'w ⇒ bool)›
  assumes
    Rd_on_W: ‹⋀wl m. Rd m wl ⟹ list_all (λw. w ∈ W) wl›
  shows False
proof -
  interpret x1: model W Rd
    by standard (auto intro: Rd_on_W)
  thm x1.T

  interpret x2: model ‹W ∪ W› Rd
    sorry
  thm x2.T

Mathias Fleury (Oct 07 2024 at 05:06):

But there is no way to do that implicitly, you really need to have it as assumption with model W Rd

Mathias Fleury (Oct 07 2024 at 05:07):

(for implicit stuff you need to go to classes)

Yiming Xu (Oct 07 2024 at 06:07):

I see. Thank you! And indeed, I was talking about avoid the assumptions like model W Rd. By classes, do you mean type class?

Mathias Fleury (Oct 07 2024 at 07:14):

Yeah I meant type classes, but they have limitations in Isabelle/HOL

Mathias Fleury (Oct 07 2024 at 07:14):

like only one class per type

Yiming Xu (Oct 07 2024 at 07:23):

I heard that type class is just a locale underneath but have not devoted time reading further about this. Only one class per type sounds a bit funny... I cannot guess why this restriction is applied. It is not problematic for my specific aim, but still sound not satisfactory. I may just use assumptions for this moment.

Mathias Fleury (Oct 07 2024 at 07:27):

I should express this better: it is not one class per type, it is each class can be used only once per type

Mathias Fleury (Oct 07 2024 at 07:29):

The main issue I had: you cannot have two orders on 'a option, one where None is the smallest and one where None is the largest. In my case, one was in the library and I needed the other

Mathias Fleury (Oct 07 2024 at 07:29):

Therefore I had to define my own option type

Yiming Xu (Oct 07 2024 at 07:41):

I see. It means if you apply "interpretation" for a type "'a" to be in type class A, then you cannot interpret it as in type class B anymore. Then it actually makes a (tiny) bit of sense to why is that restriction. Type class sounds like "a type belongs to a class of types", and this might be sort of analogue to "any type has a unique type"...

Yiming Xu (Oct 07 2024 at 07:42):

But still I would not like it.

Yiming Xu (Oct 07 2024 at 07:43):

You then need another option type just to be able to put in the class where the NONE is the largest/lowest. I hope there would be automatic tools to transfer between the two versions of options types (if such a thing exists and work will, still does not sound too bad).

Last updated: Dec 21 2024 at 16:20 UTC