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 


11 
types tr = "bool lift"


12 


13 
consts


14 
TT,FF :: "tr"


15 
Icifte :: "tr > 'c > 'c > 'c"


16 
trand :: "tr > tr > tr"


17 
tror :: "tr > tr > tr"


18 
neg :: "tr > tr"


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


20 


21 
syntax "@cifte" :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)


22 
"@andalso" :: "tr => tr => tr" ("_ andalso _" [36,35] 35)


23 
"@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30)


24 


25 
translations


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


27 
"x andalso y" == "trand`x`y"


28 
"x orelse y" == "tror`x`y"


29 
"If b then e1 else e2 fi" == "Icifte`b`e1`e2"


30 
defs


31 
TT_def "TT==Def True"


32 
FF_def "FF==Def False"


33 
neg_def "neg == flift2 not"


34 
ifte_def "Icifte == (LAM b t e.flift1(%b.if b then t else e)`b)"


35 
andalso_def "trand == (LAM x y.If x then y else FF fi)"


36 
orelse_def "tror == (LAM x y.If x then TT else y fi)"


37 
(* andalso, orelse are different from strict functions


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


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


40 
*)


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


42 


43 
(* start 8bit 1 *)


44 
syntax


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


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


47 


48 
translations


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


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


51 
(* end 8bit 1 *)


52 


53 
end


54 
