*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Locale parameters*From*: "Tim (McKenzie) Makarios" <tjm1983 at gmail.com>*Date*: Tue, 27 Sep 2011 09:19:20 +1300*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAP0k5J6BfJ02BH-tBZ17cEq__A-xvJDF+L_ohHNLkJaGoYnSpA@mail.gmail.com>*References*: <CAP0k5J6BfJ02BH-tBZ17cEq__A-xvJDF+L_ohHNLkJaGoYnSpA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.21) Gecko/20110831 Thunderbird/3.1.13

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On 27/09/11 05:57, John Munroe wrote: > Hi, > > Suppose I have two locales L1 and L2: > > locale L1 = > fixes c :: nat > assumes ax: "c = 0" > > locale L2 = > fixes c :: nat > assumes ax: "c = 1" > > and I want to prove a lemma stating that the constant 'c' in L1 does > not have the same value as the constant 'c' in L2: > > lemma lem1: "ALL a b. L1 c --> c = a & L2 c --> c = b & a ~= b" > using L1.ax L2.ax > by auto > > (hopefully the formulation matches my intended meaning.) By turning on "Show Brackets", you can see that lem1 means "ALL a b. L1 c --> ((c = a & L2 c) --> (c = b & a ~= b))" (after you've removed other superfluous brackets). I don't think this is what you meant. Perhaps you want something like this: lemma lem3: assumes "L1 c" shows "~ L2 c" using assms and L1.ax and L2.ax by auto or: lemma lem4: assumes "L1 c" and "L2 d" shows "c ? d" using assms and L1.ax and L2.ax by auto > Now, if I change the parametrisation slightly: > > lemma lem2: "ALL a b. L1 c --> c = a & L2 d --> d = b & a ~= b" > using L1.ax L2.ax > by auto > > The proof fails. Aren't the occurrences of 'c' in lem1 distinct > instances? No, I don't think so. They're not quantified separately; what would make them distinct? > Which lemma actually matches my intended meaning, if any? > > Any help will be appreciated. Thanks. > > John Tim <>< -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.10 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAk6A3kIACgkQ/cBxZIxl6rmuUQCgt2h/AVlrDZ3jAC3FJb5w+ve6 8DUAn2dfzBPNVW6uy9oOkppPApI3HcOW =k9B2 -----END PGP SIGNATURE-----

**References**:**[isabelle] Locale parameters***From:*John Munroe

- Previous by Date: [isabelle] Instantiate schematic variable in apply-script
- Next by Date: Re: [isabelle] Locale parameters
- Previous by Thread: [isabelle] Locale parameters
- Next by Thread: Re: [isabelle] Locale parameters
- Cl-isabelle-users September 2011 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