equal
deleted
inserted
replaced
123 assumes a: "Quotient R1 abs1 rep1" |
123 assumes a: "Quotient R1 abs1 rep1" |
124 and b: "Quotient R2 abs2 rep2" |
124 and b: "Quotient R2 abs2 rep2" |
125 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
125 shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" |
126 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
126 by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) |
127 |
127 |
128 lemma foldr_prs[quot_respect]: |
128 lemma foldr_prs[quot_preserve]: |
129 assumes a: "Quotient R1 abs1 rep1" |
129 assumes a: "Quotient R1 abs1 rep1" |
130 and b: "Quotient R2 abs2 rep2" |
130 and b: "Quotient R2 abs2 rep2" |
131 shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" |
131 shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" |
132 by (simp only: expand_fun_eq fun_map.simps foldr_prs_aux[OF a b]) |
132 by (simp only: expand_fun_eq fun_map.simps foldr_prs_aux[OF a b]) |
133 (simp) |
133 (simp) |