*To*: Bill Richter <richter at math.northwestern.edu>*Subject*: Re: [isabelle] locales, including documentation & possible programming bugs*From*: Brian Huffman <huffman at in.tum.de>*Date*: Sun, 6 May 2012 07:32:04 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <201205052301.q45N1LWj018526@poisson.math.northwestern.edu>*References*: <201204282058.q3SKw9NF008441@poisson.math.northwestern.edu> <CAFP4q14YwNi6RksUOkGNGWYYzkNi3ca92FH4kYW19kJeOBcT2Q@mail.gmail.com> <alpine.LNX.2.00.1204301125350.6594@macbroy21.informatik.tu-muenchen.de> <201205020207.q4227VoC013147@poisson.math.northwestern.edu> <4FA0A63C.7030904@jaist.ac.jp> <201205020409.q42497Ou014411@poisson.math.northwestern.edu> <4FA0BBE7.4060302@jaist.ac.jp> <201205040401.q4441PxX003215@poisson.math.northwestern.edu> <CAAMXsiaNt7gi9NPRAEAVvO4r8Mmor28YJprMrpkBBzUt9TUL=w@mail.gmail.com> <201205052301.q45N1LWj018526@poisson.math.northwestern.edu>

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

**Follow-Ups**:**Re: [isabelle] locales, including documentation & possible programming bugs***From:*Bill Richter

**References**:**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Bill Richter

**Re: [isabelle] rigorous axiomatic geometry proof in Isabelle***From:*Christian Sternagel

**[isabelle] locales, including documentation & possible programming bugs***From:*Bill Richter

**Re: [isabelle] locales, including documentation & possible programming bugs***From:*Brian Huffman

**Re: [isabelle] locales, including documentation & possible programming bugs***From:*Bill Richter

- Previous by Date: Re: [isabelle] locales, including documentation & possible programming bugs
- Next by Date: Re: [isabelle] locales, including documentation & possible programming bugs
- Previous by Thread: Re: [isabelle] locales, including documentation & possible programming bugs
- Next by Thread: Re: [isabelle] locales, including documentation & possible programming bugs
- Cl-isabelle-users May 2012 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