2640

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 +


10 

2766

11 
syntax


12 
tr :: "type"


13 
translations


14 
"tr" == (type) "bool lift"

2640

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"

2647

22 
plift :: "('a::term => bool) => 'a lift > tr"

2640

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"

2719

35 
neg_def "neg == flift2 Not"

2640

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 
(* andalso, orelse are different from strict functions


40 
andalso_def "trand == flift1(flift2 o (op &))"


41 
orelse_def "tror == flift1(flift2 o (op ))"


42 
*)


43 
plift_def "plift p == (LAM x. flift1(%a.Def(p a))`x)"


44 

2766

45 
(* FIXME remove?

2640

46 
syntax


47 
"GeqTT" :: "tr => bool" ("(\\<lceil>_\\<rceil>)")


48 
"GeqFF" :: "tr => bool" ("(\\<lfloor>_\\<rfloor>)")


49 


50 
translations


51 
"\\<lceil>x\\<rceil>" == "x = TT"


52 
"\\<lfloor>x\\<rfloor>" == "x = FF"

2766

53 
*)

2640

54 


55 
end


56 
