src/HOLCF/tr2.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/tr2.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 Tr2 = Tr1 +
    10 
    11 consts
    12 	"@cifte"	:: "tr=>'c=>'c=>'c"
    13                              ("(3If _/ (then _/ else _) fi)" [60,60,60] 60)
    14 	"Icifte"        :: "tr->'c->'c->'c"
    15 
    16 	"@andalso"	:: "tr => tr => tr" ("_ andalso _" [61,60] 60)
    17 	"cop @andalso"	:: "tr -> tr -> tr" ("trand")
    18 	"@orelse"	:: "tr => tr => tr" ("_ orelse _"  [61,60] 60)
    19 	"cop @orelse"	:: "tr -> tr -> tr" ("tror")
    20 
    21 
    22 rules
    23 
    24   ifte_def    "Icifte == (LAM t e1 e2.tr_when[e1][e2][t])"
    25   andalso_def "trand == (LAM t1 t2.tr_when[t2][FF][t1])"
    26   orelse_def  "tror  == (LAM t1 t2.tr_when[TT][t2][t1])"
    27 
    28 
    29 end
    30 
    31 ML
    32 
    33 (* ----------------------------------------------------------------------*)
    34 (* translations for the above mixfixes                                   *)
    35 (* ----------------------------------------------------------------------*)
    36 
    37 fun ciftetr ts =
    38 	let val Cfapp = Const("fapp",dummyT) in	
    39 	Cfapp $ 
    40 	   	(Cfapp $
    41 			(Cfapp$Const("Icifte",dummyT)$(nth_elem (0,ts)))$
    42 		(nth_elem (1,ts)))$
    43 	(nth_elem (2,ts))
    44 	end;
    45 
    46 
    47 val parse_translation = [("@andalso",mk_cinfixtr "@andalso"),
    48 			("@orelse",mk_cinfixtr "@orelse"),
    49 			("@cifte",ciftetr)];
    50 
    51 val print_translation = [];
    52 
    53 
    54 
    55 
    56