|
2640
|
1 |
(* Title: HOLCF/Tr.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Franz Regensburger
|
|
12030
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
|
2640
|
5 |
|
|
|
6 |
Introduce infix if_then_else_fi and boolean connectives andalso, orelse
|
|
|
7 |
*)
|
|
|
8 |
|
|
3327
|
9 |
Tr = Lift + Fix +
|
|
2640
|
10 |
|
|
2782
|
11 |
types
|
|
|
12 |
tr = "bool lift"
|
|
|
13 |
|
|
2766
|
14 |
translations
|
|
2782
|
15 |
"tr" <= (type) "bool lift"
|
|
2640
|
16 |
|
|
|
17 |
consts
|
|
|
18 |
TT,FF :: "tr"
|
|
|
19 |
Icifte :: "tr -> 'c -> 'c -> 'c"
|
|
|
20 |
trand :: "tr -> tr -> tr"
|
|
|
21 |
tror :: "tr -> tr -> tr"
|
|
|
22 |
neg :: "tr -> tr"
|
|
3036
|
23 |
If2 :: "tr=>'c=>'c=>'c"
|
|
2640
|
24 |
|
|
|
25 |
syntax "@cifte" :: "tr=>'c=>'c=>'c" ("(3If _/ (then _/ else _) fi)" 60)
|
|
|
26 |
"@andalso" :: "tr => tr => tr" ("_ andalso _" [36,35] 35)
|
|
|
27 |
"@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30)
|
|
|
28 |
|
|
|
29 |
translations
|
|
10834
|
30 |
"x andalso y" == "trand$x$y"
|
|
|
31 |
"x orelse y" == "tror$x$y"
|
|
|
32 |
"If b then e1 else e2 fi" == "Icifte$b$e1$e2"
|
|
2640
|
33 |
defs
|
|
|
34 |
TT_def "TT==Def True"
|
|
|
35 |
FF_def "FF==Def False"
|
|
2719
|
36 |
neg_def "neg == flift2 Not"
|
|
10834
|
37 |
ifte_def "Icifte == (LAM b t e. flift1(%b. if b then t else e)$b)"
|
|
3842
|
38 |
andalso_def "trand == (LAM x y. If x then y else FF fi)"
|
|
|
39 |
orelse_def "tror == (LAM x y. If x then TT else y fi)"
|
|
3036
|
40 |
If2_def "If2 Q x y == If Q then x else y fi"
|
|
2640
|
41 |
|
|
|
42 |
end
|
|
|
43 |
|