*To*: Dominique Unruh <unruh at ut.ee>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Handling of invalid type variable names on ML level*From*: Makarius <makarius at sketis.net>*Date*: Fri, 25 May 2018 19:44:13 +0200*Authentication-results*: mx2f26; spf=pass (sender IP is 62.216.204.104) smtp.mailfrom=makarius at sketis.net smtp.helo=[192.168.178.30]*Autocrypt*: addr=makarius at sketis.net; prefer-encrypt=mutual; keydata= xsFNBFcrF+4BEADMcXMnu3XHg6bRsGe3tajAHqvm89+ecn/Y0WhjI2FplhkZs1LwM+ZA9eXh hiBrC/yX0FJ+qjzVIfm66CX4nzVG1f8qwaervMpvpA+gbhtQiXc0t+LDcqV+5cdtpKplPHSu oW+KzJKyCdkDB5fYMOzuaXQwYi12YAEQH2r6K7Q7Np+k82Xli1pWe+Tha/BH0pKJ5Q01aPep ASrNW9F+moX7C0fxWl65LiXGmF0UJep6fqKruhy8oNF4p6I2oZhktvaR/x6tkL2PkT3r+xUS 6g5i3BOjfwhoGY57nsioeK+8VFvdRH5DK4CbrTgDl7ddcrEeENrfpDiPLs/afVbe/T9oDXmJ OJAO4WMpfZNiFhx9SSVTHohw29Fyzn0N1UQGjPqAY1jg32DAxlnMQ0co/KabEFAcoQsW1/6U ZGiNxYVIyEKGrnSY4WuLuNC8CmU1RaYSdTk1y9tYdxufM9lH9ynzJwac6FdalOOxMR2G9JG8 L9/dk3ytlP6DVwkPBSCpJaTkTyMp1wSkF1oK/BDu5xKUQh0zvvLCuZ16hiKRBBSjpVExXRZC u+NC1Y4wqm1HOH7HBwgZ1Hv9S/EPmI9iwgcW0SpDJqPf2Cm7oFMZsZ5Dbs6/nOQoe4Zegy45 ymqDRlIekP7zj+vOoR80XAYfmAH5DElJHldcjmgLBMdpvvqGZwARAQABzR5NYWthcml1cyA8 bWFrYXJpdXNAc2tldGlzLm5ldD7CwX0EEwEIACcFAlcrF+4CGyMFCQlmAYAFCwkIBwIGFQgJ CgsCBBYCAwECHgECF4AACgkQ89KUEoG/TbiVrw/9FjEBgh2CB7Qof7Y4k0yc7j+x/A0Wmkc0 iwP5jaKJuxRv1JJT8CFqm392+/cdh3EkRUk/UWD+hpNndYJwxZltrEpKVqFAWoVOg3ZJ4cuI MYhlp4tk/T0KSl/gKT16dc6uJ7M/FzW0zv50vjFtAdianEDuqLXHKaGDUwWoOTDly0gdZ7aH /eNby6ONHUSJMdTNOErh2N+uESM4aZqUuuL/dTb6xiVzCpV5saT8EMakoazUd7QhoBaHvqfs BL7DEmvcTtA79GF3ufHrF/UndIcx8aMznZ2PGNjmy5seDCoKX0EYHdLam8vgo/TuU4dRw5Zn 6E/ouyNOliXT1Mn+SomeBSXTR5MXRq4TQ9MKVGiP0Yl+7GJQU0JFtDC1ZZEOyjIiwGWOhbUR pYujVm8C1iQ7NcEn2BqOAmRML6IR6+En4RLbgCNsBNXlmTPRJOaI+iV6DZzg3x9zcaDGhoYt jkBTEFpb0F3jU9yuaEU5401NV34fUxg8tqXs0R9CKinO7kQ8N+RDjyyY8k2KZiDYBJ6r+OK0 d7TaTj7F9tmpAu2pmQ8lxOKjDZIwlbGTsC4lxISmcPzBGTKXja5nakcWYx/lZ4vje0WZ12HN amnD1weakFixRYit0d+Kz7cuj684NSbhwC0oN2t9R06Nfq8UPEWRKEitCly0OtRgio8zVZ/L eADOwU0EVysX7gEQAKs5NVOvYkE/r8KLsJ8/L/9eulpJDOFilZ9fyuqii7t1UpHZLb58QghW JM+IB2GSGsB+pOi6Je7hmwxcVdXYbGlYZ4Btqqw48/XptfbNZ8alCk6AqoVFP4MbYxij/Qqv f/Yw6GR0p1RIC/W4GF/JgDDwDFEiMT6Pv6dpM8acdNFCERDZdoOJiC+XJRwy5lZ2g5FOJkT9 rVI9EnA7mBXLLjPOMUp2/eZxN6gKOZzI3ej9vixg3adWR2yfKPgacHP/ujnVfITOl0OyLE5f zIHq85dEV4zW6Mpx7+Um0tdkwlUVMaW2nQ1bcwejgVAuD/MLSF/lSs3N5D1ctw5QUemYh7/e 2dC12UJuFDFxNPzcltQTlkBCVWV1D0SjScDHdlF6HhzpZOlt52/rwTn5GHtY4nwAL4IJ+Yvl WX8YKmyILH4Ai8c/N2IVRERQ2qorWFlsQnqrXV+hXf8aUwjc/pq4K9rsWxvle3TpeZfoBefU /s1PEX0SepZFAqAXHlQ9DZPsdPDo9EFK695G5w4nf03EhE9TV1MKGUuc1XJ6f1ZLaxu0TwTA 6qYtKIyBcU0Yn61S2Kh7Dgb5LdLV8nfl71+n/xIt2IWH5UJ9YuwEgGEP0c6ImnAUZ+nRodFI 0RwtCWlRkSJWtQln1vcphrz8PjWZH6e/nWnceXR/Al5P0WexQgtvABEBAAHCwWUEGAEIAA8F AlcrF+4CGwwFCQlmAYAACgkQ89KUEoG/Tbh7VQ/9Fc4bdwJYc3jH/LiuXv6uMg50Cv6lg2NT bL9DClWGNiYzejfM2A4c5K+GRUXhyD7S9U203MOv3z7uTbtyQL8XVolNnQlRIkB00f8nJ2sw HMXx/hemjXBvtlneq+vrMORJexldXUMFq19ZZrvj0zZL+pUnGFqt+IWTEE5GpL7wu20Demaj jYyGyKcDZyJOWZcl4e45Yn3hl0EI2xVmVh7ZinVsb3+nqgcltFy4Jt+drezwV2EiLGJHfGsT jEQb3C9VpneU4Jo+hHtfqLK4Q8+WlIOzSfyvwbabxrhyqg7i11fu8yckNW3dCURPYigV07HK 4dN0zhj53M0Q3eTwegJRPJb8XoLDcSdbsaU2HIShlGDKmzS9KL4JzLikQ9dXROC4cae3jRKH aexFi4B55Ab6FxIfXj09wUCO6Nm0owDfIBDMgiywvi2Rb2etCjBgRbSj71S2nntd9ZitoYvE yKirLkWmJRbp3ln8cHi8Uc/jr1cDPVRWuLUN0uceMj5+AR+NZVakcNUHWJCinMMjacho0SyP QmocdU8pzzupreaVWruqaSzqcpWBPwrE5OxEtJ+OyIBjKmRJ5eptjh4rKgNaVnKjhqbvr+Yz pUAgPp38jjf4HJghUGIfWArKNelKJEJOYk94DAbmT67LgqEdZ0yaA2BCHmreN727WIzV9vkX NMc=*In-reply-to*: <CAPFfTE5idxiWyHs_gB2+c+7q=1-EHodFN0P-ZEB0jCS6cH0hxQ@mail.gmail.com>*Openpgp*: preference=signencrypt*References*: <CAPFfTE5idxiWyHs_gB2+c+7q=1-EHodFN0P-ZEB0jCS6cH0hxQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.8.0

On 25/05/18 16:51, Dominique Unruh wrote: > > I am not sure the following situation should be considered a bug or not, > since it occurs only when using Isabelle incorrectly. But I feel that it > probably indicates that invalid input is not detected in time, and it may > lead to very hard to understand problems (starting from a typo). So I just > explain the problem and leave it to the Isabelle-experts to decide whether > it indicates a real problem or not. This preface already points in the direction of a "general user error", or rather a mismatch of expectations vs. the reality of how the system works. > The problem is exhibited by the theory below. But in a nutshell, we have > the following situation: > > - It is possible to prove a theorem with a type variable called *a* (not > *'a*). I understand that I should not do that, of course. But there is > no error when proving the theorem. > - Then, if we try to use OF with that theorem, we get unexpected > failures. But only if *a* is the name of a fixed variable (not type > variable). > > I guess that type variable *a* should probably just be rejected when trying > to prove the theorem. But even if not, it is surprising that the existence > of a fixed variable *a* makes a difference since I would have assumed that > free variables and free type variables have completely independent name > spaces. There are many different notions of names, variables, contexts etc. and a lot of system infrastructure to help getting Isabelle/ML tool implementations right. The "implementation" manual explains some of this -- beyond that it is important to find good examples and study them carefully. In general, the programming interfaces are much less typed than one might expect. As a start you should think of Isabelle/ML is a variant of LISP with a few static types to avoid utter nonsense. It is important to observe certain disciplines and high-level ideas -- the system often does not check or cannot check for that. For type and term variables, it is usually already an error if literal names appear in the ML text. There are operations to invent fresh variables relative to a certain context -- and using them is mandatory to make things work in arbitrary contexts. So it is unlikely to make a typo of "a" vs. "'a" in ML, because both are already wrong as literal variable names in the source. > val ctx = @{context} First note that there are hard and fast naming conventions for certain basic Isabelle/ML types (see chapter 0 in the "implementation" manual), in particular the value above needs to be called "ctxt". Otherwise there is no chance to understand the source in more complex situations, when there is a serious problem with contexts (the present example is not serious yet). The Highlighter of Isabelle/jEdit can be helpful here, when sources are written in a standard form. > fun tac {context=ctx, ...} = ALLGOALS (simp_tac ctx) At this spot you are binding the same name "ctx" again: this shadowing makes it difficult to understand and change the sources later. Anyway, the forward definition of "tac" is better inlined into the Goal.prove invocation, it makes the source more readable and robust. Here is that snippet in standard form, optimized for readability: ML ‹ val ctxt = @{context} val T = TFree ("a", @{sort type}) val l = Free ("l", T) val thm = Goal.prove ctxt ["l"] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (l, l))) (fn {context = ctxt', ...} => ALLGOALS (simp_tac ctxt')) › Now the development of the local ctxt into ctxt' becomes clear: the latter is the "eigen-context" of the goal statement. After inspecting contexts, I routinely look at variables and terms vs. these contexts. Above Goal.prove is applied to some proposition that is not declared in the context (e.g. with Variable.declare_term). Omitting that in real applications can lead to really confusing situations with the implicit Hindley-Milner polymorphism and other corner cases. See also section "6.1 Variables" in the "implementation" manual, including its minimal examples. With that you might produce fresh type/term variables robustly, such that the whole question from the start disappears. Makarius

**Follow-Ups**:**Re: [isabelle] Handling of invalid type variable names on ML level***From:*Dominique Unruh

**References**:**[isabelle] Handling of invalid type variable names on ML level***From:*Dominique Unruh

- Previous by Date: Re: [isabelle] Methods with informative failure messages
- Next by Date: Re: [isabelle] Methods with informative failure messages
- Previous by Thread: [isabelle] Handling of invalid type variable names on ML level
- Next by Thread: Re: [isabelle] Handling of invalid type variable names on ML level
- Cl-isabelle-users May 2018 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