# Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set

```Dear Lukas,

```
sorry indeed, the trick works only if you put trivial assumptions after nontrivial ones like:
```
lemma bar2: "Z A ⟹ X ⊆ A ⟹ P X"

```
If you don't want to swap assumptions, I only know a terribly naive workaround to add such rewrites like
```  "⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
as many as you need.

Best,
Akihisa

On 2021/02/08 19:49, Lukas Stevens wrote:
```
```That does not seem to work. See the example below:

theory Scratch imports Main
begin

axiomatization P :: "'a ⇒ bool"
axiomatization Z :: "'a ⇒ bool"

locale foo =
fixes A :: "'a set"
begin

lemma bar: "X ⊆ A ⟹ Z A  ⟹ P X"
sorry

end

locale bar
begin

sublocale foo UNIV
rewrites "Y ⊆ UNIV ≡ True" and "⋀Q. (True ⟹ PROP Q) ≡ Q" and "⋀Q. (True ⟹ Q) ≡ Trueprop Q"
by auto

(* ⟦True; Z UNIV⟧ ⟹ P ?X
Z UNIV ⟹ P ?X *)
thm bar
end

end

On 2/7/21 3:37 AM, YAMADA, Akihisa wrote:
```
```Hello Lukas,

```
I had the same question before but it was not concluded. As a workaround, I'm declaring the two rewrites and it works for any number of assumptions.
```
"⋀Q. (True ⟹ PROP Q) ≡ Q" and "⋀Q. (True ⟹ Q) ≡ Trueprop Q"

Best regards,
Akihisa

On 2021/02/05 22:15, Lukas Stevens wrote:
```
```Hello,

```
suppose I have a locale foo_on that assumes that some predicate P holds on a carrier set A. Often, one wants to specialise this to a locale foo where A is the UNIV. The problem is that theorems in foo_on often have assumptions of the form "X ⊆ A" which are "X ⊆ UNIV" in the context of foo. Those assumptions are trivial so I want to get rid of them using rewrites but this doesn't seem to work as the example below shows:
```
axiomatization P :: "'a ⇒ bool"

locale foo =
fixes A :: "'a set"
begin

lemma bar: "X ⊆ A ⟹ P X"
sorry

end

locale bar
begin

```
(* (True ==> Q) ≡ Trueprop Q works for the theorem bar but not for theorems with multiple assumptions. *) sublocale foo UNIV rewrites "Y ⊆ UNIV ≡ True" and "(True ⟹ PROP Q) ≡ PROP Q"
```   by auto

end

What is going wrong here?

Cheers,

Lukas

```
```
```
```
--
このEメールはアバスト アンチウイルスによりウイルススキャンされています。
https://www.avast.com/antivirus

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.