Email Gateway (Aug 18 2022 at 11:22): Email Gateway (Aug 18 2022 at 11:22):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear David,
the problem is that internally locally defined constants are just
higher-order abbreviations for certain terms. After interpretation,
these abbreviations are only input abbreviations (to avoid strange
output behavior). To get the desired behavior, you have to re-introduce
the appropriate abbreviation after interpretation <. See the following
code snippet:
interpretation pbop < bop
by unfold_locales
context pbop
begin
abbreviation bsimulate where
"bsimulate == bop.bsimulate adtA adtC"
lemma powerbsim: "bsimulate a (poweradt a)"
unfolding bsimulate_def
sorry
end
Hope this helps
Florian
florian.haftmann.vcf
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC