equal
deleted
inserted
replaced
181 apply (rule_tac xs="xa" and ys="ya" in list_induct2) |
181 apply (rule_tac xs="xa" and ys="ya" in list_induct2) |
182 apply (rule list_rel_len) |
182 apply (rule list_rel_len) |
183 apply (simp_all) |
183 apply (simp_all) |
184 done |
184 done |
185 |
185 |
186 (* Rest are unused *) |
186 lemma list_rel_eq[id_simps]: |
187 |
|
188 lemma list_rel_eq: |
|
189 shows "list_rel (op =) \<equiv> (op =)" |
187 shows "list_rel (op =) \<equiv> (op =)" |
190 apply(rule eq_reflection) |
188 apply(rule eq_reflection) |
191 unfolding expand_fun_eq |
189 unfolding expand_fun_eq |
192 apply(rule allI)+ |
190 apply(rule allI)+ |
193 apply(induct_tac x xa rule: list_induct2') |
191 apply(induct_tac x xa rule: list_induct2') |
194 apply(simp_all) |
192 apply(simp_all) |
195 done |
193 done |
196 |
194 |
|
195 (* Rest are unused *) |
|
196 |
197 lemma list_rel_refl: |
197 lemma list_rel_refl: |
198 assumes a: "\<And>x y. R x y = (R x = R y)" |
198 assumes a: "\<And>x y. R x y = (R x = R y)" |
199 shows "list_rel R x x" |
199 shows "list_rel R x x" |
200 by (induct x) (auto simp add: a) |
200 by (induct x) (auto simp add: a) |
201 |
201 |