I have the following two locales

```
locale comp_fun_commute_on =
fixes S
fixes f
assumes "x ∈ S ==> y ∈ S ==> f y o f x = f x o f y"
begin
...
end
locale comp_fun_commute =
fixes f
assumes "f y o f x = f x o f y"
begin
sublocale comp_fun_commute_on_UNIV?: comp_fun_commute_on UNIV f
by ...
end
lemma (in comp_fun_commute_on) comp_comp_fun_commute_on:
"range g ⊆ S ⟹ comp_fun_commute_on S (f o g)"
by ...
lemma (in comp_fun_commute) comp_comp_fun_commute:
"comp_fun_commute (f o g)"
sorry
```

As you can see the second locale is a specialised version of the first one where the carrier set is the universe. I want two separate locales since I can remove the assumptions of the form `S \<subseteq> UNIV`

and `x ∈ UNIV`

in `comp_fun_commute`

and to maintain backwards compatability.

Conceptually, I would like to prove the last lemma by applying the introduction rule `comp_fun_commute_on UNIV f ==> comp_fun_commute f`

but I don't have this lemma yet. Do I have to prove that or is there any way to structure the locales differently such that it reflects the fact that `comp_fun_commute_on UNIV f = comp_fun_commute f`

?

Hm, you can do `sublocale cfc_on: comp_fun_commute_on UNIV f`

in `comp_fun_commute`

.

I think there's also the `rewrites`

argument for `sublocale`

that allows you to perform some simplifications on the theorems you get out of the interpretation to get rid of things like `x ∈ UNIV`

.

Manuel Eberl said:

Hm, you can do

`sublocale cfc_on: comp_fun_commute_on UNIV f`

in`comp_fun_commute`

.

That is already in the code sample :wink:

Manuel Eberl said:

I think there's also the

`rewrites`

argument for`sublocale`

that allows you to perform some simplifications on the theorems you get out of the interpretation to get rid of things like`x ∈ UNIV`

.

I am not really sure how that rewrites thing works. Is it just `rewrites "x ∈ UNIV ≡ True"`

?

isn't your problem a pure typing problem?

`g`

has the wrong type in your second lemma

Baring copy-and-paste mistakes, it typechecks

Is that an option?

```
locale comp_fun_commute = comp_fun_commute_on UNIV f
for f
```

Then you will have the assumptions of the form `x ∈ UNIV`

in the locale conclusions.

And the locale assumption is `x ∈ UNIV ==> y ∈ UNIV ==> f y o f x = f x o f y`

instead of `f y o f x = f x o f y`

.

In this case that wouldn't be so bad but if the equivalence of the locales would be non-trivial then you wouldn't want to do that.

Lukas Stevens said:

Then you will have the assumptions of the form

`x ∈ UNIV`

in the locale conclusions.

This would break backwards-compatability as well.

Lukas Stevens said:

Manuel Eberl said:

I think there's also the

`rewrites`

argument for`sublocale`

that allows you to perform some simplifications on the theorems you get out of the interpretation to get rid of things like`x ∈ UNIV`

.I am not really sure how that rewrites thing works. Is it just

`rewrites "x ∈ UNIV ≡ True"`

?

No idea. It's probably documented somewhere. Or look at how it is used in the distribution. I never really used it myself.

Isn't the problem that locales don't express what you want?

From what I understand, locales instantiation is done in the metalogic, so there is no theorem corresponding to the sublocale.

Mathias Fleury said:

Isn't the problem that locales don't express what you want?

Yeah, it's possible that you can't express that with locales.

Hm, `rewrites "(A \<subseteq> UNIV ==> PROP P) ≡ PROP P"`

does not work.

Seems to be a problem with the prop thing.

```
axiomatization P :: "'a ⇒ bool"
locale foo =
fixes A :: "'a set"
begin
lemma bar: "X ⊆ A ⟹ P X"
sorry
end
locale bar
begin
sublocale foo UNIV rewrites "Y ⊆ UNIV ≡ True" and "(True ⟹ PROP Q) ≡ PROP Q"
by auto
```

If you replace the second `rewrites`

rule with `(True ⟹ Q) ≡ Trueprop Q`

it works. But of course that will not be enough for rules with several implications.

No idea what's going on here. Might want to ask on the mailing list.

Last updated: Oct 25 2021 at 20:20 UTC