equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Quotient_Sum.thy |
1 (* Title: HOL/Library/Quotient_Sum.thy |
2 Author: Cezary Kaliszyk and Christian Urban |
2 Author: Cezary Kaliszyk and Christian Urban |
3 *) |
3 *) |
4 |
4 |
5 section {* Quotient infrastructure for the sum type *} |
5 section \<open>Quotient infrastructure for the sum type\<close> |
6 |
6 |
7 theory Quotient_Sum |
7 theory Quotient_Sum |
8 imports Main Quotient_Syntax |
8 imports Main Quotient_Syntax |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Rules for the Quotient package *} |
11 subsection \<open>Rules for the Quotient package\<close> |
12 |
12 |
13 lemma rel_sum_map1: |
13 lemma rel_sum_map1: |
14 "rel_sum R1 R2 (map_sum f1 f2 x) y \<longleftrightarrow> rel_sum (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y" |
14 "rel_sum R1 R2 (map_sum f1 f2 x) y \<longleftrightarrow> rel_sum (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y" |
15 by (rule sum.rel_map(1)) |
15 by (rule sum.rel_map(1)) |
16 |
16 |