*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set*From*: Lukas Stevens <lukas.stevens+isabelle-users at in.tum.de>*Date*: Tue, 16 Feb 2021 11:35:51 +0100*In-reply-to*: <aace188a9582150041c51d65d16855ff@in.tum.de>*References*: <aace188a9582150041c51d65d16855ff@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.3.1

You can achieve the desired behaviour by adding a premise swapping rule:

rewrites "⋀P. (True ⟹ P) ≡ Trueprop P" and "⋀P Q. (True ⟹ PROP P ⟹ PROP Q) ≡ (PROP P ⟹ True ⟹ PROP Q)"

Since the rewrite mechanism is not intended to be used that way, would you recommend against it? What would be an alternative?

Cheers,

Lukas

On 13.02.21 17:52, Clemens Ballarin
wrote:

Thanks for sharing these observations.

Rewrite morphisms are based on Pattern.rewrite_term. This is for efficiency and robustness (morphisms are composed along the locale hierarchy). That rewrite morphisms can be used to delete certain assumptions could be considered a lucky coincident. They are not intended to be used that way.

Clemens

On 2021-02-07 03:37, 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

**References**:**Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set***From:*Clemens Ballarin

- Previous by Date: Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer
- Next by Date: Re: [isabelle] Isabelle2021-RC3 New failure mode for "try"/sledgehammer
- Previous by Thread: Re: [isabelle] Rewrites for a sublocale with UNIV as the carrier set
- Next by Thread: [isabelle] Incompatibility between code generation, HOL-Library.Numeral_Type, and Containers.Set_Impl
- 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