*To*: Steve W <s.wong.731 at gmail.com>*Subject*: Re: [isabelle] --> vs. ==>*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Fri, 6 Aug 2010 10:37:34 -0500*Cc*: Lawrence Paulson <lp15 at cam.ac.uk>, isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <B62BC77D-ADD3-4542-B921-DF9537D0FE3C@cam.ac.uk>*References*: <AANLkTinsLRQUesQspHmDGAuwYcRfp2aM96X-pdxg6Mse@mail.gmail.com> <B62BC77D-ADD3-4542-B921-DF9537D0FE3C@cam.ac.uk>*Sender*: huffman.brian.c at gmail.com

Hi Steve, You may notice that the two implication operators actually have different types: "==>" has type "prop => prop => prop", where "prop" is the type of propositions in Isabelle's logical framework. On the other hand, "-->" has type "bool => bool => bool", with "bool" being the type of HOL formulae. The types "bool" and "prop" are related by a special constant "Trueprop :: bool => prop", which you can think of as the "is-a-true-HOL-formula" predicate in the logical framework. Occurrences of "Trueprop" are automatically inserted by Isabelle's parser just where they are needed, and hidden by the pretty-printer; however you are free to write them explicitly if you want to. Here's the precise sense in which --> and ==> are equivalent: For any P, Q :: bool, "Trueprop (P --> Q)" and "Trueprop P ==> Trueprop Q" are logically equivalent as propositions. This means that replacing "-->" with "==>" should preserve the meaning of your theorems. But as Larry points out, within HOL formulae only "-->" can be used; only the outermost "-->" (next to an invisible "Trueprop") can be replaced with "==>". - Brian On Fri, Aug 6, 2010 at 2:47 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > The connective ==> is part of the logical framework, and is not part of higher-order logic at all. Therefore, the expression A ==> B is not a higher-order logic formula and cannot be written where a formula is expected, such as a set comprehension. > > Larry Paulson > > > On 6 Aug 2010, at 05:23, Steve W wrote: > >> >> I see that both --> and ==> mean implication, whereas the first is the >> logical connective and the second is for inference rules. However, can a HOL >> formula containing --> be proved as one with ==> instead? It seems it >> doesn't make much difference as impI replaces --> by ==>. My feeling is that >> it's not safe to replace --> with ==>, but what really are the issues? >> > > >

**References**:**[isabelle] --> vs. ==>***From:*Steve W

**Re: [isabelle] --> vs. ==>***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Schematic goal
- Next by Date: [isabelle] CFPart : iFM 2010
- Previous by Thread: Re: [isabelle] --> vs. ==>
- Next by Thread: [isabelle] CFPart : iFM 2010
- Cl-isabelle-users August 2010 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