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