equal
deleted
inserted
replaced
23 Isfst :: "('a ** 'b) => 'a" |
23 Isfst :: "('a ** 'b) => 'a" |
24 Issnd :: "('a ** 'b) => 'b" |
24 Issnd :: "('a ** 'b) => 'b" |
25 |
25 |
26 rules |
26 rules |
27 |
27 |
28 Spair_Rep_def "Spair_Rep == (%a b. %x y.\ |
28 Spair_Rep_def "Spair_Rep == (%a b. %x y. |
29 \ (~a=UU & ~b=UU --> x=a & y=b ))" |
29 (~a=UU & ~b=UU --> x=a & y=b ))" |
30 |
30 |
31 Sprod_def "Sprod == {f. ? a b. f = Spair_Rep(a,b)}" |
31 Sprod_def "Sprod == {f. ? a b. f = Spair_Rep(a,b)}" |
32 |
32 |
33 (*faking a type definition... *) |
33 (*faking a type definition... *) |
34 (* "**" is isomorphic to Sprod *) |
34 (* "**" is isomorphic to Sprod *) |
39 |
39 |
40 (*defining the abstract constants*) |
40 (*defining the abstract constants*) |
41 |
41 |
42 Ispair_def "Ispair(a,b) == Abs_Sprod(Spair_Rep(a,b))" |
42 Ispair_def "Ispair(a,b) == Abs_Sprod(Spair_Rep(a,b))" |
43 |
43 |
44 Isfst_def "Isfst(p) == @z.\ |
44 Isfst_def "Isfst(p) == @z. |
45 \ (p=Ispair(UU,UU) --> z=UU)\ |
45 (p=Ispair(UU,UU) --> z=UU) |
46 \ &(! a b. ~a=UU & ~b=UU & p=Ispair(a,b) --> z=a)" |
46 &(! a b. ~a=UU & ~b=UU & p=Ispair(a,b) --> z=a)" |
47 |
47 |
48 Issnd_def "Issnd(p) == @z.\ |
48 Issnd_def "Issnd(p) == @z. |
49 \ (p=Ispair(UU,UU) --> z=UU)\ |
49 (p=Ispair(UU,UU) --> z=UU) |
50 \ &(! a b. ~a=UU & ~b=UU & p=Ispair(a,b) --> z=b)" |
50 &(! a b. ~a=UU & ~b=UU & p=Ispair(a,b) --> z=b)" |
51 |
51 |
52 end |
52 end |
53 |
53 |