equal
deleted
inserted
replaced
14 | "LIST_REL R [] (x#xs) = False" |
14 | "LIST_REL R [] (x#xs) = False" |
15 | "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)" |
15 | "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)" |
16 |
16 |
17 lemma LIST_REL_EQ: |
17 lemma LIST_REL_EQ: |
18 shows "LIST_REL (op =) \<equiv> (op =)" |
18 shows "LIST_REL (op =) \<equiv> (op =)" |
|
19 apply(rule eq_reflection) |
19 unfolding expand_fun_eq |
20 unfolding expand_fun_eq |
20 apply(rule allI)+ |
21 apply(rule allI)+ |
21 apply(induct_tac x xa rule: list_induct2') |
22 apply(induct_tac x xa rule: list_induct2') |
22 apply(simp_all) |
23 apply(simp_all) |
23 done |
24 done |