equal
deleted
inserted
replaced
45 assumes "remdups xa = remdups ya" |
45 assumes "remdups xa = remdups ya" |
46 shows "remdups (map f xa) = remdups (map f ya)" |
46 shows "remdups (map f xa) = remdups (map f ya)" |
47 using assms |
47 using assms |
48 by (induct xa ya arbitrary: fx fy rule: list_induct2') |
48 by (induct xa ya arbitrary: fx fy rule: list_induct2') |
49 (metis (full_types) remdups_nil_noteq_cons(2) remdups_map_remdups)+ |
49 (metis (full_types) remdups_nil_noteq_cons(2) remdups_map_remdups)+ |
|
50 |
|
51 lemma remdups_eq_member_eq: |
|
52 assumes "remdups xa = remdups ya" |
|
53 shows "List.member xa = List.member ya" |
|
54 using assms |
|
55 unfolding fun_eq_iff List.member_def |
|
56 by (induct xa ya rule: list_induct2') |
|
57 (metis remdups_nil_noteq_cons set_remdups)+ |
50 |
58 |
51 text {* Setting up the quotient type *} |
59 text {* Setting up the quotient type *} |
52 |
60 |
53 definition |
61 definition |
54 dlist_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
62 dlist_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
89 "(dlist_eq ===> op =) remdups remdups" |
97 "(dlist_eq ===> op =) remdups remdups" |
90 "(op = ===> dlist_eq ===> op =) foldr_remdups foldr_remdups" |
98 "(op = ===> dlist_eq ===> op =) foldr_remdups foldr_remdups" |
91 "(op = ===> dlist_eq ===> dlist_eq) map map" |
99 "(op = ===> dlist_eq ===> dlist_eq) map map" |
92 "(op = ===> dlist_eq ===> dlist_eq) filter filter" |
100 "(op = ===> dlist_eq ===> dlist_eq) filter filter" |
93 by (auto intro!: fun_relI simp add: remdups_filter) |
101 by (auto intro!: fun_relI simp add: remdups_filter) |
94 (metis (full_types) member_set set_remdups remdups_eq_map_eq)+ |
102 (metis (full_types) set_remdups remdups_eq_map_eq remdups_eq_member_eq)+ |
95 |
103 |
96 quotient_definition empty where "empty :: 'a dlist" |
104 quotient_definition empty where "empty :: 'a dlist" |
97 is "Nil" |
105 is "Nil" |
98 |
106 |
99 quotient_definition insert where "insert :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" |
107 quotient_definition insert where "insert :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist" |