Re: [isabelle] Locale parameters



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





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