equal
deleted
inserted
replaced
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 *) |
3 *) |
4 theory QuotSum |
4 theory QuotSum |
5 imports QuotMain |
5 imports QuotMain |
6 begin |
6 begin |
|
7 |
|
8 section {* Quotient infrastructure for the sum type. *} |
7 |
9 |
8 fun |
10 fun |
9 sum_rel |
11 sum_rel |
10 where |
12 where |
11 "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" |
13 "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" |
23 |
25 |
24 |
26 |
25 text {* should probably be in Sum_Type.thy *} |
27 text {* should probably be in Sum_Type.thy *} |
26 lemma split_sum_all: |
28 lemma split_sum_all: |
27 shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))" |
29 shows "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (Inl x)) \<and> (\<forall>x. P (Inr x))" |
28 apply(auto) |
30 apply(auto) |
29 apply(case_tac x) |
31 apply(case_tac x) |
30 apply(simp_all) |
32 apply(simp_all) |
31 done |
33 done |
32 |
34 |
33 lemma sum_equivp[quot_equiv]: |
35 lemma sum_equivp[quot_equiv]: |
34 assumes a: "equivp R1" |
36 assumes a: "equivp R1" |
35 assumes b: "equivp R2" |
37 assumes b: "equivp R2" |
36 shows "equivp (sum_rel R1 R2)" |
38 shows "equivp (sum_rel R1 R2)" |