equal
deleted
inserted
replaced
80 shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" |
80 shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" |
81 apply(simp add: expand_fun_eq) |
81 apply(simp add: expand_fun_eq) |
82 apply(simp add: Quotient_abs_rep[OF q2]) |
82 apply(simp add: Quotient_abs_rep[OF q2]) |
83 done |
83 done |
84 |
84 |
|
85 lemma split_rsp[quot_respect]: |
|
86 shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" |
|
87 by auto |
|
88 |
|
89 lemma split_prs[quot_preserve]: |
|
90 assumes q1: "Quotient R1 Abs1 Rep1" |
|
91 and q2: "Quotient R2 Abs2 Rep2" |
|
92 shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split" |
|
93 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
|
94 |
85 lemma prod_fun_id[id_simps]: |
95 lemma prod_fun_id[id_simps]: |
86 shows "prod_fun id id \<equiv> id" |
96 shows "prod_fun id id = id" |
87 by (rule eq_reflection) (simp add: prod_fun_def) |
97 by (simp add: prod_fun_def) |
88 |
98 |
89 lemma prod_rel_eq[id_simps]: |
99 lemma prod_rel_eq[id_simps]: |
90 shows "prod_rel (op =) (op =) \<equiv> (op =)" |
100 shows "prod_rel (op =) (op =) = (op =)" |
91 apply (rule eq_reflection) |
101 by (simp add: expand_fun_eq) |
92 apply (simp add: expand_fun_eq) |
102 |
93 done |
|
94 |
103 |
95 end |
104 end |