Email Gateway (Feb 05 2021 at 13:16): Email Gateway (Feb 05 2021 at 13:16):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
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
Email Gateway (Feb 07 2021 at 02:38):From: "YAMADA, Akihisa" <ayamada@trs.cm.is.nagoya-u.ac.jp>
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
Email Gateway (Feb 08 2021 at 10:50):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
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
Email Gateway (Feb 08 2021 at 12:02):From: "YAMADA, Akihisa" <ayamada@trs.cm.is.nagoya-u.ac.jp>
Dear Lukas,
sorry indeed, the trick works only if you put trivial assumptions after
nontrivial ones like:
lemma bar2: "Z A ⟹ X ⊆ A ⟹ P X"
If you don't want to swap assumptions, I only know a terribly naive
workaround to add such rewrites like
"⋀P1 P2. (True ⟹ PROP P1 ⟹ PROP P2) ≡ (PROP P1 ⟹ PROP P2)"
as many as you need.
Best,
Akihisa
Email Gateway (Feb 08 2021 at 19:38):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Lukas Stevens and Akihisa Yamada/All,
I would like to make a side remark with regard to the discussion and ask a
couple of related questions to the developers/maintainers of Isabelle.
While I am also not certain whether and how one could construct a rewrite
system capable of coping with the problem outlined by Lukas Stevens
(although it seems like the application of the attribute "simplified" with
the default simpset can remove "True" in most cases, so it may be worth
trying to understand the principle employed), there is little that could
stop one from batch-processing the theorems after the locale
interpretation: see the code listing in the appendix. Potentially, one can
even override the theorems that were produced during the interpretation in
this manner. However, keep in mind that the code is merely a very rough
sketch of the idea, not a working implementation (e.g. one would need to
consider how to propagate the effects of the attributes that were applied
to the original theorems and several other issues).
In this context, I would like to ask two questions to the developers of
Isabelle:
I am curious as to what exactly is preventing from allowing users to
provide more general/arbitrary theorem transformations during the locale
interpretation, instead of plain rewriting.
I am curious if there is a way to allow for an application of a given
predefined rewrite system repeatedly to different distinct interpretations.
For example, if one was to develop a rewrite system for eliminating "True"
from theorems, it would be useful to allow for its repeated application
without code duplication. However, at the moment, it seems like one would
have to restate the relevant terms explicitly for every interpretation
(unless I am mistaken, and there already exists an implementation of this
functionality).
Kind Regards,
Mikhail Chekhov
theory Scratch
imports Main
keywords "attributes_for_qual" :: thy_defn
begin
ML‹
(*copied with amendments from the file Proof_Context.ML
in the main distribution of Isabelle2021-RC2*)
fun get_local_facts verbose ctxt =
let
val facts = Proof_Context.facts_of ctxt
val props = map #1 (Facts.props facts)
val local_facts =
(if null props then [] else [("<unnamed>", props)]) @
Facts.dest_static
verbose [Global_Theory.facts_of (Proof_Context.theory_of ctxt)]
facts
in local_facts end;
fun append_local c = "local." ^ c ^ ".";
fun remove_local c = String.extract (c, 6, NONE);
fun prep_attrb_facts ctxt attrbs (b, thms) =
let
val facts' =
((b, attrbs) ||> map (Attrib.check_src ctxt), single (thms, []))
|> single
|> Attrib.partial_evaluation ctxt
in facts' end;
fun process_simplify (qualc, attrbs) ctxt =
let
val mk_name = remove_local
#> curry (swap #> op^) "'"
#> Binding.qualified_name
val thmss = get_local_facts false ctxt
|> filter (fn (c, _) => String.isPrefix (append_local qualc) c)
|> map (apfst mk_name)
val factss = thmss |> map (prep_attrb_facts ctxt attrbs)
in fold (curry (uncurry Local_Theory.notes #> snd)) factss ctxt end;
val _ = Outer_Syntax.local_theory
\<^command_keyword>‹attributes_for_qual›
"apply attributes to a set of theorems in the local context"
(Parse.string -- Parse.attribs >> process_simplify);
›
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: foo UNIV
rewrites "Y ⊆ UNIV ≡ True"
and "⋀Q. (True ⟹ PROP Q) ≡ Q"
and "⋀Q. (True ⟹ Q) ≡ Trueprop Q"
by auto
attributes_for_qual "foo" [simplified]
thm foo.bar'
end
end
Email Gateway (Feb 13 2021 at 16:53):From: Clemens Ballarin <ballarin@in.tum.de>
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
Email Gateway (Feb 16 2021 at 10:36):From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
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
Last updated: Jul 15 2022 at 23:21 UTC