*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Rewrites for a sublocale with UNIV as the carrier set*From*: Lukas Stevens <lukas.stevens+isabelle-users at in.tum.de>*Date*: Fri, 5 Feb 2021 14:15:27 +0100*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.6.1

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

**Follow-Ups**:**Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set***From:*YAMADA, Akihisa

- Previous by Date: Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use?
- Next by Date: [isabelle] Incompatibility between code generation, HOL-Library.Numeral_Type, and Containers.Set_Impl
- Previous by Thread: Re: [isabelle] Isabelle2021-RC1 - Any way to limit "veriT" memory use?
- Next by Thread: Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set
- Cl-isabelle-users February 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list