author | paulson |
Mon, 23 Sep 1996 17:41:57 +0200 | |
changeset 2002 | ed423882c6a9 |
parent 1479 | 21eb5e156d91 |
permissions | -rw-r--r-- |
1479 | 1 |
(* Title: HOLCF/tr2.thy |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
1479 | 3 |
Author: Franz Regensburger |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
4 |
Copyright 1993 Technische Universitaet Muenchen |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
Introduce infix if_then_else_fi and boolean connectives andalso, orelse |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
7 |
*) |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
8 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
9 |
Tr2 = Tr1 + |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
10 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
11 |
consts |
1479 | 12 |
Icifte :: "tr -> 'c -> 'c -> 'c" |
13 |
trand :: "tr -> tr -> tr" |
|
14 |
tror :: "tr -> tr -> tr" |
|
15 |
neg :: "tr -> tr" |
|
752
b89462f9d5f1
----------------------------------------------------------------------
regensbu
parents:
625
diff
changeset
|
16 |
|
1479 | 17 |
syntax "@cifte" :: "tr=>'c=>'c=>'c" |
430 | 18 |
("(3If _/ (then _/ else _) fi)" 60) |
1479 | 19 |
"@andalso" :: "tr => tr => tr" ("_ andalso _" [36,35] 35) |
20 |
"@orelse" :: "tr => tr => tr" ("_ orelse _" [31,30] 30) |
|
752
b89462f9d5f1
----------------------------------------------------------------------
regensbu
parents:
625
diff
changeset
|
21 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
22 |
translations "x andalso y" == "trand`x`y" |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
23 |
"x orelse y" == "tror`x`y" |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
24 |
"If b then e1 else e2 fi" == "Icifte`b`e1`e2" |
625 | 25 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
26 |
defs |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
27 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
28 |
ifte_def "Icifte == (LAM t e1 e2.tr_when`e1`e2`t)" |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
29 |
andalso_def "trand == (LAM t1 t2.tr_when`t2`FF`t1)" |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
30 |
orelse_def "tror == (LAM t1 t2.tr_when`TT`t2`t1)" |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
752
diff
changeset
|
31 |
neg_def "neg == (LAM t. tr_when`FF`TT`t)" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
32 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
33 |
end |