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?
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:
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
"⋀Q. (True ⟹ PROP Q) ≡ Q" and "⋀Q. (True ⟹ Q) ≡ Trueprop Q"
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"
(* (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"
What is going wrong here?