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