equal
deleted
inserted
replaced
154 apply (simp add: list_rel_empty) |
154 apply (simp add: list_rel_empty) |
155 apply (case_tac b) |
155 apply (case_tac b) |
156 apply simp_all |
156 apply simp_all |
157 done |
157 done |
158 |
158 |
159 (* TODO: induct_tac doesn't accept 'arbitrary'. |
159 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) |
160 induct doesn't accept 'rule'. |
|
161 that's why the proof uses manual generalisation and needs assumptions |
|
162 both in conclusion for induction and in assumptions. *) |
|
163 lemma foldl_rsp[quot_respect]: |
160 lemma foldl_rsp[quot_respect]: |
164 assumes q1: "Quotient R1 Abs1 Rep1" |
161 assumes q1: "Quotient R1 Abs1 Rep1" |
165 and q2: "Quotient R2 Abs2 Rep2" |
162 and q2: "Quotient R2 Abs2 Rep2" |
166 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
163 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
167 apply auto |
164 apply auto |