Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Fri, 28 Feb 92 11:31:49 GMT
From: John.Van-Tassel@uk.ac.cam.cl
Message-Id: <9202281131.AA00958@cormorant.cl.cam.ac.uk>
To: chou@edu.ucla.cs, info-hol@edu.uidaho.cs.ted
Subject: Re: Strange behavior of quotation parser & a question

Hi,

The confusion arrises due to the fact that $and is already
"defined" as a part of the HOL quotation parser in dealing with
let-expressions in the logic.  Since this is done as a parser and
pretty printer thing, it is quite possible to re-define it in the
way that you did.  The problem is that the HOL parser and typechecker
are thouroughly confused as a result!  This is unfortunate.  I enclose
a versionn of "tla" making use of an uppercase version of your
definition for "$and".  Everything now works just fine.

Hope this helps,

JVT

   #new_theory `tla`;;
   () : void

   #new_definition(`map_binary_DEF`, "
     map_binary (op : *2 -> *1 -> *0) (A2 : * -> *2) (A1 : * -> *1)
     = \ x : * . op (A2 x) (A1 x)
   ") ;;
   new_infix_definition(    `AND_DEF`, "
     $AND   : (* -> bool) -> (* -> bool) -> (* -> bool) = map_binary $/\
   ") ;;
   new_infix_definition(     `or_DEF`, "
     $or    : (* -> bool) -> (* -> bool) -> (* -> bool) = map_binary $\/
   ") ;;
   ###|- !op A2 A1. map_binary op A2 A1 = (\x. op(A2 x)(A1 x))

   ###|- $AND = map_binary $/\

   ###|- $or = map_binary $\/

   #"((A:*->bool) AND B or C)";;
   "A AND (B or C)" : term

   #"((A:*->bool) AND B or X AND Y";;
   bad paren balance
   skipping: Y " ;; parse failed

   #"((A:*->bool) AND B or X AND Y)";;
   "A AND (B or (X AND Y))" : term

   #"((A:*->bool)AND B or C)" ;;
   "A AND (B or C)" : term

------------------------------------------------------------------------------
John Van Tassel                 |  Tel: +44-223-334729
Univ. of Cambridge              |  Fax: +44-223-334678
Computer Laboratory             |
Pembroke Street                 |  Email: jvt@cl.cam.ac.uk
Cambridge CB2 3QG               |
England                         |