equal
deleted
inserted
replaced
9 | "[] \<approx> []" |
9 | "[] \<approx> []" |
10 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs" |
10 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs" |
11 | "a#a#xs \<approx> a#xs" |
11 | "a#a#xs \<approx> a#xs" |
12 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
12 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
13 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
13 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
|
14 |
|
15 lemma |
|
16 "(list_eq ===> (list_eq ===> (op =))) (list_eq) (list_eq)" |
|
17 apply(simp add: FUN_REL.simps) |
|
18 apply(rule allI | rule impI)+ |
|
19 sorry |
14 |
20 |
15 lemma list_eq_refl: |
21 lemma list_eq_refl: |
16 shows "xs \<approx> xs" |
22 shows "xs \<approx> xs" |
17 by (induct xs) (auto intro: list_eq.intros) |
23 by (induct xs) (auto intro: list_eq.intros) |
18 |
24 |