src/HOLCF/Tr.thy
changeset 2640 ee4dfce170a0
child 2647 83c9bdff7fdc
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Tr.thy	Mon Feb 17 10:57:11 1997 +0100
@@ -0,0 +1,54 @@
+(*  Title:      HOLCF/Tr.thy
+    ID:         $Id$
+    Author:     Franz Regensburger
+    Copyright   1993 Technische Universitaet Muenchen
+
+Introduce infix if_then_else_fi and boolean connectives andalso, orelse
+*)
+
+Tr = Lift +
+
+types tr = "bool lift"
+
+consts
+	TT,FF           :: "tr"
+        Icifte          :: "tr -> 'c -> 'c -> 'c"
+        trand           :: "tr -> tr -> tr"
+        tror            :: "tr -> tr -> tr"
+        neg             :: "tr -> tr"
+        plift           :: "('a => bool) => 'a lift -> tr"
+
+syntax  "@cifte"        :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)
+        "@andalso"      :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
+        "@orelse"       :: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
+ 
+translations 
+	     "tr" ==(type) "bool lift" 
+	     "x andalso y" == "trand`x`y"
+             "x orelse y"  == "tror`x`y"
+             "If b then e1 else e2 fi" == "Icifte`b`e1`e2"
+defs
+  TT_def      "TT==Def True"
+  FF_def      "FF==Def False"
+  neg_def     "neg == flift2 not"
+  ifte_def    "Icifte == (LAM b t e.flift1(%b.if b then t else e)`b)"
+  andalso_def "trand == (LAM x y.If x then y else FF fi)"
+  orelse_def  "tror == (LAM x y.If x then TT else y fi)"
+(* andalso, orelse are different from strict functions 
+  andalso_def "trand == flift1(flift2 o (op &))"
+  orelse_def  "tror == flift1(flift2 o (op |))"
+*)
+  plift_def   "plift p == (LAM x. flift1(%a.Def(p a))`x)"
+
+(* start 8bit 1 *)
+syntax
+  "GeqTT"        :: "tr => bool"               ("(\\<lceil>_\\<rceil>)")
+  "GeqFF"        :: "tr => bool"               ("(\\<lfloor>_\\<rfloor>)")
+
+translations
+  "\\<lceil>x\\<rceil>" == "x = TT"
+  "\\<lfloor>x\\<rfloor>" == "x = FF"
+(* end 8bit 1 *)
+
+end
+