<commit_before>(*  Title:      HOL/Quotient_Examples/DList.thy
    Author:     <NAME>, University of Tsukuba

Based on typedef version "Library/Dlist" by <NAME>
and theory morphism version by <NAME>
*)

header {* Lists with distinct elements *}

theory DList
imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_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 \<Longrightarrow> h \<notin> set t"
  by (induct dl arbitrary: h t)
     (case_tac [!] "a \<in> set dl", auto)

lemma remdups_repeat:
  "remdups dl = h # t \<Longrightarrow> t = remdups t"
  by (induct dl arbitrary: h t, case_tac [!] "a \<in> set dl")
     (simp_all, metis remdups_remdups)

lemma remdups_nil_noteq_cons:
  "remdups (h # t) \<noteq> remdups []"
  "remdups [] \<noteq> 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 arbitrary: fx fy rule: list_induct2')
     (metis (full_types) remdups_nil_noteq_cons(2) remdups_map_remdups)+

text {* Setting up the quotient type *}

definition
  dlist_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
where
  [simp]: "dlist_eq xs ys \<longleftrightarrow> 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 \<circ> remdups"
definition [simp]: "foldr_remdups f xs e = foldr f (remdups xs) e"

lemma [quot_respect]:
  "(dlist_eq) Nil Nil"
  "(dlist_eq ===> op =) List.member List.member"
  "(op = ===> dlist_eq ===> dlist_eq) Cons Cons"
  "(op = ===> dlist_eq ===> dlist_eq) removeAll removeAll"
  "(dlist_eq ===> op =) card_remdups card_remdups"
  "(dlist_eq ===> op =) remdups remdups"
  "(op = ===> dlist_eq ===> op =) foldr_remdups foldr_remdups"
  "(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)+

quotient_definition empty where "empty :: 'a dlist"
  is "Nil"<commit_msg>Quotient_Examples/DList: explicit proof of remdups_eq_member_eq needed for explicit set type.<commit_after>(*  Title:      HOL/Quotient_Examples/DList.thy
    Author:     <NAME>, University of Tsukuba

Based on typedef version "Library/Dlist" by <NAME>
and theory morphism version by <NAME>
*)

header {* Lists with distinct elements *}

theory DList
imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_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 \<Longrightarrow> h \<notin> set t"
  by (induct dl arbitrary: h t)
     (case_tac [!] "a \<in> set dl", auto)

lemma remdups_repeat:
  "remdups dl = h # t \<Longrightarrow> t = remdups t"
  by (induct dl arbitrary: h t, case_tac [!] "a \<in> set dl")
     (simp_all, metis remdups_remdups)

lemma remdups_nil_noteq_cons:
  "remdups (h # t) \<noteq> remdups []"
  "remdups [] \<noteq> 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 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
  dlist_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
where
  [simp]: "dlist_eq xs ys \<longleftrightarrow> 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 \<circ> remdups"
definition [simp]: "foldr_remdups f xs e = foldr f (remdups xs) e"

lemma [quot_respect]:
  "(dlist_eq) Nil Nil"
  "(dlist_eq ===> op =) List.member List.member"
  "(op = ===> dlist_eq ===> dlist_eq) Cons Cons"
  "(op = ===> dlist_eq ===> dlist_eq) removeAll removeAll"
  "(dlist_eq ===> op =) card_remdups card_remdups"
  "(dlist_eq ===> op =) remdups remdups"
  "(op = ===> dlist_eq ===> op =) foldr_remdups foldr_remdups"
  "(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) set_remdups remdups_eq_map_eq remdups_eq_member_eq)+

quotient_definition empty where "empty :: 'a dlist"
  is "Nil"
{'fraction_non_alphanumeric': 0.12506154603643527, 'fraction_numerical': 0.0008206138191367143, 'mean_word_length': 4.285342584562012, 'pattern_counts': {'":': 0, '<': 31, '<?xml version=': 0, '>': 57, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2538182', 'n_tokens_mistral': 2509, 'n_tokens_neox': 2454, 'n_words': 690}