Email Gateway (Aug 23 2022 at 08:49): Email Gateway (Aug 23 2022 at 08:49):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
Recently, I encountered another relatively minor technical issue. I am
using interpretation with rewriting in my work very extensively and
frequently. However, some of the rewrite rules need to be repeated for
different interpretations. Luckily, the rewrite rules can be stated (and
even proven) outside of the context of any particular locale. However, it
is very cumbersome (and error-prone) to restate them for every locale
interpretation. Therefore, I am curious whether it is possible to store the
rewrite rules externally in a manner similar to the way theorems can be
stored in a collection of named_theorems. Even if this functionality is not
available natively, I am curious if anyone is aware of any third-party
tools that could allow one to achieve similar functionality?
Hopefully, the following example will clarify my question, if it is not
entirely transparent:
locale A =
fixes a b :: int
assumes a1: "a = 1"
and b0: "b = 0"
begin
lemma id_a: "x*a = x" using a1 by auto
end
definition c :: int where "c = -1"
(* named_terms my_terms
term [my_terms] = "c * c = 1" *)
locale B =
fixes b :: int
assumes b: "b = 0"
―‹Instead of›
sublocale B ⊆ A: A ‹c * c› b
rewrites "c * c = 1"
subgoal by (simp add: A.intro b c_def)
subgoal unfolding c_def by simp
done
―‹
I would like to be able to write
‹
sublocale B ⊆ A ‹c * c› b
rewrites my_terms
sorry
›
›
Kind Regards,
Mikhail Chekhov
Last updated: Apr 19 2024 at 12:27 UTC