equal
deleted
inserted
replaced
72 shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" |
72 shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" |
73 apply (simp add: expand_fun_eq) |
73 apply (simp add: expand_fun_eq) |
74 apply (simp add: Quotient_abs_rep[OF q2]) |
74 apply (simp add: Quotient_abs_rep[OF q2]) |
75 done |
75 done |
76 |
76 |
|
77 lemma split_rsp[quot_respect]: |
|
78 "((R1 ===> R2 ===> op =) ===> (prod_rel R1 R2) ===> op =) split split" |
|
79 by auto |
|
80 |
|
81 lemma split_prs[quot_preserve]: |
|
82 assumes q1: "Quotient R1 Abs1 Rep1" |
|
83 and q2: "Quotient R2 Abs2 Rep2" |
|
84 shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split" |
|
85 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
|
86 |
77 lemma prod_fun_id[id_simps]: |
87 lemma prod_fun_id[id_simps]: |
78 shows "prod_fun id id = id" |
88 shows "prod_fun id id = id" |
79 by (simp add: prod_fun_def) |
89 by (simp add: prod_fun_def) |
80 |
90 |
81 lemma prod_rel_eq[id_simps]: |
91 lemma prod_rel_eq[id_simps]: |