*To*: lukas.stevens+isabelle-users at in.tum.de, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set*From*: "YAMADA, Akihisa" <ayamada at trs.cm.is.nagoya-u.ac.jp>*Date*: Mon, 8 Feb 2021 21:01:26 +0900*In-reply-to*: <c56491b0-7af9-56dc-9b19-9e6bebda5ab8@in.tum.de>*References*: <4f696043-2b46-d647-7f67-74f23957acf8@in.tum.de> <3b568042-7a61-b36a-aeca-8cebe1babe9f@trs.cm.is.nagoya-u.ac.jp> <c56491b0-7af9-56dc-9b19-9e6bebda5ab8@in.tum.de>*User-agent*: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.7.0

Dear Lukas,

lemma bar2: "Z A ⟹ X ⊆ A ⟹ P X"

"⋀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 instead of 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 aworkaround, I'm declaring the two rewrites and it works for any numberof 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 Pholds on a carrier set A. Often, one wants to specialise this to alocale foo where A is the UNIV. The problem is that theorems infoo_on often have assumptions of the form "X ⊆ A" which are "X ⊆UNIV" in the context of foo. Those assumptions are trivial so I wantto get rid of them using rewrites but this doesn't seem to work asthe 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 fortheorems 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

**References**:**[isabelle] Rewrites for a sublocale with UNIV as the carrier set***From:*Lukas Stevens

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

**Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set***From:*Lukas Stevens

- Previous by Date: Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set
- Next by Date: Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set
- Previous by Thread: Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set
- 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