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