src/HOLCF/Tr.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 3842 b55686a7b22c
child 10834 a7897aebbffc
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/Tr.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Introduce infix if_then_else_fi and boolean connectives andalso, orelse
     7 *)
     8 
     9 Tr = Lift + Fix +
    10 
    11 types
    12   tr = "bool lift"
    13 
    14 translations
    15   "tr" <= (type) "bool lift" 
    16 
    17 consts
    18 	TT,FF           :: "tr"
    19         Icifte          :: "tr -> 'c -> 'c -> 'c"
    20         trand           :: "tr -> tr -> tr"
    21         tror            :: "tr -> tr -> tr"
    22         neg             :: "tr -> tr"
    23         If2             :: "tr=>'c=>'c=>'c"
    24 
    25 syntax  "@cifte"        :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)
    26         "@andalso"      :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
    27         "@orelse"       :: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
    28  
    29 translations 
    30 	     "x andalso y" == "trand`x`y"
    31              "x orelse y"  == "tror`x`y"
    32              "If b then e1 else e2 fi" == "Icifte`b`e1`e2"
    33 defs
    34   TT_def      "TT==Def True"
    35   FF_def      "FF==Def False"
    36   neg_def     "neg == flift2 Not"
    37   ifte_def    "Icifte == (LAM b t e. flift1(%b. if b then t else e)`b)"
    38   andalso_def "trand == (LAM x y. If x then y else FF fi)"
    39   orelse_def  "tror == (LAM x y. If x then TT else y fi)"
    40   If2_def     "If2 Q x y == If Q then x else y fi"
    41 
    42 end
    43