author | huffman |
Wed, 02 Mar 2005 22:57:08 +0100 | |
changeset 15563 | 9e125b675253 |
parent 14981 | e73f8140af78 |
child 15568 | 41bfe19eabe2 |
permissions | -rw-r--r-- |
1479 | 1 |
(* Title: HOLCF/ssum3.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 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
5 |
Class instance of ++ for class pcpo |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
6 |
*) |
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 |
Ssum3 = Ssum2 + |
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
9 |
|
2640 | 10 |
instance "++" :: (pcpo,pcpo)pcpo (least_ssum,cpo_ssum) |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
11 |
|
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
12 |
consts |
1479 | 13 |
sinl :: "'a -> ('a++'b)" |
14 |
sinr :: "'b -> ('a++'b)" |
|
5439 | 15 |
sscase :: "('a->'c)->('b->'c)->('a ++ 'b)-> 'c" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
16 |
|
1168
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
442
diff
changeset
|
17 |
defs |
74be52691d62
The curried version of HOLCF is now just called HOLCF. The old
regensbu
parents:
442
diff
changeset
|
18 |
|
3842 | 19 |
sinl_def "sinl == (LAM x. Isinl(x))" |
20 |
sinr_def "sinr == (LAM x. Isinr(x))" |
|
5439 | 21 |
sscase_def "sscase == (LAM f g s. Iwhen(f)(g)(s))" |
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
22 |
|
1274 | 23 |
translations |
10834 | 24 |
"case s of sinl$x => t1 | sinr$y => t2" == "sscase$(LAM x. t1)$(LAM y. t2)$s" |
1274 | 25 |
|
243
c22b85994e17
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
nipkow
parents:
diff
changeset
|
26 |
end |