equal
deleted
inserted
replaced
49 |
49 |
50 lemma Pair_prs[quot_preserve]: |
50 lemma Pair_prs[quot_preserve]: |
51 assumes q1: "Quotient R1 Abs1 Rep1" |
51 assumes q1: "Quotient R1 Abs1 Rep1" |
52 assumes q2: "Quotient R2 Abs2 Rep2" |
52 assumes q2: "Quotient R2 Abs2 Rep2" |
53 shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" |
53 shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" |
54 apply(simp add: ext_iff) |
54 apply(simp add: fun_eq_iff) |
55 apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
55 apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
56 done |
56 done |
57 |
57 |
58 lemma fst_rsp[quot_respect]: |
58 lemma fst_rsp[quot_respect]: |
59 assumes "Quotient R1 Abs1 Rep1" |
59 assumes "Quotient R1 Abs1 Rep1" |
63 |
63 |
64 lemma fst_prs[quot_preserve]: |
64 lemma fst_prs[quot_preserve]: |
65 assumes q1: "Quotient R1 Abs1 Rep1" |
65 assumes q1: "Quotient R1 Abs1 Rep1" |
66 assumes q2: "Quotient R2 Abs2 Rep2" |
66 assumes q2: "Quotient R2 Abs2 Rep2" |
67 shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst" |
67 shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst" |
68 apply(simp add: ext_iff) |
68 apply(simp add: fun_eq_iff) |
69 apply(simp add: Quotient_abs_rep[OF q1]) |
69 apply(simp add: Quotient_abs_rep[OF q1]) |
70 done |
70 done |
71 |
71 |
72 lemma snd_rsp[quot_respect]: |
72 lemma snd_rsp[quot_respect]: |
73 assumes "Quotient R1 Abs1 Rep1" |
73 assumes "Quotient R1 Abs1 Rep1" |
77 |
77 |
78 lemma snd_prs[quot_preserve]: |
78 lemma snd_prs[quot_preserve]: |
79 assumes q1: "Quotient R1 Abs1 Rep1" |
79 assumes q1: "Quotient R1 Abs1 Rep1" |
80 assumes q2: "Quotient R2 Abs2 Rep2" |
80 assumes q2: "Quotient R2 Abs2 Rep2" |
81 shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" |
81 shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd" |
82 apply(simp add: ext_iff) |
82 apply(simp add: fun_eq_iff) |
83 apply(simp add: Quotient_abs_rep[OF q2]) |
83 apply(simp add: Quotient_abs_rep[OF q2]) |
84 done |
84 done |
85 |
85 |
86 lemma split_rsp[quot_respect]: |
86 lemma split_rsp[quot_respect]: |
87 shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" |
87 shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split" |
89 |
89 |
90 lemma split_prs[quot_preserve]: |
90 lemma split_prs[quot_preserve]: |
91 assumes q1: "Quotient R1 Abs1 Rep1" |
91 assumes q1: "Quotient R1 Abs1 Rep1" |
92 and q2: "Quotient R2 Abs2 Rep2" |
92 and q2: "Quotient R2 Abs2 Rep2" |
93 shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split" |
93 shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split" |
94 by (simp add: ext_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
94 by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
95 |
95 |
96 lemma [quot_respect]: |
96 lemma [quot_respect]: |
97 shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===> |
97 shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===> |
98 prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel" |
98 prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel" |
99 by auto |
99 by auto |
101 lemma [quot_preserve]: |
101 lemma [quot_preserve]: |
102 assumes q1: "Quotient R1 abs1 rep1" |
102 assumes q1: "Quotient R1 abs1 rep1" |
103 and q2: "Quotient R2 abs2 rep2" |
103 and q2: "Quotient R2 abs2 rep2" |
104 shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) ---> |
104 shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) ---> |
105 prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel" |
105 prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel" |
106 by (simp add: ext_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
106 by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
107 |
107 |
108 lemma [quot_preserve]: |
108 lemma [quot_preserve]: |
109 shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2) |
109 shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2) |
110 (l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))" |
110 (l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))" |
111 by simp |
111 by simp |
116 shows "prod_fun id id = id" |
116 shows "prod_fun id id = id" |
117 by (simp add: prod_fun_def) |
117 by (simp add: prod_fun_def) |
118 |
118 |
119 lemma prod_rel_eq[id_simps]: |
119 lemma prod_rel_eq[id_simps]: |
120 shows "prod_rel (op =) (op =) = (op =)" |
120 shows "prod_rel (op =) (op =) = (op =)" |
121 by (simp add: ext_iff) |
121 by (simp add: fun_eq_iff) |
122 |
122 |
123 end |
123 end |