[isabelle] Shared free variables in locale assumptions



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

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.