equal
deleted
inserted
replaced
50 done |
50 done |
51 |
51 |
52 lemma list_rel_transp: |
52 lemma list_rel_transp: |
53 assumes a: "equivp R" |
53 assumes a: "equivp R" |
54 shows "list_rel R xs1 xs2 \<Longrightarrow> list_rel R xs2 xs3 \<Longrightarrow> list_rel R xs1 xs3" |
54 shows "list_rel R xs1 xs2 \<Longrightarrow> list_rel R xs2 xs3 \<Longrightarrow> list_rel R xs1 xs3" |
55 apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2') |
55 using a |
56 apply(simp_all) |
56 apply(induct R xs1 xs2 arbitrary: xs3 rule: list_rel.induct) |
|
57 apply(simp) |
|
58 apply(simp) |
|
59 apply(simp) |
57 apply(case_tac xs3) |
60 apply(case_tac xs3) |
58 apply(simp_all) |
61 apply(clarify) |
59 apply(rule equivp_transp[OF a]) |
62 apply(simp (no_asm_use)) |
60 apply(auto) |
63 apply(clarify) |
|
64 apply(simp (no_asm_use)) |
|
65 apply(auto intro: equivp_transp) |
61 done |
66 done |
62 |
67 |
63 lemma list_equivp[quot_equiv]: |
68 lemma list_equivp[quot_equiv]: |
64 assumes a: "equivp R" |
69 assumes a: "equivp R" |
65 shows "equivp (list_rel R)" |
70 shows "equivp (list_rel R)" |