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

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.


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,

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

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"

lemma bar: "X ⊆ A ⟹ P X"


locale bar

(* (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


What is going wrong here?



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