src/HOLCF/Tr.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12030 46d57d0290a2
child 15649 f8345ee4f607
permissions -rw-r--r--
Merged in license change from Isabelle2004
     1 (*  Title:      HOLCF/Tr.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4 
     5 Introduce infix if_then_else_fi and boolean connectives andalso, orelse
     6 *)
     7 
     8 Tr = Lift + Fix +
     9 
    10 types
    11   tr = "bool lift"
    12 
    13 translations
    14   "tr" <= (type) "bool lift" 
    15 
    16 consts
    17 	TT,FF           :: "tr"
    18         Icifte          :: "tr -> 'c -> 'c -> 'c"
    19         trand           :: "tr -> tr -> tr"
    20         tror            :: "tr -> tr -> tr"
    21         neg             :: "tr -> tr"
    22         If2             :: "tr=>'c=>'c=>'c"
    23 
    24 syntax  "@cifte"        :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)
    25         "@andalso"      :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
    26         "@orelse"       :: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
    27  
    28 translations 
    29 	     "x andalso y" == "trand$x$y"
    30              "x orelse y"  == "tror$x$y"
    31              "If b then e1 else e2 fi" == "Icifte$b$e1$e2"
    32 defs
    33   TT_def      "TT==Def True"
    34   FF_def      "FF==Def False"
    35   neg_def     "neg == flift2 Not"
    36   ifte_def    "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
    37   andalso_def "trand == (LAM x y. If x then y else FF fi)"
    38   orelse_def  "tror == (LAM x y. If x then TT else y fi)"
    39   If2_def     "If2 Q x y == If Q then x else y fi"
    40 
    41 end
    42