Email Gateway (Aug 22 2022 at 16:54): Email Gateway (Aug 22 2022 at 16:54):From: Lars Hupel <hupel@in.tum.de>
Dear list,
classes give rise to a constant definition, like so:
class eq =
fixes eq :: "'a ⇒ 'a ⇒ bool"
assumes refl: "eq x x" and
sym: "eq x y ⟹ eq y x" and
trans: "eq x y ⟹ eq y z ⟹ eq x z"
(* print_statement class.eq_def *)
theorem eq_def:
fixes eq :: "'a ⇒ 'a ⇒ bool"
shows "class.eq eq ≡ (∀x. eq x x) ∧ (∀x y. eq x y ⟶ eq y x) ∧ (∀x y z.
eq x y ⟶ eq y z ⟶ eq x z)"
I didn't find a way to obtain that theorem from ML, neither in structure
"Axclass" nor in "Class". Is it available somewhere?
Cheers
Lars
Email Gateway (Aug 22 2022 at 17:07):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,
the primitive definition of the locale predicate is indeed not stored in
the locale bookkeeping – but it could be added there of course.
Cheers,
Florian
signature.asc
Last updated: Apr 24 2024 at 01:07 UTC