equal
deleted
inserted
replaced
39 |
39 |
40 defs |
40 defs |
41 Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))" |
41 Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))" |
42 Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))" |
42 Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))" |
43 sum_case_def "sum_case f g p == @z. (!x. p=Inl(x) --> z=f(x)) |
43 sum_case_def "sum_case f g p == @z. (!x. p=Inl(x) --> z=f(x)) |
44 & (!y. p=Inr(y) --> z=g(y))" |
44 & (!y. p=Inr(y) --> z=g(y))" |
45 |
45 |
46 sum_def "A plus B == (Inl``A) Un (Inr``B)" |
46 sum_def "A plus B == (Inl``A) Un (Inr``B)" |
47 |
47 |
48 (*for selecting out the components of a mutually recursive definition*) |
48 (*for selecting out the components of a mutually recursive definition*) |
49 Part_def "Part A h == A Int {x. ? z. x = h(z)}" |
49 Part_def "Part A h == A Int {x. ? z. x = h(z)}" |