Email Gateway (Aug 23 2022 at 08:57): Email Gateway (Aug 23 2022 at 08:57):From: Peter Lammich <lammich@in.tum.de>
Hi
A congruence rule can only be provided on a per-definition base,
not
on a per-interpretation base: the critical syntactic constant c.f
appears in any interpretation.Having a default congruence rules that must be removed in certain
non-trivial situations is a bad idea: few users are getting in touch
with congruence rules ever.
what are the special situations where you actually want
simplification of locale parameters?
In my memory, I only remember very odd effects due to unwanted
simplifications, but I never wanted to simplify locale parameters fixed
by an interpretation.
The only case I can imagine right now are partial interpretations, like
in this artificial example:
locale Invariant = fixes A B state
begin
definition "I == A state & B state"
...
end
interpretation my_inv: Invariant (%s. assn1 s) (%s. assn2 s) state
for state .
and the subsequent usage of "my_inv.I" as a predicate over states.
In this case, in term "my_inv.I s" == "Invariant.I assn1 assn2 s", I
want s to be simplified, but not assn1 and assn2.
Last updated: Apr 26 2024 at 20:16 UTC