equal
deleted
inserted
replaced
159 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) |
159 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *) |
160 lemma foldl_rsp[quot_respect]: |
160 lemma foldl_rsp[quot_respect]: |
161 assumes q1: "Quotient R1 Abs1 Rep1" |
161 assumes q1: "Quotient R1 Abs1 Rep1" |
162 and q2: "Quotient R2 Abs2 Rep2" |
162 and q2: "Quotient R2 Abs2 Rep2" |
163 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
163 shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" |
164 apply auto |
164 apply(auto) |
165 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
165 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)") |
166 apply simp |
166 apply simp |
167 apply (rule_tac x="xa" in spec) |
167 apply (rule_tac x="xa" in spec) |
168 apply (rule_tac x="ya" in spec) |
168 apply (rule_tac x="ya" in spec) |
169 apply (rule_tac xs="xb" and ys="yb" in list_induct2) |
169 apply (rule_tac xs="xb" and ys="yb" in list_induct2) |
190 apply(rule allI)+ |
190 apply(rule allI)+ |
191 apply(induct_tac x xa rule: list_induct2') |
191 apply(induct_tac x xa rule: list_induct2') |
192 apply(simp_all) |
192 apply(simp_all) |
193 done |
193 done |
194 |
194 |
|
195 |
195 (* Rest are unused *) |
196 (* Rest are unused *) |
196 |
197 text {* |
197 lemma list_rel_refl: |
198 lemma list_rel_refl: |
198 assumes a: "\<And>x y. R x y = (R x = R y)" |
199 assumes a: "\<And>x y. R x y = (R x = R y)" |
199 shows "list_rel R x x" |
200 shows "list_rel R x x" |
200 by (induct x) (auto simp add: a) |
201 by (induct x) (auto simp add: a) |
|
202 *} |
201 |
203 |
202 end |
204 end |