Email Gateway (Aug 22 2022 at 20:42): Email Gateway (Aug 22 2022 at 20:42):From: Martin Desharnais <martin.desharnais@gmail.com>
Dear Isabelle users,
I just encountered an unexpected behaviour when stating assumptions of a
locale. I would have expected the three following locale definitions to
be equivalent, but it turned out that C is invalid.
locale A =
fixes foo :: "'a ⇒ 'b" and bar :: "'b ⇒ 'a"
assumes
h1: "foo (bar x) = x" and
h2: "bar (foo y) = y"
locale B =
fixes foo :: "'a ⇒ 'b" and bar :: "'b ⇒ 'a"
assumes
h1: "⋀x. foo (bar x) = x" and
h2: "⋀x. bar (foo x) = x"
(*
Type unification failed
Type error in application: incompatible operand type
Operator: foo :: 'a ⇒ 'b
Operand: x :: 'b
*)
locale C =
fixes foo :: "'a ⇒ 'b" and bar :: "'b ⇒ 'a"
assumes
h1: "foo (bar x) = x" and
h2: "bar (foo x) = x"
thm A.h1 B.h1 (* C.h1 *)
(*
A ?foo ?bar ⟹ ?foo (?bar ?x) = ?x
B ?foo ?bar ⟹ ?foo (?bar ?x) = ?x
*)
It turns out that x is shared in the two assumptions, which makes h2
ill-typed.
In the tutorial on locales, I found the following explication (§2).
Isabelle recognises unbound names as free variables. In locale
assumptions, these are implicitly universally quantified.
In the isar-ref documentation, I found the following explication (§5.7.2).
assumes a: φ1 ... φn introduces local premises, similar to assume
within a proof (cf. §6.2.1).
I did not notice anything in section 6.2.1 explaining this behaviour. It
seems that the automatic insertion of universal variables is done on the
set of assumptions instead of all assumption individually. I was just
surprised by this behaviour and wanted to suggest raising this point
more clearly in the documentation or tutorial.
Regards,
Martin Desharnais
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC