*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Shared free variables in locale assumptions*From*: Martin Desharnais <martin.desharnais at gmail.com>*Date*: Fri, 4 Oct 2019 18:17:57 +0200*Autocrypt*: addr=martin.desharnais at gmail.com; prefer-encrypt=mutual; keydata= mDMEWeXYxRYJKwYBBAHaRw8BAQdAsOV1c6NtNeZBj4FQWywoTTKNwQNx8oCLJOQtQXKx/Ku0 L01hcnRpbiBEZXNoYXJuYWlzIDxtYXJ0aW4uZGVzaGFybmFpc0BnbWFpbC5jb20+iJYEExYI AD4WIQSQsb+oyQIj1XPAsM96+p9h8fpD5gUCWeXYxQIbAwUJCWYBgAULCQgHAgYVCAkKCwIE FgIDAQIeAQIXgAAKCRB6+p9h8fpD5hVIAQDQsCvKjL3JErp33GHs+PdD1gUIdPCG50Crsbrd 5zNVmAEAwadxF17qkhcAXcqr2galgofB4rYEp8HmJO+sXj2KJwe4OARZ5djFEgorBgEEAZdV AQUBAQdAojxcR37buaV6a1MGo/O19BAixUlmCNccrH8Uab+L+kkDAQgHiH4EGBYIACYWIQSQ sb+oyQIj1XPAsM96+p9h8fpD5gUCWeXYxQIbDAUJCWYBgAAKCRB6+p9h8fpD5m8RAQDb4yBL kq0ZjR6Jl4vHsz0wF5SosX96To4vlzucTQq/RwD/SgY4mEUbKq7e4s/YT/jUJMUcGf+UCWUS z11mIqDZdAU=*Openpgp*: preference=signencrypt*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.9.0

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**

- Previous by Date: Re: [isabelle] Sledgehammer: veriT in Isabelle 2019
- Next by Date: [isabelle] PhD / Postdoc position at Open University of The Netherlands
- Previous by Thread: Re: [isabelle] Sledgehammer: veriT in Isabelle 2019
- Next by Thread: [isabelle] PhD / Postdoc position at Open University of The Netherlands
- Cl-isabelle-users October 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list