(* Title: HOL/Quotient_Examples/DList.thy Author: Cezary Kaliszyk, University of Tsukuba Based on typedef version "Library/Dlist" by Florian Haftmann and theory morphism version by Maksym Bortin *) section {* Lists with distinct elements *} theory DList imports "~~/src/HOL/Library/Quotient_List" begin text {* Some facts about lists *} lemma remdups_removeAll_commute[simp]: "remdups (removeAll x l) = removeAll x (remdups l)" by (induct l) auto lemma removeAll_distinct[simp]: assumes "distinct l" shows "distinct (removeAll x l)" using assms by (induct l) simp_all lemma removeAll_commute: "removeAll x (removeAll y l) = removeAll y (removeAll x l)" by (induct l) auto lemma remdups_hd_notin_tl: "remdups dl = h # t ⟹ h ∉ set t" proof (induct dl arbitrary: h t) case Nil then show ?case by simp next case (Cons a dl) then show ?case by (cases "a ∈ set dl") auto qed lemma remdups_repeat: "remdups dl = h # t ⟹ t = remdups t" proof (induct dl arbitrary: h t) case Nil then show ?case by simp next case (Cons a dl) then show ?case by (cases "a ∈ set dl") (auto simp: remdups_remdups) qed lemma remdups_nil_noteq_cons: "remdups (h # t) ≠ remdups []" "remdups [] ≠ remdups (h # t)" by auto lemma remdups_eq_map_eq: assumes "remdups xa = remdups ya" shows "remdups (map f xa) = remdups (map f ya)" using assms by (induct xa ya 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 dlist_eq :: "'a list ⇒ 'a list ⇒ bool" where [simp]: "dlist_eq xs ys ⟷ remdups xs = remdups ys" lemma dlist_eq_reflp: "reflp dlist_eq" by (auto intro: reflpI) lemma dlist_eq_symp: "symp dlist_eq" by (auto intro: sympI) lemma dlist_eq_transp: "transp dlist_eq" by (auto intro: transpI) lemma dlist_eq_equivp: "equivp dlist_eq" by (auto intro: equivpI dlist_eq_reflp dlist_eq_symp dlist_eq_transp) quotient_type 'a dlist = "'a list" / "dlist_eq" by (rule dlist_eq_equivp) text {* respectfulness and constant definitions *} definition [simp]: "card_remdups = length ∘ remdups" definition [simp]: "foldr_remdups f xs e = foldr f (remdups xs) e" quotient_definition empty where "empty :: 'a dlist" is "Nil" . quotient_definition insert where "insert :: 'a ⇒ 'a dlist ⇒ 'a dlist" is "Cons" by (metis (mono_tags) List.insert_def dlist_eq_def remdups.simps(2) set_remdups) quotient_definition "member :: 'a dlist ⇒ 'a ⇒ bool" is "List.member" by (metis dlist_eq_def remdups_eq_member_eq) quotient_definition foldr where "foldr :: ('a ⇒ 'b ⇒ 'b) ⇒ 'a dlist ⇒ 'b ⇒ 'b" is "foldr_remdups" by auto quotient_definition "remove :: 'a ⇒ 'a dlist ⇒ 'a dlist" is "removeAll" by force quotient_definition card where "card :: 'a dlist ⇒ nat" is "card_remdups" by fastforce quotient_definition map where "map :: ('a ⇒ 'b) ⇒ 'a dlist ⇒ 'b dlist" is "List.map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" by (metis dlist_eq_def remdups_eq_map_eq) quotient_definition filter where "filter :: ('a ⇒ bool) ⇒ 'a dlist ⇒ 'a dlist" is "List.filter" by (metis dlist_eq_def remdups_filter) quotient_definition "list_of_dlist :: 'a dlist ⇒ 'a list" is "remdups" by simp text {* lifted theorems *} lemma dlist_member_insert: "member dl x ⟹ insert x dl = dl" by descending (simp add: List.member_def) lemma dlist_member_insert_eq: "member (insert y dl) x = (x = y ∨ member dl x)" by descending (simp add: List.member_def) lemma dlist_insert_idem: "insert x (insert x dl) = insert x dl" by descending simp lemma dlist_insert_not_empty: "insert x dl ≠ empty" by descending auto lemma not_dlist_member_empty: "¬ member empty x" by descending (simp add: List.member_def) lemma not_dlist_member_remove: "¬ member (remove x dl) x" by descending (simp add: List.member_def) lemma dlist_in_remove: "a ≠ b ⟹ member (remove b dl) a = member dl a" by descending (simp add: List.member_def) lemma dlist_not_memb_remove: "¬ member dl x ⟹ remove x dl = dl" by descending (simp add: List.member_def) lemma dlist_no_memb_remove_insert: "¬ member dl x ⟹ remove x (insert x dl) = dl" by descending (simp add: List.member_def) lemma dlist_remove_empty: "remove x empty = empty" by descending simp lemma dlist_remove_insert_commute: "a ≠ b ⟹ remove a (insert b dl) = insert b (remove a dl)" by descending simp lemma dlist_remove_commute: "remove a (remove b dl) = remove b (remove a dl)" by (lifting removeAll_commute) lemma dlist_foldr_empty: "foldr f empty e = e" by descending simp lemma dlist_no_memb_foldr: assumes "¬ member dl x" shows "foldr f (insert x dl) e = f x (foldr f dl e)" using assms by descending (simp add: List.member_def) lemma dlist_foldr_insert_not_memb: assumes "¬member t h" shows "foldr f (insert h t) e = f h (foldr f t e)" using assms by descending (simp add: List.member_def) lemma list_of_dlist_empty[simp]: "list_of_dlist empty = []" by descending simp lemma list_of_dlist_insert[simp]: "list_of_dlist (insert x xs) = (if member xs x then (remdups (list_of_dlist xs)) else x # (remdups (list_of_dlist xs)))" by descending (simp add: List.member_def remdups_remdups) lemma list_of_dlist_remove[simp]: "list_of_dlist (remove x dxs) = remove1 x (list_of_dlist dxs)" by descending (simp add: distinct_remove1_removeAll) lemma list_of_dlist_map[simp]: "list_of_dlist (map f dxs) = remdups (List.map f (list_of_dlist dxs))" by descending (simp add: remdups_map_remdups) lemma list_of_dlist_filter [simp]: "list_of_dlist (filter P dxs) = List.filter P (list_of_dlist dxs)" by descending (simp add: remdups_filter) lemma dlist_map_empty: "map f empty = empty" by descending simp lemma dlist_map_insert: "map f (insert x xs) = insert (f x) (map f xs)" by descending simp lemma dlist_eq_iff: "dxs = dys ⟷ list_of_dlist dxs = list_of_dlist dys" by descending simp lemma dlist_eqI: "list_of_dlist dxs = list_of_dlist dys ⟹ dxs = dys" by (simp add: dlist_eq_iff) abbreviation "dlist xs ≡ abs_dlist xs" lemma distinct_list_of_dlist [simp, intro]: "distinct (list_of_dlist dxs)" by descending simp lemma list_of_dlist_dlist [simp]: "list_of_dlist (dlist xs) = remdups xs" unfolding list_of_dlist_def map_fun_apply id_def by (metis Quotient3_rep_abs[OF Quotient3_dlist] dlist_eq_def) lemma remdups_list_of_dlist [simp]: "remdups (list_of_dlist dxs) = list_of_dlist dxs" by simp lemma dlist_list_of_dlist [simp, code abstype]: "dlist (list_of_dlist dxs) = dxs" by (simp add: list_of_dlist_def) (metis Quotient3_def Quotient3_dlist dlist_eqI list_of_dlist_dlist remdups_list_of_dlist) lemma dlist_filter_simps: "filter P empty = empty" "filter P (insert x xs) = (if P x then insert x (filter P xs) else filter P xs)" by (lifting filter.simps) lemma dlist_induct: assumes "P empty" and "⋀a dl. P dl ⟹ P (insert a dl)" shows "P dl" using assms by descending (drule list.induct, simp) lemma dlist_induct_stronger: assumes a1: "P empty" and a2: "⋀x dl. ⟦¬member dl x; P dl⟧ ⟹ P (insert x dl)" shows "P dl" proof(induct dl rule: dlist_induct) show "P empty" using a1 by simp next fix x dl assume "P dl" then show "P (insert x dl)" using a2 by (cases "member dl x") (simp_all add: dlist_member_insert) qed lemma dlist_card_induct: assumes "⋀xs. (⋀ys. card ys < card xs ⟹ P ys) ⟹ P xs" shows "P xs" using assms by descending (rule measure_induct [of card_remdups], blast) lemma dlist_cases: "dl = empty ∨ (∃h t. dl = insert h t ∧ ¬ member t h)" by descending (metis List.member_def dlist_eq_def hd_Cons_tl list_of_dlist_dlist remdups_hd_notin_tl remdups_list_of_dlist) lemma dlist_exhaust: obtains "y = empty" | a dl where "y = insert a dl" by (lifting list.exhaust) lemma dlist_exhaust_stronger: obtains "y = empty" | a dl where "y = insert a dl" "¬ member dl a" by (metis dlist_cases) end