Re: [isabelle] locales, including documentation & possible programming bugs



On Sun, May 6, 2012 at 1:01 AM, Bill Richter
<richter at math.northwestern.edu> wrote:
> Brian, I read ref.pdf p 30--32 on misfixes, but I could not figure out
> how to write (in my code below)
> C a b c d as a b \<equiv> c d.
> I seem to have a priority problem.  I'm using the priority stuff
> ps = [99,99,99,99] and p = 70, and I've tried lots of others.
>
> My "\<forall> a b . a b \<equiv> b a" gets me the error, a
> do-not-enter on locale, and when I click on locale, I see in the
> output window
> Ambiguous input.  2 types are correct:
> (\<forall> (a b) . (a b \<equiv> b a))
> ((\<forall> (a b) . (a b)) \<equiv> (b a))

Your syntax is ambiguous because \<equiv> is also used to write
meta-equality (i.e. definitional equality) in Isabelle. "a b \<equiv>
c d" looks like an equality between two function applications.

You will have a much easier time avoiding ambiguous parse
warnings/errors if you simply use a different symbol, such as \<cong>.

fixes C :: "'a => 'a => 'a => 'a => bool" ("_ _ \<cong> _ _" [99,99,99,99] 70)

The other potential source of ambiguous parsing here is when one of
the arguments to C is a function application:

term "(f x) b \<cong> c d"

This parses fine, but it prints out as "f x b \<cong> c d". If you try
to parse it again without the parentheses, you get an ambiguity.

To fix this, I would bump up the argument precedences to the maximum
(1000), which is higher than function application. This makes it so
every argument to C must be either a variable or a parenthesized
expression (which will also be the case for the pretty-printer's
output).

fixes C :: "'a => 'a => 'a => 'a => bool" ("_ _ \<cong> _ _"
[1000,1000,1000,1000] 70)


> II tried to write a simple proof following p 40--42 of isar-ref.pdf,
> but it didn't work. I get do-not-enter signs on every line of the
> proof.  The following commented proof is no better.
[...]
>  assumes A1: "a b \<equiv> b a"
>   and A2: "a b \<equiv> p q \<and> a b \<equiv> r s --> p q \<equiv> r s"

Rules stated in terms of object logic connectives, like "P \<and> Q
--> R", aren't very useful with the "rule" method. You had better
state rules using "==>", like
"P ==> Q ==> R" instead.

Hope this helps,

- Brian





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