equal
deleted
inserted
replaced
1 (* Title: HOLCF/ssum1.thy |
1 (* Title: HOLCF/Ssum1.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
4 Copyright 1993 Technische Universitaet Muenchen |
4 Copyright 1993 Technische Universitaet Muenchen |
5 |
5 |
6 Partial ordering for the strict sum ++ |
6 Partial ordering for the strict sum ++ |
7 *) |
7 *) |
8 |
8 |
9 Ssum1 = Ssum0 + |
9 Ssum1 = Ssum0 + |
10 |
10 |
11 consts |
11 defs |
12 |
12 less_ssum_def "less == (%s1 s2.@z. |
13 less_ssum :: "[('a ++ 'b),('a ++ 'b)] => bool" |
13 (! u x.s1=Isinl u & s2=Isinl x --> z = u << x) |
14 |
14 &(! v y.s1=Isinr v & s2=Isinr y --> z = v << y) |
15 rules |
15 &(! u y.s1=Isinl u & s2=Isinr y --> z = (u = UU)) |
16 |
16 &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))" |
17 less_ssum_def "less_ssum s1 s2 == (@z. |
|
18 (! u x.s1=Isinl(u) & s2=Isinl(x) --> z = (u << x)) |
|
19 &(! v y.s1=Isinr(v) & s2=Isinr(y) --> z = (v << y)) |
|
20 &(! u y.s1=Isinl(u) & s2=Isinr(y) --> z = (u = UU)) |
|
21 &(! v x.s1=Isinr(v) & s2=Isinl(x) --> z = (v = UU)))" |
|
22 |
17 |
23 end |
18 end |
24 |
19 |
25 |
20 |