# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1313653939 -32400
# Node ID 971d1be5d5ce531cbe36bf0b10bca4225e2356b6
# Parent  355d5438f5fb5091155e3dd10ad9dc6ea6167a94
Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.

diff -r 355d5438f5fb -r 971d1be5d5ce src/HOL/Quotient_Examples/DList.thy
--- a/src/HOL/Quotient_Examples/DList.thy	Wed Aug 17 15:12:34 2011 -0700
+++ b/src/HOL/Quotient_Examples/DList.thy	Thu Aug 18 16:52:19 2011 +0900
@@ -48,6 +48,14 @@
   by (induct xa ya arbitrary: fx fy rule: list_induct2')
      (metis (full_types) remdups_nil_noteq_cons(2) remdups_map_remdups)+
 
+lemma remdups_eq_member_eq:
+  assumes "remdups xa = remdups ya"
+    shows "List.member xa = List.member ya"
+  using assms
+  unfolding fun_eq_iff List.member_def
+  by (induct xa ya rule: list_induct2')
+     (metis remdups_nil_noteq_cons set_remdups)+
+
 text {* Setting up the quotient type *}
 
 definition
@@ -91,7 +99,7 @@
   "(op = ===> dlist_eq ===> dlist_eq) map map"
   "(op = ===> dlist_eq ===> dlist_eq) filter filter"
   by (auto intro!: fun_relI simp add: remdups_filter)
-     (metis (full_types) member_set set_remdups remdups_eq_map_eq)+
+     (metis (full_types) set_remdups remdups_eq_map_eq remdups_eq_member_eq)+
 
 quotient_definition empty where "empty :: 'a dlist"
   is "Nil"