Email Gateway (Aug 18 2022 at 11:41): Email Gateway (Aug 18 2022 at 11:41):From: Clemens Ballarin <ballarin@in.tum.de>
Hi David,
interpretation is an operation on locales. Interpretations cannot be
assumed.
This is not the case. In your theory, bop.refine_def is a
conditional equation, applicable in contexts where the locale bop is
present. In the lemma you don't have this information. The
assumption "a \<sqsubseteq> b" gives you the refine relation between
a and b, but you do not have "bop a b", and consequently neither
"ADType a" nor "ADType b".
Clemens
Email Gateway (Aug 18 2022 at 11:41):From: Makarius <makarius@sketis.net>
BTW, Isar proofs work out more smoothly when presenting statements in
natural rule format. This prevents having to walk through the outermost
structure first, both in the proof and the application of the result later
on. E.g. compare these two versions:
lemma transitive1: "a <= b --> b <= c --> a <= c"
proof
assume ab: "a <= b"
show "b <= c --> a <= c"
proof
assume bc: "b <= c"
show "a <= c"
using ab bc sorry
qed
qed
lemma transitive2:
assumes ab: "a <= b"
and bc: "b <= c"
shows "a <= c"
proof -
show ?thesis using ab bc sorry
qed
Makarius
Last updated: May 03 2024 at 12:27 UTC