equal
deleted
inserted
replaced
3 *) |
3 *) |
4 theory QuotProd |
4 theory QuotProd |
5 imports QuotMain |
5 imports QuotMain |
6 begin |
6 begin |
7 |
7 |
8 section {* Quotient infrastructure for product type *} |
8 section {* Quotient infrastructure for the product type. *} |
9 |
9 |
10 fun |
10 fun |
11 prod_rel |
11 prod_rel |
12 where |
12 where |
13 "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)" |
13 "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)" |
42 |
42 |
43 lemma Pair_rsp[quot_respect]: |
43 lemma Pair_rsp[quot_respect]: |
44 assumes q1: "Quotient R1 Abs1 Rep1" |
44 assumes q1: "Quotient R1 Abs1 Rep1" |
45 assumes q2: "Quotient R2 Abs2 Rep2" |
45 assumes q2: "Quotient R2 Abs2 Rep2" |
46 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" |
46 shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" |
47 by simp |
47 by simp |
48 |
48 |
49 lemma Pair_prs[quot_preserve]: |
49 lemma Pair_prs[quot_preserve]: |
50 assumes q1: "Quotient R1 Abs1 Rep1" |
50 assumes q1: "Quotient R1 Abs1 Rep1" |
51 assumes q2: "Quotient R2 Abs2 Rep2" |
51 assumes q2: "Quotient R2 Abs2 Rep2" |
52 shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" |
52 shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" |