91 assumes a: "Quotient R1 abs1 rep1" |
91 assumes a: "Quotient R1 abs1 rep1" |
92 and b: "Quotient R2 abs2 rep2" |
92 and b: "Quotient R2 abs2 rep2" |
93 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
93 shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" |
94 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
94 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
95 |
95 |
96 lemma map_rsp: |
96 lemma map_rsp[quotient_rsp]: |
97 assumes q1: "Quotient R1 Abs1 Rep1" |
97 assumes q1: "Quotient R1 Abs1 Rep1" |
98 and q2: "Quotient R2 Abs2 Rep2" |
98 and q2: "Quotient R2 Abs2 Rep2" |
99 shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" |
99 shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" |
100 apply(simp) |
100 apply(simp) |
101 apply(rule allI)+ |
101 apply(rule allI)+ |
102 apply(rule impI) |
102 apply(rule impI) |
103 apply(rule allI)+ |
103 apply(rule allI)+ |
104 apply (induct_tac xa ya rule: list_induct2') |
104 apply (induct_tac xa ya rule: list_induct2') |
105 apply simp_all |
105 apply simp_all |
106 done |
106 done |
107 |
|
108 (* TODO: if the above is correct, we can remove this one *) |
|
109 lemma map_rsp_lo: |
|
110 assumes q1: "Quotient R1 Abs1 Rep1" |
|
111 and q2: "Quotient R2 Abs2 Rep2" |
|
112 and a: "(R1 ===> R2) f1 f2" |
|
113 and b: "list_rel R1 l1 l2" |
|
114 shows "list_rel R2 (map f1 l1) (map f2 l2)" |
|
115 using b a |
|
116 by (induct l1 l2 rule: list_induct2') (simp_all) |
|
117 |
107 |
118 lemma foldr_prs: |
108 lemma foldr_prs: |
119 assumes a: "Quotient R1 abs1 rep1" |
109 assumes a: "Quotient R1 abs1 rep1" |
120 and b: "Quotient R2 abs2 rep2" |
110 and b: "Quotient R2 abs2 rep2" |
121 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
111 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |